Skip to main content

​
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.
First-order logic provides a powerful framework for representing complex statements about objects, their properties, and their relationships in a mathematically precise way.

​
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”)
# 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:

Unary Predicates

Express properties of a single entity
  • IsTall(x) - “x is tall”
  • LovesCheese(x) - “x loves cheese”

Binary Predicates

Express relationships between two entities
  • IsTouching(a,b) - “a is touching b”
  • IsGiven(a,b) - “a is given to b”
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:
OperatorSymbolMeaningExample
Conjunction& or andLogical ANDIsTall(x) & LovesCheese(x)
Disjunction| or orLogical ORIsTall(x) | IsShort(x)
Implication-> or =>If…thenIsSmacked(x) -> ~HasBadBehavior(x)
Negation~ or notNOT~HasBadBehavior(x)
The system applies heuristics to normalize operators, replacing -> with & in claims and converting all connectives to their word forms (and, or) for processing.

​
Quantifiers

Quantifiers specify how many individuals satisfy a given property:
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.
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.

​
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

Let’s see how the system converts a hasty generalization fallacy:
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

# 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
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.

​
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
For logical fallacies, we expect the formula to be invalid (the negation should be satisfiable), indicating the reasoning is flawed.

​
Next Steps

Logical Fallacies

Learn about the types of fallacies the system can detect

Translation Pipeline

Understand how natural language is converted to FOL

Build docs developers (and LLMs) love

Get started for freeTalk to us