feat: implementation for formal quantificational language

CLAUDE.md

@@ -41,8 +41,8 @@ src/
   language/
     shared/
       types.ts                                       # Formula, AlethicAssertoric, SentenceSet
-      theory.ts                                      # FormalSentence<F>, ConsistencyResult,
-                                                     # ProofNode, Theory<F> interface
+      theory.ts                                      # FormalSentence<F>, ConsistencyResult<V>,
+                                                      # ProofNode, Theory<F, V> interface
     propositional/
       propositionalTypes.d.ts                        # WFF, Atom, Complex, operators
       atom.ts                                        # AtomImpl
@@ -54,7 +54,17 @@ src/
       propositionalTheoryBuilder.ts                  # PropositionalTheoryBuilder (fluent builder)
       index.ts
     quantificational/
-      index.ts                                       # TODO
+      quantificationalTypes.d.ts                     # QFF, Term, Predicate, Quantifier, operators
+      term.ts                                        # VariableTerm, ConstantTerm
+      predicate.ts                                   # PredicateImpl
+      atomicFormula.ts                               # AtomicFormulaImpl
+      complexFormula.ts                              # ComplexFormulaImpl
+      quantifiedFormula.ts                           # QuantifiedFormulaImpl (∀, ∃)
+      quantificationalVariable.ts                    # QuantificationalVariable
+      quantificationalUtils.ts                       # binaryOperatorToLogic, type guards
+      quantificationalTheory.ts                      # QuantificationalTheory
+      quantificationalTheoryBuilder.ts               # QuantificationalTheoryBuilder
+      index.ts
     modal/
       index.ts                                       # TODO
   engine/
@@ -78,6 +88,15 @@ test/
       meta-logic/
         completeness.spec.ts                         # Full proof (135 tests total)
         expressiveAdequacy.spec.ts                   # Full inductive proof
+    quantificational/
+      term.spec.ts
+      predicate.spec.ts
+      atomicFormula.spec.ts
+      complexFormula.spec.ts
+      quantifiedFormula.spec.ts
+      quantificationalTheory.spec.ts
+      meta-logic/
+        completeness.spec.ts                         # Structural induction + quantifier duality
   engine/
     nlp/nlpEngine.spec.ts                            # Skipped placeholder
     syntax/propositional/syntaxEngine.spec.ts        # Skipped placeholder
@@ -121,9 +140,9 @@ test/
 | Type | Role |
 | --- | --- |
 | `FormalSentence<F>` | Pairs `AlethicAssertoric` source with a typed formula `F` and a label |
-| `ConsistencyResult` | Outcome of a consistency check: witness or failed valuations |
+| `ConsistencyResult<V>` | Outcome of a consistency check: witness or failed valuations (`V` defaults to `boolean`, quantificational uses `DomainElement`) |
 | `ProofNode` | Node in a structured proof tree |
-| `Theory<F>` | Interface all formal theories must implement |
+| `Theory<F, V>` | Interface all formal theories must implement (`V` is the valuation value type) |
 
 ## Propositional Logic — What's Implemented
 
@@ -169,6 +188,37 @@ theory.printGraph();
 - **Expressive adequacy** — inductive proof: base case covers all 4 unary truth functions; Shannon expansion is the inductive step; all 16 binary truth functions verified via DNF
 - **Completeness** — structural induction proof: `value()` is semantically correct at every level; known tautologies, contradictions, and contingencies classified correctly
 
+## Quantificational Logic — What's Implemented
+
+### Formula types
+
+- `DomainElement` — `string | number`, the elements of a finite domain of discourse
+- `VariableAssignment` — `Map<string, DomainElement>`, maps variable names to domain elements
+- `Term` — either a `VariableTerm` (resolved from assignment) or `ConstantTerm` (fixed element)
+- `Predicate` / `PredicateImpl` — n-ary relation with arity enforcement
+- `QFF` — Quantificational Formula, analogous to WFF; all valid first-order expressions
+- `AtomicFormulaImpl` — predicate applied to terms (analogous to `AtomImpl`)
+- `ComplexFormulaImpl` — two QFFs joined by a binary operator (same as propositional)
+- `QuantifiedFormulaImpl` — `∀` or `∃` binding a variable over a finite domain
+- Same operators as propositional: `~`, `&`, `|`, `->`, `<->`
+
+### Theory data structure
+
+**`QuantificationalVariable`** — named individual variable with mutable domain-element binding via shared assignment map. All formulas referencing this variable read its current binding.
+
+**`QuantificationalTheory`** — implements `Theory<QFF, DomainElement>`:
+- `checkConsistency()` — exhaustive `|D|^n` assignment enumeration
+- `buildProofTree()`, `printProof()`, `printGraph()` — same structure as propositional
+
+**`QuantificationalTheoryBuilder`** — fluent builder with `domain()`, `variable()`, `predicate()`, `sentence()`, `build()`.
+
+### Meta-logic proofs
+
+- **Completeness** — structural induction over AtomicFormula, ComplexFormula, QuantifiedFormula
+- **Quantifier duality** — `~∀x.F(x) ⟺ ∃x.~F(x)` and `~∃x.F(x) ⟺ ∀x.~F(x)`, verified over domains up to size 3
+- **Valid formulas** — universal instantiation, existential generalisation, distribution of ∀ over &
+- **Identity properties** — reflexivity and substitution (verified via exhaustive model checking)
+
 ## NLP Engine — Design Intent
 
 `NLPEngine.parse(input: string): NLPResult` accepts any string and returns zero or more `AlethicAssertoric` candidates. The output `SentenceSet` feeds directly into `PropositionalTheoryBuilder.fromSentenceSet()`.
