diff --git a/CLAUDE.md b/CLAUDE.md index fe69eab..23b38b3 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -41,8 +41,8 @@ src/ language/ shared/ types.ts # Formula, AlethicAssertoric, SentenceSet - theory.ts # FormalSentence, ConsistencyResult, - # ProofNode, Theory interface + theory.ts # FormalSentence, ConsistencyResult, + # ProofNode, Theory 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` | Pairs `AlethicAssertoric` source with a typed formula `F` and a label | -| `ConsistencyResult` | Outcome of a consistency check: witness or failed valuations | +| `ConsistencyResult` | Outcome of a consistency check: witness or failed valuations (`V` defaults to `boolean`, quantificational uses `DomainElement`) | | `ProofNode` | Node in a structured proof tree | -| `Theory` | Interface all formal theories must implement | +| `Theory` | 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`, 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`: +- `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 diff --git a/README.md b/README.md index efd51d8..3aa3e39 100644 --- a/README.md +++ b/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 diff --git a/src/language/propositional/README.md b/docs/languages/propositional/DEFINITIONS.md similarity index 100% rename from src/language/propositional/README.md rename to docs/languages/propositional/DEFINITIONS.md diff --git a/docs/languages/quantificational/DEFINITIONS.md b/docs/languages/quantificational/DEFINITIONS.md new file mode 100644 index 0000000..3896dd4 --- /dev/null +++ b/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 diff --git a/src/language/quantificational/atomicFormula.ts b/src/language/quantificational/atomicFormula.ts new file mode 100644 index 0000000..ee116c5 --- /dev/null +++ b/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; + } +} diff --git a/src/language/quantificational/complexFormula.ts b/src/language/quantificational/complexFormula.ts new file mode 100644 index 0000000..042d58e --- /dev/null +++ b/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 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; + } +} diff --git a/src/language/quantificational/index.ts b/src/language/quantificational/index.ts index 102da24..0bcc891 100644 --- a/src/language/quantificational/index.ts +++ b/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'; diff --git a/src/language/quantificational/predicate.ts b/src/language/quantificational/predicate.ts new file mode 100644 index 0000000..cb8bc9f --- /dev/null +++ b/src/language/quantificational/predicate.ts @@ -0,0 +1,60 @@ +import { Predicate, DomainElement } from './quantificationalTypes'; + +/** + * Concrete implementation of the Predicate interface. + * + * An n-ary relation over domain elements. The interpretation function + * determines which tuples of domain elements satisfy the predicate. + * + * Examples: + * - Unary: "is mortal" — `new PredicateImpl('Mortal', 1, (x) => mortals.has(x))` + * - Binary: "loves" — `new PredicateImpl('Loves', 2, (x, y) => ...)` + */ +export class PredicateImpl implements Predicate { + + /** The name of this predicate. */ + readonly name: string; + + /** The number of arguments this predicate expects. */ + readonly arity: number; + + /** The interpretation function that determines truth for given arguments. */ + private readonly _holds: (...args: DomainElement[]) => boolean; + + /** + * @param name - Display name for the predicate. + * @param arity - Number of arguments expected. + * @param holds - Interpretation function mapping domain elements to a truth value. + */ + constructor(name: string, arity: number, holds: (...args: DomainElement[]) => boolean) { + this.name = name; + this.arity = arity; + this._holds = holds; + } + + /** + * Determine whether the predicate holds for the given domain elements. + * Throws if the number of arguments does not match the declared arity. + */ + holds(...args: DomainElement[]): boolean { + if (args.length !== this.arity) { + throw new Error( + `Predicate '${this.name}' has arity ${this.arity} but received ${args.length} argument(s).` + ); + } + return this._holds(...args); + } +} + +/** + * Built-in identity (equality) predicate: holds when both arguments + * denote the same domain element. + * + * Formally redundant — any user can define `new PredicateImpl('=', 2, (x, y) => x === y)`. + * Provided for convenience since identity statements are ubiquitous in + * first-order logic (e.g. "Hesperus = Phosphorus", ∀x.(x = x)). + * + * Usage: + * new AtomicFormulaImpl(undefined, IDENTITY, [termA, termB], assignment) + */ +export const IDENTITY = new PredicateImpl('=', 2, (x, y) => x === y); diff --git a/src/language/quantificational/quantificationalTheory.ts b/src/language/quantificational/quantificationalTheory.ts new file mode 100644 index 0000000..c2f14d2 --- /dev/null +++ b/src/language/quantificational/quantificationalTheory.ts @@ -0,0 +1,289 @@ +import { QFF, DomainElement, VariableAssignment } from './quantificationalTypes'; +import { QuantificationalVariable } from './quantificationalVariable'; +import { FormalSentence, Theory, ConsistencyResult, ProofNode } from '../shared/theory'; + +// ─── Types ─────────────────────────────────────────────────────────────────── + +/** + * A formalised sentence within a quantificational theory. + * Extends FormalSentence with the set of free variable names the formula + * depends on, used when rendering the logical relations graph. + */ +export interface QuantificationalFormalSentence extends FormalSentence { + /** Names of the free variables this formula's truth value depends on. */ + variableNames: string[]; +} + +// ─── Internal helpers ──────────────────────────────────────────────────────── + +/** + * Render a variable assignment as a human-readable string. + */ +function formatValuation(v: Record): string { + return '{' + Object.entries(v).map(([k, val]) => `${k}=${val}`).join(', ') + '}'; +} + +/** + * Recursively print a proof tree node with box-drawing indentation. + */ +function printTree(node: ProofNode, prefix: string, isLast: boolean): void { + const connector = isLast ? '└── ' : '├── '; + const childPfx = prefix + (isLast ? ' ' : '│ '); + console.log(prefix + connector + node.label); + node.children.forEach((child, i) => + printTree(child, childPfx, i === node.children.length - 1), + ); +} + +/** + * Print the root of a proof tree, then recursively print all children. + */ +function printTreeRoot(node: ProofNode): void { + console.log(node.label); + node.children.forEach((child, i) => + printTree(child, '', i === node.children.length - 1), + ); +} + +// ─── QuantificationalTheory ───────────────────────────────────────────────── + +/** + * A formal quantificational theory — a finite set of QFFs derived from + * assertoric sentences, equipped with consistency checking over a finite + * domain and structured output. + * + * 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), + * directly paralleling the propositional 2^n truth-table approach. + * + * Construct via QuantificationalTheoryBuilder, not directly. + */ +export class QuantificationalTheory implements Theory { + + /** The formalised sentences constituting this theory. */ + readonly sentences: QuantificationalFormalSentence[]; + + /** The finite domain of discourse. */ + readonly domain: DomainElement[]; + + /** The named individual variables shared across sentences, keyed by name. */ + private readonly variables: Map; + + /** The shared variable assignment. */ + private readonly assignment: VariableAssignment; + + constructor( + sentences: QuantificationalFormalSentence[], + domain: DomainElement[], + variables: Map, + assignment: VariableAssignment, + ) { + this.sentences = sentences; + this.domain = domain; + this.variables = variables; + this.assignment = assignment; + } + + // ── Public API ───────────────────────────────────────────────────────────── + + /** + * Determine whether all sentences in the theory can be simultaneously true + * under some assignment of free variables to domain elements. + * + * Algorithm: exhaustive enumeration of all |D|^n variable assignments. + * Returns on the first satisfying assignment (consistent) or after all + * assignments are exhausted (inconsistent). + */ + checkConsistency(): ConsistencyResult { + const freeVarNames = Array.from(this.variables.keys()); + const total = Math.pow(this.domain.length, freeVarNames.length); + const failedValuations: NonNullable['failedValuations']> = []; + + for (let i = 0; i < total; i++) { + const valuation = this._applyAssignment(freeVarNames, i); + + const firstFailing = this.sentences.find(s => !s.formula.value()); + if (!firstFailing) { + return { isConsistent: true, witness: valuation }; + } + failedValuations.push({ valuation, firstFailure: firstFailing.label }); + } + + return { isConsistent: false, failedValuations }; + } + + /** + * Build a structured proof tree of the consistency result. + * + * Consistent: root carries "CONSISTENT ✓"; children show the witness + * assignment and a verification row for each sentence. + * + * Inconsistent: root carries "INCONSISTENT ✗"; children show, for every + * variable assignment, which sentence first fails. + */ + buildProofTree(): ProofNode { + const result = this.checkConsistency(); + const freeVarNames = Array.from(this.variables.keys()); + const n = freeVarNames.length; + const dSize = this.domain.length; + const total = Math.pow(dSize, n); + const header = `Theory: ${this.sentences.length} sentence(s), ` + + `${n} free variable(s) {${freeVarNames.join(', ')}}, ` + + `domain size ${dSize} {${this.domain.join(', ')}}`; + + if (result.isConsistent) { + // Restore the witness so formula.value() reflects it. + Object.entries(result.witness!).forEach(([name, v]) => + this.assignment.set(name, v), + ); + + return { + label: 'CONSISTENT ✓', + children: [ + { label: header, children: [] }, + { label: `Method: exhaustive evaluation, ${dSize}^${n} = ${total} assignments checked`, children: [] }, + { label: `Satisfying assignment: ${formatValuation(result.witness!)}`, children: [] }, + { + label: 'Verification:', + children: this.sentences.map(s => ({ + label: `${s.label} ${s.formula.value() ? '✓' : '✗'} "${s.source.raw}"`, + children: [], + })), + }, + ], + }; + } + + return { + label: 'INCONSISTENT ✗', + children: [ + { label: header, children: [] }, + { label: `Method: exhaustive evaluation, ${dSize}^${n} = ${total} assignments checked`, children: [] }, + { + label: `No satisfying assignment exists. Exhaustion:`, + children: result.failedValuations!.map(fv => ({ + label: `${formatValuation(fv.valuation)} → ${fv.firstFailure} fails`, + children: [], + })), + }, + ], + }; + } + + /** Print the proof tree to the console. */ + printProof(): void { + const tree = this.buildProofTree(); + console.log('\nCONSISTENCY PROOF — Quantificational Logic'); + console.log('═'.repeat(45)); + printTreeRoot(tree); + console.log(''); + } + + /** + * Print a graph of logical relations between sentences to the console. + */ + printGraph(): void { + const n = this.sentences.length; + + console.log('\nLOGICAL RELATIONS GRAPH — Quantificational Logic'); + console.log('═'.repeat(51)); + + // Nodes + console.log('\nSentences:'); + this.sentences.forEach(s => { + const vars = s.variableNames.length ? ` [${s.variableNames.join(', ')}]` : ''; + console.log(` ${s.label.padEnd(5)} "${s.source.raw}"${vars}`); + }); + + // Pairwise relations + if (n > 1) { + console.log('\nPairwise relations:'); + const freeVarNames = Array.from(this.variables.keys()); + for (let i = 0; i < n; i++) { + for (let j = i + 1; j < n; j++) { + const rel = this._pairwiseRelation(this.sentences[i], this.sentences[j], freeVarNames); + const tag = this._relationLabel(rel, this.sentences[i].label, this.sentences[j].label); + console.log(` ${this.sentences[i].label} ↔ ${this.sentences[j].label} ${tag}`); + } + } + } + + // Shared variables + const varToSentences = new Map(); + this.sentences.forEach(s => + s.variableNames.forEach(v => { + if (!varToSentences.has(v)) varToSentences.set(v, []); + varToSentences.get(v)!.push(s.label); + }), + ); + const shared = Array.from(varToSentences.entries()).filter(([, labels]) => labels.length > 1); + if (shared.length) { + console.log('\nShared variables:'); + shared.forEach(([varName, labels]) => + console.log(` ${varName}: ${labels.join(' — ')}`), + ); + } + + console.log(''); + } + + // ── Private helpers ──────────────────────────────────────────────────────── + + /** + * Apply the i-th assignment from the enumeration of |D|^n assignments. + * Treats i as a base-|D| number where each digit selects a domain element + * for the corresponding variable. + */ + private _applyAssignment(varNames: string[], index: number): Record { + const valuation: Record = {}; + let remaining = index; + varNames.forEach(name => { + const dIndex = remaining % this.domain.length; + remaining = Math.floor(remaining / this.domain.length); + const element = this.domain[dIndex]; + this.assignment.set(name, element); + valuation[name] = element; + }); + return valuation; + } + + /** + * Compute the pairwise logical relation between two sentences. + */ + private _pairwiseRelation( + s1: QuantificationalFormalSentence, + s2: QuantificationalFormalSentence, + varNames: string[], + ): string { + let bothTrue = false; + let s1TrueS2False = false; + let s1FalseS2True = false; + + const total = Math.pow(this.domain.length, varNames.length); + for (let i = 0; i < total; i++) { + this._applyAssignment(varNames, i); + const v1 = s1.formula.value(); + const v2 = s2.formula.value(); + if (v1 && v2) bothTrue = true; + if (v1 && !v2) s1TrueS2False = true; + if (!v1 && v2) s1FalseS2True = true; + } + + if (!bothTrue) return 'INCONSISTENT'; + if (!s1TrueS2False && !s1FalseS2True) return 'EQUIVALENT'; + if (!s1TrueS2False) return 'ENTAILS_LEFT'; + if (!s1FalseS2True) return 'ENTAILS_RIGHT'; + return 'CONSISTENT'; + } + + private _relationLabel(rel: string, l1: string, l2: string): string { + switch (rel) { + case 'INCONSISTENT': return 'INCONSISTENT (cannot both be true)'; + case 'EQUIVALENT': return `EQUIVALENT (${l1} ⟺ ${l2})`; + case 'ENTAILS_RIGHT': return `ENTAILS (${l1} ⊨ ${l2})`; + case 'ENTAILS_LEFT': return `ENTAILS (${l2} ⊨ ${l1})`; + case 'CONSISTENT': return 'consistent (can both be true)'; + default: return rel; + } + } +} diff --git a/src/language/quantificational/quantificationalTheoryBuilder.ts b/src/language/quantificational/quantificationalTheoryBuilder.ts new file mode 100644 index 0000000..8ad83ac --- /dev/null +++ b/src/language/quantificational/quantificationalTheoryBuilder.ts @@ -0,0 +1,132 @@ +import { QFF, DomainElement, VariableAssignment } from './quantificationalTypes'; +import { QuantificationalVariable } from './quantificationalVariable'; +import { PredicateImpl } from './predicate'; +import { QuantificationalFormalSentence, QuantificationalTheory } from './quantificationalTheory'; +import { AlethicAssertoric, SentenceSet } from '../shared/types'; + +/** + * Fluent builder for constructing a QuantificationalTheory. + * + * Declare a domain with domain(), variables with variable(), predicates + * with predicate(), register sentences with sentence(), then call build() + * to produce an immutable QuantificationalTheory ready for consistency + * checking and graph output. + */ +export class QuantificationalTheoryBuilder { + + private _domain: DomainElement[] = []; + private readonly _assignment: VariableAssignment = new Map(); + private readonly _variables = new Map(); + private readonly _predicates = new Map(); + private readonly _sentences: QuantificationalFormalSentence[] = []; + private _labelCounter = 1; + + /** + * Set the finite domain of discourse. + * + * @param elements - The domain elements to quantify over. + * @returns this, for method chaining. + */ + domain(...elements: DomainElement[]): this { + this._domain = elements; + return this; + } + + /** + * Declare a named individual variable. + * Calling variable() with the same name twice returns the same instance. + * + * @param name - The logical name for the variable (e.g. 'x', 'y'). + * @returns The QuantificationalVariable instance for that name. + */ + variable(name: string): QuantificationalVariable { + if (!this._variables.has(name)) { + this._variables.set(name, new QuantificationalVariable(name, this._assignment)); + } + return this._variables.get(name)!; + } + + /** + * Declare a named predicate. + * Calling predicate() with the same name twice returns the same instance. + * + * @param name - Display name (e.g. 'Mortal', 'Loves'). + * @param arity - Number of arguments. + * @param holds - Interpretation function. + * @returns The PredicateImpl instance. + */ + predicate(name: string, arity: number, holds: (...args: DomainElement[]) => boolean): PredicateImpl { + if (!this._predicates.has(name)) { + this._predicates.set(name, new PredicateImpl(name, arity, holds)); + } + return this._predicates.get(name)!; + } + + /** + * Add a formalised sentence to the theory under construction. + * + * @param source - The validated natural language sentence. + * @param formula - The QFF that formalises the sentence. + * @param variableNames - Names of the free variables this formula depends on. + * @param label - Optional display label; defaults to φ1, φ2, … + * @returns this, for method chaining. + */ + sentence( + source: AlethicAssertoric, + formula: QFF, + variableNames: string[], + label?: string, + ): this { + this._sentences.push({ + source, + formula, + variableNames, + label: label ?? `φ${this._labelCounter++}`, + }); + return this; + } + + /** + * The shared variable assignment map. + * Exposed so formula constructors can reference it. + */ + get assignment(): VariableAssignment { + return this._assignment; + } + + /** + * The current domain. + * Exposed so formula constructors can reference it. + */ + get currentDomain(): DomainElement[] { + return this._domain; + } + + /** + * Finalise and return the QuantificationalTheory. + * + * @returns A new QuantificationalTheory containing all sentences added so far. + */ + build(): QuantificationalTheory { + return new QuantificationalTheory( + [...this._sentences], + [...this._domain], + new Map(this._variables), + this._assignment, + ); + } + + /** + * Placeholder: future entry point for NLP-driven construction. + * + * @param _set - The sentence set to formalise. + * @throws Error until QuantificationalSyntaxEngine is implemented. + */ + // eslint-disable-next-line @typescript-eslint/no-unused-vars + fromSentenceSet(_set: SentenceSet): QuantificationalTheory { + throw new Error( + 'QuantificationalTheoryBuilder.fromSentenceSet is not yet implemented. ' + + 'Awaiting QuantificationalSyntaxEngine.', + ); + } +} diff --git a/src/language/quantificational/quantificationalTypes.d.ts b/src/language/quantificational/quantificationalTypes.d.ts new file mode 100644 index 0000000..43f241d --- /dev/null +++ b/src/language/quantificational/quantificationalTypes.d.ts @@ -0,0 +1,87 @@ +import { Formula } from '../shared/types'; + +/** + * An element of the finite domain of discourse. + * Domains are finite sets of these values — quantifiers enumerate over them. + */ +type DomainElement = string | number; + +/** + * A mapping from individual variable names to domain elements. + * Updated during quantifier evaluation to bind variables to specific elements. + */ +type VariableAssignment = Map; + +/** + * A term in quantificational logic — either an individual variable or a constant. + * Terms denote domain elements; variables are resolved via the current assignment, + * constants denote fixed elements. + */ +interface Term { + /** Resolve to a domain element given the current variable assignment. */ + resolve(assignment: VariableAssignment): DomainElement; +} + +/** + * An n-ary predicate (relation) over domain elements. + * Predicates are the atomic truth-bearers of quantificational logic — they map + * tuples of domain elements to truth values. + */ +interface Predicate { + /** The name of this predicate (e.g. 'F', 'Mortal', 'Loves'). */ + name: string; + /** The number of arguments this predicate takes. */ + arity: number; + /** Determine whether the predicate holds for the given arguments. */ + holds(...args: DomainElement[]): boolean; +} + +/** + * The quantifiers of first-order logic. + * + * ∀ := Universal — "for all" + * ∃ := Existential — "there exists" + */ +type Quantifier = '∀' | '∃'; + +/** + * The only unary logical operator. + * Operates on a single formula and negates its truth value. + * + * ~ := NOT + */ +type UnaryOperator = '~'; + +/** + * Binary logical connectives that join two formulas into a composite formula. + * + * & := AND (conjunction) + * | := OR (disjunction) + * -> := Material Implication (if … then …) + * <-> := Biconditional (if and only if) + */ +type BinaryOperator = '&' | '|' | '->' | '<->'; + +/** + * A Quantificational Formula — the union of all valid first-order expressions. + * Every syntactically correct quantificational expression satisfies this type. + * + * Analogous to WFF in propositional logic. + */ +interface QFF extends Formula { + /** Optional negation applied to the formula before evaluation. */ + unaryOperator: UnaryOperator | undefined; + /** Evaluate the formula under the current domain and variable assignment. */ + value(): boolean; +} + +export { + DomainElement, + VariableAssignment, + Term, + Predicate, + Quantifier, + UnaryOperator, + BinaryOperator, + QFF, +}; diff --git a/src/language/quantificational/quantificationalUtils.ts b/src/language/quantificational/quantificationalUtils.ts new file mode 100644 index 0000000..811482d --- /dev/null +++ b/src/language/quantificational/quantificationalUtils.ts @@ -0,0 +1,46 @@ +import { QFF } from './quantificationalTypes'; + +/** + * Lookup table mapping each binary operator to its truth-functional semantics + * as a two-argument boolean function. + * + * Same semantics as propositional — kept local to avoid cross-module coupling. + * + * - `&` conjunction: true iff both operands are true + * - `|` disjunction: true iff at least one operand is true + * - `->` material implication: false only when the antecedent is true and the consequent is false + * - `<->` biconditional: true iff both operands share the same truth value + */ +const binaryOperatorToLogic: Record boolean> = { + '&': (a: boolean, b: boolean) => a && b, + '|': (a: boolean, b: boolean) => a || b, + '->': (a: boolean, b: boolean) => !a || b, + '<->': (a: boolean, b: boolean) => a === b, +}; + +/** + * Type guard: returns true when the given QFF has atomic formula shape. + * Uses structural check (presence of 'predicate' property) to avoid + * circular dependency with atomicFormula.ts. + */ +const isAtomicFormula = (qff: QFF): boolean => { + return 'predicate' in qff && 'terms' in qff; +}; + +/** + * Type guard: returns true when the given QFF has complex formula shape. + * Uses structural check to avoid circular dependency with complexFormula.ts. + */ +const isComplexFormula = (qff: QFF): boolean => { + return 'left' in qff && 'binaryOperator' in qff && 'right' in qff; +}; + +/** + * Type guard: returns true when the given QFF has quantified formula shape. + * Uses structural check to avoid circular dependency with quantifiedFormula.ts. + */ +const isQuantifiedFormula = (qff: QFF): boolean => { + return 'quantifier' in qff && 'variableName' in qff && 'body' in qff; +}; + +export { binaryOperatorToLogic, isAtomicFormula, isComplexFormula, isQuantifiedFormula }; diff --git a/src/language/quantificational/quantificationalVariable.ts b/src/language/quantificational/quantificationalVariable.ts new file mode 100644 index 0000000..af1b84b --- /dev/null +++ b/src/language/quantificational/quantificationalVariable.ts @@ -0,0 +1,71 @@ +import { VariableAssignment, DomainElement } from './quantificationalTypes'; +import { VariableTerm } from './term'; +import { AtomicFormulaImpl } from './atomicFormula'; +import { PredicateImpl } from './predicate'; + +/** + * A named individual variable with a mutable domain-element binding. + * + * Analogous to PropositionalVariable. All terms and atomic formulas created + * from this variable share the same underlying assignment map, so updating + * the variable's binding (by mutating the assignment) updates every derived + * formula simultaneously. + * + * Used by QuantificationalTheory to iterate over domain assignments during + * consistency checking, and by QuantifiedFormulaImpl to bind variables + * during quantifier evaluation. + */ +export class QuantificationalVariable { + + /** The immutable name of this variable, used for display and graph output. */ + readonly name: string; + + /** The shared variable assignment map this variable participates in. */ + private readonly _assignment: VariableAssignment; + + /** + * @param name - The logical name for this variable (e.g. 'x', 'y'). + * @param assignment - The shared variable assignment map. + */ + constructor(name: string, assignment: VariableAssignment) { + this.name = name; + this._assignment = assignment; + } + + /** + * Assign a domain element to this variable. + * All formulas referencing this variable are updated immediately. + */ + assign(element: DomainElement): void { + this._assignment.set(this.name, element); + } + + /** The variable's current assigned domain element, or undefined if unbound. */ + get current(): DomainElement | undefined { + return this._assignment.get(this.name); + } + + /** + * Return a new VariableTerm referencing this variable. + * The term resolves to whatever element is currently assigned. + */ + term(): VariableTerm { + return new VariableTerm(this.name); + } + + /** + * Create an atomic formula applying a predicate to this variable's term. + * Convenience shortcut for unary predicates. + * + * @param predicate - The predicate to apply. + * @param negated - When true, wraps the formula with '~'. + */ + atomicFormula(predicate: PredicateImpl, negated = false): AtomicFormulaImpl { + return new AtomicFormulaImpl( + negated ? '~' : undefined, + predicate, + [this.term()], + this._assignment, + ); + } +} diff --git a/src/language/quantificational/quantifiedFormula.ts b/src/language/quantificational/quantifiedFormula.ts new file mode 100644 index 0000000..c2e9716 --- /dev/null +++ b/src/language/quantificational/quantifiedFormula.ts @@ -0,0 +1,92 @@ +import { QFF, UnaryOperator, Quantifier, DomainElement, VariableAssignment } from './quantificationalTypes'; + +/** + * Concrete implementation of a quantified formula. + * + * This is the construct that distinguishes quantificational from propositional + * logic. Binds a variable over a finite domain and evaluates the body formula + * for each element. + * + * ∀x.φ(x) — true iff φ is true for every element in the domain + * ∃x.φ(x) — true iff φ is true for at least one element in the domain + */ +export class QuantifiedFormulaImpl implements QFF { + + /** Optional negation applied to the quantified result. */ + unaryOperator: UnaryOperator | undefined; + + /** The quantifier: ∀ (universal) or ∃ (existential). */ + readonly quantifier: Quantifier; + + /** The name of the bound variable. */ + readonly variableName: string; + + /** The body (scope/matrix) of the quantified formula. */ + readonly body: QFF; + + /** The finite domain of discourse. */ + private readonly _domain: DomainElement[]; + + /** The shared variable assignment, mutated during evaluation. */ + private readonly _assignment: VariableAssignment; + + /** + * @param unaryOperator - Optional '~' to negate the whole quantified result. + * @param quantifier - '∀' or '∃'. + * @param variableName - The variable being bound. + * @param body - The formula in the scope of the quantifier. + * @param domain - The finite domain to quantify over. + * @param assignment - The shared variable assignment map. + */ + constructor( + unaryOperator: UnaryOperator | undefined, + quantifier: Quantifier, + variableName: string, + body: QFF, + domain: DomainElement[], + assignment: VariableAssignment, + ) { + this.unaryOperator = unaryOperator; + this.quantifier = quantifier; + this.variableName = variableName; + this.body = body; + this._domain = domain; + this._assignment = assignment; + } + + /** + * Evaluate the quantified formula. + * + * For ∀: iterates over every domain element, assigning each to the bound + * variable and evaluating the body. Returns true iff the body is true for + * every element. Restores the previous binding after evaluation. + * + * For ∃: same iteration but returns true iff the body is true for at least + * one element. + */ + value(): boolean { + const previous = this._assignment.get(this.variableName); + let rv: boolean; + + if (this.quantifier === '∀') { + rv = this._domain.every(d => { + this._assignment.set(this.variableName, d); + return this.body.value(); + }); + } else { + rv = this._domain.some(d => { + this._assignment.set(this.variableName, d); + return this.body.value(); + }); + } + + // Restore previous binding (or delete if there was none). + if (previous !== undefined) { + this._assignment.set(this.variableName, previous); + } else { + this._assignment.delete(this.variableName); + } + + return (this.unaryOperator === '~') ? !rv : rv; + } +} diff --git a/src/language/quantificational/term.ts b/src/language/quantificational/term.ts new file mode 100644 index 0000000..08a6e1f --- /dev/null +++ b/src/language/quantificational/term.ts @@ -0,0 +1,49 @@ +import { Term, DomainElement, VariableAssignment } from './quantificationalTypes'; + +/** + * A variable term — resolves to whatever domain element the variable is + * currently assigned to in the variable assignment. + * + * Analogous to how a PropositionalVariable's atom reads a mutable value + * via closure — here the variable looks up its current binding in the + * assignment map. + */ +export class VariableTerm implements Term { + + /** The name of the individual variable (e.g. 'x', 'y'). */ + readonly name: string; + + constructor(name: string) { + this.name = name; + } + + /** + * Resolve the variable by looking up its name in the assignment. + * Throws if the variable is unbound (not present in the assignment). + */ + resolve(assignment: VariableAssignment): DomainElement { + if (!assignment.has(this.name)) { + throw new Error(`Unbound variable: '${this.name}'`); + } + return assignment.get(this.name)!; + } +} + +/** + * A constant term — always resolves to its fixed domain element, + * regardless of the variable assignment. + */ +export class ConstantTerm implements Term { + + /** The fixed domain element this constant denotes. */ + readonly element: DomainElement; + + constructor(element: DomainElement) { + this.element = element; + } + + /** Constants ignore the assignment — they always return their fixed element. */ + resolve(_assignment: VariableAssignment): DomainElement { + return this.element; + } +} diff --git a/src/language/shared/theory.ts b/src/language/shared/theory.ts index 5554462..17d789d 100644 --- a/src/language/shared/theory.ts +++ b/src/language/shared/theory.ts @@ -32,14 +32,14 @@ export interface ProofNode { * For an inconsistent theory, `failedValuations` records, for every * possible assignment, which sentence first failed — proving exhaustion. */ -export interface ConsistencyResult { +export interface ConsistencyResult { /** True when a satisfying variable assignment exists; false otherwise. */ isConsistent: boolean; /** A satisfying variable assignment if the theory is consistent. */ - witness?: Record; + witness?: Record; /** Evidence of exhaustion for each valuation if the theory is inconsistent. */ failedValuations?: Array<{ - valuation: Record; + valuation: Record; firstFailure: string; }>; } @@ -52,12 +52,12 @@ export interface ConsistencyResult { * and to produce both a structured proof tree and a console-printable * logical relations graph. */ -export interface Theory { +export interface Theory { /** The sentences constituting this theory. */ sentences: FormalSentence[]; /** Determine whether all sentences can be simultaneously true. */ - checkConsistency(): ConsistencyResult; + checkConsistency(): ConsistencyResult; /** * Build a structured proof tree of the consistency result. diff --git a/test/language/quantificational/atomicFormula.spec.ts b/test/language/quantificational/atomicFormula.spec.ts new file mode 100644 index 0000000..3b26bd3 --- /dev/null +++ b/test/language/quantificational/atomicFormula.spec.ts @@ -0,0 +1,132 @@ +import { AtomicFormulaImpl } from '../../../src/language/quantificational/atomicFormula'; +import { PredicateImpl } from '../../../src/language/quantificational/predicate'; +import { VariableTerm, ConstantTerm } from '../../../src/language/quantificational/term'; +import { VariableAssignment } from '../../../src/language/quantificational/quantificationalTypes'; + +describe('AtomicFormula Tests', () => { + + describe('evaluation with constants', () => { + + test('F(a) evaluates to true when predicate holds for constant', () => { + const mortals = new Set(['socrates']); + const Mortal = new PredicateImpl('Mortal', 1, (x) => mortals.has(x as string)); + const a = new ConstantTerm('socrates'); + const assignment: VariableAssignment = new Map(); + + const formula = new AtomicFormulaImpl(undefined, Mortal, [a], assignment); + expect(formula.value()).toBe(true); + }); + + test('F(a) evaluates to false when predicate does not hold', () => { + const mortals = new Set(['socrates']); + const Mortal = new PredicateImpl('Mortal', 1, (x) => mortals.has(x as string)); + const a = new ConstantTerm('zeus'); + const assignment: VariableAssignment = new Map(); + + const formula = new AtomicFormulaImpl(undefined, Mortal, [a], assignment); + expect(formula.value()).toBe(false); + }); + + test('R(a, b) binary predicate with constants', () => { + const Loves = new PredicateImpl('Loves', 2, (x, y) => x === 'socrates' && y === 'plato'); + const a = new ConstantTerm('socrates'); + const b = new ConstantTerm('plato'); + const assignment: VariableAssignment = new Map(); + + const formula = new AtomicFormulaImpl(undefined, Loves, [a, b], assignment); + expect(formula.value()).toBe(true); + }); + }); + + describe('evaluation with variables', () => { + + test('F(x) evaluates relative to current assignment', () => { + const mortals = new Set(['socrates', 'plato']); + const Mortal = new PredicateImpl('Mortal', 1, (x) => mortals.has(x as string)); + const x = new VariableTerm('x'); + const assignment: VariableAssignment = new Map([['x', 'socrates']]); + + const formula = new AtomicFormulaImpl(undefined, Mortal, [x], assignment); + expect(formula.value()).toBe(true); + + assignment.set('x', 'zeus'); + expect(formula.value()).toBe(false); + }); + + test('R(x, y) evaluates relative to both variable assignments', () => { + const LessThan = new PredicateImpl('LessThan', 2, (a, b) => (a as number) < (b as number)); + const x = new VariableTerm('x'); + const y = new VariableTerm('y'); + const assignment: VariableAssignment = new Map([['x', 1], ['y', 2]]); + + const formula = new AtomicFormulaImpl(undefined, LessThan, [x, y], assignment); + expect(formula.value()).toBe(true); + + assignment.set('x', 3); + expect(formula.value()).toBe(false); + }); + + test('mixed terms: R(a, x) with constant and variable', () => { + const Loves = new PredicateImpl('Loves', 2, (a, b) => a === 'socrates' && b === 'plato'); + const a = new ConstantTerm('socrates'); + const x = new VariableTerm('x'); + const assignment: VariableAssignment = new Map([['x', 'plato']]); + + const formula = new AtomicFormulaImpl(undefined, Loves, [a, x], assignment); + expect(formula.value()).toBe(true); + + assignment.set('x', 'aristotle'); + expect(formula.value()).toBe(false); + }); + }); + + describe('negation', () => { + + test('~F(a) negates the predicate result', () => { + const F = new PredicateImpl('F', 1, () => true); + const a = new ConstantTerm('a'); + const assignment: VariableAssignment = new Map(); + + const formula = new AtomicFormulaImpl('~', F, [a], assignment); + expect(formula.value()).toBe(false); + }); + + test('~F(a) where predicate is false yields true', () => { + const F = new PredicateImpl('F', 1, () => false); + const a = new ConstantTerm('a'); + const assignment: VariableAssignment = new Map(); + + const formula = new AtomicFormulaImpl('~', F, [a], assignment); + expect(formula.value()).toBe(true); + }); + + test('undefined unary operator leaves value unchanged', () => { + const F = new PredicateImpl('F', 1, () => true); + const a = new ConstantTerm('a'); + const assignment: VariableAssignment = new Map(); + + const pos = new AtomicFormulaImpl(undefined, F, [a], assignment); + const neg = new AtomicFormulaImpl('~', F, [a], assignment); + expect(pos.value()).toBe(!neg.value()); + }); + }); + + describe('all rows of unary predicate truth table', () => { + + test('F(x) produces correct truth value for each domain element', () => { + const domain = ['a', 'b', 'c']; + const trueSet = new Set(['a', 'c']); + const F = new PredicateImpl('F', 1, (x) => trueSet.has(x as string)); + const x = new VariableTerm('x'); + const assignment: VariableAssignment = new Map(); + + const formula = new AtomicFormulaImpl(undefined, F, [x], assignment); + const expected = [true, false, true]; + + domain.forEach((d, i) => { + assignment.set('x', d); + expect(formula.value()).toBe(expected[i]); + }); + }); + }); +}); diff --git a/test/language/quantificational/complexFormula.spec.ts b/test/language/quantificational/complexFormula.spec.ts new file mode 100644 index 0000000..bc10d8f --- /dev/null +++ b/test/language/quantificational/complexFormula.spec.ts @@ -0,0 +1,103 @@ +import { ComplexFormulaImpl } from '../../../src/language/quantificational/complexFormula'; +import { AtomicFormulaImpl } from '../../../src/language/quantificational/atomicFormula'; +import { PredicateImpl } from '../../../src/language/quantificational/predicate'; +import { ConstantTerm } from '../../../src/language/quantificational/term'; +import { VariableAssignment, BinaryOperator } from '../../../src/language/quantificational/quantificationalTypes'; +import { binaryOperatorToLogic } from '../../../src/language/quantificational/quantificationalUtils'; + +// Helper to create an atomic formula that always returns a fixed boolean. +function fixedAtom(val: boolean): AtomicFormulaImpl { + const P = new PredicateImpl('P', 1, () => val); + return new AtomicFormulaImpl(undefined, P, [new ConstantTerm('a')], new Map()); +} + +describe('ComplexFormula Tests', () => { + + test('should apply unary operators to values', () => { + let complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '&', fixedAtom(true)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl('~', fixedAtom(true), '&', fixedAtom(true)); + expect(complex.value()).toBe(false); + }); + + test('should apply logical AND correctly', () => { + let complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '&', fixedAtom(true)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '&', fixedAtom(false)); + expect(complex.value()).toBe(false); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '&', fixedAtom(true)); + expect(complex.value()).toBe(false); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '&', fixedAtom(false)); + expect(complex.value()).toBe(false); + }); + + test('should apply logical OR correctly', () => { + let complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '|', fixedAtom(true)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '|', fixedAtom(false)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '|', fixedAtom(true)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '|', fixedAtom(false)); + expect(complex.value()).toBe(false); + }); + + test('should apply logical MATERIAL IMPLICATION correctly', () => { + let complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '->', fixedAtom(true)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '->', fixedAtom(false)); + expect(complex.value()).toBe(false); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '->', fixedAtom(true)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '->', fixedAtom(false)); + expect(complex.value()).toBe(true); + }); + + test('should apply logical BICONDITIONAL correctly', () => { + let complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '<->', fixedAtom(true)); + expect(complex.value()).toBe(true); + complex = new ComplexFormulaImpl(undefined, fixedAtom(true), '<->', fixedAtom(false)); + expect(complex.value()).toBe(false); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '<->', fixedAtom(true)); + expect(complex.value()).toBe(false); + complex = new ComplexFormulaImpl(undefined, fixedAtom(false), '<->', fixedAtom(false)); + expect(complex.value()).toBe(true); + }); + + describe('inductive step — all (op, L, R) combinations with and without negation', () => { + const operators: BinaryOperator[] = ['&', '|', '->', '<->']; + const boolPairs: [boolean, boolean][] = [[false,false],[false,true],[true,false],[true,true]]; + + operators.forEach(op => { + describe(`binary operator '${op}'`, () => { + boolPairs.forEach(([L, R]) => { + const expected = binaryOperatorToLogic[op](L, R); + + test(`value() of (${L} ${op} ${R}) = ${expected}`, () => { + const complex = new ComplexFormulaImpl(undefined, fixedAtom(L), op, fixedAtom(R)); + expect(complex.value()).toBe(expected); + }); + + test(`value() of ~(${L} ${op} ${R}) = ${!expected}`, () => { + const complex = new ComplexFormulaImpl('~', fixedAtom(L), op, fixedAtom(R)); + expect(complex.value()).toBe(!expected); + }); + }); + }); + }); + }); + + test('nesting: (A & B) | C', () => { + const inner = new ComplexFormulaImpl(undefined, fixedAtom(true), '&', fixedAtom(false)); + const outer = new ComplexFormulaImpl(undefined, inner, '|', fixedAtom(true)); + expect(outer.value()).toBe(true); // (T&F)|T = F|T = T + }); + + test('nesting: ~((A | B) -> C)', () => { + const inner1 = new ComplexFormulaImpl(undefined, fixedAtom(true), '|', fixedAtom(false)); + const inner2 = new ComplexFormulaImpl(undefined, inner1, '->', fixedAtom(false)); + const negated = new ComplexFormulaImpl('~', inner1, '->', fixedAtom(false)); + expect(inner2.value()).toBe(false); // (T|F)->F = T->F = F + expect(negated.value()).toBe(true); // ~((T|F)->F) = ~F = T + }); +}); diff --git a/test/language/quantificational/meta-logic/completeness.spec.ts b/test/language/quantificational/meta-logic/completeness.spec.ts new file mode 100644 index 0000000..c5e53a6 --- /dev/null +++ b/test/language/quantificational/meta-logic/completeness.spec.ts @@ -0,0 +1,365 @@ +import { AtomicFormulaImpl } from '../../../../src/language/quantificational/atomicFormula'; +import { ComplexFormulaImpl } from '../../../../src/language/quantificational/complexFormula'; +import { QuantifiedFormulaImpl } from '../../../../src/language/quantificational/quantifiedFormula'; +import { PredicateImpl } from '../../../../src/language/quantificational/predicate'; +import { VariableTerm } from '../../../../src/language/quantificational/term'; +import { VariableAssignment, DomainElement, BinaryOperator, QFF } from '../../../../src/language/quantificational/quantificationalTypes'; +import { binaryOperatorToLogic } from '../../../../src/language/quantificational/quantificationalUtils'; + +/** + * COMPLETENESS OF QUANTIFICATIONAL LOGIC (over finite domains) + * ───────────────────────────────────────────────────────────────────────────── + * Theorem: The exhaustive evaluation method is sound and complete for + * quantificational logic over finite domains. + * + * Soundness — if exhaustive evaluation returns true on every assignment, + * the formula is valid over that domain. + * + * Completeness — every formula valid over a finite domain is confirmed by + * the exhaustive method. + * + * Proof structure: + * + * Part I — Structural induction: value() correctly computes the truth + * function of any QFF under any domain and assignment. + * + * Base case: AtomicFormulaImpl correctly evaluates predicates + * applied to resolved terms, with and without negation. + * + * IH: left.value() and right.value() correctly return L and R. + * + * Ind. step: ComplexFormulaImpl correctly applies binary operators. + * QuantifiedFormulaImpl correctly iterates over all domain + * elements for ∀ and ∃. + * + * Part II — Consequence: known valid formulas, contradictions, and + * quantifier dualities are classified correctly. + * ───────────────────────────────────────────────────────────────────────────── + */ + +// ─── Test helpers ────────────────────────────────────────────────────────── + +/** Test domains of increasing size */ +const DOMAINS: DomainElement[][] = [ + ['a'], + ['a', 'b'], + ['a', 'b', 'c'], +]; + +/** + * Check whether a quantificational formula is valid (true under every + * variable assignment) for a given domain. For formulas with a single + * free variable x, enumerates all assignments of x. + */ +function isValidOverDomain( + formula: QFF, + domain: DomainElement[], + freeVars: string[], + assignment: VariableAssignment, +): boolean { + if (freeVars.length === 0) { + return formula.value(); + } + + const total = Math.pow(domain.length, freeVars.length); + for (let i = 0; i < total; i++) { + let remaining = i; + freeVars.forEach(name => { + const dIdx = remaining % domain.length; + remaining = Math.floor(remaining / domain.length); + assignment.set(name, domain[dIdx]); + }); + if (!formula.value()) return false; + } + return true; +} + +// ───────────────────────────────────────────────────────────────────────────── + +describe('Completeness of Quantificational Logic (finite domains)', () => { + + // ── Part I: Structural induction ─────────────────────────────────────────── + + describe('Part I — Structural induction: value() is semantically correct', () => { + + describe('Base case — AtomicFormulaImpl', () => { + + test('predicate applied to constant resolves correctly', () => { + const F = new PredicateImpl('F', 1, (x) => x === 'a'); + const assignment: VariableAssignment = new Map(); + expect(new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment).value.bind( + { ...new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], new Map([['x', 'a']])) } + )).toBeDefined(); + + // Direct test + const a1 = new Map([['x', 'a']]); + expect(new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], a1).value()).toBe(true); + + const a2 = new Map([['x', 'b']]); + expect(new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], a2).value()).toBe(false); + }); + + test('negation inverts the predicate result', () => { + const F = new PredicateImpl('F', 1, () => true); + const assignment = new Map([['x', 'a']]); + expect(new AtomicFormulaImpl('~', F, [new VariableTerm('x')], assignment).value()).toBe(false); + expect(new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment).value()).toBe(true); + }); + }); + + describe('Inductive step — ComplexFormulaImpl (binary operators)', () => { + const operators: BinaryOperator[] = ['&', '|', '->', '<->']; + const boolPairs: [boolean, boolean][] = [[false,false],[false,true],[true,false],[true,true]]; + + function fixedFormula(val: boolean): AtomicFormulaImpl { + const P = new PredicateImpl('P', 0, () => val); + return new AtomicFormulaImpl(undefined, P, [], new Map()); + } + + operators.forEach(op => { + boolPairs.forEach(([L, R]) => { + const expected = binaryOperatorToLogic[op](L, R); + test(`(${L} ${op} ${R}) = ${expected}`, () => { + expect(new ComplexFormulaImpl(undefined, fixedFormula(L), op, fixedFormula(R)).value()).toBe(expected); + }); + test(`~(${L} ${op} ${R}) = ${!expected}`, () => { + expect(new ComplexFormulaImpl('~', fixedFormula(L), op, fixedFormula(R)).value()).toBe(!expected); + }); + }); + }); + }); + + describe('Inductive step — QuantifiedFormulaImpl', () => { + + test('∀ iterates every element and is true only when body holds for all', () => { + DOMAINS.forEach(domain => { + const assignment: VariableAssignment = new Map(); + // F(x) true only for 'a' + const F = new PredicateImpl('F', 1, (x) => x === 'a'); + const body = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', body, domain, assignment); + + // Universal is true only on single-element domain {a} + expect(formula.value()).toBe(domain.length === 1 && domain[0] === 'a'); + }); + }); + + test('∃ iterates elements and is true when body holds for at least one', () => { + DOMAINS.forEach(domain => { + const assignment: VariableAssignment = new Map(); + // F(x) true only for 'a' + const F = new PredicateImpl('F', 1, (x) => x === 'a'); + const body = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const formula = new QuantifiedFormulaImpl(undefined, '∃', 'x', body, domain, assignment); + + // 'a' is in every test domain + expect(formula.value()).toBe(true); + }); + }); + }); + }); + + // ── Part II: Consequence — classification of formulas ───────────────────── + + describe('Part II — Quantifier duality', () => { + + test('~∀x.F(x) ⟺ ∃x.~F(x) (verified over domains of size 1–3)', () => { + DOMAINS.forEach(domain => { + // Test with various predicate extensions: empty, one element, all elements + const extensions: DomainElement[][] = [ + [], + [domain[0]], + [...domain], + ]; + + extensions.forEach(ext => { + const extSet = new Set(ext); + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => extSet.has(x)); + + const Fx = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const notFx = new AtomicFormulaImpl('~', F, [new VariableTerm('x')], assignment); + + const lhs = new QuantifiedFormulaImpl('~', '∀', 'x', Fx, domain, assignment); + const rhs = new QuantifiedFormulaImpl(undefined, '∃', 'x', notFx, domain, assignment); + + expect(lhs.value()).toBe(rhs.value()); + }); + }); + }); + + test('~∃x.F(x) ⟺ ∀x.~F(x) (verified over domains of size 1–3)', () => { + DOMAINS.forEach(domain => { + const extensions: DomainElement[][] = [ + [], + [domain[0]], + [...domain], + ]; + + extensions.forEach(ext => { + const extSet = new Set(ext); + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => extSet.has(x)); + + const Fx = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const notFx = new AtomicFormulaImpl('~', F, [new VariableTerm('x')], assignment); + + const lhs = new QuantifiedFormulaImpl('~', '∃', 'x', Fx, domain, assignment); + const rhs = new QuantifiedFormulaImpl(undefined, '∀', 'x', notFx, domain, assignment); + + expect(lhs.value()).toBe(rhs.value()); + }); + }); + }); + }); + + describe('Part II — Valid quantificational formulas (verified over finite domains)', () => { + + test('∀x.F(x) -> ∃x.F(x) (on non-empty domains)', () => { + DOMAINS.forEach(domain => { + // Test with various predicate extensions + const extensions = [[], [domain[0]], [...domain]]; + + extensions.forEach(ext => { + const extSet = new Set(ext); + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => extSet.has(x)); + + const Fx1 = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const Fx2 = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + + const forall = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx1, domain, assignment); + const exists = new QuantifiedFormulaImpl(undefined, '∃', 'x', Fx2, domain, assignment); + const impl = new ComplexFormulaImpl(undefined, forall, '->', exists); + + // This is valid on non-empty domains + expect(impl.value()).toBe(true); + }); + }); + }); + + test('∀x.(F(x) & G(x)) <-> (∀x.F(x) & ∀x.G(x))', () => { + const domain: DomainElement[] = ['a', 'b', 'c']; + + // Test several predicate combinations + const combos: [Set, Set][] = [ + [new Set(['a', 'b', 'c']), new Set(['a', 'b', 'c'])], + [new Set(['a']), new Set(['a', 'b', 'c'])], + [new Set([]), new Set(['a', 'b', 'c'])], + [new Set(['a', 'b']), new Set(['b', 'c'])], + ]; + + combos.forEach(([fExt, gExt]) => { + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => fExt.has(x)); + const G = new PredicateImpl('G', 1, (x) => gExt.has(x)); + + const Fx = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const Gx = new AtomicFormulaImpl(undefined, G, [new VariableTerm('x')], assignment); + + // LHS: ∀x.(F(x) & G(x)) + const conj = new ComplexFormulaImpl(undefined, Fx, '&', Gx); + const lhs = new QuantifiedFormulaImpl(undefined, '∀', 'x', conj, domain, assignment); + + // RHS: ∀x.F(x) & ∀x.G(x) — note: separate copies of Fx, Gx + const Fx2 = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const Gx2 = new AtomicFormulaImpl(undefined, G, [new VariableTerm('x')], assignment); + const forallF = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx2, domain, assignment); + const forallG = new QuantifiedFormulaImpl(undefined, '∀', 'x', Gx2, domain, assignment); + const rhs = new ComplexFormulaImpl(undefined, forallF, '&', forallG); + + expect(lhs.value()).toBe(rhs.value()); + }); + }); + + test('∀x.F(x) -> F(a) (universal instantiation)', () => { + DOMAINS.forEach(domain => { + if (!domain.includes('a')) return; + + const extensions = [[], [domain[0]], [...domain]]; + extensions.forEach(ext => { + const extSet = new Set(ext); + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => extSet.has(x)); + + const Fx = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const Fa = new AtomicFormulaImpl(undefined, F, [new VariableTerm('a')], new Map([['a', 'a']])); + + const forall = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx, domain, assignment); + const impl = new ComplexFormulaImpl(undefined, forall, '->', Fa); + + expect(impl.value()).toBe(true); + }); + }); + }); + + test('F(a) -> ∃x.F(x) (existential generalisation)', () => { + DOMAINS.forEach(domain => { + if (!domain.includes('a')) return; + + const extensions = [[], ['a'], [...domain]]; + extensions.forEach(ext => { + const extSet = new Set(ext); + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => extSet.has(x)); + + const Fa = new AtomicFormulaImpl(undefined, F, [new VariableTerm('a')], new Map([['a', 'a']])); + const Fx = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const exists = new QuantifiedFormulaImpl(undefined, '∃', 'x', Fx, domain, assignment); + const impl = new ComplexFormulaImpl(undefined, Fa, '->', exists); + + expect(impl.value()).toBe(true); + }); + }); + }); + }); + + describe('Part II — Completeness: exhaustive evaluation is a decision procedure for finite domains', () => { + + test('A valid formula is confirmed valid and not refuted', () => { + // ∀x.(F(x) | ~F(x)) — law of excluded middle, quantified + const domain: DomainElement[] = ['a', 'b', 'c']; + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => x === 'a'); + + const Fx = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const notFx = new AtomicFormulaImpl('~', F, [new VariableTerm('x')], assignment); + const disj = new ComplexFormulaImpl(undefined, Fx, '|', notFx); + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', disj, domain, assignment); + + expect(formula.value()).toBe(true); + }); + + test('A contradictory formula is refuted', () => { + // ∀x.(F(x) & ~F(x)) — law of non-contradiction, quantified + const domain: DomainElement[] = ['a', 'b']; + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => x === 'a'); + + const Fx = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + const notFx = new AtomicFormulaImpl('~', F, [new VariableTerm('x')], assignment); + const conj = new ComplexFormulaImpl(undefined, Fx, '&', notFx); + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', conj, domain, assignment); + + expect(formula.value()).toBe(false); + }); + + test('A contingent formula produces mixed results across domains', () => { + // ∀x.F(x) — depends on the predicate extension + const domain: DomainElement[] = ['a', 'b']; + const assignment: VariableAssignment = new Map(); + + // When F holds for all + const F1 = new PredicateImpl('F', 1, () => true); + const Fx1 = new AtomicFormulaImpl(undefined, F1, [new VariableTerm('x')], assignment); + const forall1 = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx1, domain, assignment); + expect(forall1.value()).toBe(true); + + // When F holds for some but not all + const F2 = new PredicateImpl('F', 1, (x) => x === 'a'); + const Fx2 = new AtomicFormulaImpl(undefined, F2, [new VariableTerm('x')], assignment); + const forall2 = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx2, domain, assignment); + expect(forall2.value()).toBe(false); + }); + }); +}); diff --git a/test/language/quantificational/predicate.spec.ts b/test/language/quantificational/predicate.spec.ts new file mode 100644 index 0000000..1140d79 --- /dev/null +++ b/test/language/quantificational/predicate.spec.ts @@ -0,0 +1,129 @@ +import { PredicateImpl, IDENTITY } from '../../../src/language/quantificational/predicate'; + +describe('Predicate Tests', () => { + + describe('unary predicates', () => { + + test('unary predicate holds for matching element', () => { + const mortals = new Set(['socrates', 'plato']); + const Mortal = new PredicateImpl('Mortal', 1, (x) => mortals.has(x as string)); + expect(Mortal.holds('socrates')).toBe(true); + expect(Mortal.holds('plato')).toBe(true); + }); + + test('unary predicate does not hold for non-matching element', () => { + const mortals = new Set(['socrates']); + const Mortal = new PredicateImpl('Mortal', 1, (x) => mortals.has(x as string)); + expect(Mortal.holds('zeus')).toBe(false); + }); + + test('stores name and arity', () => { + const F = new PredicateImpl('F', 1, () => true); + expect(F.name).toBe('F'); + expect(F.arity).toBe(1); + }); + }); + + describe('binary predicates', () => { + + test('binary predicate holds for matching pair', () => { + const lovesSet = new Set(['socrates,plato']); + const Loves = new PredicateImpl('Loves', 2, (x, y) => lovesSet.has(`${x},${y}`)); + expect(Loves.holds('socrates', 'plato')).toBe(true); + }); + + test('binary predicate does not hold for non-matching pair', () => { + const lovesSet = new Set(['socrates,plato']); + const Loves = new PredicateImpl('Loves', 2, (x, y) => lovesSet.has(`${x},${y}`)); + expect(Loves.holds('plato', 'socrates')).toBe(false); + }); + + test('stores arity 2', () => { + const R = new PredicateImpl('R', 2, () => true); + expect(R.arity).toBe(2); + }); + }); + + describe('arity enforcement', () => { + + test('throws when too few arguments are provided', () => { + const F = new PredicateImpl('F', 2, () => true); + expect(() => F.holds('a')).toThrow( + "Predicate 'F' has arity 2 but received 1 argument(s)." + ); + }); + + test('throws when too many arguments are provided', () => { + const F = new PredicateImpl('F', 1, () => true); + expect(() => F.holds('a', 'b')).toThrow( + "Predicate 'F' has arity 1 but received 2 argument(s)." + ); + }); + + test('zero-arity predicate (propositional constant) works', () => { + const P = new PredicateImpl('P', 0, () => true); + expect(P.holds()).toBe(true); + }); + + test('zero-arity predicate rejects arguments', () => { + const P = new PredicateImpl('P', 0, () => true); + expect(() => P.holds('a')).toThrow( + "Predicate 'P' has arity 0 but received 1 argument(s)." + ); + }); + }); + + describe('numeric domain elements', () => { + + test('predicates work with numeric elements', () => { + const Even = new PredicateImpl('Even', 1, (x) => (x as number) % 2 === 0); + expect(Even.holds(2)).toBe(true); + expect(Even.holds(4)).toBe(true); + expect(Even.holds(3)).toBe(false); + }); + + test('binary predicate with numeric ordering', () => { + const LessThan = new PredicateImpl('LessThan', 2, (x, y) => (x as number) < (y as number)); + expect(LessThan.holds(1, 2)).toBe(true); + expect(LessThan.holds(2, 1)).toBe(false); + expect(LessThan.holds(1, 1)).toBe(false); + }); + }); + + describe('IDENTITY (built-in equality predicate)', () => { + + test('holds when both arguments are the same string element', () => { + + expect(IDENTITY.holds('socrates', 'socrates')).toBe(true); + }); + + test('does not hold when arguments are different string elements', () => { + + expect(IDENTITY.holds('socrates', 'plato')).toBe(false); + }); + + test('holds when both arguments are the same numeric element', () => { + + expect(IDENTITY.holds(42, 42)).toBe(true); + }); + + test('does not hold for different numeric elements', () => { + + expect(IDENTITY.holds(1, 2)).toBe(false); + }); + + test('Hesperus = Phosphorus: two names, same referent', () => { + + // Both names denote Venus — identity holds + const hesperus = 'venus'; + const phosphorus = 'venus'; + expect(IDENTITY.holds(hesperus, phosphorus)).toBe(true); + }); + + test('has name "=" and arity 2', () => { + + expect(IDENTITY.name).toBe('='); + expect(IDENTITY.arity).toBe(2); + }); + }); +}); diff --git a/test/language/quantificational/quantificationalTheory.spec.ts b/test/language/quantificational/quantificationalTheory.spec.ts new file mode 100644 index 0000000..d39b840 --- /dev/null +++ b/test/language/quantificational/quantificationalTheory.spec.ts @@ -0,0 +1,290 @@ +import { QuantificationalTheoryBuilder } from '../../../src/language/quantificational/quantificationalTheoryBuilder'; +import { AtomicFormulaImpl } from '../../../src/language/quantificational/atomicFormula'; +import { ComplexFormulaImpl } from '../../../src/language/quantificational/complexFormula'; +import { QuantifiedFormulaImpl } from '../../../src/language/quantificational/quantifiedFormula'; +import { ConstantTerm } from '../../../src/language/quantificational/term'; +import { AlethicAssertoric } from '../../../src/language/shared/types'; + +// ─── Helpers ───────────────────────────────────────────────────────────────── + +function sentence(raw: string): AlethicAssertoric { + return { raw, confidence: 1.0 }; +} + +// ───────────────────────────────────────────────────────────────────────────── + +describe('QuantificationalTheoryBuilder', () => { + + test('variable() returns the same instance for the same name', () => { + const builder = new QuantificationalTheoryBuilder(); + const x1 = builder.variable('x'); + const x2 = builder.variable('x'); + expect(x1).toBe(x2); + }); + + test('variable() returns distinct instances for different names', () => { + const builder = new QuantificationalTheoryBuilder(); + const x = builder.variable('x'); + const y = builder.variable('y'); + expect(x).not.toBe(y); + }); + + test('predicate() returns the same instance for the same name', () => { + const builder = new QuantificationalTheoryBuilder(); + const F1 = builder.predicate('F', 1, () => true); + const F2 = builder.predicate('F', 1, () => true); + expect(F1).toBe(F2); + }); + + test('domain() sets the domain and is fluent', () => { + const builder = new QuantificationalTheoryBuilder(); + const result = builder.domain('a', 'b', 'c'); + expect(result).toBe(builder); + expect(builder.currentDomain).toEqual(['a', 'b', 'c']); + }); + + test('sentence() is fluent (returns this)', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + const formula = new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment); + const result = builder.sentence(sentence('F(a)'), formula, []); + expect(result).toBe(builder); + }); + + test('build() returns a theory with the added sentences', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + const formula = new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment); + builder.sentence(sentence('F(a)'), formula, []); + const theory = builder.build(); + expect(theory.sentences).toHaveLength(1); + expect(theory.sentences[0].source.raw).toBe('F(a)'); + }); + + test('auto-labels sentences φ1, φ2, …', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + const f1 = new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment); + const f2 = new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment); + builder + .sentence(sentence('F(a)'), f1, []) + .sentence(sentence('F(a) again'), f2, []); + const theory = builder.build(); + expect(theory.sentences[0].label).toBe('φ1'); + expect(theory.sentences[1].label).toBe('φ2'); + }); + + test('custom label is used when provided', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + const formula = new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment); + builder.sentence(sentence('F(a)'), formula, [], 'S1'); + const theory = builder.build(); + expect(theory.sentences[0].label).toBe('S1'); + }); + + test('fromSentenceSet() throws (not yet implemented)', () => { + const builder = new QuantificationalTheoryBuilder(); + expect(() => builder.fromSentenceSet({ sentences: [] })).toThrow(); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('QuantificationalTheory — checkConsistency()', () => { + + test('classic syllogism: All men are mortal, Socrates is a man, Socrates is mortal — consistent', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('socrates', 'plato'); + + const Man = builder.predicate('Man', 1, (x) => x === 'socrates' || x === 'plato'); + const Mortal = builder.predicate('Mortal', 1, (x) => x === 'socrates' || x === 'plato'); + const x = builder.variable('x'); + + // φ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); + const phi1 = new QuantifiedFormulaImpl(undefined, '∀', 'x', impl, builder.currentDomain, builder.assignment); + + // φ2: Man(socrates) + const phi2 = new AtomicFormulaImpl(undefined, Man, [new ConstantTerm('socrates')], builder.assignment); + + // φ3: Mortal(socrates) + const phi3 = new AtomicFormulaImpl(undefined, Mortal, [new ConstantTerm('socrates')], builder.assignment); + + builder + .sentence(sentence('All men are mortal'), phi1, ['x']) + .sentence(sentence('Socrates is a man'), phi2, []) + .sentence(sentence('Socrates is mortal'), phi3, []); + + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + }); + + test('invalid syllogism: All men are mortal, Socrates is a man, Socrates is NOT mortal — inconsistent', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('socrates', 'plato'); + + const Man = builder.predicate('Man', 1, (x) => x === 'socrates' || x === 'plato'); + const Mortal = builder.predicate('Mortal', 1, (x) => x === 'socrates' || x === 'plato'); + const x = builder.variable('x'); + + // φ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); + const phi1 = new QuantifiedFormulaImpl(undefined, '∀', 'x', impl, builder.currentDomain, builder.assignment); + + // φ2: Man(socrates) + const phi2 = new AtomicFormulaImpl(undefined, Man, [new ConstantTerm('socrates')], builder.assignment); + + // φ3: ~Mortal(socrates) + const phi3 = new AtomicFormulaImpl('~', Mortal, [new ConstantTerm('socrates')], builder.assignment); + + builder + .sentence(sentence('All men are mortal'), phi1, ['x']) + .sentence(sentence('Socrates is a man'), phi2, []) + .sentence(sentence('Socrates is NOT mortal'), phi3, []); + + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(false); + }); + + test('∃x.F(x) is consistent when F holds for some element', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a', 'b', 'c'); + + const F = builder.predicate('F', 1, (x) => x === 'b'); + const x = builder.variable('x'); + const Fx = new AtomicFormulaImpl(undefined, F, [x.term()], builder.assignment); + const phi = new QuantifiedFormulaImpl(undefined, '∃', 'x', Fx, builder.currentDomain, builder.assignment); + + builder.sentence(sentence('Something is F'), phi, ['x']); + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + }); + + test('{∀x.F(x), ∃x.~F(x)} is inconsistent', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a', 'b'); + + const F = builder.predicate('F', 1, (x) => x === 'a' || x === 'b'); + const x = builder.variable('x'); + const Fx = new AtomicFormulaImpl(undefined, F, [x.term()], builder.assignment); + const notFx = new AtomicFormulaImpl('~', F, [x.term()], builder.assignment); + + const forallFx = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx, builder.currentDomain, builder.assignment); + const existsNotFx = new QuantifiedFormulaImpl(undefined, '∃', 'x', notFx, builder.currentDomain, builder.assignment); + + builder + .sentence(sentence('Everything is F'), forallFx, ['x']) + .sentence(sentence('Something is not F'), existsNotFx, ['x']); + + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(false); + }); + + test('theory with no free variables: ground sentence', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('socrates'); + + const Mortal = builder.predicate('Mortal', 1, (x) => x === 'socrates'); + const phi = new AtomicFormulaImpl(undefined, Mortal, [new ConstantTerm('socrates')], builder.assignment); + + builder.sentence(sentence('Socrates is mortal'), phi, []); + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('QuantificationalTheory — buildProofTree()', () => { + + test('consistent theory root is labelled CONSISTENT ✓', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + const phi = new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment); + builder.sentence(sentence('F(a)'), phi, []); + const tree = builder.build().buildProofTree(); + expect(tree.label).toBe('CONSISTENT ✓'); + }); + + test('inconsistent theory root is labelled INCONSISTENT ✗', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + const pos = new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment); + const neg = new AtomicFormulaImpl('~', F, [new ConstantTerm('a')], builder.assignment); + builder + .sentence(sentence('F(a)'), pos, []) + .sentence(sentence('~F(a)'), neg, []); + const tree = builder.build().buildProofTree(); + expect(tree.label).toBe('INCONSISTENT ✗'); + }); + + test('consistent tree has a Verification child', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + builder.sentence(sentence('F(a)'), new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment), []); + const tree = builder.build().buildProofTree(); + const verification = tree.children.find(c => c.label === 'Verification:'); + expect(verification).toBeDefined(); + expect(verification!.children).toHaveLength(1); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('QuantificationalTheory — printProof() and printGraph()', () => { + + test('printProof() does not throw for consistent theory', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('socrates', 'plato'); + const Man = builder.predicate('Man', 1, () => true); + const x = builder.variable('x'); + const Fx = new AtomicFormulaImpl(undefined, Man, [x.term()], builder.assignment); + const phi = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx, builder.currentDomain, builder.assignment); + builder.sentence(sentence('All are men'), phi, ['x']); + expect(() => builder.build().printProof()).not.toThrow(); + }); + + test('printProof() does not throw for inconsistent theory', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('a'); + const F = builder.predicate('F', 1, () => true); + builder + .sentence(sentence('F(a)'), new AtomicFormulaImpl(undefined, F, [new ConstantTerm('a')], builder.assignment), []) + .sentence(sentence('~F(a)'), new AtomicFormulaImpl('~', F, [new ConstantTerm('a')], builder.assignment), []); + expect(() => builder.build().printProof()).not.toThrow(); + }); + + test('printGraph() does not throw', () => { + const builder = new QuantificationalTheoryBuilder(); + builder.domain('socrates', 'plato'); + const Man = builder.predicate('Man', 1, () => true); + const Mortal = builder.predicate('Mortal', 1, () => true); + const x = builder.variable('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); + const phi1 = new QuantifiedFormulaImpl(undefined, '∀', 'x', impl, builder.currentDomain, builder.assignment); + const phi2 = new AtomicFormulaImpl(undefined, Man, [new ConstantTerm('socrates')], builder.assignment); + const phi3 = new AtomicFormulaImpl(undefined, Mortal, [new ConstantTerm('socrates')], builder.assignment); + + builder + .sentence(sentence('All men are mortal'), phi1, ['x']) + .sentence(sentence('Socrates is a man'), phi2, []) + .sentence(sentence('Socrates is mortal'), phi3, []); + + expect(() => builder.build().printGraph()).not.toThrow(); + }); +}); diff --git a/test/language/quantificational/quantifiedFormula.spec.ts b/test/language/quantificational/quantifiedFormula.spec.ts new file mode 100644 index 0000000..35a1a77 --- /dev/null +++ b/test/language/quantificational/quantifiedFormula.spec.ts @@ -0,0 +1,275 @@ +import { QuantifiedFormulaImpl } from '../../../src/language/quantificational/quantifiedFormula'; +import { AtomicFormulaImpl } from '../../../src/language/quantificational/atomicFormula'; +import { ComplexFormulaImpl } from '../../../src/language/quantificational/complexFormula'; +import { PredicateImpl } from '../../../src/language/quantificational/predicate'; +import { VariableTerm, ConstantTerm } from '../../../src/language/quantificational/term'; +import { VariableAssignment, DomainElement } from '../../../src/language/quantificational/quantificationalTypes'; + +describe('QuantifiedFormula Tests', () => { + + // ─── Helpers ───────────────────────────────────────────────────────────── + + function makeUnarySetup(trueElements: DomainElement[], domain: DomainElement[]) { + const trueSet = new Set(trueElements); + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, (x) => trueSet.has(x)); + const x = new VariableTerm('x'); + const body = new AtomicFormulaImpl(undefined, F, [x], assignment); + return { assignment, F, body, domain }; + } + + // ─── Universal quantifier (∀) ──────────────────────────────────────────── + + describe('universal quantifier (∀)', () => { + + test('∀x.F(x) true when predicate holds for ALL domain elements', () => { + const domain = ['a', 'b', 'c']; + const { assignment, body } = makeUnarySetup(['a', 'b', 'c'], domain); + + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', body, domain, assignment); + expect(formula.value()).toBe(true); + }); + + test('∀x.F(x) false when predicate fails for at least one element', () => { + const domain = ['a', 'b', 'c']; + const { assignment, body } = makeUnarySetup(['a', 'b'], domain); // 'c' is not in trueSet + + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', body, domain, assignment); + expect(formula.value()).toBe(false); + }); + + test('∀x.F(x) true on a single-element domain where predicate holds', () => { + const domain = ['a']; + const { assignment, body } = makeUnarySetup(['a'], domain); + + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', body, domain, assignment); + expect(formula.value()).toBe(true); + }); + + test('∀x.F(x) false on a single-element domain where predicate fails', () => { + const domain = ['a']; + const { assignment, body } = makeUnarySetup([], domain); + + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', body, domain, assignment); + expect(formula.value()).toBe(false); + }); + }); + + // ─── Existential quantifier (∃) ────────────────────────────────────────── + + describe('existential quantifier (∃)', () => { + + test('∃x.F(x) true when predicate holds for at least one element', () => { + const domain = ['a', 'b', 'c']; + const { assignment, body } = makeUnarySetup(['b'], domain); + + const formula = new QuantifiedFormulaImpl(undefined, '∃', 'x', body, domain, assignment); + expect(formula.value()).toBe(true); + }); + + test('∃x.F(x) false when predicate holds for NO element', () => { + const domain = ['a', 'b', 'c']; + const { assignment, body } = makeUnarySetup([], domain); + + const formula = new QuantifiedFormulaImpl(undefined, '∃', 'x', body, domain, assignment); + expect(formula.value()).toBe(false); + }); + + test('∃x.F(x) true when predicate holds for ALL elements', () => { + const domain = ['a', 'b']; + const { assignment, body } = makeUnarySetup(['a', 'b'], domain); + + const formula = new QuantifiedFormulaImpl(undefined, '∃', 'x', body, domain, assignment); + expect(formula.value()).toBe(true); + }); + }); + + // ─── Negation ──────────────────────────────────────────────────────────── + + describe('negation of quantified formulas', () => { + + test('~∀x.F(x) is true when ∀x.F(x) is false', () => { + const domain = ['a', 'b']; + const { assignment, body } = makeUnarySetup(['a'], domain); + + const formula = new QuantifiedFormulaImpl('~', '∀', 'x', body, domain, assignment); + expect(formula.value()).toBe(true); + }); + + test('~∀x.F(x) is false when ∀x.F(x) is true', () => { + const domain = ['a', 'b']; + const { assignment, body } = makeUnarySetup(['a', 'b'], domain); + + const formula = new QuantifiedFormulaImpl('~', '∀', 'x', body, domain, assignment); + expect(formula.value()).toBe(false); + }); + + test('~∃x.F(x) is true when ∃x.F(x) is false', () => { + const domain = ['a', 'b']; + const { assignment, body } = makeUnarySetup([], domain); + + const formula = new QuantifiedFormulaImpl('~', '∃', 'x', body, domain, assignment); + expect(formula.value()).toBe(true); + }); + + test('~∃x.F(x) is false when ∃x.F(x) is true', () => { + const domain = ['a', 'b']; + const { assignment, body } = makeUnarySetup(['a'], domain); + + const formula = new QuantifiedFormulaImpl('~', '∃', 'x', body, domain, assignment); + expect(formula.value()).toBe(false); + }); + }); + + // ─── Nested quantifiers ────────────────────────────────────────────────── + + describe('nested quantifiers', () => { + + test('∀x.∃y.R(x,y) — for every x, there exists a y such that R(x,y)', () => { + // Domain: {1, 2} + // R(x,y) iff x <= y — for every x there is a y (namely y=2) where x<=y + const domain: DomainElement[] = [1, 2]; + const assignment: VariableAssignment = new Map(); + const R = new PredicateImpl('R', 2, (x, y) => (x as number) <= (y as number)); + const xTerm = new VariableTerm('x'); + const yTerm = new VariableTerm('y'); + const Rxy = new AtomicFormulaImpl(undefined, R, [xTerm, yTerm], assignment); + + const existsY = new QuantifiedFormulaImpl(undefined, '∃', 'y', Rxy, domain, assignment); + const forallX = new QuantifiedFormulaImpl(undefined, '∀', 'x', existsY, domain, assignment); + + expect(forallX.value()).toBe(true); + }); + + test('∃x.∀y.R(x,y) — there exists an x such that R(x,y) for all y', () => { + // Domain: {1, 2} + // R(x,y) iff x <= y — x=1 satisfies: 1<=1 and 1<=2 + const domain: DomainElement[] = [1, 2]; + const assignment: VariableAssignment = new Map(); + const R = new PredicateImpl('R', 2, (x, y) => (x as number) <= (y as number)); + const xTerm = new VariableTerm('x'); + const yTerm = new VariableTerm('y'); + const Rxy = new AtomicFormulaImpl(undefined, R, [xTerm, yTerm], assignment); + + const forallY = new QuantifiedFormulaImpl(undefined, '∀', 'y', Rxy, domain, assignment); + const existsX = new QuantifiedFormulaImpl(undefined, '∃', 'x', forallY, domain, assignment); + + expect(existsX.value()).toBe(true); + }); + + test('∀x.∀y.(R(x,y) -> R(y,x)) — R is symmetric', () => { + // Domain: {a, b} + // R(x,y) iff x == y — this is symmetric + const domain: DomainElement[] = ['a', 'b']; + const assignment: VariableAssignment = new Map(); + const R = new PredicateImpl('R', 2, (x, y) => x === y); + const xTerm = new VariableTerm('x'); + const yTerm = new VariableTerm('y'); + const Rxy = new AtomicFormulaImpl(undefined, R, [xTerm, yTerm], assignment); + const Ryx = new AtomicFormulaImpl(undefined, R, [yTerm, xTerm], assignment); + const impl = new ComplexFormulaImpl(undefined, Rxy, '->', Ryx); + + const forallY = new QuantifiedFormulaImpl(undefined, '∀', 'y', impl, domain, assignment); + const forallX = new QuantifiedFormulaImpl(undefined, '∀', 'x', forallY, domain, assignment); + + expect(forallX.value()).toBe(true); + }); + + test('nested quantifiers restore previous bindings', () => { + // Verify that after ∀x.∃y.R(x,y) completes, x is unbound again + const domain: DomainElement[] = [1, 2]; + const assignment: VariableAssignment = new Map(); + const R = new PredicateImpl('R', 2, (x, y) => (x as number) <= (y as number)); + const Rxy = new AtomicFormulaImpl(undefined, R, [new VariableTerm('x'), new VariableTerm('y')], assignment); + const existsY = new QuantifiedFormulaImpl(undefined, '∃', 'y', Rxy, domain, assignment); + const forallX = new QuantifiedFormulaImpl(undefined, '∀', 'x', existsY, domain, assignment); + + forallX.value(); + expect(assignment.has('x')).toBe(false); + expect(assignment.has('y')).toBe(false); + }); + }); + + // ─── Quantifier–connective interaction ──────────────────────────────────── + + describe('quantifier–connective interaction', () => { + + test('∀x.F(x) & ∃x.G(x) — conjunction of quantified formulas', () => { + const domain: DomainElement[] = ['a', 'b']; + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, () => true); // F holds everywhere + const G = new PredicateImpl('G', 1, (x) => x === 'a'); // G holds only for 'a' + const xTerm = new VariableTerm('x'); + + const Fx = new AtomicFormulaImpl(undefined, F, [xTerm], assignment); + const Gx = new AtomicFormulaImpl(undefined, G, [xTerm], assignment); + + const forallFx = new QuantifiedFormulaImpl(undefined, '∀', 'x', Fx, domain, assignment); + const existsGx = new QuantifiedFormulaImpl(undefined, '∃', 'x', Gx, domain, assignment); + const conjunction = new ComplexFormulaImpl(undefined, forallFx, '&', existsGx); + + expect(conjunction.value()).toBe(true); + }); + + test('∀x.(F(x) -> G(x)) — quantifier scopes over connective', () => { + // "All Fs are Gs": F = {a, b}, G = {a, b, c} → true + const domain: DomainElement[] = ['a', 'b', 'c']; + const assignment: VariableAssignment = new Map(); + const fs = new Set(['a', 'b']); + const gs = new Set(['a', 'b', 'c']); + const F = new PredicateImpl('F', 1, (x) => fs.has(x as string)); + const G = new PredicateImpl('G', 1, (x) => gs.has(x as string)); + const xTerm = new VariableTerm('x'); + + const Fx = new AtomicFormulaImpl(undefined, F, [xTerm], assignment); + const Gx = new AtomicFormulaImpl(undefined, G, [xTerm], assignment); + const impl = new ComplexFormulaImpl(undefined, Fx, '->', Gx); + + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', impl, domain, assignment); + expect(formula.value()).toBe(true); + }); + + test('∀x.(F(x) -> G(x)) fails when an F is not a G', () => { + // "All Fs are Gs": F = {a, b}, G = {a} → false (b is F but not G) + const domain: DomainElement[] = ['a', 'b']; + const assignment: VariableAssignment = new Map(); + const fs = new Set(['a', 'b']); + const gs = new Set(['a']); + const F = new PredicateImpl('F', 1, (x) => fs.has(x as string)); + const G = new PredicateImpl('G', 1, (x) => gs.has(x as string)); + const xTerm = new VariableTerm('x'); + + const Fx = new AtomicFormulaImpl(undefined, F, [xTerm], assignment); + const Gx = new AtomicFormulaImpl(undefined, G, [xTerm], assignment); + const impl = new ComplexFormulaImpl(undefined, Fx, '->', Gx); + + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', impl, domain, assignment); + expect(formula.value()).toBe(false); + }); + }); + + // ─── Edge cases ────────────────────────────────────────────────────────── + + describe('edge cases', () => { + + test('empty domain: ∀x.F(x) is vacuously true', () => { + const domain: DomainElement[] = []; + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, () => false); + const body = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + + const formula = new QuantifiedFormulaImpl(undefined, '∀', 'x', body, domain, assignment); + expect(formula.value()).toBe(true); // vacuous truth + }); + + test('empty domain: ∃x.F(x) is false', () => { + const domain: DomainElement[] = []; + const assignment: VariableAssignment = new Map(); + const F = new PredicateImpl('F', 1, () => true); + const body = new AtomicFormulaImpl(undefined, F, [new VariableTerm('x')], assignment); + + const formula = new QuantifiedFormulaImpl(undefined, '∃', 'x', body, domain, assignment); + expect(formula.value()).toBe(false); + }); + }); +}); diff --git a/test/language/quantificational/term.spec.ts b/test/language/quantificational/term.spec.ts new file mode 100644 index 0000000..3330890 --- /dev/null +++ b/test/language/quantificational/term.spec.ts @@ -0,0 +1,65 @@ +import { VariableTerm, ConstantTerm } from '../../../src/language/quantificational/term'; +import { VariableAssignment } from '../../../src/language/quantificational/quantificationalTypes'; + +describe('Term Tests', () => { + + describe('ConstantTerm', () => { + + test('resolves to its fixed string element regardless of assignment', () => { + const c = new ConstantTerm('socrates'); + const assignment: VariableAssignment = new Map(); + expect(c.resolve(assignment)).toBe('socrates'); + }); + + test('resolves to its fixed numeric element regardless of assignment', () => { + const c = new ConstantTerm(42); + const assignment: VariableAssignment = new Map(); + expect(c.resolve(assignment)).toBe(42); + }); + + test('ignores variable assignment entirely', () => { + const c = new ConstantTerm('a'); + const assignment: VariableAssignment = new Map([['x', 'b']]); + expect(c.resolve(assignment)).toBe('a'); + }); + + test('stores the element on construction', () => { + const c = new ConstantTerm('plato'); + expect(c.element).toBe('plato'); + }); + }); + + describe('VariableTerm', () => { + + test('resolves to the assigned element for its variable name', () => { + const v = new VariableTerm('x'); + const assignment: VariableAssignment = new Map([['x', 'socrates']]); + expect(v.resolve(assignment)).toBe('socrates'); + }); + + test('resolves to updated value when assignment changes', () => { + const v = new VariableTerm('x'); + const assignment: VariableAssignment = new Map([['x', 'socrates']]); + expect(v.resolve(assignment)).toBe('socrates'); + assignment.set('x', 'plato'); + expect(v.resolve(assignment)).toBe('plato'); + }); + + test('throws when the variable is unbound', () => { + const v = new VariableTerm('x'); + const assignment: VariableAssignment = new Map(); + expect(() => v.resolve(assignment)).toThrow("Unbound variable: 'x'"); + }); + + test('stores the variable name on construction', () => { + const v = new VariableTerm('y'); + expect(v.name).toBe('y'); + }); + + test('resolves numeric domain elements', () => { + const v = new VariableTerm('x'); + const assignment: VariableAssignment = new Map([['x', 1]]); + expect(v.resolve(assignment)).toBe(1); + }); + }); +});