<!-- https://mathlive.io/compute-engine/guides/logic/ -->

# Logic and First-Order Logic

This guide covers working with logical expressions and First-Order Logic (FOL)
in the Compute Engine. You'll learn how to parse, manipulate, evaluate, and
transform Boolean and quantified expressions.

## Boolean Expressions

### Basic Logical Operators

The Compute Engine supports standard logical operators:

```js example
const ce = new ComputeEngine();

// Conjunction (AND)
ce.parse('p \\land q');           // → ["And", "p", "q"]

// Disjunction (OR)
ce.parse('p \\lor q');            // → ["Or", "p", "q"]

// Negation (NOT)
ce.parse('\\lnot p');             // → ["Not", "p"]

// Implication (multiple notations supported)
ce.parse('p \\implies q');        // → ["Implies", "p", "q"]
ce.parse('p \\Rightarrow q');     // → ["Implies", "p", "q"]
ce.parse('p \\rightarrow q');     // → ["Implies", "p", "q"]

// Equivalence (biconditional, multiple notations)
ce.parse('p \\iff q');            // → ["Equivalent", "p", "q"]
ce.parse('p \\Leftrightarrow q'); // → ["Equivalent", "p", "q"]
ce.parse('p \\leftrightarrow q'); // → ["Equivalent", "p", "q"]
```

**Note:** `\to` is reserved for function/set mapping notation (e.g., `f: A \to B`)
and parses as `To`, not `Implies`.

### Additional Operators

The Compute Engine also supports exclusive OR, NAND, and NOR:

```js example
// Exclusive OR (XOR)
ce.parse('p \\veebar q');         // → ["Xor", "p", "q"]

// NAND (Not AND)
ce.parse('p \\barwedge q');       // → ["Nand", "p", "q"]
```

These operators support any number of arguments:

```js example
// N-ary XOR: true when an odd number of arguments are true
ce.expr(['Xor', 'True', 'True', 'True']).evaluate();   // → True (3 is odd)
ce.expr(['Xor', 'True', 'True', 'False']).evaluate();  // → False (2 is even)

// N-ary NAND: NOT(AND(a, b, c, ...))
ce.expr(['Nand', 'True', 'True', 'False']).evaluate(); // → True

// N-ary NOR: NOT(OR(a, b, c, ...))
ce.expr(['Nor', 'False', 'False', 'False']).evaluate(); // → True
```

### Operator Precedence

Logical operators are designed to work naturally with comparison operators.
Comparisons bind tighter than logical operators, so you can write compound
conditions without parentheses:

```js example
// Comparisons bind tighter than Or
ce.parse('x = 1 \\lor y = 2');
// → ["Or", ["Equal", "x", 1], ["Equal", "y", 2]]

// And binds tighter than Or
ce.parse('a \\land b \\lor c');
// → ["Or", ["And", "a", "b"], "c"]

// Or binds tighter than Implies
ce.parse('p \\lor q \\implies r');
// → ["Implies", ["Or", "p", "q"], "r"]
```

**Important:** `Not` (`\lnot`, `\neg`) has very high precedence and only applies
to the immediately following atom. This matches standard mathematical convention:

```js example
// \lnot only applies to p, not the whole expression
ce.parse('\\lnot p \\land q');
// → ["And", ["Not", "p"], "q"]

// Use parentheses to negate compound expressions
ce.parse('\\lnot(p \\land q)');
// → ["Not", ["And", "p", "q"]]

// Similarly for comparisons
ce.parse('\\lnot x = 1');
// → ["Equal", ["Not", "x"], 1]  -- probably not what you want!

ce.parse('\\lnot(x = 1)');
// → ["Not", ["Equal", "x", 1]]  -- correct way to negate a comparison
```

### Evaluating Boolean Expressions

Boolean expressions with concrete `True`/`False` values evaluate to their
logical result:

```js example
ce.expr(['And', 'True', 'False']).evaluate();     // → False
ce.expr(['Or', 'True', 'False']).evaluate();      // → True
ce.expr(['Not', 'False']).evaluate();             // → True
ce.expr(['Implies', 'True', 'False']).evaluate(); // → False
ce.expr(['Implies', 'False', 'True']).evaluate(); // → True
ce.expr(['Xor', 'True', 'False']).evaluate();     // → True
ce.expr(['Nand', 'True', 'True']).evaluate();     // → False
ce.expr(['Nor', 'False', 'False']).evaluate();    // → True
```

## First-Order Logic

First-Order Logic extends propositional logic with quantifiers and predicates,
allowing you to make statements about objects in a domain.