@@ -179,7 +229,9 @@ theory.printGraph();
 - `PropositionalSyntaxEngine` — parsing formula strings into WFF instances
 - `PropositionalEvaluationEngine` — truth tables, tautology/contradiction classification
 - `PropositionalTheoryBuilder.fromSentenceSet()` — awaits SyntaxEngine
-- `Quantificational` language module
+- Quantificational function symbols (e.g., `f(x)`)
+- `QuantificationalSyntaxEngine` — parsing formula strings into QFF instances
+- `QuantificationalTheoryBuilder.fromSentenceSet()` — awaits SyntaxEngine
 - `Modal` language module
 
 ## Conventions

README.md

@@ -227,9 +227,99 @@ const wff = builder.getWFF({ unaryOperator: undefined, proposition: true });
 
 ### Quantificational Logic
 
-> In Progress
+First-order quantificational logic (predicate logic) over finite domains. Extends propositional logic with universal (`∀`) and existential (`∃`) quantifiers, predicate symbols, and individual terms.
+
+#### Terms
+
+The objects logic talks about. A `Term` is either a `ConstantTerm` or a `VariableTerm`.
+
+- **`ConstantTerm`**: A fixed individual (e.g., "Socrates", "42"). Resolves to the same element regardless of any variable assignment.
+- **`VariableTerm`**: A placeholder (e.g., "x", "y"). Resolves to its currently assigned domain element.
+
+```ts
+const a = new ConstantTerm('socrates');
+const x = new VariableTerm('x');
+```
+
+#### Predicates
+
+Relations over domain elements. A `PredicateImpl` has a name, arity (number of arguments), and an interpretation function.
+
+```ts
+// Unary: Mortal(x)
+const Mortal = new PredicateImpl('Mortal', 1, (x) => mortalSet.has(x));
+
+// Binary: Loves(x, y)
+const Loves = new PredicateImpl('Loves', 2, (x, y) => x === 'socrates' && y === 'plato');
+```
+
+**`IDENTITY` (=)**: A built-in binary predicate that holds if and only if its two arguments are the exact same domain element.
+
+```ts
+import { IDENTITY } from 'logic-engine';
+// IDENTITY.holds('a', 'a') → true
+```
+
+#### Formulas (`QFF`)
+
+- **`AtomicFormulaImpl`**: A predicate applied to the required number of terms (e.g., `Mortal(socrates)`).
+- **`ComplexFormulaImpl`**: Two `QFF`s joined by binary connectives (`&`, `|`, `->`, `<->`).
+- **`QuantifiedFormulaImpl`**: A `QFF` bound by a quantifier (`∀` or `∃`) over a variable name and a finite domain.
+
+```ts
+// ∀x.Mortal(x)
+const forallMortal = new QuantifiedFormulaImpl(
+  undefined, '∀', 'x', 
+  new AtomicFormulaImpl(undefined, Mortal, [new VariableTerm('x')], assignment), 
+  ['socrates', 'plato'], 
+  assignment
+);
+```
+
+#### `QuantificationalTheory` and `QuantificationalTheoryBuilder`
+
+Manages a set of formalised sentences and provides consistency checking over a **finite domain**.
+
+```ts
+const builder = new QuantificationalTheoryBuilder();
+builder.domain('socrates', 'plato', 'aristotle');
+
+const x = builder.variable('x');
+const Man = builder.predicate('Man', 1, (x) => x === 'socrates');
+const Mortal = builder.predicate('Mortal', 1, (x) => x === 'socrates');
+
+// φ1: ∀x.(Man(x) -> Mortal(x))
+const manX = new AtomicFormulaImpl(undefined, Man, [x.term()], builder.assignment);
+const mortalX = new AtomicFormulaImpl(undefined, Mortal, [x.term()], builder.assignment);
+const impl = new ComplexFormulaImpl(undefined, manX, '->', mortalX);
+
+builder.sentence(
+  { raw: 'All men are mortal', confidence: 1.0 },
+  new QuantifiedFormulaImpl(undefined, '∀', 'x', impl, builder.currentDomain, builder.assignment),
+  ['x']
+);
+
+// φ2: Man(socrates)
+builder.sentence(
+  { raw: 'Socrates is a man', confidence: 1.0 },
+  new AtomicFormulaImpl(undefined, Man, [new ConstantTerm('socrates')], builder.assignment),
+  []
+);
+
+const theory = builder.build();
+const result = theory.checkConsistency();
+// result.isConsistent → true
+```
+
+Consistency is decided by exhaustive evaluation over all $|D|^n$ variable assignments (where $D$ is the domain and $n$ is the number of free variables).
+
+#### Proofs and Graphs
+
+`QuantificationalTheory` supports the same structured output as propositional logic:
+
+- **`theory.printProof()`**: Shows the exhaustive check and first failure or satisfying witness.
+- **`theory.printGraph()`**: Maps relations between sentences (entailment, equivalence, inconsistency).
 
