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.

Note: \equiv is not a spelling of Equivalent: it parses as IdenticallyEqual, the mathematical identity operator. Use \iff or \Leftrightarrow for a biconditional. (Over boolean operands the two agree, since two propositions are identically equal exactly when they are equivalent.)

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

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

Short-Circuit Evaluation

And and Or evaluate their operands left to right, in the order written, and stop at the first operand that decides the result: And stops at the first False, Or at the first True. The remaining operands are never evaluated — no side effect, error, or random draw is produced by them. This is the behavior of && and || in most programming languages, and it is what a guard relies on:

// The out-of-range read never happens: `i <= 3` is False, so `And` stops.
ce.assign('xs', ce.expr(['List', 1, 2, 3]));
ce.assign('i', 5);
ce.expr(['And', ['LessEqual', 'i', 3], ['Greater', ['At', 'xs', 'i'], 0]])
  .evaluate();
// → False

Because the written order is meaningful, And and Or are not sorted at canonicalization: ["And", "q", "p"] stays ["And", "q", "p"]. Nested conjunctions/disjunctions are still flattened (And(And(a, b), c) → And(a, b, c)), which preserves the order. Symbolic simplifications (duplicate removal, A ∧ ¬A → False, absorption) are unaffected — they do not depend on operand order.

Element-wise applications are the exception. When an operand is a collection (by type — a list literal, a symbol bound to a list, or a call declared to return a list<boolean>), the conjunction or disjunction is applied cell by cell and the result is a list; every operand is then evaluated once, left to right, and there is no per-cell short-circuit:

ce.expr(['And', 'False', ['List', 'True', 'False']]).evaluate();
// → ["List", "False", "False"]

An operand that evaluates to an error also stops the walk: the error is the result, and the operands after it do not run.

Nand, Nor and Implies short-circuit the same way: Nand stops at the first False (result True), Nor at the first True (result False), and Implies does not evaluate its consequent when the antecedent is False. Xor and Equivalent cannot short-circuit — every operand affects the result — so every operand is evaluated. Chained comparisons are conjunctions of their adjacent pairs and short-circuit too: in Less(a, b, c) (a < b < c) the operand c is not evaluated once a < b is False.

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"]

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:

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

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

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

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

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

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

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

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

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

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

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

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

Boolean Expressions​

Basic Logical Operators​

Additional Operators​

Operator Precedence​

Evaluating Boolean Expressions​

Short-Circuit Evaluation​

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​