### Predicates

In FOL, predicates are functions that return Boolean values. They are typically
written as uppercase letters followed by arguments.

**Inside quantifier scopes**, predicates are wrapped in a `Predicate` expression
to distinguish them from regular function applications:

```js example
ce.parse('\\forall x, P(x)');
// → ["ForAll", "x", ["Predicate", "P", "x"]]

ce.parse('\\exists x, Q(x, y)');
// → ["Exists", "x", ["Predicate", "Q", "x", "y"]]
```

**Outside quantifier scopes**, single uppercase letters followed by parentheses
are parsed as regular function applications to maintain backward compatibility:

```js example
ce.parse('P(x)');           // → ["P", "x"]
ce.parse('Q(a, b)');        // → ["Q", "a", "b"]
```

For multi-letter predicate names, declare them explicitly:

```js example
ce.declare('Loves', { signature: '(value, value) -> boolean' });
ce.parse('Loves(x, y)');    // → ["Loves", "x", "y"]
```

This applies to the library functions `D` and `N` too: outside a quantifier
scope they parse as their function equivalents, so they behave as expected:
- `D(f, x)` parses as the derivative function `["D", ...]`
- `N(\sqrt{10})` parses as the numeric evaluation function `["N", ["Sqrt", 10]]`

Inside a quantifier scope, these names are wrapped as predicates like any other
single uppercase letter (e.g. `\forall x, D(x)` →
`["ForAll", "x", ["Predicate", "D", "x"]]`).

### Quantifiers

The Compute Engine supports universal and existential quantifiers:

```js example
// Universal quantifier: "for all x"
ce.parse('\\forall x, P(x)');
// → ["ForAll", "x", ["Predicate", "P", "x"]]

// Existential quantifier: "there exists x"
ce.parse('\\exists x, P(x)');
// → ["Exists", "x", ["Predicate", "P", "x"]]

// Unique existential: "there exists exactly one x"
ce.parse('\\exists! x, P(x)');
// → ["ExistsUnique", "x", ["Predicate", "P", "x"]]
```

Negated quantifiers are also supported: `NotForAll` and `NotExists`.

Quantifiers can also specify a domain using set membership:

```js example
ce.parse('\\forall x \\in \\R, x^2 \\geq 0');
// → ["ForAll", ["Element", "x", "RealNumbers"], ["GreaterEqual", ["Square", "x"], 0]]
```

### Quantifier Scope

By default, quantifiers use **tight binding** following standard FOL conventions.
The scope extends only to the immediately following formula:

```js example
ce.parse('\\forall x. P(x) \\implies Q(x)');
// Parses as: (∀x. P(x)) → Q(x)
// → ["Implies", ["ForAll", "x", ["Predicate", "P", "x"]], ["Q", "x"]]
```

Note that `P(x)` inside the quantifier becomes `["Predicate", "P", "x"]`, while
`Q(x)` outside the quantifier scope becomes `["Q", "x"]`.

Use parentheses to extend the quantifier's scope:

```js example
ce.parse('\\forall x. (P(x) \\implies Q(x))');
// Parses as: ∀x. (P(x) → Q(x))
// → ["ForAll", "x", ["Delimiter", ["Implies", ["Predicate", "P", "x"], ["Predicate", "Q", "x"]]]]
```

You can change this behavior with the `quantifierScope` option:

```js example
// Loose binding - scope extends to end of expression
ce.parse('\\forall x. P(x) \\implies Q(x)', { quantifierScope: 'loose' });
// → ["ForAll", "x", ["Implies", ["Predicate", "P", "x"], ["Predicate", "Q", "x"]]]
```

## Evaluating Quantifiers

Quantifiers can be evaluated to Boolean values when the bound variable is
constrained to a finite domain.

### Finite Domain Evaluation

Specify a finite domain using `Element` with a `Set`, `List`, `Range`, or
`Interval`:

```js example
// Universal: all elements satisfy the predicate
ce.expr(['ForAll',
  ['Element', 'x', ['Set', 1, 2, 3]],
  ['Greater', 'x', 0]
]).evaluate();
// → True (1 > 0, 2 > 0, 3 > 0 all hold)

// Existential: at least one element satisfies the predicate
ce.expr(['Exists',
  ['Element', 'x', ['Set', 1, 2, 3]],
  ['Greater', 'x', 2]
]).evaluate();
// → True (3 > 2 holds)

// Unique existential: exactly one element satisfies the predicate
ce.expr(['ExistsUnique',
  ['Element', 'x', ['Set', 1, 2, 3]],
  ['Equal', 'x', 2]
]).evaluate();
// → True (only 2 equals 2)
```