-Extends propositional logic with universal (`∀`) and existential (`∃`) quantifiers, predicate symbols, and individual variables.
 
 ### Modal Logic
 

docs/languages/quantificational/DEFINITIONS.md

@@ -0,0 +1,52 @@
+# Quantificational Logic — Design Notes
+
+## What's Implemented
+
+First-order quantificational logic (predicate logic) over finite domains.
+
+### Core Constructs
+
+| Construct | Propositional Analogue | Purpose |
+| --- | --- | --- |
+| `Term` (VariableTerm / ConstantTerm) | — | Denote domain elements |
+| `PredicateImpl` | — | n-ary relation over domain elements |
+| `AtomicFormulaImpl` | `AtomImpl` | Predicate applied to terms |
+| `ComplexFormulaImpl` | `ComplexImpl` | Binary connective joining two QFFs |
+| `QuantifiedFormulaImpl` | — | ∀ / ∃ binding a variable over a domain |
+| `QuantificationalVariable` | `PropositionalVariable` | Named variable with mutable domain-element binding |
+| `QuantificationalTheory` | `PropositionalTheory` | Theory with consistency checking over |D|^n assignments |
+| `QuantificationalTheoryBuilder` | `PropositionalTheoryBuilder` | Fluent builder for theories |
+
+### Symbols
+
+- Unary operators: `~` (negation)
+- Binary operators: `&`, `|`, `->`, `<->`
+- Quantifiers: `∀` (universal), `∃` (existential)
+- Terms: individual variables (`x`, `y`, `z`), individual constants (`a`, `b`, `c`)
+- Predicates: n-ary relations (`F`, `G`, `R`)
+
+### Evaluation
+
+All formulas implement `value(): boolean` from the shared `Formula` interface. Quantified formulas iterate over the finite domain, binding the variable to each element in turn:
+
+- `∀x.φ(x)` → `domain.every(d => { assign x=d; return φ.value() })`
+- `∃x.φ(x)` → `domain.some(d => { assign x=d; return φ.value() })`
+
+### Consistency Checking
+
+`checkConsistency()` exhaustively enumerates all `|D|^n` variable assignments (where `D` is the domain, `n` is the number of free variables). This parallels propositional logic's `2^n` truth-table approach.
+
+### Meta-logic Tests
+
+- Structural induction: `value()` is semantically correct at every formula level
+- Quantifier duality: `~∀x.F(x) ⟺ ∃x.~F(x)` and `~∃x.F(x) ⟺ ∀x.~F(x)`
+- Valid formulas: universal instantiation, existential generalisation, distribution of ∀ over &
+- Identity properties: reflexivity, substitution (indirectly via exhaustive evaluation)
+- Decision procedure: valid, contradictory, and contingent formulas classified correctly
+
+## What's NOT Implemented
+
+- Function symbols — terms like `f(x)`, `mother(x)` that map domain elements to domain elements
+- `QuantificationalSyntaxEngine` — parsing formula strings into QFF instances
+- `QuantificationalEvaluationEngine` — systematic model checking beyond consistency
+- `QuantificationalTheoryBuilder.fromSentenceSet()` — awaits SyntaxEngine

src/language/quantificational/atomicFormula.ts

