> ## Documentation Index
> Fetch the complete documentation index at: https://mintlify.com/lovishchopra/NL2FOL/llms.txt
> Use this file to discover all available pages before exploring further.

# First-Order Logic

> Understanding first-order logic fundamentals for fallacy detection

## What is First-Order Logic?

First-order logic (FOL), also known as predicate logic or first-order predicate calculus, is a formal system used in mathematics, philosophy, linguistics, and computer science. It extends propositional logic by allowing quantification over individuals and the use of predicates and functions.

<Info>
  First-order logic provides a powerful framework for representing complex statements about objects, their properties, and their relationships in a mathematically precise way.
</Info>

## Core Components

### Variables and Constants

In the NL2FOL system, variables are typically represented using lowercase letters (a, b, c, x, y, z):

* **Variables**: Represent entities that can take different values (e.g., `x`, `y`)
* **Constants**: Represent specific entities (e.g., `a` for "tall man", `b` for "cheese")

```python theme={null}
# From src/nl_to_fol.py:260-280
current_char='a'
for (s1,s2) in self.equal_entities:
    if s1 in self.entity_mappings:
        self.entity_mappings[s2]=self.entity_mappings[s1]
    elif s2 in self.entity_mappings:
        self.entity_mappings[s1]=self.entity_mappings[s2]
    else:
        self.entity_mappings[s1]=current_char
        self.entity_mappings[s2]=current_char
        current_char=chr(ord(current_char)+1)
```

### Predicates

Predicates express properties or relationships between entities. In NL2FOL, predicates are extracted from natural language:

<CardGroup cols={2}>
  <Card title="Unary Predicates" icon="circle-dot">
    Express properties of a single entity

    * `IsTall(x)` - "x is tall"
    * `LovesCheese(x)` - "x loves cheese"
  </Card>

  <Card title="Binary Predicates" icon="link">
    Express relationships between two entities

    * `IsTouching(a,b)` - "a is touching b"
    * `IsGiven(a,b)` - "a is given to b"
  </Card>
</CardGroup>

**Example from the system:**

```
Input: "A tall man loves cheese"
Referring Expressions: tall man: a, cheese: b
Properties: IsTall(a), LovesCheese(a)
```

### Logical Connectives

The system uses standard logical operators to connect formulas:

| Operator    | Symbol       | Meaning     | Example                              |
| ----------- | ------------ | ----------- | ------------------------------------ |
| Conjunction | `&` or `and` | Logical AND | `IsTall(x) & LovesCheese(x)`         |
| Disjunction | `\|` or `or` | Logical OR  | `IsTall(x) \| IsShort(x)`            |
| Implication | `->` or `=>` | If...then   | `IsSmacked(x) -> ~HasBadBehavior(x)` |
| Negation    | `~` or `not` | NOT         | `~HasBadBehavior(x)`                 |

<Note>
  The system applies heuristics to normalize operators, replacing `->` with `&` in claims and converting all connectives to their word forms (`and`, `or`) for processing.
</Note>

### Quantifiers

Quantifiers specify how many individuals satisfy a given property:

<Accordion title="Universal Quantifier (∀ / forall)">
  **Universal quantification** states that a property holds for **all** individuals in the domain.

  ```
  forall x (IsTall(x) -> LikesBasketball(x))
  ```

  This means: "For all x, if x is tall, then x likes basketball."

  **In the system:** Used primarily in implications to represent generalizations.
</Accordion>

<Accordion title="Existential Quantifier (∃ / exists)">
  **Existential quantification** states that there exists **at least one** individual with a property.

  ```
  exists x (IsTall(x) & LovesCheese(x))
  ```

  This means: "There exists an x such that x is tall and x loves cheese."

  **In the system:** Used primarily in claims to represent specific instances.
</Accordion>

## FOL in NL2FOL

The NL2FOL system converts natural language fallacies into first-order logic formulas following this pattern:

```
(claim_fol) -> (implication_fol)
```

Where:

* **Claim**: The observation or premise (often with existential quantifiers)
* **Implication**: The conclusion drawn (often with universal quantifiers)

### Example Transformation

<Tip>
  Let's see how the system converts a hasty generalization fallacy:
</Tip>

```
Input: "I met a tall man who loved to eat cheese, now I believe all tall people like cheese"

Step 1 - Extract Claim and Implication:
  Claim: "A tall man loves cheese"
  Implication: "All tall people like cheese"

Step 2 - Extract Referring Expressions:
  Claim: "A tall man" → x
  Implication: "tall people" → y

Step 3 - Extract Properties:
  Claim: IsTall(x), LovesCheese(x)
  Implication: IsTall(y), LovesCheese(y)

Step 4 - Generate FOL:
  Claim FOL: IsTall(x) and LovesCheese(x)
  Implication FOL: IsTall(y) and LovesCheese(y)

Step 5 - Apply Quantifiers:
  Final FOL: exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y))
```

## Sorts and Type System

The system uses a sophisticated sort (type) system to ensure logical consistency:

### Sort Types

```python theme={null}
# From src/cvc.py:12-26
class Sort:
    def __init__(self, sort=None):
        self.sort = sort
    
    def getSort(self):
        return self.sort
    
    def setSort(self, sort):
        self.sort = sort
```

**Three main sorts:**

1. **BoundSet**: For quantified variables (bound by `exists` or `forall`)
2. **UnboundSet**: For free variables without explicit binding
3. **Bool**: For boolean expressions and compound formulas

<Info>
  The sort system ensures that predicates are used consistently throughout the formula - if `IsTall(x)` expects a `BoundSet` variable, it will always expect that sort.
</Info>

## Logical Validity

A first-order logic formula is **valid** if it's true under all interpretations. The NL2FOL system checks validity by:

1. Converting the FOL formula to SMT-LIB format
2. Checking if the **negation** of the formula is unsatisfiable
3. If the negation is unsatisfiable, the original formula is valid

<Note>
  For logical fallacies, we expect the formula to be **invalid** (the negation should be satisfiable), indicating the reasoning is flawed.
</Note>

## Next Steps

<CardGroup cols={2}>
  <Card title="Logical Fallacies" icon="triangle-exclamation" href="/concepts/logical-fallacies">
    Learn about the types of fallacies the system can detect
  </Card>

  <Card title="Translation Pipeline" icon="diagram-project" href="/concepts/translation-pipeline">
    Understand how natural language is converted to FOL
  </Card>
</CardGroup>