diff --git a/CLAUDE.md b/CLAUDE.md index 23b38b3..f370f79 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -66,7 +66,16 @@ src/ quantificationalTheoryBuilder.ts # QuantificationalTheoryBuilder index.ts modal/ - index.ts # TODO + modalTypes.d.ts # MFF, World, ModalOperator, ModalEvaluationState, ModalSystemSpec + modalSystems.ts # SystemK, SystemT, SystemD, SystemS4, SystemS5 + modalAtom.ts # ModalAtomImpl + modalComplex.ts # ModalComplexImpl + modalFormula.ts # ModalFormulaImpl (□, ◇) + modalVariable.ts # ModalVariable + modalUtils.ts # binaryOperatorToLogic, type guards + modalTheory.ts # ModalTheory, ModalFormalSentence + modalTheoryBuilder.ts # ModalTheoryBuilder + index.ts engine/ nlp/ nlpTypes.ts # NLPResult (imports AlethicAssertoric from shared) @@ -97,6 +106,13 @@ test/ quantificationalTheory.spec.ts meta-logic/ completeness.spec.ts # Structural induction + quantifier duality + modal/ + modalAtom.spec.ts + modalComplex.spec.ts + modalFormula.spec.ts + modalTheory.spec.ts # Builder, consistency, proof tree, system validation + meta-logic/ + completeness.spec.ts # K axiom, modal duality, distribution, non-theorems engine/ nlp/nlpEngine.spec.ts # Skipped placeholder syntax/propositional/syntaxEngine.spec.ts # Skipped placeholder @@ -219,6 +235,62 @@ theory.printGraph(); - **Valid formulas** — universal instantiation, existential generalisation, distribution of ∀ over & - **Identity properties** — reflexivity and substitution (verified via exhaustive model checking) +## Modal Logic — What's Implemented + +### Type system + +- `World` — `string`, the points of evaluation in Kripke semantics +- `ModalEvaluationState` — shared mutable state: `currentWorld: World` + `valuation: Map>` +- `MFF` — Modal Formula, the union of all valid modal expressions (analogous to WFF/QFF) +- `ModalSystemSpec` — interface: `name` + `validateFrame(worlds, accessibility)` — encapsulates frame conditions independently of the language layer +- Same operators as propositional: `~`, `&`, `|`, `->`, `<->` +- Modal operators: `□` (necessity), `◇` (possibility) + +### Modal formula types + +- `ModalAtomImpl` — proposition letter; reads truth value from `valuation[name]` at `currentWorld` +- `ModalComplexImpl` — two MFFs joined by a binary connective (identical semantics to propositional) +- `ModalFormulaImpl` — `□` or `◇` operator; iterates over worlds accessible from `currentWorld` via the accessibility relation (directly parallels `QuantifiedFormulaImpl` iterating over domain elements); restores `currentWorld` after evaluation + +### Systems (frame conditions) + +Five concrete `ModalSystemSpec` objects are provided: + +| Export | Name | Frame condition | +| --- | --- | --- | +| `SystemK` | K | None — any frame valid | +| `SystemT` | T | Reflexive: `wRw` for all `w` | +| `SystemD` | D | Serial: every world has at least one successor | +| `SystemS4` | S4 | Reflexive + Transitive | +| `SystemS5` | S5 | Reflexive + Transitive + Symmetric | + +**Language layer is system-agnostic.** `ModalAtomImpl`, `ModalComplexImpl`, `ModalFormulaImpl`, and `ModalVariable` contain zero system references. Systems only affect `ModalTheoryBuilder.build()` validation and `printProof()`/`printGraph()` labels. + +### Theory data structure + +**`ModalVariable`** — named proposition letter; `atom(negated?)` returns a `ModalAtomImpl` referencing the shared state. + +**`ModalTheory`** — implements `Theory`: + +- `checkConsistency()` — exhaustive 2^(|P|×|W|) enumeration; witness keyed as `prop@world` +- `buildProofTree()` — includes Kripke frame node (worlds, accessibility pairs, designated world) and per-world valuation table; distinct from propositional/quantificational proof trees which show variable assignments +- `printProof()`, `printGraph()` — same interface as other theories; system name appears in header + +**`ModalTheoryBuilder`** — fluent builder: `system()` (default `SystemK`), `worlds()`, `accessibility()`, `designatedWorld()`, `proposition()`, `sentence()`, `build()`. `build()` calls `system.validateFrame()` before constructing the theory — throws with a descriptive message if the frame violates the system's conditions. + +### Meta-logic proofs + +- **Completeness** — structural induction over `ModalAtomImpl`, `ModalComplexImpl`, `ModalFormulaImpl`; exhaustive evaluation verified as a decision procedure +- **Modal duality** — `□p ⟺ ~◇~p` and `◇p ⟺ ~□~p`, verified over 6 distinct frame structures +- **K axiom** — `□(p → q) → (□p → □q)`, verified exhaustively on all test frames +- **Distribution** — `□(p & q) ⟺ (□p & □q)`, verified exhaustively +- **Necessitation** — `□(p | ~p)` valid on every frame +- **Non-theorems of K** — `□p → p` (requires T), `□p → □□p` (requires 4), `◇p → □◇p` (requires 5): countermodels constructed and verified + +### Design notes + +`docs/modal/design.md` covers Kripke semantics, system hierarchy, and the analogy table between quantificational and modal constructs (domain ↔ worlds, ∀/∃ ↔ □/◇, etc.). + ## 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()`. @@ -232,7 +304,9 @@ theory.printGraph(); - Quantificational function symbols (e.g., `f(x)`) - `QuantificationalSyntaxEngine` — parsing formula strings into QFF instances - `QuantificationalTheoryBuilder.fromSentenceSet()` — awaits SyntaxEngine -- `Modal` language module +- `ModalSyntaxEngine` — parsing formula strings into MFF instances +- `ModalTheoryBuilder.fromSentenceSet()` — awaits ModalSyntaxEngine +- Quantified modal logic (combining QFF quantifiers with modal operators) ## Conventions diff --git a/README.md b/README.md index 3aa3e39..5850899 100644 --- a/README.md +++ b/README.md @@ -323,9 +323,203 @@ Consistency is decided by exhaustive evaluation over all $|D|^n$ variable assign ### Modal Logic -> In Progress +Extends propositional logic with operators for necessity (`□`) and possibility (`◇`), evaluated over possible-worlds (Kripke) semantics. A **Kripke model** is a triple (W, R, V) where W is a finite set of worlds, R is an accessibility relation on W, and V assigns each proposition a set of worlds where it is true. Truth is always evaluated relative to a world. + +```text +M, w ⊨ □φ iff for all w' with wRw', M, w' ⊨ φ +M, w ⊨ ◇φ iff there exists w' with wRw' such that M, w' ⊨ φ +``` + +#### `MFF` — Modal Well-Formed Formula + +Every modal expression is an `MFF`. All formula types satisfy `Formula` and expose `value(): boolean` evaluated at the current world in the shared model state. + +```ts +interface MFF extends Formula { + unaryOperator: '~' | undefined; + value(): boolean; +} +``` + +#### `ModalAtomImpl` + +A proposition letter. Its truth value varies by world, read from the shared valuation at the current world. + +```ts +const state: ModalEvaluationState = { currentWorld: 'w0', valuation: new Map() }; + +state.valuation.set('p', new Set(['w0', 'w1'])); +const p = new ModalAtomImpl(undefined, 'p', state); + +p.value() // → true (w0 ∈ extension of p) +state.currentWorld = 'w2'; +p.value() // → false (w2 ∉ extension of p) +``` + +#### `ModalComplexImpl` + +Two `MFF`s joined by a binary connective. Evaluated at the current world with the same truth-functional semantics as propositional logic. + +```ts +const conj = new ModalComplexImpl(undefined, p, '&', q); +const impl = new ModalComplexImpl(undefined, p, '->', q); +``` + +#### `ModalFormulaImpl` + +A necessity or possibility claim. Iterates over accessible worlds from the current world, exactly as a quantifier iterates over domain elements. + +```ts +// □p: true at w iff p is true at every world accessible from w +const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, accessibility, state); + +// ◇p: true at w iff p is true at some world accessible from w +const diaP = new ModalFormulaImpl(undefined, '◇', p, worlds, accessibility, state); +``` + +**`□` is vacuously true when no worlds are accessible.** This means `□p & ~p` is consistent in System K — the designated world need not access itself. + +Nesting works naturally since `ModalFormulaImpl` is itself an `MFF`: + +```ts +// □□p — necessarily necessarily p +const boxBoxP = new ModalFormulaImpl(undefined, '□', boxP, worlds, accessibility, state); +``` + +#### `ModalVariable` + +A named proposition letter that creates atoms sharing the same evaluation state. Analogous to `PropositionalVariable`. + +```ts +const p = new ModalVariable('p', state); +const pAtom = p.atom(); // ModalAtomImpl for p +const notPAtom = p.atom(true); // ModalAtomImpl for ~p +``` + +#### Modal Systems + +A `ModalSystemSpec` encapsulates a system's name and its frame validation logic. The language layer (formula evaluation) is system-agnostic — the system only influences which frames are accepted on `build()` and how output is labelled. + +```ts +interface ModalSystemSpec { + readonly name: string; + validateFrame(worlds: World[], accessibility: (from: World, to: World) => boolean): void; +} +``` + +Five systems are provided out of the box: + +| Export | System | Frame condition | Key non-theorem | +| --- | --- | --- | --- | +| `SystemK` | K | None (any frame) | □p → p | +| `SystemT` | T | Reflexive: wRw | □p → □□p | +| `SystemD` | D | Serial: ∀w.∃w'.wRw' | □p → p | +| `SystemS4` | S4 | Reflexive + Transitive | ◇p → □◇p | +| `SystemS5` | S5 | Reflexive + Transitive + Symmetric | — | + +`build()` calls `validateFrame()` and throws a descriptive error if the frame does not satisfy the chosen system's conditions: + +```ts +new ModalTheoryBuilder() + .system(SystemT) + .worlds('w0', 'w1') + .accessibility((f, t) => f === 'w0' && t === 'w1') // w1 has no self-loop + .designatedWorld('w0') + .build(); +// Error: System T requires a reflexive frame: world 'w1' does not access itself. +``` + +Custom systems are first-class — implement `ModalSystemSpec` and pass it to `.system()`. + +#### `ModalTheory` and `ModalTheoryBuilder` + +Build a modal theory with `ModalTheoryBuilder`. The default system is `SystemK`. + +```ts +const builder = new ModalTheoryBuilder(); +builder + .system(SystemK) + .worlds('actual', 'possible') + .accessibility((f, t) => f === 'actual' && t === 'possible') + .designatedWorld('actual'); + +const p = builder.proposition('p'); + +// □p — it necessarily rains (p must be true at 'possible') +const boxP = new ModalFormulaImpl( + undefined, '□', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, +); + +// ◇p — it possibly rains (p is true at some accessible world) +const diaP = new ModalFormulaImpl( + undefined, '◇', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, +); + +builder + .sentence({ raw: 'Necessarily it rains', confidence: 1.0 }, boxP, ['p']) + .sentence({ raw: 'Possibly it rains', confidence: 1.0 }, diaP, ['p']); + +const theory = builder.build(); +``` + +**Check consistency:** + +```ts +const result = theory.checkConsistency(); +// result.isConsistent → true +// result.witness → { 'p@actual': false, 'p@possible': true } +``` + +Consistency is decided by exhaustive enumeration of all 2^(|P|×|W|) valuations (P = proposition letters, W = worlds). The witness is keyed as `prop@world`. -Extends propositional logic with operators for necessity (`□`) and possibility (`◇`), evaluated over possible-worlds semantics. +**Print a proof tree:** + +```ts +theory.printProof(); +``` + +```text +CONSISTENCY PROOF — Modal Logic (System K) +═════════════════════════════════════════════ +CONSISTENT ✓ +├── Theory: 2 sentence(s), 1 proposition(s) {p}, 2 world(s) {actual, possible} +├── Kripke frame: +│ ├── Worlds: {actual, possible} +│ ├── Accessibility: {actualRpossible} +│ └── Designated world: actual +├── Method: exhaustive evaluation, 2^(1×2) = 4 valuations checked +├── Per-world valuation: +│ ├── actual: {p=false} +│ └── possible: {p=true} +└── Verification (at designated world): + ├── φ1 ✓ "Necessarily it rains" + └── φ2 ✓ "Possibly it rains" +``` + +**Print a logical relations graph:** + +```ts +theory.printGraph(); +``` + +```text +LOGICAL RELATIONS GRAPH — Modal Logic (System K) +═══════════════════════════════════════════════════ + +Frame: 2 world(s), designated: actual + +Sentences: + φ1 "Necessarily it rains" [p] + φ2 "Possibly it rains" [p] + +Pairwise relations: + φ1 ↔ φ2 ENTAILS (φ1 ⊨ φ2) + +Shared propositions: + p: φ1 — φ2 +``` ## NLP Engine diff --git a/docs/languages/modal/DEFINITIONS.md b/docs/languages/modal/DEFINITIONS.md new file mode 100644 index 0000000..1878bb5 --- /dev/null +++ b/docs/languages/modal/DEFINITIONS.md @@ -0,0 +1,102 @@ +# Modal Logic — Design Notes + +## System K (Initial Implementation) + +System K is the minimal normal modal logic. It adds two operators to propositional logic: + +- **Box** `□φ` — "necessarily φ" — true at world w iff φ is true at every world accessible from w +- **Diamond** `◇φ` — "possibly φ" — true at world w iff φ is true at some world accessible from w + +### Kripke Semantics + +A **Kripke model** M = (W, R, V) consists of: + +- **W** — a finite set of possible worlds +- **R** — an accessibility relation on W (R ⊆ W × W) +- **V** — a valuation function: for each proposition letter p, V(p) ⊆ W (the worlds where p is true) + +Truth is defined relative to a world: + +- M, w ⊨ p iff w ∈ V(p) +- M, w ⊨ ~φ iff M, w ⊭ φ +- M, w ⊨ φ & ψ iff M, w ⊨ φ and M, w ⊨ ψ +- M, w ⊨ φ | ψ iff M, w ⊨ φ or M, w ⊨ ψ +- M, w ⊨ φ -> ψ iff M, w ⊭ φ or M, w ⊨ ψ +- M, w ⊨ φ <-> ψ iff M, w ⊨ φ iff M, w ⊨ ψ +- M, w ⊨ □φ iff for all w' such that wRw', M, w' ⊨ φ +- M, w ⊨ ◇φ iff there exists w' such that wRw', M, w' ⊨ φ + +### System K — No Frame Conditions + +System K imposes **no constraints** on R. Any accessibility relation is valid. +This means □p → p is NOT a theorem of K (that requires reflexivity = system T). + +### Valid in K + +- **K axiom**: □(p → q) → (□p → □q) — distribution of □ over → +- **Necessitation rule**: if φ is valid, then □φ is valid +- **Modal duality**: □p ⟺ ~◇~p, ◇p ⟺ ~□~p +- **Distribution**: □(p & q) ⟺ (□p & □q) + +### NOT valid in K + +- □p → p (reflexivity — valid in T) +- □p → □□p (transitivity — valid in S4) +- ◇p → □◇p (symmetry + transitivity — valid in S5) + +## Architecture + +### Evaluation Model + +Parallels quantificational logic exactly: + +| Quantificational | Modal | +| --- | --- | +| Domain elements | Worlds | +| Variable assignment | Current world + valuation | +| ∀x.φ(x) | □φ | +| ∃x.φ(x) | ◇φ | +| Predicates | Proposition letters (world-relative) | + +### Shared Mutable State + +All formulas reference a shared `ModalEvaluationState`: + +```typescript +interface ModalEvaluationState { + currentWorld: World; + valuation: Map>; // propName → worlds where true +} +``` + +### Consistency Check + +Given a frame (W, R) and designated world w₀: + +- Enumerate all 2^(|P|×|W|) valuations (P = proposition letters) +- For each valuation, check if all sentences are true at w₀ +- Complexity: exponential in propositions × worlds + +### Proof Tree Differences from Propositional/Quantificational + +Modal proof trees must show the **Kripke model structure**: + +- Frame: worlds and accessibility pairs +- Designated world +- Per-world truth table (which propositions are true at which worlds) +- How modal operators traverse the accessibility relation + +## Future Systems + +Each system adds frame conditions: + +| System | Frame Condition | +| --- | --- | +| K | (none) | +| T | Reflexive: wRw | +| S4 | Reflexive + Transitive | +| S5 | Equivalence relation | +| D | Serial: ∀w.∃w'.wRw' | + +Implementation: add a `ModalSystem` type and frame validation in the builder/theory. +For now, only K is implemented. diff --git a/src/language/index.ts b/src/language/index.ts index b799b1b..22b978c 100644 --- a/src/language/index.ts +++ b/src/language/index.ts @@ -1,3 +1,43 @@ +// Shared base types export * from './shared/types'; export * from './shared/theory'; + +// Propositional logic — establishes the shared operator types +// (BinaryOperator, UnaryOperator, binaryOperatorToLogic) used across all languages. export * from './propositional/index'; + +// Quantificational logic — unique exports only; operator types already exported above. +export { + DomainElement, + VariableAssignment, + Term, + Predicate, + Quantifier, + QFF, +} from './quantificational/quantificationalTypes'; +export { VariableTerm, ConstantTerm } from './quantificational/term'; +export { PredicateImpl, IDENTITY } from './quantificational/predicate'; +export { AtomicFormulaImpl } from './quantificational/atomicFormula'; +export { ComplexFormulaImpl } from './quantificational/complexFormula'; +export { QuantifiedFormulaImpl } from './quantificational/quantifiedFormula'; +export { QuantificationalVariable } from './quantificational/quantificationalVariable'; +export { isAtomicFormula, isComplexFormula, isQuantifiedFormula } from './quantificational/quantificationalUtils'; +export { QuantificationalFormalSentence, QuantificationalTheory } from './quantificational/quantificationalTheory'; +export { QuantificationalTheoryBuilder } from './quantificational/quantificationalTheoryBuilder'; + +// Modal logic — unique exports only; operator types already exported above. +export { + World, + ModalOperator, + ModalEvaluationState, + MFF, + ModalSystemSpec, +} from './modal/modalTypes'; +export { SystemK, SystemT, SystemD, SystemS4, SystemS5 } from './modal/modalSystems'; +export { ModalAtomImpl } from './modal/modalAtom'; +export { ModalComplexImpl } from './modal/modalComplex'; +export { ModalFormulaImpl } from './modal/modalFormula'; +export { ModalVariable } from './modal/modalVariable'; +export { isModalAtom, isModalComplex, isModalFormula } from './modal/modalUtils'; +export { ModalFormalSentence, ModalTheory } from './modal/modalTheory'; +export { ModalTheoryBuilder } from './modal/modalTheoryBuilder'; diff --git a/src/language/modal/index.ts b/src/language/modal/index.ts index 343d50c..cc89999 100644 --- a/src/language/modal/index.ts +++ b/src/language/modal/index.ts @@ -1,4 +1,9 @@ -// TODO: Modal logic -// Extends propositional logic with modal operators for necessity (□) and possibility (◇), -// evaluated over possible-worlds semantics (Kripke frames). -export {}; +export * from './modalTypes'; +export * from './modalSystems'; +export * from './modalAtom'; +export * from './modalComplex'; +export * from './modalFormula'; +export * from './modalVariable'; +export * from './modalUtils'; +export * from './modalTheory'; +export * from './modalTheoryBuilder'; diff --git a/src/language/modal/modalAtom.ts b/src/language/modal/modalAtom.ts new file mode 100644 index 0000000..eb5a84f --- /dev/null +++ b/src/language/modal/modalAtom.ts @@ -0,0 +1,51 @@ +import { MFF, UnaryOperator, ModalEvaluationState } from './modalTypes'; + +/** + * Concrete implementation of a modal atomic formula (proposition letter). + * + * A proposition letter has a truth value that varies by world. The truth + * value is looked up from the shared evaluation state's valuation map + * at the current world. + * + * Analogous to AtomImpl in propositional logic and AtomicFormulaImpl in + * quantificational logic. + * + * Example: p, q, r (proposition letters evaluated at the current world) + */ +export class ModalAtomImpl implements MFF { + + /** Optional negation applied to the proposition's truth value. */ + unaryOperator: UnaryOperator | undefined; + + /** The name of this proposition letter. */ + readonly propositionName: string; + + /** The shared evaluation state — holds current world and valuation. */ + private readonly _state: ModalEvaluationState; + + /** + * @param unaryOperator - Optional '~' to negate the result. + * @param propositionName - The name of the proposition letter (e.g. 'p', 'q'). + * @param state - The shared modal evaluation state. + */ + constructor( + unaryOperator: UnaryOperator | undefined, + propositionName: string, + state: ModalEvaluationState, + ) { + this.unaryOperator = unaryOperator; + this.propositionName = propositionName; + this._state = state; + } + + /** + * Evaluate the proposition letter at the current world. + * Returns true iff the current world is in the proposition's extension + * (the set of worlds where it is true), then applies negation if present. + */ + value(): boolean { + const extension = this._state.valuation.get(this.propositionName); + const rv = extension ? extension.has(this._state.currentWorld) : false; + return (this.unaryOperator === '~') ? !rv : rv; + } +} diff --git a/src/language/modal/modalComplex.ts b/src/language/modal/modalComplex.ts new file mode 100644 index 0000000..0293afc --- /dev/null +++ b/src/language/modal/modalComplex.ts @@ -0,0 +1,54 @@ +import { MFF, BinaryOperator, UnaryOperator } from './modalTypes'; + +/** 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 modal formula. + * + * Joins two MFFs 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 and quantificational + * ComplexFormulaImpl. + */ +export class ModalComplexImpl implements MFF { + + /** The left-hand sub-formula. */ + left: MFF; + /** 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: MFF; + + /** + * @param unaryOperator - Optional '~' to negate the whole formula. + * @param left - The left-hand MFF. + * @param binaryOperator - The connective joining left and right. + * @param right - The right-hand MFF. + */ + constructor(unaryOperator: UnaryOperator | undefined, left: MFF, binaryOperator: BinaryOperator, right: MFF) { + this.left = left; + this.unaryOperator = unaryOperator; + this.binaryOperator = binaryOperator; + this.right = right; + } + + /** + * Evaluate the complex formula at the current world. + * 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/modal/modalFormula.ts b/src/language/modal/modalFormula.ts new file mode 100644 index 0000000..99b6589 --- /dev/null +++ b/src/language/modal/modalFormula.ts @@ -0,0 +1,92 @@ +import { MFF, UnaryOperator, ModalOperator, World, ModalEvaluationState } from './modalTypes'; + +/** + * Concrete implementation of a modal formula (□ or ◇). + * + * This is the construct that distinguishes modal from propositional logic. + * Evaluates the body formula across worlds reachable via the accessibility + * relation from the current world. + * + * □φ — true at w iff φ is true at every world accessible from w + * ◇φ — true at w iff φ is true at some world accessible from w + * + * Directly parallels QuantifiedFormulaImpl: quantifiers iterate over domain + * elements, modal operators iterate over accessible worlds. + */ +export class ModalFormulaImpl implements MFF { + + /** Optional negation applied to the modal result. */ + unaryOperator: UnaryOperator | undefined; + + /** The modal operator: □ (necessity) or ◇ (possibility). */ + readonly modalOperator: ModalOperator; + + /** The body (scope) of the modal formula. */ + readonly body: MFF; + + /** The set of all worlds in the model. */ + private readonly _worlds: World[]; + + /** The accessibility relation: returns true when from can see to. */ + private readonly _accessibility: (from: World, to: World) => boolean; + + /** The shared evaluation state, mutated during evaluation. */ + private readonly _state: ModalEvaluationState; + + /** + * @param unaryOperator - Optional '~' to negate the whole modal result. + * @param modalOperator - '□' or '◇'. + * @param body - The formula in the scope of the modal operator. + * @param worlds - All worlds in the model. + * @param accessibility - The accessibility relation. + * @param state - The shared evaluation state. + */ + constructor( + unaryOperator: UnaryOperator | undefined, + modalOperator: ModalOperator, + body: MFF, + worlds: World[], + accessibility: (from: World, to: World) => boolean, + state: ModalEvaluationState, + ) { + this.unaryOperator = unaryOperator; + this.modalOperator = modalOperator; + this.body = body; + this._worlds = worlds; + this._accessibility = accessibility; + this._state = state; + } + + /** + * Evaluate the modal formula at the current world. + * + * For □: returns true iff the body is true at every world accessible + * from the current world. Restores the previous world after evaluation. + * + * For ◇: returns true iff the body is true at some world accessible + * from the current world. + */ + value(): boolean { + const currentWorld = this._state.currentWorld; + const accessibleWorlds = this._worlds.filter(w => this._accessibility(currentWorld, w)); + + let rv: boolean; + + if (this.modalOperator === '□') { + rv = accessibleWorlds.every(w => { + this._state.currentWorld = w; + return this.body.value(); + }); + } else { + rv = accessibleWorlds.some(w => { + this._state.currentWorld = w; + return this.body.value(); + }); + } + + // Restore the previous world. + this._state.currentWorld = currentWorld; + + return (this.unaryOperator === '~') ? !rv : rv; + } +} diff --git a/src/language/modal/modalSystems.ts b/src/language/modal/modalSystems.ts new file mode 100644 index 0000000..9126c2e --- /dev/null +++ b/src/language/modal/modalSystems.ts @@ -0,0 +1,118 @@ +import { ModalSystemSpec, World } from './modalTypes'; + +/** + * System K — the minimal normal modal logic. + * + * No frame conditions. Any accessibility relation is valid. + * All other normal modal systems extend K with additional axioms + * corresponding to additional frame conditions. + * + * Valid axiom: K — □(p → q) → (□p → □q) + */ +export const SystemK: ModalSystemSpec = { + name: 'K', + validateFrame(_worlds: World[], _accessibility: (from: World, to: World) => boolean): void { + // K imposes no frame conditions — all frames are valid. + }, +}; + +/** + * System T — reflexive frames. + * + * Adds to K: every world accesses itself. + * Corresponds to axiom T: □p → p ("what is necessary is true"). + * + * Frame condition: ∀w. wRw (reflexivity) + */ +export const SystemT: ModalSystemSpec = { + name: 'T', + validateFrame(worlds: World[], accessibility: (from: World, to: World) => boolean): void { + const violated = worlds.find(w => !accessibility(w, w)); + if (violated !== undefined) { + throw new Error( + `System T requires a reflexive frame: world '${violated}' does not access itself. ` + + `Ensure accessibility(w, w) = true for every world w.`, + ); + } + }, +}; + +/** + * System D — serial frames. + * + * Adds to K: every world accesses at least one world. + * Corresponds to axiom D: □p → ◇p ("what is necessary is possible"). + * + * Frame condition: ∀w. ∃w'. wRw' (seriality) + */ +export const SystemD: ModalSystemSpec = { + name: 'D', + validateFrame(worlds: World[], accessibility: (from: World, to: World) => boolean): void { + const violated = worlds.find(w => !worlds.some(w2 => accessibility(w, w2))); + if (violated !== undefined) { + throw new Error( + `System D requires a serial frame: world '${violated}' accesses no other world. ` + + `Every world must access at least one world.`, + ); + } + }, +}; + +/** + * System S4 — reflexive and transitive frames. + * + * Adds to T: if w accesses w' and w' accesses w'', then w accesses w''. + * Corresponds to axiom 4: □p → □□p ("if necessary, then necessarily necessary"). + * + * Frame conditions: reflexivity + transitivity + */ +export const SystemS4: ModalSystemSpec = { + name: 'S4', + validateFrame(worlds: World[], accessibility: (from: World, to: World) => boolean): void { + // Reflexivity (same as T) + SystemT.validateFrame(worlds, accessibility); + + // Transitivity: if wRw' and w'Rw'' then wRw'' + for (const w of worlds) { + for (const w2 of worlds) { + if (!accessibility(w, w2)) continue; + for (const w3 of worlds) { + if (accessibility(w2, w3) && !accessibility(w, w3)) { + throw new Error( + `System S4 requires a transitive frame: ${w}R${w2} and ${w2}R${w3} ` + + `but not ${w}R${w3}. Ensure transitivity holds.`, + ); + } + } + } + } + }, +}; + +/** + * System S5 — equivalence frames (reflexive, transitive, symmetric). + * + * Adds to S4: if w accesses w' then w' accesses w. + * Corresponds to axiom 5: ◇p → □◇p ("if possible, then necessarily possible"). + * + * Frame conditions: reflexivity + transitivity + symmetry + */ +export const SystemS5: ModalSystemSpec = { + name: 'S5', + validateFrame(worlds: World[], accessibility: (from: World, to: World) => boolean): void { + // Reflexivity + Transitivity (same as S4) + SystemS4.validateFrame(worlds, accessibility); + + // Symmetry: if wRw' then w'Rw + for (const w of worlds) { + for (const w2 of worlds) { + if (accessibility(w, w2) && !accessibility(w2, w)) { + throw new Error( + `System S5 requires a symmetric frame: ${w}R${w2} but not ${w2}R${w}. ` + + `Ensure symmetry holds.`, + ); + } + } + } + }, +}; diff --git a/src/language/modal/modalTheory.ts b/src/language/modal/modalTheory.ts new file mode 100644 index 0000000..f72bc60 --- /dev/null +++ b/src/language/modal/modalTheory.ts @@ -0,0 +1,361 @@ +import { MFF, World, ModalEvaluationState, ModalSystemSpec } from './modalTypes'; +import { ModalVariable } from './modalVariable'; +import { FormalSentence, Theory, ConsistencyResult, ProofNode } from '../shared/theory'; + +// ─── Types ─────────────────────────────────────────────────────────────────── + +/** + * A formalised sentence within a modal theory. + * Extends FormalSentence with the set of proposition names the formula + * depends on, used when rendering the logical relations graph. + */ +export interface ModalFormalSentence extends FormalSentence { + /** Names of the proposition letters this formula's truth value depends on. */ + propositionNames: string[]; +} + +// ─── Internal helpers ──────────────────────────────────────────────────────── + +/** + * Render a valuation as a human-readable string showing per-world truth values. + */ +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), + ); +} + +// ─── ModalTheory ───────────────────────────────────────────────────────────── + +/** + * A formal modal theory — a finite set of MFFs derived from assertoric + * sentences, equipped with consistency checking over a Kripke frame + * and structured output. + * + * Consistency is decided by exhaustive evaluation over all 2^(|P|×|W|) + * valuations, where P is the set of proposition letters and W is the set + * of worlds. For each valuation, all sentences are evaluated at the + * designated world. + * + * Construct via ModalTheoryBuilder, not directly. + */ +export class ModalTheory implements Theory { + + /** The formalised sentences constituting this theory. */ + readonly sentences: ModalFormalSentence[]; + + /** The set of possible worlds. */ + readonly worlds: World[]; + + /** The accessibility relation. */ + readonly accessibility: (from: World, to: World) => boolean; + + /** The designated world (where sentences are evaluated). */ + readonly designatedWorld: World; + + /** The modal system spec (determines frame conditions and display name). */ + readonly system: ModalSystemSpec; + + /** The named proposition variables, keyed by name. */ + private readonly variables: Map; + + /** The shared evaluation state. */ + private readonly state: ModalEvaluationState; + + constructor( + sentences: ModalFormalSentence[], + worlds: World[], + accessibility: (from: World, to: World) => boolean, + designatedWorld: World, + variables: Map, + state: ModalEvaluationState, + system: ModalSystemSpec, + ) { + this.sentences = sentences; + this.worlds = worlds; + this.accessibility = accessibility; + this.designatedWorld = designatedWorld; + this.variables = variables; + this.state = state; + this.system = system; + } + + // ── Public API ───────────────────────────────────────────────────────────── + + /** + * Determine whether all sentences in the theory can be simultaneously true + * at the designated world under some valuation. + * + * Algorithm: exhaustive enumeration of all 2^(|P|×|W|) valuations. + * Each bit in the enumeration index determines whether a proposition + * is true at a particular world. + */ + checkConsistency(): ConsistencyResult { + const propNames = Array.from(this.variables.keys()); + const numBits = propNames.length * this.worlds.length; + const total = Math.pow(2, numBits); + const failedValuations: NonNullable['failedValuations']> = []; + + for (let i = 0; i < total; i++) { + const valuation = this._applyValuation(propNames, i); + this.state.currentWorld = this.designatedWorld; + + 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. + * + * Modal proof trees include the Kripke frame structure (worlds and + * accessibility pairs) in addition to the standard verdict, method, + * and witness/exhaustion nodes. + */ + buildProofTree(): ProofNode { + const result = this.checkConsistency(); + const propNames = Array.from(this.variables.keys()); + const numBits = propNames.length * this.worlds.length; + const total = Math.pow(2, numBits); + + const accessPairs: string[] = []; + for (const w1 of this.worlds) { + for (const w2 of this.worlds) { + if (this.accessibility(w1, w2)) { + accessPairs.push(`${w1}R${w2}`); + } + } + } + + const header = `Theory: ${this.sentences.length} sentence(s), ` + + `${propNames.length} proposition(s) {${propNames.join(', ')}}, ` + + `${this.worlds.length} world(s) {${this.worlds.join(', ')}}`; + + const frameNode: ProofNode = { + label: 'Kripke frame:', + children: [ + { label: `Worlds: {${this.worlds.join(', ')}}`, children: [] }, + { label: `Accessibility: {${accessPairs.join(', ') || '(empty)'}}`, children: [] }, + { label: `Designated world: ${this.designatedWorld}`, children: [] }, + ], + }; + + if (result.isConsistent) { + // Restore the witness so formula.value() reflects it. + this._restoreValuation(propNames, result.witness!); + this.state.currentWorld = this.designatedWorld; + + const worldTable: ProofNode = { + label: 'Per-world valuation:', + children: this.worlds.map(w => { + const vals = propNames.map(p => { + const isTrue = this.state.valuation.get(p)?.has(w) ?? false; + return `${p}=${isTrue}`; + }); + return { label: `${w}: {${vals.join(', ')}}`, children: [] }; + }), + }; + + return { + label: 'CONSISTENT ✓', + children: [ + { label: header, children: [] }, + frameNode, + { label: `Method: exhaustive evaluation, 2^(${propNames.length}×${this.worlds.length}) = ${total} valuations checked`, children: [] }, + worldTable, + { + label: 'Verification (at designated world):', + children: this.sentences.map(s => ({ + label: `${s.label} ${s.formula.value() ? '✓' : '✗'} "${s.source.raw}"`, + children: [], + })), + }, + ], + }; + } + + return { + label: 'INCONSISTENT ✗', + children: [ + { label: header, children: [] }, + frameNode, + { label: `Method: exhaustive evaluation, 2^(${propNames.length}×${this.worlds.length}) = ${total} valuations checked`, children: [] }, + { + label: `No satisfying valuation 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 — Modal Logic (System ${this.system.name})`); + 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 — Modal Logic (System ${this.system.name})`); + console.log('═'.repeat(51)); + + // Frame summary + console.log(`\nFrame: ${this.worlds.length} world(s), designated: ${this.designatedWorld}`); + + // Nodes + console.log('\nSentences:'); + this.sentences.forEach(s => { + const props = s.propositionNames.length ? ` [${s.propositionNames.join(', ')}]` : ''; + console.log(` ${s.label.padEnd(5)} "${s.source.raw}"${props}`); + }); + + // Pairwise relations + if (n > 1) { + console.log('\nPairwise relations:'); + const propNames = 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], propNames); + 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 propositions + const propToSentences = new Map(); + this.sentences.forEach(s => + s.propositionNames.forEach(p => { + if (!propToSentences.has(p)) propToSentences.set(p, []); + propToSentences.get(p)!.push(s.label); + }), + ); + const shared = Array.from(propToSentences.entries()).filter(([, labels]) => labels.length > 1); + if (shared.length) { + console.log('\nShared propositions:'); + shared.forEach(([propName, labels]) => + console.log(` ${propName}: ${labels.join(' — ')}`), + ); + } + + console.log(''); + } + + // ── Private helpers ──────────────────────────────────────────────────────── + + /** + * Apply the i-th valuation from the enumeration of 2^(|P|×|W|) valuations. + * Each bit in i determines whether proposition p is true at world w. + * + * Bit layout: for propositions [p0, p1, ...] and worlds [w0, w1, ...], + * bit (pIdx * |W| + wIdx) controls p_pIdx at w_wIdx. + */ + private _applyValuation(propNames: string[], index: number): Record { + const valuation: Record = {}; + + propNames.forEach((prop, pIdx) => { + const extension = new Set(); + this.worlds.forEach((w, wIdx) => { + const bitPos = pIdx * this.worlds.length + wIdx; + const isTrue = ((index >> bitPos) & 1) === 1; + const key = `${prop}@${w}`; + valuation[key] = isTrue; + if (isTrue) extension.add(w); + }); + this.state.valuation.set(prop, extension); + }); + + return valuation; + } + + /** + * Restore a valuation from a witness record (used after consistency check + * to make formula.value() reflect the witness). + */ + private _restoreValuation(propNames: string[], witness: Record): void { + propNames.forEach(prop => { + const extension = new Set(); + this.worlds.forEach(w => { + if (witness[`${prop}@${w}`]) extension.add(w); + }); + this.state.valuation.set(prop, extension); + }); + } + + /** + * Compute the pairwise logical relation between two sentences. + */ + private _pairwiseRelation( + s1: ModalFormalSentence, + s2: ModalFormalSentence, + propNames: string[], + ): string { + let bothTrue = false; + let s1TrueS2False = false; + let s1FalseS2True = false; + + const numBits = propNames.length * this.worlds.length; + const total = Math.pow(2, numBits); + for (let i = 0; i < total; i++) { + this._applyValuation(propNames, i); + this.state.currentWorld = this.designatedWorld; + 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/modal/modalTheoryBuilder.ts b/src/language/modal/modalTheoryBuilder.ts new file mode 100644 index 0000000..5ae3b67 --- /dev/null +++ b/src/language/modal/modalTheoryBuilder.ts @@ -0,0 +1,179 @@ +import { MFF, World, ModalEvaluationState, ModalSystemSpec } from './modalTypes'; +import { SystemK } from './modalSystems'; +import { ModalVariable } from './modalVariable'; +import { ModalFormalSentence, ModalTheory } from './modalTheory'; +import { AlethicAssertoric, SentenceSet } from '../shared/types'; + +/** + * Fluent builder for constructing a ModalTheory. + * + * Declare a system with system() (defaults to SystemK), worlds with worlds(), + * the accessibility relation with accessibility(), the designated world with + * designatedWorld(), proposition letters with proposition(), register sentences + * with sentence(), then call build() to produce an immutable ModalTheory. + * + * build() validates the accessibility relation against the chosen system's + * frame conditions before constructing the theory — it throws if the frame + * does not satisfy the system's requirements. + */ +export class ModalTheoryBuilder { + + private _system: ModalSystemSpec = SystemK; + private _worlds: World[] = []; + private _accessibility: (from: World, to: World) => boolean = () => false; + private _designatedWorld: World = ''; + private readonly _state: ModalEvaluationState = { + currentWorld: '', + valuation: new Map(), + }; + private readonly _variables = new Map(); + private readonly _sentences: ModalFormalSentence[] = []; + private _labelCounter = 1; + + /** + * Set the modal system. + * + * The system determines which frame conditions are enforced on build(). + * Defaults to SystemK (no conditions). Pass SystemT, SystemS4, SystemS5, + * or any custom ModalSystemSpec to enforce stricter conditions. + * + * @param spec - The modal system specification. + * @returns this, for method chaining. + */ + system(spec: ModalSystemSpec): this { + this._system = spec; + return this; + } + + /** + * Set the possible worlds. + * + * @param ws - The world identifiers. + * @returns this, for method chaining. + */ + worlds(...ws: World[]): this { + this._worlds = ws; + return this; + } + + /** + * Set the accessibility relation. + * + * @param fn - A function returning true when the first world can access the second. + * @returns this, for method chaining. + */ + accessibility(fn: (from: World, to: World) => boolean): this { + this._accessibility = fn; + return this; + } + + /** + * Set the designated world (where sentences are evaluated). + * + * @param w - The designated world. + * @returns this, for method chaining. + */ + designatedWorld(w: World): this { + this._designatedWorld = w; + this._state.currentWorld = w; + return this; + } + + /** + * Declare a named proposition letter. + * Calling proposition() with the same name twice returns the same instance. + * + * @param name - The logical name for the proposition (e.g. 'p', 'q'). + * @returns The ModalVariable instance for that name. + */ + proposition(name: string): ModalVariable { + if (!this._variables.has(name)) { + this._variables.set(name, new ModalVariable(name, this._state)); + } + return this._variables.get(name)!; + } + + /** + * Add a formalised sentence to the theory under construction. + * + * @param source - The validated natural language sentence. + * @param formula - The MFF that formalises the sentence. + * @param propositionNames - Names of the propositions this formula depends on. + * @param label - Optional display label; defaults to φ1, φ2, … + * @returns this, for method chaining. + */ + sentence( + source: AlethicAssertoric, + formula: MFF, + propositionNames: string[], + label?: string, + ): this { + this._sentences.push({ + source, + formula, + propositionNames, + label: label ?? `φ${this._labelCounter++}`, + }); + return this; + } + + /** + * The shared evaluation state. + * Exposed so formula constructors can reference it. + */ + get state(): ModalEvaluationState { + return this._state; + } + + /** + * The current worlds list. + * Exposed so formula constructors can reference it. + */ + get currentWorlds(): World[] { + return this._worlds; + } + + /** + * The current accessibility relation. + * Exposed so formula constructors can reference it. + */ + get currentAccessibility(): (from: World, to: World) => boolean { + return this._accessibility; + } + + /** + * Finalise and return the ModalTheory. + * + * Validates the accessibility relation against the chosen system's frame + * conditions before constructing. Throws if the frame is invalid for the + * chosen system. + * + * @returns A new ModalTheory containing all sentences added so far. + */ + build(): ModalTheory { + this._system.validateFrame(this._worlds, this._accessibility); + return new ModalTheory( + [...this._sentences], + [...this._worlds], + this._accessibility, + this._designatedWorld, + new Map(this._variables), + this._state, + this._system, + ); + } + + /** + * Placeholder: future entry point for NLP-driven construction. + * + * @param _set - The sentence set to formalise. + * @throws Error until ModalSyntaxEngine is implemented. + */ + // eslint-disable-next-line @typescript-eslint/no-unused-vars + fromSentenceSet(_set: SentenceSet): ModalTheory { + throw new Error( + 'ModalTheoryBuilder.fromSentenceSet is not yet implemented. ' + + 'Awaiting ModalSyntaxEngine.', + ); + } +} diff --git a/src/language/modal/modalTypes.d.ts b/src/language/modal/modalTypes.d.ts new file mode 100644 index 0000000..34edb1d --- /dev/null +++ b/src/language/modal/modalTypes.d.ts @@ -0,0 +1,95 @@ +import { Formula } from '../shared/types'; + +/** + * A possible world identifier. + * Worlds are the points of evaluation in Kripke semantics. + */ +type World = string; + +/** + * The modal operators. + * + * □ := Necessity — "necessarily" — true at w iff true at all accessible worlds + * ◇ := Possibility — "possibly" — true at w iff true at some accessible world + */ +type ModalOperator = '□' | '◇'; + +/** + * 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 = '&' | '|' | '->' | '<->'; + +/** + * Shared mutable state for modal formula evaluation. + * + * All formulas in a modal theory reference the same state object. + * The theory mutates `currentWorld` and `valuation` during consistency + * checking, and modal operators mutate `currentWorld` when traversing + * the accessibility relation. + */ +interface ModalEvaluationState { + /** The world at which formulas are currently being evaluated. */ + currentWorld: World; + /** For each proposition name, the set of worlds where it is true. */ + valuation: Map>; +} + +/** + * A Modal Formula — the union of all valid modal logic expressions. + * Every syntactically correct modal expression satisfies this type. + * + * Analogous to WFF (propositional) and QFF (quantificational). + */ +interface MFF extends Formula { + /** Optional negation applied to the formula before evaluation. */ + unaryOperator: UnaryOperator | undefined; + /** Evaluate the formula at the current world in the current model. */ + value(): boolean; +} + +/** + * Specification for a modal logic system. + * + * A modal system is a set of frame conditions that constrain which Kripke + * frames are valid for that system. The spec encapsulates both the system + * name (used in output) and its frame validation logic. + * + * Concrete instances live in modalSystems.ts. The language layer + * (formula evaluation) is entirely system-agnostic — only the theory + * builder and theory output depend on this interface. + */ +interface ModalSystemSpec { + /** Display name of the system (e.g. 'K', 'T', 'S4', 'S5'). */ + readonly name: string; + /** + * Validate that the given frame satisfies this system's conditions. + * Throws a descriptive error if any condition is violated. + * + * @param worlds - The set of possible worlds. + * @param accessibility - The accessibility relation to validate. + */ + validateFrame(worlds: World[], accessibility: (from: World, to: World) => boolean): void; +} + +export { + World, + ModalOperator, + UnaryOperator, + BinaryOperator, + ModalEvaluationState, + MFF, + ModalSystemSpec, +}; diff --git a/src/language/modal/modalUtils.ts b/src/language/modal/modalUtils.ts new file mode 100644 index 0000000..9aadc6a --- /dev/null +++ b/src/language/modal/modalUtils.ts @@ -0,0 +1,41 @@ +import { MFF } from './modalTypes'; + +/** + * Lookup table mapping each binary operator to its truth-functional semantics + * as a two-argument boolean function. + * + * Same semantics as propositional and quantificational — kept local to + * avoid cross-module coupling. + */ +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 MFF has modal atom shape. + * Uses structural check (presence of 'propositionName' property). + */ +const isModalAtom = (mff: MFF): boolean => { + return 'propositionName' in mff; +}; + +/** + * Type guard: returns true when the given MFF has complex formula shape. + * Uses structural check to avoid circular dependency with modalComplex.ts. + */ +const isModalComplex = (mff: MFF): boolean => { + return 'left' in mff && 'binaryOperator' in mff && 'right' in mff; +}; + +/** + * Type guard: returns true when the given MFF has modal formula shape (□ or ◇). + * Uses structural check to avoid circular dependency with modalFormula.ts. + */ +const isModalFormula = (mff: MFF): boolean => { + return 'modalOperator' in mff && 'body' in mff; +}; + +export { binaryOperatorToLogic, isModalAtom, isModalComplex, isModalFormula }; diff --git a/src/language/modal/modalVariable.ts b/src/language/modal/modalVariable.ts new file mode 100644 index 0000000..49326e3 --- /dev/null +++ b/src/language/modal/modalVariable.ts @@ -0,0 +1,44 @@ +import { ModalEvaluationState } from './modalTypes'; +import { ModalAtomImpl } from './modalAtom'; + +/** + * A named proposition letter with world-relative truth values. + * + * Analogous to PropositionalVariable and QuantificationalVariable. + * All ModalAtomImpl instances created from this variable share the same + * underlying evaluation state, so updating the valuation updates every + * derived atom simultaneously. + * + * Used by ModalTheory to iterate over valuations during consistency + * checking, and by ModalFormulaImpl when modal operators traverse worlds. + */ +export class ModalVariable { + + /** The immutable name of this proposition letter (e.g. 'p', 'q'). */ + readonly name: string; + + /** The shared evaluation state this variable participates in. */ + private readonly _state: ModalEvaluationState; + + /** + * @param name - The logical name for this proposition letter. + * @param state - The shared evaluation state. + */ + constructor(name: string, state: ModalEvaluationState) { + this.name = name; + this._state = state; + } + + /** + * Create a ModalAtomImpl for this proposition letter. + * + * @param negated - When true, wraps the atom with '~'. + */ + atom(negated = false): ModalAtomImpl { + return new ModalAtomImpl( + negated ? '~' : undefined, + this.name, + this._state, + ); + } +} diff --git a/test/language/modal/meta-logic/completeness.spec.ts b/test/language/modal/meta-logic/completeness.spec.ts new file mode 100644 index 0000000..b5ba4ea --- /dev/null +++ b/test/language/modal/meta-logic/completeness.spec.ts @@ -0,0 +1,510 @@ +import { ModalAtomImpl } from '../../../../src/language/modal/modalAtom'; +import { ModalComplexImpl } from '../../../../src/language/modal/modalComplex'; +import { ModalFormulaImpl } from '../../../../src/language/modal/modalFormula'; +import { ModalEvaluationState, BinaryOperator, World, MFF } from '../../../../src/language/modal/modalTypes'; +import { binaryOperatorToLogic } from '../../../../src/language/modal/modalUtils'; + +/** + * COMPLETENESS OF MODAL LOGIC — SYSTEM K (over finite Kripke models) + * ───────────────────────────────────────────────────────────────────────────── + * Theorem: The exhaustive evaluation method is sound and complete for + * modal logic system K over finite Kripke models. + * + * Soundness — if exhaustive evaluation returns true on every valuation + * for a given frame, the formula is valid on that frame. + * + * Completeness — every formula valid on a finite frame is confirmed by + * the exhaustive method. + * + * Proof structure: + * + * Part I — Structural induction: value() correctly computes the truth + * function of any MFF at any world in any Kripke model. + * + * Base case: ModalAtomImpl correctly reads the valuation at the + * current world, with and without negation. + * + * IH: left.value() and right.value() correctly return L and R. + * + * Ind. step: ModalComplexImpl correctly applies binary operators. + * ModalFormulaImpl correctly iterates over accessible + * worlds for □ and ◇. + * + * Part II — Consequence: theorems and non-theorems of K are classified + * correctly. Includes K axiom, modal duality, and distribution. + * ───────────────────────────────────────────────────────────────────────────── + */ + +// ─── Test helpers ────────────────────────────────────────────────────────── + +function makeState(currentWorld: World, valuation: Record): ModalEvaluationState { + const map = new Map>(); + for (const [prop, worlds] of Object.entries(valuation)) { + map.set(prop, new Set(worlds)); + } + return { currentWorld, valuation: map }; +} + +/** Test frames of increasing complexity */ +interface TestFrame { + worlds: World[]; + accessibility: (from: World, to: World) => boolean; + label: string; +} + +const FRAMES: TestFrame[] = [ + { + worlds: ['w0'], + accessibility: () => false, + label: 'isolated single world', + }, + { + worlds: ['w0'], + accessibility: (f, t) => f === 'w0' && t === 'w0', + label: 'reflexive single world', + }, + { + worlds: ['w0', 'w1'], + accessibility: (f, t) => f === 'w0' && t === 'w1', + label: 'two worlds, w0→w1', + }, + { + worlds: ['w0', 'w1'], + accessibility: () => true, + label: 'two worlds, fully connected', + }, + { + worlds: ['w0', 'w1', 'w2'], + accessibility: (f, t) => f === 'w0' && (t === 'w1' || t === 'w2'), + label: 'three worlds, w0→w1, w0→w2', + }, + { + worlds: ['w0', 'w1', 'w2'], + accessibility: (f, t) => + (f === 'w0' && t === 'w1') || (f === 'w1' && t === 'w2'), + label: 'three worlds, chain w0→w1→w2', + }, +]; + +/** + * Check whether a modal formula is valid on a given frame (true under every + * valuation at every world). For formulas with propositions props, enumerates + * all 2^(|props|×|W|) valuations and checks at the designated world. + */ +function isValidOnFrame( + formula: MFF, + frame: TestFrame, + props: string[], + state: ModalEvaluationState, + designatedWorld: World, +): boolean { + const numBits = props.length * frame.worlds.length; + const total = Math.pow(2, numBits); + + for (let i = 0; i < total; i++) { + // Apply valuation + props.forEach((prop, pIdx) => { + const extension = new Set(); + frame.worlds.forEach((w, wIdx) => { + const bitPos = pIdx * frame.worlds.length + wIdx; + if (((i >> bitPos) & 1) === 1) extension.add(w); + }); + state.valuation.set(prop, extension); + }); + + state.currentWorld = designatedWorld; + if (!formula.value()) return false; + } + return true; +} + +/** + * Check validity at ALL worlds in the frame (stronger than single-world validity). + */ +function isValidOnFrameAtAllWorlds( + formulaFactory: (state: ModalEvaluationState, frame: TestFrame) => MFF, + frame: TestFrame, + props: string[], +): boolean { + const state = makeState(frame.worlds[0], {}); + const formula = formulaFactory(state, frame); + + for (const w of frame.worlds) { + if (!isValidOnFrame(formula, frame, props, state, w)) return false; + } + return true; +} + +// ───────────────────────────────────────────────────────────────────────────── + +describe('Completeness of Modal Logic — System K (finite Kripke models)', () => { + + // ── Part I: Structural induction ─────────────────────────────────────────── + + describe('Part I — Structural induction: value() is semantically correct', () => { + + describe('Base case — ModalAtomImpl', () => { + + test('proposition reads correct value from valuation at current world', () => { + const state = makeState('w0', { p: ['w0', 'w2'] }); + const atom = new ModalAtomImpl(undefined, 'p', state); + + expect(atom.value()).toBe(true); // w0 in extension + state.currentWorld = 'w1'; + expect(atom.value()).toBe(false); // w1 not in extension + state.currentWorld = 'w2'; + expect(atom.value()).toBe(true); // w2 in extension + }); + + test('negation inverts the proposition value', () => { + const state = makeState('w0', { p: ['w0'] }); + expect(new ModalAtomImpl('~', 'p', state).value()).toBe(false); + expect(new ModalAtomImpl(undefined, 'p', state).value()).toBe(true); + }); + }); + + describe('Inductive step — ModalComplexImpl (binary operators)', () => { + const operators: BinaryOperator[] = ['&', '|', '->', '<->']; + const boolPairs: [boolean, boolean][] = [[false,false],[false,true],[true,false],[true,true]]; + + function fixedAtom(state: ModalEvaluationState, val: boolean, id: string): ModalAtomImpl { + if (val) { + state.valuation.set(id, new Set([state.currentWorld])); + } else { + state.valuation.set(id, new Set()); + } + return new ModalAtomImpl(undefined, id, state); + } + + operators.forEach(op => { + boolPairs.forEach(([L, R]) => { + const expected = binaryOperatorToLogic[op](L, R); + test(`(${L} ${op} ${R}) = ${expected}`, () => { + const state = makeState('w0', {}); + expect(new ModalComplexImpl( + undefined, fixedAtom(state, L, '_L'), op, fixedAtom(state, R, '_R'), + ).value()).toBe(expected); + }); + test(`~(${L} ${op} ${R}) = ${!expected}`, () => { + const state = makeState('w0', {}); + expect(new ModalComplexImpl( + '~', fixedAtom(state, L, '_L'), op, fixedAtom(state, R, '_R'), + ).value()).toBe(!expected); + }); + }); + }); + }); + + describe('Inductive step — ModalFormulaImpl (□ and ◇)', () => { + + test('□ iterates every accessible world and is true only when body holds for all', () => { + FRAMES.forEach(frame => { + const state = makeState(frame.worlds[0], { p: [frame.worlds[0]] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const boxP = new ModalFormulaImpl( + undefined, '□', p, frame.worlds, frame.accessibility, state, + ); + + // Compute expected: p must be true at all worlds accessible from worlds[0] + const accessibleWorlds = frame.worlds.filter(w => frame.accessibility(frame.worlds[0], w)); + const expected = accessibleWorlds.every(w => state.valuation.get('p')!.has(w)); + + state.currentWorld = frame.worlds[0]; + expect(boxP.value()).toBe(expected); + }); + }); + + test('◇ iterates accessible worlds and is true when body holds for at least one', () => { + FRAMES.forEach(frame => { + const state = makeState(frame.worlds[0], { p: [frame.worlds[0]] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const diaP = new ModalFormulaImpl( + undefined, '◇', p, frame.worlds, frame.accessibility, state, + ); + + const accessibleWorlds = frame.worlds.filter(w => frame.accessibility(frame.worlds[0], w)); + const expected = accessibleWorlds.some(w => state.valuation.get('p')!.has(w)); + + state.currentWorld = frame.worlds[0]; + expect(diaP.value()).toBe(expected); + }); + }); + + test('□ and ◇ restore current world after evaluation', () => { + const state = makeState('w0', { p: ['w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1']; + const R = (f: World, t: World) => f === 'w0' && t === 'w1'; + + new ModalFormulaImpl(undefined, '□', p, worlds, R, state).value(); + expect(state.currentWorld).toBe('w0'); + + new ModalFormulaImpl(undefined, '◇', p, worlds, R, state).value(); + expect(state.currentWorld).toBe('w0'); + }); + }); + }); + + // ── Part II: Consequence — theorems and non-theorems of K ────────────────── + + describe('Part II — Modal duality', () => { + + test('□p ⟺ ~◇~p (verified over all frames and valuations)', () => { + FRAMES.forEach(frame => { + const result = isValidOnFrameAtAllWorlds( + (state, fr) => { + const p = new ModalAtomImpl(undefined, 'p', state); + const notP = new ModalAtomImpl('~', 'p', state); + + const boxP = new ModalFormulaImpl(undefined, '□', p, fr.worlds, fr.accessibility, state); + const diaNegP = new ModalFormulaImpl(undefined, '◇', notP, fr.worlds, fr.accessibility, state); + const negDiaNegP = new ModalFormulaImpl('~', '◇', notP, fr.worlds, fr.accessibility, state); + + // □p <-> ~◇~p + return new ModalComplexImpl(undefined, boxP, '<->', negDiaNegP); + }, + frame, + ['p'], + ); + expect(result).toBe(true); + }); + }); + + test('◇p ⟺ ~□~p (verified over all frames and valuations)', () => { + FRAMES.forEach(frame => { + const result = isValidOnFrameAtAllWorlds( + (state, fr) => { + const p = new ModalAtomImpl(undefined, 'p', state); + const notP = new ModalAtomImpl('~', 'p', state); + + const diaP = new ModalFormulaImpl(undefined, '◇', p, fr.worlds, fr.accessibility, state); + const boxNegP = new ModalFormulaImpl(undefined, '□', notP, fr.worlds, fr.accessibility, state); + const negBoxNegP = new ModalFormulaImpl('~', '□', notP, fr.worlds, fr.accessibility, state); + + // ◇p <-> ~□~p + return new ModalComplexImpl(undefined, diaP, '<->', negBoxNegP); + }, + frame, + ['p'], + ); + expect(result).toBe(true); + }); + }); + }); + + describe('Part II — K axiom: □(p → q) → (□p → □q)', () => { + + test('K axiom is valid on every frame (verified exhaustively)', () => { + FRAMES.forEach(frame => { + const result = isValidOnFrameAtAllWorlds( + (state, fr) => { + const p = new ModalAtomImpl(undefined, 'p', state); + const q = new ModalAtomImpl(undefined, 'q', state); + + // p -> q + const impl = new ModalComplexImpl(undefined, p, '->', q); + + // □(p -> q) + const boxImpl = new ModalFormulaImpl(undefined, '□', impl, fr.worlds, fr.accessibility, state); + + // □p + const boxP = new ModalFormulaImpl(undefined, '□', p, fr.worlds, fr.accessibility, state); + + // □q + const boxQ = new ModalFormulaImpl(undefined, '□', q, fr.worlds, fr.accessibility, state); + + // □p → □q + const boxPtoBoxQ = new ModalComplexImpl(undefined, boxP, '->', boxQ); + + // □(p → q) → (□p → □q) + return new ModalComplexImpl(undefined, boxImpl, '->', boxPtoBoxQ); + }, + frame, + ['p', 'q'], + ); + expect(result).toBe(true); + }); + }); + }); + + describe('Part II — Distribution: □(p & q) ⟺ (□p & □q)', () => { + + test('□(p & q) <-> (□p & □q) is valid on every frame', () => { + FRAMES.forEach(frame => { + const result = isValidOnFrameAtAllWorlds( + (state, fr) => { + const p = new ModalAtomImpl(undefined, 'p', state); + const q = new ModalAtomImpl(undefined, 'q', state); + + // □(p & q) + const conj = new ModalComplexImpl(undefined, p, '&', q); + const lhs = new ModalFormulaImpl(undefined, '□', conj, fr.worlds, fr.accessibility, state); + + // □p & □q + const boxP = new ModalFormulaImpl(undefined, '□', p, fr.worlds, fr.accessibility, state); + const boxQ = new ModalFormulaImpl(undefined, '□', q, fr.worlds, fr.accessibility, state); + const rhs = new ModalComplexImpl(undefined, boxP, '&', boxQ); + + return new ModalComplexImpl(undefined, lhs, '<->', rhs); + }, + frame, + ['p', 'q'], + ); + expect(result).toBe(true); + }); + }); + }); + + describe('Part II — Necessitation: tautologies are necessarily true', () => { + + test('□(p | ~p) is valid on every frame', () => { + FRAMES.forEach(frame => { + const result = isValidOnFrameAtAllWorlds( + (state, fr) => { + const p = new ModalAtomImpl(undefined, 'p', state); + const notP = new ModalAtomImpl('~', 'p', state); + const lem = new ModalComplexImpl(undefined, p, '|', notP); + return new ModalFormulaImpl(undefined, '□', lem, fr.worlds, fr.accessibility, state); + }, + frame, + ['p'], + ); + expect(result).toBe(true); + }); + }); + }); + + describe('Part II — Non-theorems of K (valid only under frame conditions)', () => { + + test('□p → p is NOT valid on all K-frames (requires reflexivity = system T)', () => { + // Should fail on at least one frame (any non-reflexive frame) + const nonReflexiveFrame = FRAMES.find(f => f.label === 'two worlds, w0→w1'); + expect(nonReflexiveFrame).toBeDefined(); + + const state = makeState('w0', {}); + const p = new ModalAtomImpl(undefined, 'p', state); + const boxP = new ModalFormulaImpl( + undefined, '□', p, + nonReflexiveFrame!.worlds, nonReflexiveFrame!.accessibility, state, + ); + const tAxiom = new ModalComplexImpl(undefined, boxP, '->', p); + + // Countermodel: p false at w0, p true at w1 + // □p is true at w0 (only accessible world is w1 where p is true) + // but p is false at w0 + // So □p → p is false + state.valuation.set('p', new Set(['w1'])); + state.currentWorld = 'w0'; + expect(tAxiom.value()).toBe(false); + }); + + test('□p → □□p is NOT valid on all K-frames (requires transitivity = system 4)', () => { + // Chain frame: w0→w1→w2 + const chainFrame = FRAMES.find(f => f.label === 'three worlds, chain w0→w1→w2'); + expect(chainFrame).toBeDefined(); + + const state = makeState('w0', {}); + const p = new ModalAtomImpl(undefined, 'p', state); + const boxP = new ModalFormulaImpl( + undefined, '□', p, + chainFrame!.worlds, chainFrame!.accessibility, state, + ); + const boxBoxP = new ModalFormulaImpl( + undefined, '□', boxP, + chainFrame!.worlds, chainFrame!.accessibility, state, + ); + const fourAxiom = new ModalComplexImpl(undefined, boxP, '->', boxBoxP); + + // Countermodel: p true at w1, p false at w2 + // □p at w0: accessible is {w1}, p@w1=true → true + // □□p at w0: accessible is {w1}, need □p at w1 + // □p at w1: accessible is {w2}, p@w2=false → false + // So □p → □□p is false at w0 + state.valuation.set('p', new Set(['w1'])); + state.currentWorld = 'w0'; + expect(fourAxiom.value()).toBe(false); + }); + + test('◇p → □◇p is NOT valid on all K-frames (requires Euclidean = system 5)', () => { + // Frame: w0→w1, w0→w2 (non-Euclidean: w1 does not access w2) + const frame = FRAMES.find(f => f.label === 'three worlds, w0→w1, w0→w2'); + expect(frame).toBeDefined(); + + const state = makeState('w0', {}); + const p = new ModalAtomImpl(undefined, 'p', state); + const diaP = new ModalFormulaImpl( + undefined, '◇', p, + frame!.worlds, frame!.accessibility, state, + ); + const boxDiaP = new ModalFormulaImpl( + undefined, '□', diaP, + frame!.worlds, frame!.accessibility, state, + ); + const fiveAxiom = new ModalComplexImpl(undefined, diaP, '->', boxDiaP); + + // Countermodel: p true at w1 only + // ◇p at w0: accessible {w1, w2}, p@w1=true → true + // □◇p at w0: need ◇p at w1 AND ◇p at w2 + // ◇p at w1: accessible from w1 = {} (no worlds) → false + // So ◇p → □◇p is false + state.valuation.set('p', new Set(['w1'])); + state.currentWorld = 'w0'; + expect(fiveAxiom.value()).toBe(false); + }); + }); + + describe('Part II — Completeness: exhaustive evaluation is a decision procedure', () => { + + test('A valid modal formula is confirmed valid', () => { + // □(p | ~p) — necessitated excluded middle + const state = makeState('w0', {}); + const worlds: World[] = ['w0', 'w1']; + const R = (f: World, t: World) => f === 'w0' && t === 'w1'; + + const p = new ModalAtomImpl(undefined, 'p', state); + const notP = new ModalAtomImpl('~', 'p', state); + const lem = new ModalComplexImpl(undefined, p, '|', notP); + const boxLem = new ModalFormulaImpl(undefined, '□', lem, worlds, R, state); + + const frame: TestFrame = { worlds, accessibility: R, label: '' }; + expect(isValidOnFrame(boxLem, frame, ['p'], state, 'w0')).toBe(true); + }); + + test('A satisfiable but non-valid formula produces mixed results', () => { + // □p — not valid (depends on valuation), but satisfiable + const state = makeState('w0', {}); + const worlds: World[] = ['w0', 'w1']; + const R = (f: World, t: World) => f === 'w0' && t === 'w1'; + + const p = new ModalAtomImpl(undefined, 'p', state); + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + + // True when p is true at w1 + state.valuation.set('p', new Set(['w1'])); + state.currentWorld = 'w0'; + expect(boxP.value()).toBe(true); + + // False when p is false at w1 + state.valuation.set('p', new Set(['w0'])); + state.currentWorld = 'w0'; + expect(boxP.value()).toBe(false); + }); + + test('An unsatisfiable modal formula is refuted', () => { + // □p & ◇~p on a frame where w0 accesses only w1 + // This means p must be true at w1 (□p) AND false at w1 (◇~p) + const state = makeState('w0', {}); + const worlds: World[] = ['w0', 'w1']; + const R = (f: World, t: World) => f === 'w0' && t === 'w1'; + + const p = new ModalAtomImpl(undefined, 'p', state); + const notP = new ModalAtomImpl('~', 'p', state); + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + const diaNegP = new ModalFormulaImpl(undefined, '◇', notP, worlds, R, state); + const conj = new ModalComplexImpl(undefined, boxP, '&', diaNegP); + + const frame: TestFrame = { worlds, accessibility: R, label: '' }; + expect(isValidOnFrame(conj, frame, ['p'], state, 'w0')).toBe(false); + }); + }); +}); diff --git a/test/language/modal/modalAtom.spec.ts b/test/language/modal/modalAtom.spec.ts new file mode 100644 index 0000000..0bb2e92 --- /dev/null +++ b/test/language/modal/modalAtom.spec.ts @@ -0,0 +1,127 @@ +import { ModalAtomImpl } from '../../../src/language/modal/modalAtom'; +import { ModalEvaluationState, World } from '../../../src/language/modal/modalTypes'; + +// ─── Helpers ──────────────────────────────────────────────────────────────── + +function makeState(currentWorld: World, valuation: Record): ModalEvaluationState { + const map = new Map>(); + for (const [prop, worlds] of Object.entries(valuation)) { + map.set(prop, new Set(worlds)); + } + return { currentWorld, valuation: map }; +} + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalAtomImpl', () => { + + describe('evaluation at current world', () => { + + test('p is true when current world is in the extension of p', () => { + const state = makeState('w0', { p: ['w0', 'w1'] }); + const atom = new ModalAtomImpl(undefined, 'p', state); + expect(atom.value()).toBe(true); + }); + + test('p is false when current world is not in the extension of p', () => { + const state = makeState('w2', { p: ['w0', 'w1'] }); + const atom = new ModalAtomImpl(undefined, 'p', state); + expect(atom.value()).toBe(false); + }); + + test('p is false when proposition has no extension entry', () => { + const state = makeState('w0', {}); + const atom = new ModalAtomImpl(undefined, 'p', state); + expect(atom.value()).toBe(false); + }); + + test('p is false when extension is empty', () => { + const state = makeState('w0', { p: [] }); + const atom = new ModalAtomImpl(undefined, 'p', state); + expect(atom.value()).toBe(false); + }); + }); + + describe('world-relative truth', () => { + + test('same atom gives different values at different worlds', () => { + const state = makeState('w0', { p: ['w0'] }); + const atom = new ModalAtomImpl(undefined, 'p', state); + + expect(atom.value()).toBe(true); + + state.currentWorld = 'w1'; + expect(atom.value()).toBe(false); + }); + + test('different propositions can have different extensions', () => { + const state = makeState('w0', { p: ['w0'], q: ['w1'] }); + const atomP = new ModalAtomImpl(undefined, 'p', state); + const atomQ = new ModalAtomImpl(undefined, 'q', state); + + expect(atomP.value()).toBe(true); + expect(atomQ.value()).toBe(false); + }); + }); + + describe('negation', () => { + + test('~p negates the truth value', () => { + const state = makeState('w0', { p: ['w0'] }); + const atom = new ModalAtomImpl('~', 'p', state); + expect(atom.value()).toBe(false); + }); + + test('~p is true when p is false at current world', () => { + const state = makeState('w1', { p: ['w0'] }); + const atom = new ModalAtomImpl('~', 'p', state); + expect(atom.value()).toBe(true); + }); + + test('undefined unary operator leaves value unchanged', () => { + const state = makeState('w0', { p: ['w0'] }); + const pos = new ModalAtomImpl(undefined, 'p', state); + const neg = new ModalAtomImpl('~', 'p', state); + expect(pos.value()).toBe(!neg.value()); + }); + }); + + describe('mutable state sharing', () => { + + test('updating valuation changes atom truth value', () => { + const state = makeState('w0', { p: [] }); + const atom = new ModalAtomImpl(undefined, 'p', state); + + expect(atom.value()).toBe(false); + + state.valuation.set('p', new Set(['w0'])); + expect(atom.value()).toBe(true); + }); + + test('multiple atoms share the same state', () => { + const state = makeState('w0', { p: ['w0', 'w1'] }); + const atom1 = new ModalAtomImpl(undefined, 'p', state); + const atom2 = new ModalAtomImpl(undefined, 'p', state); + + expect(atom1.value()).toBe(atom2.value()); + + state.currentWorld = 'w2'; + expect(atom1.value()).toBe(atom2.value()); + }); + }); + + describe('exhaustive truth table over worlds', () => { + + test('p produces correct truth value for each world', () => { + const worlds: World[] = ['w0', 'w1', 'w2']; + const state = makeState('w0', { p: ['w0', 'w2'] }); + const atom = new ModalAtomImpl(undefined, 'p', state); + const expected = [true, false, true]; + + worlds.forEach((w, i) => { + state.currentWorld = w; + expect(atom.value()).toBe(expected[i]); + }); + }); + }); +}); diff --git a/test/language/modal/modalComplex.spec.ts b/test/language/modal/modalComplex.spec.ts new file mode 100644 index 0000000..a049970 --- /dev/null +++ b/test/language/modal/modalComplex.spec.ts @@ -0,0 +1,87 @@ +import { ModalAtomImpl } from '../../../src/language/modal/modalAtom'; +import { ModalComplexImpl } from '../../../src/language/modal/modalComplex'; +import { ModalEvaluationState, BinaryOperator, World } from '../../../src/language/modal/modalTypes'; +import { binaryOperatorToLogic } from '../../../src/language/modal/modalUtils'; + +// ─── Helpers ──────────────────────────────────────────────────────────────── + +function makeState(currentWorld: World, valuation: Record): ModalEvaluationState { + const map = new Map>(); + for (const [prop, worlds] of Object.entries(valuation)) { + map.set(prop, new Set(worlds)); + } + return { currentWorld, valuation: map }; +} + +function fixedAtom(state: ModalEvaluationState, val: boolean): ModalAtomImpl { + // Use a unique prop name with pre-set extension + const name = `_fixed_${val}`; + if (val) { + state.valuation.set(name, new Set([state.currentWorld])); + } else { + state.valuation.set(name, new Set()); + } + return new ModalAtomImpl(undefined, name, state); +} + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalComplexImpl', () => { + + describe('all rows of each binary operator truth table', () => { + + const operators: BinaryOperator[] = ['&', '|', '->', '<->']; + const boolPairs: [boolean, boolean][] = [[false,false],[false,true],[true,false],[true,true]]; + + operators.forEach(op => { + boolPairs.forEach(([L, R]) => { + const expected = binaryOperatorToLogic[op](L, R); + + test(`(${L} ${op} ${R}) = ${expected}`, () => { + const state = makeState('w0', {}); + const left = fixedAtom(state, L); + const right = fixedAtom(state, R); + expect(new ModalComplexImpl(undefined, left, op, right).value()).toBe(expected); + }); + + test(`~(${L} ${op} ${R}) = ${!expected}`, () => { + const state = makeState('w0', {}); + const left = fixedAtom(state, L); + const right = fixedAtom(state, R); + expect(new ModalComplexImpl('~', left, op, right).value()).toBe(!expected); + }); + }); + }); + }); + + describe('world-relative evaluation', () => { + + test('p & q evaluates relative to current world', () => { + // p true at w0, q true at w0 + const state = makeState('w0', { p: ['w0'], q: ['w0', 'w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const q = new ModalAtomImpl(undefined, 'q', state); + const conj = new ModalComplexImpl(undefined, p, '&', q); + + expect(conj.value()).toBe(true); + + // Move to w1: p false, q true + state.currentWorld = 'w1'; + expect(conj.value()).toBe(false); + }); + + test('p -> q evaluates correctly across worlds', () => { + const state = makeState('w0', { p: ['w0', 'w1'], q: ['w0'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const q = new ModalAtomImpl(undefined, 'q', state); + const impl = new ModalComplexImpl(undefined, p, '->', q); + + // w0: p=true, q=true → true + expect(impl.value()).toBe(true); + + // w1: p=true, q=false → false + state.currentWorld = 'w1'; + expect(impl.value()).toBe(false); + }); + }); +}); diff --git a/test/language/modal/modalFormula.spec.ts b/test/language/modal/modalFormula.spec.ts new file mode 100644 index 0000000..1e11587 --- /dev/null +++ b/test/language/modal/modalFormula.spec.ts @@ -0,0 +1,213 @@ +import { ModalAtomImpl } from '../../../src/language/modal/modalAtom'; +import { ModalComplexImpl } from '../../../src/language/modal/modalComplex'; +import { ModalFormulaImpl } from '../../../src/language/modal/modalFormula'; +import { ModalEvaluationState, World } from '../../../src/language/modal/modalTypes'; + +// ─── Helpers ──────────────────────────────────────────────────────────────── + +function makeState(currentWorld: World, valuation: Record): ModalEvaluationState { + const map = new Map>(); + for (const [prop, worlds] of Object.entries(valuation)) { + map.set(prop, new Set(worlds)); + } + return { currentWorld, valuation: map }; +} + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalFormulaImpl — □ (necessity)', () => { + + test('□p is true when p is true at all accessible worlds', () => { + const state = makeState('w0', { p: ['w0', 'w1', 'w2'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1', 'w2']; + // w0 can see w1 and w2 + const R = (from: World, to: World) => from === 'w0' && (to === 'w1' || to === 'w2'); + + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + expect(boxP.value()).toBe(true); + }); + + test('□p is false when p is false at some accessible world', () => { + const state = makeState('w0', { p: ['w0', 'w1'] }); // p false at w2 + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => from === 'w0' && (to === 'w1' || to === 'w2'); + + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + expect(boxP.value()).toBe(false); + }); + + test('□p is vacuously true when no worlds are accessible', () => { + const state = makeState('w0', { p: [] }); // p false everywhere + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1']; + const R = () => false; // no accessibility + + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + expect(boxP.value()).toBe(true); + }); + + test('□p restores current world after evaluation', () => { + const state = makeState('w0', { p: ['w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1']; + const R = (from: World, to: World) => from === 'w0' && to === 'w1'; + + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + boxP.value(); + expect(state.currentWorld).toBe('w0'); + }); +}); + +describe('ModalFormulaImpl — ◇ (possibility)', () => { + + test('◇p is true when p is true at some accessible world', () => { + const state = makeState('w0', { p: ['w2'] }); // p only true at w2 + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => from === 'w0' && (to === 'w1' || to === 'w2'); + + const diaP = new ModalFormulaImpl(undefined, '◇', p, worlds, R, state); + expect(diaP.value()).toBe(true); + }); + + test('◇p is false when p is false at all accessible worlds', () => { + const state = makeState('w0', { p: ['w0'] }); // p only true at w0 (not accessible from w0) + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => from === 'w0' && (to === 'w1' || to === 'w2'); + + const diaP = new ModalFormulaImpl(undefined, '◇', p, worlds, R, state); + expect(diaP.value()).toBe(false); + }); + + test('◇p is false when no worlds are accessible', () => { + const state = makeState('w0', { p: ['w0', 'w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1']; + const R = () => false; + + const diaP = new ModalFormulaImpl(undefined, '◇', p, worlds, R, state); + expect(diaP.value()).toBe(false); + }); + + test('◇p restores current world after evaluation', () => { + const state = makeState('w0', { p: ['w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1']; + const R = (from: World, to: World) => from === 'w0' && to === 'w1'; + + const diaP = new ModalFormulaImpl(undefined, '◇', p, worlds, R, state); + diaP.value(); + expect(state.currentWorld).toBe('w0'); + }); +}); + +describe('ModalFormulaImpl — negation', () => { + + test('~□p negates the box result', () => { + const state = makeState('w0', { p: ['w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1']; + const R = (from: World, to: World) => from === 'w0' && to === 'w1'; + + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + const negBoxP = new ModalFormulaImpl('~', '□', p, worlds, R, state); + expect(negBoxP.value()).toBe(!boxP.value()); + }); + + test('~◇p negates the diamond result', () => { + const state = makeState('w0', { p: ['w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1']; + const R = (from: World, to: World) => from === 'w0' && to === 'w1'; + + const diaP = new ModalFormulaImpl(undefined, '◇', p, worlds, R, state); + const negDiaP = new ModalFormulaImpl('~', '◇', p, worlds, R, state); + expect(negDiaP.value()).toBe(!diaP.value()); + }); +}); + +describe('ModalFormulaImpl — nested modalities', () => { + + test('□□p evaluates over two levels of accessibility', () => { + // w0 → w1 → w2, p true everywhere + const state = makeState('w0', { p: ['w0', 'w1', 'w2'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => + (from === 'w0' && to === 'w1') || (from === 'w1' && to === 'w2'); + + const innerBox = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + const outerBox = new ModalFormulaImpl(undefined, '□', innerBox, worlds, R, state); + + // □□p at w0: accessible from w0 is {w1}, at w1 accessible is {w2}, p@w2=true → true + expect(outerBox.value()).toBe(true); + }); + + test('□□p fails when inner world lacks p', () => { + // w0 → w1 → w2, p false at w2 + const state = makeState('w0', { p: ['w0', 'w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => + (from === 'w0' && to === 'w1') || (from === 'w1' && to === 'w2'); + + const innerBox = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + const outerBox = new ModalFormulaImpl(undefined, '□', innerBox, worlds, R, state); + + // □□p at w0: need □p at w1, which needs p at w2 — p false at w2 → false + expect(outerBox.value()).toBe(false); + }); + + test('◇□p: possibly necessarily p', () => { + // w0 → w1, w0 → w2; from w1 accessible: w1 (reflexive); from w2 accessible: w2 + // p true at w1, false at w2 + const state = makeState('w0', { p: ['w1'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => + (from === 'w0' && (to === 'w1' || to === 'w2')) || + (from === 'w1' && to === 'w1') || + (from === 'w2' && to === 'w2'); + + const boxP = new ModalFormulaImpl(undefined, '□', p, worlds, R, state); + const diaBoxP = new ModalFormulaImpl(undefined, '◇', boxP, worlds, R, state); + + // ◇□p at w0: need □p at w1 or □p at w2 + // □p at w1: accessible from w1 is {w1}, p@w1=true → true + // So ◇□p is true + expect(diaBoxP.value()).toBe(true); + }); +}); + +describe('ModalFormulaImpl — complex body', () => { + + test('□(p -> q) evaluates the implication at each accessible world', () => { + // p -> q should be true at all accessible worlds + const state = makeState('w0', { p: ['w1'], q: ['w1', 'w2'] }); + const p = new ModalAtomImpl(undefined, 'p', state); + const q = new ModalAtomImpl(undefined, 'q', state); + const impl = new ModalComplexImpl(undefined, p, '->', q); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => from === 'w0' && (to === 'w1' || to === 'w2'); + + const boxImpl = new ModalFormulaImpl(undefined, '□', impl, worlds, R, state); + // w1: p=true, q=true → true; w2: p=false, q=true → true + expect(boxImpl.value()).toBe(true); + }); + + test('□(p & q) requires both at every accessible world', () => { + const state = makeState('w0', { p: ['w1', 'w2'], q: ['w1'] }); // q false at w2 + const p = new ModalAtomImpl(undefined, 'p', state); + const q = new ModalAtomImpl(undefined, 'q', state); + const conj = new ModalComplexImpl(undefined, p, '&', q); + const worlds: World[] = ['w0', 'w1', 'w2']; + const R = (from: World, to: World) => from === 'w0' && (to === 'w1' || to === 'w2'); + + const boxConj = new ModalFormulaImpl(undefined, '□', conj, worlds, R, state); + // w1: p&q = true; w2: p&q = false → false + expect(boxConj.value()).toBe(false); + }); +}); diff --git a/test/language/modal/modalTheory.spec.ts b/test/language/modal/modalTheory.spec.ts new file mode 100644 index 0000000..6741860 --- /dev/null +++ b/test/language/modal/modalTheory.spec.ts @@ -0,0 +1,529 @@ +import { ModalTheoryBuilder } from '../../../src/language/modal/modalTheoryBuilder'; +import { ModalComplexImpl } from '../../../src/language/modal/modalComplex'; +import { ModalFormulaImpl } from '../../../src/language/modal/modalFormula'; +import { SystemK, SystemT, SystemD, SystemS4, SystemS5 } from '../../../src/language/modal/modalSystems'; +import { AlethicAssertoric } from '../../../src/language/shared/types'; +import { World } from '../../../src/language/modal/modalTypes'; + +// ─── Helpers ──────────────────────────────────────────────────────────────── + +function sentence(raw: string): AlethicAssertoric { + return { raw, confidence: 1.0 }; +} + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalTheoryBuilder', () => { + + test('proposition() returns the same instance for the same name', () => { + const builder = new ModalTheoryBuilder(); + const p1 = builder.proposition('p'); + const p2 = builder.proposition('p'); + expect(p1).toBe(p2); + }); + + test('proposition() returns distinct instances for different names', () => { + const builder = new ModalTheoryBuilder(); + const p = builder.proposition('p'); + const q = builder.proposition('q'); + expect(p).not.toBe(q); + }); + + test('worlds() sets the worlds and is fluent', () => { + const builder = new ModalTheoryBuilder(); + const result = builder.worlds('w0', 'w1', 'w2'); + expect(result).toBe(builder); + expect(builder.currentWorlds).toEqual(['w0', 'w1', 'w2']); + }); + + test('accessibility() is fluent', () => { + const builder = new ModalTheoryBuilder(); + const result = builder.accessibility(() => true); + expect(result).toBe(builder); + }); + + test('designatedWorld() is fluent', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0'); + const result = builder.designatedWorld('w0'); + expect(result).toBe(builder); + }); + + test('sentence() is fluent (returns this)', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + const result = builder.sentence(sentence('p'), p.atom(), ['p']); + expect(result).toBe(builder); + }); + + test('build() returns a theory with the added sentences', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder.sentence(sentence('p is true'), p.atom(), ['p']); + const theory = builder.build(); + expect(theory.sentences).toHaveLength(1); + expect(theory.sentences[0].source.raw).toBe('p is true'); + }); + + test('auto-labels sentences φ1, φ2, …', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder + .sentence(sentence('p'), p.atom(), ['p']) + .sentence(sentence('~p'), p.atom(true), ['p']); + 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 ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder.sentence(sentence('p'), p.atom(), ['p'], 'S1'); + const theory = builder.build(); + expect(theory.sentences[0].label).toBe('S1'); + }); + + test('fromSentenceSet() throws (not yet implemented)', () => { + const builder = new ModalTheoryBuilder(); + expect(() => builder.fromSentenceSet({ sentences: [] })).toThrow(); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalTheory — checkConsistency()', () => { + + test('single proposition p at a single world — consistent', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder.sentence(sentence('p is true'), p.atom(), ['p']); + + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + expect(result.witness!['p@w0']).toBe(true); + }); + + test('p & ~p at same world — inconsistent', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder + .sentence(sentence('p'), p.atom(), ['p']) + .sentence(sentence('~p'), p.atom(true), ['p']); + + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(false); + }); + + test('□p requires p at all accessible worlds — consistent when met', () => { + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1', 'w2') + .accessibility((from: World, to: World) => from === 'w0' && (to === 'w1' || to === 'w2')) + .designatedWorld('w0'); + + const p = builder.proposition('p'); + const boxP = new ModalFormulaImpl( + undefined, '□', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + + builder.sentence(sentence('Necessarily p'), boxP, ['p']); + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + // Witness must have p true at w1 and w2 + expect(result.witness!['p@w1']).toBe(true); + expect(result.witness!['p@w2']).toBe(true); + }); + + test('□p & ◇~p — inconsistent (on same accessibility)', () => { + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1') + .accessibility((from: World, to: World) => from === 'w0' && to === 'w1') + .designatedWorld('w0'); + + const p = builder.proposition('p'); + const boxP = new ModalFormulaImpl( + undefined, '□', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + const diaNegP = new ModalFormulaImpl( + undefined, '◇', p.atom(true), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + + builder + .sentence(sentence('Necessarily p'), boxP, ['p']) + .sentence(sentence('Possibly not p'), diaNegP, ['p']); + + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(false); + }); + + test('◇p is consistent when there exists an accessible world where p can be true', () => { + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1') + .accessibility((from: World, to: World) => from === 'w0' && to === 'w1') + .designatedWorld('w0'); + + const p = builder.proposition('p'); + const diaP = new ModalFormulaImpl( + undefined, '◇', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + + builder.sentence(sentence('Possibly p'), diaP, ['p']); + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + }); + + test('□p does not entail p in system K (no reflexivity)', () => { + // □p & ~p should be consistent in K because w0 might not access itself + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1') + .accessibility((from: World, to: World) => from === 'w0' && to === 'w1') // w0 does NOT access w0 + .designatedWorld('w0'); + + const p = builder.proposition('p'); + const boxP = new ModalFormulaImpl( + undefined, '□', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + + builder + .sentence(sentence('Necessarily p'), boxP, ['p']) + .sentence(sentence('Not p'), p.atom(true), ['p']); + + const result = builder.build().checkConsistency(); + // In K, □p & ~p is satisfiable: p false at w0, p true at w1 + expect(result.isConsistent).toBe(true); + }); + + test('theory with no propositions and no sentences — consistent (vacuously)', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + }); + + test('multi-proposition modal theory', () => { + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1') + .accessibility((from: World, to: World) => from === 'w0' && to === 'w1') + .designatedWorld('w0'); + + const p = builder.proposition('p'); + const q = builder.proposition('q'); + + // □(p -> q): necessarily, if p then q + const impl = new ModalComplexImpl(undefined, p.atom(), '->', q.atom()); + const boxImpl = new ModalFormulaImpl( + undefined, '□', impl, + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + + // ◇p: possibly p + const diaP = new ModalFormulaImpl( + undefined, '◇', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + + // ◇q: possibly q + const diaQ = new ModalFormulaImpl( + undefined, '◇', q.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + + builder + .sentence(sentence('Necessarily if p then q'), boxImpl, ['p', 'q']) + .sentence(sentence('Possibly p'), diaP, ['p']) + .sentence(sentence('Possibly q'), diaQ, ['q']); + + const result = builder.build().checkConsistency(); + expect(result.isConsistent).toBe(true); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalTheory — buildProofTree()', () => { + + test('consistent theory root is labelled CONSISTENT ✓', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder.sentence(sentence('p'), p.atom(), ['p']); + const tree = builder.build().buildProofTree(); + expect(tree.label).toBe('CONSISTENT ✓'); + }); + + test('inconsistent theory root is labelled INCONSISTENT ✗', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder + .sentence(sentence('p'), p.atom(), ['p']) + .sentence(sentence('~p'), p.atom(true), ['p']); + const tree = builder.build().buildProofTree(); + expect(tree.label).toBe('INCONSISTENT ✗'); + }); + + test('proof tree includes Kripke frame node', () => { + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1') + .accessibility((from: World, to: World) => from === 'w0' && to === 'w1') + .designatedWorld('w0'); + const p = builder.proposition('p'); + builder.sentence(sentence('p'), p.atom(), ['p']); + + const tree = builder.build().buildProofTree(); + const frameNode = tree.children.find(c => c.label === 'Kripke frame:'); + expect(frameNode).toBeDefined(); + expect(frameNode!.children).toHaveLength(3); // Worlds, Accessibility, Designated world + }); + + test('consistent tree has a per-world valuation node', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder.sentence(sentence('p'), p.atom(), ['p']); + + const tree = builder.build().buildProofTree(); + const worldValuation = tree.children.find(c => c.label === 'Per-world valuation:'); + expect(worldValuation).toBeDefined(); + }); + + test('consistent tree has a verification node', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder.sentence(sentence('p'), p.atom(), ['p']); + + const tree = builder.build().buildProofTree(); + const verification = tree.children.find(c => c.label === 'Verification (at designated world):'); + expect(verification).toBeDefined(); + expect(verification!.children).toHaveLength(1); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalTheory — printProof() and printGraph()', () => { + + test('printProof() does not throw for consistent theory', () => { + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1') + .accessibility((from: World, to: World) => from === 'w0' && to === 'w1') + .designatedWorld('w0'); + const p = builder.proposition('p'); + const boxP = new ModalFormulaImpl( + undefined, '□', p.atom(), + builder.currentWorlds, builder.currentAccessibility, builder.state, + ); + builder.sentence(sentence('Necessarily p'), boxP, ['p']); + expect(() => builder.build().printProof()).not.toThrow(); + }); + + test('printProof() does not throw for inconsistent theory', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + const p = builder.proposition('p'); + builder + .sentence(sentence('p'), p.atom(), ['p']) + .sentence(sentence('~p'), p.atom(true), ['p']); + expect(() => builder.build().printProof()).not.toThrow(); + }); + + test('printGraph() does not throw', () => { + const builder = new ModalTheoryBuilder(); + builder + .worlds('w0', 'w1') + .accessibility((from: World, to: World) => from === 'w0' && to === 'w1') + .designatedWorld('w0'); + const p = builder.proposition('p'); + const q = builder.proposition('q'); + builder + .sentence(sentence('p'), p.atom(), ['p']) + .sentence(sentence('q'), q.atom(), ['q']); + expect(() => builder.build().printGraph()).not.toThrow(); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalTheory — system field', () => { + + test('theory built without .system() defaults to K', () => { + const builder = new ModalTheoryBuilder(); + builder.worlds('w0').designatedWorld('w0'); + expect(builder.build().system.name).toBe('K'); + }); + + test('.system(SystemK) produces a theory with system.name === "K"', () => { + const builder = new ModalTheoryBuilder(); + builder.system(SystemK).worlds('w0').designatedWorld('w0'); + expect(builder.build().system.name).toBe('K'); + }); + + test('.system(SystemT) produces a theory with system.name === "T"', () => { + const builder = new ModalTheoryBuilder(); + builder + .system(SystemT) + .worlds('w0') + .accessibility((f: World, t: World) => f === t) // reflexive + .designatedWorld('w0'); + expect(builder.build().system.name).toBe('T'); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('ModalTheoryBuilder — frame validation on build()', () => { + + describe('SystemK — accepts any frame', () => { + + test('accepts a frame with no accessibility', () => { + const builder = new ModalTheoryBuilder(); + builder.system(SystemK).worlds('w0', 'w1').accessibility(() => false).designatedWorld('w0'); + expect(() => builder.build()).not.toThrow(); + }); + + test('accepts a non-reflexive frame', () => { + const builder = new ModalTheoryBuilder(); + builder.system(SystemK).worlds('w0').accessibility(() => false).designatedWorld('w0'); + expect(() => builder.build()).not.toThrow(); + }); + }); + + describe('SystemT — requires reflexivity', () => { + + test('accepts a reflexive frame', () => { + const builder = new ModalTheoryBuilder(); + builder + .system(SystemT) + .worlds('w0', 'w1') + .accessibility((f: World, t: World) => f === t) + .designatedWorld('w0'); + expect(() => builder.build()).not.toThrow(); + }); + + test('rejects a non-reflexive frame', () => { + const builder = new ModalTheoryBuilder(); + builder + .system(SystemT) + .worlds('w0', 'w1') + .accessibility((f: World, t: World) => f === 'w0' && t === 'w1') // w0→w1 only, no self-loops + .designatedWorld('w0'); + expect(() => builder.build()).toThrow(/System T/); + }); + + test('error message names the violating world', () => { + const builder = new ModalTheoryBuilder(); + builder + .system(SystemT) + .worlds('w0', 'w1') + .accessibility((f: World, t: World) => f === 'w0' && t === 'w0') // w1 has no self-loop + .designatedWorld('w0'); + expect(() => builder.build()).toThrow(/w1/); + }); + }); + + describe('SystemD — requires seriality', () => { + + test('accepts a serial frame', () => { + const builder = new ModalTheoryBuilder(); + // w0→w1, w1→w0: every world has at least one successor + builder + .system(SystemD) + .worlds('w0', 'w1') + .accessibility((f: World, t: World) => + (f === 'w0' && t === 'w1') || (f === 'w1' && t === 'w0'), + ) + .designatedWorld('w0'); + expect(() => builder.build()).not.toThrow(); + }); + + test('rejects a frame with a dead-end world', () => { + const builder = new ModalTheoryBuilder(); + builder + .system(SystemD) + .worlds('w0', 'w1') + .accessibility(() => false) // no world accesses anything + .designatedWorld('w0'); + expect(() => builder.build()).toThrow(/System D/); + }); + }); + + describe('SystemS4 — requires reflexivity + transitivity', () => { + + test('accepts a reflexive and transitive frame', () => { + const builder = new ModalTheoryBuilder(); + // All worlds see all worlds (complete = reflexive + transitive + symmetric) + builder + .system(SystemS4) + .worlds('w0', 'w1', 'w2') + .accessibility(() => true) + .designatedWorld('w0'); + expect(() => builder.build()).not.toThrow(); + }); + + test('rejects a non-reflexive frame', () => { + const builder = new ModalTheoryBuilder(); + builder + .system(SystemS4) + .worlds('w0', 'w1') + .accessibility((f: World, t: World) => f === 'w0' && t === 'w1') + .designatedWorld('w0'); + expect(() => builder.build()).toThrow(/System T/); // S4 delegates reflexivity check to T + }); + + test('rejects a reflexive but non-transitive frame', () => { + const builder = new ModalTheoryBuilder(); + // w0→w0, w1→w1, w2→w2, w0→w1, w1→w2 but NOT w0→w2 + builder + .system(SystemS4) + .worlds('w0', 'w1', 'w2') + .accessibility((f: World, t: World) => + f === t || (f === 'w0' && t === 'w1') || (f === 'w1' && t === 'w2'), + ) + .designatedWorld('w0'); + expect(() => builder.build()).toThrow(/System S4/); + }); + }); + + describe('SystemS5 — requires reflexivity + transitivity + symmetry', () => { + + test('accepts an equivalence-relation frame', () => { + const builder = new ModalTheoryBuilder(); + builder + .system(SystemS5) + .worlds('w0', 'w1') + .accessibility(() => true) // fully connected = equivalence relation + .designatedWorld('w0'); + expect(() => builder.build()).not.toThrow(); + }); + + test('rejects a reflexive+transitive but asymmetric frame', () => { + const builder = new ModalTheoryBuilder(); + // w0→w0, w1→w1, w0→w1, but NOT w1→w0 + builder + .system(SystemS5) + .worlds('w0', 'w1') + .accessibility((f: World, t: World) => f === t || (f === 'w0' && t === 'w1')) + .designatedWorld('w0'); + expect(() => builder.build()).toThrow(/System S5/); + }); + }); +});