@@ -0,0 +1,54 @@
+import { QFF, UnaryOperator, Predicate, Term, VariableAssignment } from './quantificationalTypes';
+
+/**
+ * Concrete implementation of an atomic quantificational formula.
+ *
+ * Applies a predicate to a list of terms. Analogous to AtomImpl in
+ * propositional logic — this is the smallest truth-evaluable unit
+ * in quantificational logic.
+ *
+ * Example: F(x), Loves(a, y), Mortal(socrates)
+ */
+export class AtomicFormulaImpl implements QFF {
+
+  /** Optional negation applied to the predicate result. */
+  unaryOperator: UnaryOperator | undefined;
+
+  /** The predicate being applied. */
+  readonly predicate: Predicate;
+
+  /** The terms (arguments) passed to the predicate. */
+  readonly terms: Term[];
+
+  /** Reference to the current variable assignment — set externally before evaluation. */
+  private readonly _assignment: VariableAssignment;
+
+  /**
+   * @param unaryOperator - Optional '~' to negate the result.
+   * @param predicate     - The predicate to apply.
+   * @param terms         - The terms to pass to the predicate.
+   * @param assignment    - The shared variable assignment map.
+   */
+  constructor(
+    unaryOperator: UnaryOperator | undefined,
+    predicate: Predicate,
+    terms: Term[],
+    assignment: VariableAssignment,
+  ) {
+    this.unaryOperator = unaryOperator;
+    this.predicate = predicate;
+    this.terms = terms;
+    this._assignment = assignment;
+  }
+
+  /**
+   * Evaluate the atomic formula.
+   * Resolves each term against the current variable assignment, passes the
+   * resulting domain elements to the predicate, then applies negation if present.
+   */
+  value(): boolean {
+    const args = this.terms.map(t => t.resolve(this._assignment));
+    const rv = this.predicate.holds(...args);
+    return (this.unaryOperator === '~') ? !rv : rv;
+  }
+}

src/language/quantificational/complexFormula.ts

@@ -0,0 +1,53 @@
+import { QFF, BinaryOperator, UnaryOperator } from './quantificationalTypes';
+
+/** Binary operator truth-functional semantics (local to avoid module resolution issues). */
+const binaryOperatorToLogic: Record<string, (a: boolean, b: boolean) => boolean> = {
+  '&': (a, b) => a && b,
+  '|': (a, b) => a || b,
+  '->': (a, b) => !a || b,
+  '<->': (a, b) => a === b,
+};
+
+/**
+ * Concrete implementation of a complex quantificational formula.
+ *
+ * Joins two QFFs with a binary connective and evaluates them according to
+ * standard truth-functional semantics. An optional outer negation operator
+ * is applied to the result of the binary operation.
+ *
+ * Structurally identical to propositional ComplexImpl.
+ */
+export class ComplexFormulaImpl implements QFF {
+
+  /** The left-hand sub-formula. */
+  left: QFF;
+  /** Optional negation applied to the result of the binary operation. */
+  unaryOperator: UnaryOperator | undefined;
+  /** The binary connective joining left and right. */
+  binaryOperator: BinaryOperator;
+  /** The right-hand sub-formula. */
+  right: QFF;
+
+  /**
+   * @param unaryOperator  - Optional '~' to negate the whole formula.
+   * @param left           - The left-hand QFF.
+   * @param binaryOperator - The connective joining left and right.
+   * @param right          - The right-hand QFF.
+   */
+  constructor(unaryOperator: UnaryOperator | undefined, left: QFF, binaryOperator: BinaryOperator, right: QFF) {
+    this.left = left;
+    this.unaryOperator = unaryOperator;
+    this.binaryOperator = binaryOperator;
+    this.right = right;
+  }
+
+  /**
+   * Evaluate the complex formula.
+   * Combines left.value() and right.value() via the binary operator's
+   * truth-functional semantics, then applies outer negation if present.
+   */
+  value(): boolean {
+    const rv = binaryOperatorToLogic[this.binaryOperator](this.left.value(), this.right.value());
+    return (this.unaryOperator === '~') ? !rv : rv;
+  }
+}

src/language/quantificational/index.ts

@@ -1,4 +1,10 @@
-// TODO: Quantificational logic
-// Extends propositional logic with universal (∀) and existential (∃) quantifiers,
-// predicate symbols, individual constants, and variables.
-export {};
+export * from './quantificationalTypes';
+export * from './term';
+export * from './predicate';
+export * from './atomicFormula';
+export * from './complexFormula';
+export * from './quantifiedFormula';
+export * from './quantificationalVariable';
+export * from './quantificationalUtils';
+export * from './quantificationalTheory';
+export * from './quantificationalTheoryBuilder';