### Using Range Domains

For integer ranges, use `Range`:

```js example
// All integers from 1 to 100 are positive
ce.expr(['ForAll',
  ['Element', 'n', ['Range', 1, 100]],
  ['Greater', 'n', 0]
]).evaluate();
// → True

// Some integer from 1 to 10 is a perfect square greater than 5
ce.expr(['Exists',
  ['Element', 'n', ['Range', 1, 10]],
  ['And', ['Greater', 'n', 5], ['Equal', ['Sqrt', 'n'], ['Floor', ['Sqrt', 'n']]]]
]).evaluate();
// → True (9 is a perfect square > 5)
```

### Nested Quantifiers

Nested quantifiers are evaluated over the Cartesian product of their domains:

```js example
// For all pairs (x, y) in {1,2} × {1,2}: x + y > 0
ce.expr(['ForAll', ['Element', 'x', ['Set', 1, 2]],
  ['ForAll', ['Element', 'y', ['Set', 1, 2]],
    ['Greater', ['Add', 'x', 'y'], 0]
  ]
]).evaluate();
// → True (checks all 4 pairs: (1,1), (1,2), (2,1), (2,2))

// There exist x, y in {1,2,3} such that x + y = 5
ce.expr(['Exists', ['Element', 'x', ['Set', 1, 2, 3]],
  ['Exists', ['Element', 'y', ['Set', 1, 2, 3]],
    ['Equal', ['Add', 'x', 'y'], 5]
  ]
]).evaluate();
// → True (x=2, y=3 or x=3, y=2)
```

### Symbolic Simplification

Quantifiers simplify automatically in certain cases:

```js example
// Constant body
ce.expr(['ForAll', 'x', 'True']).evaluate();   // → True
ce.expr(['ForAll', 'x', 'False']).evaluate();  // → False
ce.expr(['Exists', 'x', 'True']).evaluate();   // → True
ce.expr(['Exists', 'x', 'False']).evaluate();  // → False

// Body doesn't contain the quantified variable
ce.expr(['ForAll', 'x', ['Greater', 'y', 0]]).evaluate();
// → y > 0 (the quantifier is eliminated)
```

## Normal Forms

The Compute Engine can convert Boolean expressions to standard normal forms,
useful for automated reasoning and satisfiability checking.

### Conjunctive Normal Form (CNF)

CNF is a conjunction (AND) of disjunctions (OR) of literals:

```js example
// Convert (A ∧ B) ∨ C to CNF
ce.expr(['ToCNF', ['Or', ['And', 'A', 'B'], 'C']]).evaluate();
// → (A ∨ C) ∧ (B ∨ C)

// Convert implication to CNF
ce.expr(['ToCNF', ['Implies', 'A', 'B']]).evaluate();
// → ¬A ∨ B

// De Morgan's law is applied automatically
ce.expr(['ToCNF', ['Not', ['And', 'A', 'B']]]).evaluate();
// → ¬A ∨ ¬B
```

### Disjunctive Normal Form (DNF)

DNF is a disjunction (OR) of conjunctions (AND) of literals:

```js example
// Convert (A ∨ B) ∧ C to DNF
ce.expr(['ToDNF', ['And', ['Or', 'A', 'B'], 'C']]).evaluate();
// → (A ∧ C) ∨ (B ∧ C)

// De Morgan's law
ce.expr(['ToDNF', ['Not', ['Or', 'A', 'B']]]).evaluate();
// → ¬A ∧ ¬B
```

### How Conversion Works

