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:

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:

// 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:

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

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

// N-ary NOR: NOT(OR(a, b, c, ...))
ce.box(['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:

// 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:

// \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:

ce.box(['And', 'True', 'False']).evaluate();     // → False
ce.box(['Or', 'True', 'False']).evaluate();      // → True
ce.box(['Not', 'False']).evaluate();             // → True
ce.box(['Implies', 'True', 'False']).evaluate(); // → False
ce.box(['Implies', 'False', 'True']).evaluate(); // → True
ce.box(['Xor', 'True', 'False']).evaluate();     // → True
ce.box(['Nand', 'True', 'True']).evaluate();     // → False
ce.box(['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:

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:

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

For multi-letter predicate names, declare them explicitly:

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

Note about D(f, x) and N(x): These notations in LaTeX are not interpreted as their library function equivalents:

D(f, x) parses as ["Predicate", "D", "f", "x"] (not the derivative)
N(x) parses as ["Predicate", "N", "x"] (not numeric evaluation)

Use Leibniz notation (\frac{d}{dx}f) for derivatives, or construct directly in MathJSON. For numeric evaluation, use the .N() method on expressions.

Quantifiers

The Compute Engine supports universal and existential quantifiers:

// 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:

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:

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:

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:

// 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:

// Universal: all elements satisfy the predicate
ce.box(['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.box(['Exists',
  ['Element', 'x', ['Set', 1, 2, 3]],
  ['Greater', 'x', 2]
]).evaluate();
// → True (3 > 2 holds)

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

Using Range Domains

For integer ranges, use Range:

// All integers from 1 to 100 are positive
ce.box(['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.box(['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:

// For all pairs (x, y) in {1,2} × {1,2}: x + y > 0
ce.box(['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.box(['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:

// Constant body
ce.box(['ForAll', 'x', 'True']).evaluate();   // → True
ce.box(['ForAll', 'x', 'False']).evaluate();  // → False
ce.box(['Exists', 'x', 'True']).evaluate();   // → True
ce.box(['Exists', 'x', 'False']).evaluate();  // → False

// Body doesn't contain the quantified variable
ce.box(['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:

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

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

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

Disjunctive Normal Form (DNF)

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

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

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

How Conversion Works

The conversion process:

Eliminate implications: A → B becomes ¬A ∨ B
Eliminate equivalences: A ↔ B becomes (¬A ∨ B) ∧ (¬B ∨ A)
Push negations inward (De Morgan's laws): ¬(A ∧ B) becomes ¬A ∨ ¬B
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:

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

ce.box(['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:

// Commutativity of addition for small integers
ce.box(['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.box(['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:

// 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.box(['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:

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

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

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

Tautology Checking

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

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

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

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

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

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

Truth Table Generation

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

// Truth table for AND
ce.box(['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.box(['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.

Boolean Expressions​

Basic Logical Operators​

Additional Operators​

Operator Precedence​

Evaluating Boolean Expressions​

First-Order Logic​

Predicates​

Quantifiers​

Quantifier Scope​

Evaluating Quantifiers​

Finite Domain Evaluation​

Using Range Domains​

Nested Quantifiers​

Symbolic Simplification​

Normal Forms​

Conjunctive Normal Form (CNF)​

Disjunctive Normal Form (DNF)​

How Conversion Works​

Practical Examples​

Validating Logical Arguments​

Checking Properties Over Domains​

Database-Style Queries​

Satisfiability and Tautology Checking​

Satisfiability​

Tautology Checking​

Truth Table Generation​

Performance Considerations​

See Also​