The conversion process:
1. **Eliminate implications**: `A → B` becomes `¬A ∨ B`
2. **Eliminate equivalences**: `A ↔ B` becomes `(¬A ∨ B) ∧ (¬B ∨ A)`
3. **Push negations inward** (De Morgan's laws): `¬(A ∧ B)` becomes `¬A ∨ ¬B`
4. **Distribute** to get the target form:
   - For CNF: distribute OR over AND
   - For DNF: distribute AND over OR

## Practical Examples

### Validating Logical Arguments

Check if an argument is valid by verifying the conclusion follows from premises:

```js example
// Modus Ponens: If P → Q and P, then Q
// Check: for all truth values, (P → Q) ∧ P → Q is a tautology

ce.expr(['ForAll', ['Element', 'p', ['Set', 'True', 'False']],
  ['ForAll', ['Element', 'q', ['Set', 'True', 'False']],
    ['Implies',
      ['And', ['Implies', 'p', 'q'], 'p'],
      'q'
    ]
  ]
]).evaluate();
// → True (Modus Ponens is valid)
```

### Checking Properties Over Domains

Verify mathematical properties:

```js example
// Commutativity of addition for small integers
ce.expr(['ForAll', ['Element', 'a', ['Range', -5, 5]],
  ['ForAll', ['Element', 'b', ['Range', -5, 5]],
    ['Equal', ['Add', 'a', 'b'], ['Add', 'b', 'a']]
  ]
]).evaluate();
// → True

// Check if a function is injective over a domain
// f(x) = x² is not injective on {-2, -1, 0, 1, 2}
ce.expr(['Exists', ['Element', 'x', ['Set', -2, -1, 0, 1, 2]],
  ['Exists', ['Element', 'y', ['Set', -2, -1, 0, 1, 2]],
    ['And',
      ['NotEqual', 'x', 'y'],
      ['Equal', ['Square', 'x'], ['Square', 'y']]
    ]
  ]
]).evaluate();
// → True (x=-1, y=1 both give 1)
```

### Database-Style Queries

Use quantifiers for set-based queries:

```js example
// Define a "database" of people and their ages
const people = ['Set',
  ['List', 'Alice', 25],
  ['List', 'Bob', 30],
  ['List', 'Carol', 22]
];

// Check if someone is over 28
ce.expr(['Exists', ['Element', 'person', people],
  ['Greater', ['At', 'person', 2], 28]
]).evaluate();
// → True (Bob is 30)
```

## Satisfiability and Tautology Checking

The Compute Engine can check whether Boolean formulas are satisfiable (can be
made true) or are tautologies (always true).

### Satisfiability

Use `IsSatisfiable` to check if there exists an assignment of truth values that
makes the expression true:

```js example
// A contradiction is not satisfiable
ce.expr(['IsSatisfiable', ['And', 'A', ['Not', 'A']]]).evaluate();
// → False

// Most formulas are satisfiable
ce.expr(['IsSatisfiable', ['And', 'A', 'B']]).evaluate();
// → True (set A=True, B=True)

// A tautology is satisfiable
ce.expr(['IsSatisfiable', ['Or', 'A', ['Not', 'A']]]).evaluate();
// → True
```

### Tautology Checking

Use `IsTautology` to check if an expression is true for all possible assignments:

```js example
// Law of excluded middle
ce.expr(['IsTautology', ['Or', 'A', ['Not', 'A']]]).evaluate();
// → True

// Double negation
ce.expr(['IsTautology', ['Equivalent', ['Not', ['Not', 'A']], 'A']]).evaluate();
// → True

// De Morgan's law
ce.expr(['IsTautology', ['Equivalent',
  ['Not', ['And', 'A', 'B']],
  ['Or', ['Not', 'A'], ['Not', 'B']]
]]).evaluate();
// → True

// Modus Ponens
ce.expr(['IsTautology', ['Implies',
  ['And', ['Implies', 'A', 'B'], 'A'],
  'B'
]]).evaluate();
// → True

// A simple conjunction is not a tautology
ce.expr(['IsTautology', ['And', 'A', 'B']]).evaluate();
// → False
```

## Truth Table Generation

Use `TruthTable` to generate a complete truth table for any Boolean expression:

```js example
// Truth table for AND
ce.expr(['TruthTable', ['And', 'A', 'B']]).evaluate();
// → [["A", "B", "Result"],
//    ["False", "False", "False"],
//    ["False", "True", "False"],
//    ["True", "False", "False"],
//    ["True", "True", "True"]]

// Truth table for implication
ce.expr(['TruthTable', ['Implies', 'P', 'Q']]).evaluate();
// → [["P", "Q", "Result"],
//    ["False", "False", "True"],
//    ["False", "True", "True"],
//    ["True", "False", "False"],
//    ["True", "True", "True"]]
```

Truth tables are limited to 10 variables (1024 rows) to prevent excessive output.

## Performance Considerations

- **Domain size**: Evaluation iterates through all domain elements. Keep domains
  under 1000 elements.
- **Nested quantifiers**: With n quantifiers over domains of size k, evaluation
  checks k^n combinations. Use sparingly.
- **Short-circuit evaluation**: `ForAll` stops at the first `False`, `Exists`
  stops at the first `True`.
- **Satisfiability/Tautology**: These check all 2^n truth assignments for n
  variables. Limited to 20 variables.

## See Also

- [Logic Reference](/compute-engine/reference/logic/) - Complete list of logic
  operators and their signatures
- [Sets Reference](/compute-engine/reference/sets/) - Working with sets and
  set operations