import { ModalArgument, ModalFormula, ModalSystem, SolutionStep } from '../types.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.modal;
/**
* Modal Proof Generator using Natural Deduction
* Implements proof construction for modal logic systems K, T, D, B, K4, KB, S4, S5, KD45
*/
export class ModalProofGenerator {
/**
* Generate a natural deduction proof for a modal argument
*/
generateProof(argument: ModalArgument, isValid: boolean): SolutionStep[] {
if (!isValid) {
return [{
index: 1,
statement: 'Argument is invalid - no proof exists',
rule: 'Invalid',
justification: 'Countermodel exists (use validate to see it)'
}];
}
const steps: SolutionStep[] = [];
let stepIndex = 1;
// Add premises
argument.premises.forEach((premise, idx) => {
steps.push({
index: stepIndex++,
statement: this.formatFormula(premise),
rule: 'Premise',
justification: `Premise ${idx + 1}`
});
});
// Add system-specific axioms
steps.push(...this.addSystemAxioms(argument.system, stepIndex));
stepIndex += steps.length - argument.premises.length;
// Try to derive conclusion using modal rules
const derivationSteps = this.deriveConclusion(argument, stepIndex);
steps.push(...derivationSteps);
return steps;
}
/**
* Add axioms specific to the modal system
*/
private addSystemAxioms(system: ModalSystem, startIndex: number): SolutionStep[] {
const steps: SolutionStep[] = [];
let index = startIndex;
// K axiom (all systems)
steps.push({
index: index++,
statement: '□(P → Q) → (□P → □Q)',
rule: 'K Axiom',
justification: 'Distribution of necessity over implication (valid in all systems)'
});
// Necessitation rule (all systems)
steps.push({
index: index++,
statement: 'Necessitation: If ⊢ φ then ⊢ □φ',
rule: 'Necessitation',
justification: 'If φ is a theorem, then □φ is a theorem'
});
// Duality
steps.push({
index: index++,
statement: '◇φ ≡ ¬□¬φ',
rule: 'Duality',
justification: 'Possibility defined in terms of necessity'
});
// System-specific axioms
switch (system) {
case 'T':
case 'B':
case 'S4':
case 'S5':
case 'KD45':
steps.push({
index: index++,
statement: '□P → P',
rule: 'T Axiom',
justification: 'Reflexivity: what is necessary is actual'
});
break;
}
switch (system) {
case 'D':
case 'KD45':
steps.push({
index: index++,
statement: '□P → ◇P',
rule: 'D Axiom',
justification: 'Seriality: necessity implies possibility'
});
break;
}
switch (system) {
case 'B':
case 'KB':
steps.push({
index: index++,
statement: 'P → □◇P',
rule: 'B Axiom',
justification: 'Symmetry: what is actual is necessarily possible'
});
break;
}
switch (system) {
case 'K4':
case 'S4':
case 'S5':
case 'KD45':
steps.push({
index: index++,
statement: '□P → □□P',
rule: '4 Axiom',
justification: 'Transitivity: necessity iterates'
});
break;
}
switch (system) {
case 'S5':
case 'KD45':
steps.push({
index: index++,
statement: '◇P → □◇P',
rule: '5 Axiom',
justification: 'Euclidean property: possibility is necessary'
});
break;
}
return steps;
}
/**
* Attempt to derive the conclusion from premises
*/
private deriveConclusion(argument: ModalArgument, startIndex: number): SolutionStep[] {
const steps: SolutionStep[] = [];
let index = startIndex;
// Simple heuristic-based derivation
// In a full implementation, this would use tableau or sequent calculus
const conclusion = argument.conclusion;
// Check for simple modus ponens cases
if (this.isModalOperator(conclusion, '□')) {
// Try to apply necessitation
const inner = this.getModalOperand(conclusion);
if (inner && this.isPremiseOrTheorem(inner, argument.premises)) {
steps.push({
index: index++,
statement: this.formatFormula(inner),
rule: 'Previous Steps',
justification: 'Derived or assumed'
});
steps.push({
index: index++,
statement: this.formatFormula(conclusion),
rule: 'Necessitation',
justification: `Apply necessitation to step ${index - 1}`
});
return steps;
}
}
// Check for K axiom application
const kApplication = this.tryKAxiom(argument, index);
if (kApplication.length > 0) {
return kApplication;
}
// Check for system-specific rules
const systemDerivation = this.trySystemSpecificRules(argument, index);
if (systemDerivation.length > 0) {
return systemDerivation;
}
// Default: state that conclusion follows
steps.push({
index: index++,
statement: this.formatFormula(conclusion),
rule: 'Modal Rules',
justification: `Conclusion follows from premises and ${argument.system} axioms`
});
return steps;
}
/**
* Try to apply K axiom: □(P → Q) → (□P → □Q)
*/
private tryKAxiom(argument: ModalArgument, startIndex: number): SolutionStep[] {
const steps: SolutionStep[] = [];
let index = startIndex;
// Look for premises of the form □(P → Q) and □P
for (let i = 0; i < argument.premises.length; i++) {
const p1 = argument.premises[i];
if (!this.isModalOperator(p1, '□')) continue;
const inner1 = this.getModalOperand(p1);
if (!inner1 || !this.isImplication(inner1)) continue;
// Found □(P → Q), now look for □P
for (let j = 0; j < argument.premises.length; j++) {
if (i === j) continue;
const p2 = argument.premises[j];
if (!this.isModalOperator(p2, '□')) continue;
// Check if we can apply K axiom
steps.push({
index: index++,
statement: `Apply K axiom to premises ${i + 1} and ${j + 1}`,
rule: 'K Axiom',
justification: '□(P → Q) and □P give us □Q'
});
steps.push({
index: index++,
statement: this.formatFormula(argument.conclusion),
rule: 'Modus Ponens',
justification: 'Derived from K axiom application'
});
return steps;
}
}
return [];
}
/**
* Try system-specific rules
*/
private trySystemSpecificRules(argument: ModalArgument, startIndex: number): SolutionStep[] {
const steps: SolutionStep[] = [];
let index = startIndex;
// Try T axiom: □P → P
if (['T', 'B', 'S4', 'S5', 'KD45'].includes(argument.system)) {
for (let i = 0; i < argument.premises.length; i++) {
const premise = argument.premises[i];
if (this.isModalOperator(premise, '□')) {
const inner = this.getModalOperand(premise);
if (inner && this.formulasEqual(inner, argument.conclusion)) {
steps.push({
index: index++,
statement: `Apply T axiom to premise ${i + 1}`,
rule: 'T Axiom',
justification: '□P → P (reflexivity)'
});
steps.push({
index: index++,
statement: this.formatFormula(argument.conclusion),
rule: 'Modus Ponens',
justification: 'Conclusion follows from T axiom'
});
return steps;
}
}
}
}
return [];
}
// Helper methods for formula inspection
private isModalOperator(formula: ModalFormula, op: '□' | '◇'): boolean {
return 'type' in formula && formula.type === 'modal' &&
(formula.operator === op ||
(op === '□' && formula.operator === 'necessary') ||
(op === '◇' && formula.operator === 'possible'));
}
private getModalOperand(formula: ModalFormula): ModalFormula | null {
if ('type' in formula && formula.type === 'modal') {
return formula.operand;
}
return null;
}
private isImplication(formula: ModalFormula): boolean {
return 'type' in formula && formula.type === 'binary' &&
('operator' in formula && (formula.operator === 'implies' || formula.operator === '→'));
}
private isPremiseOrTheorem(formula: ModalFormula, premises: ModalFormula[]): boolean {
return premises.some(p => this.formulasEqual(p, formula));
}
private formulasEqual(f1: ModalFormula, f2: ModalFormula): boolean {
// Simple structural equality check
return JSON.stringify(f1) === JSON.stringify(f2);
}
private formatFormula(formula: ModalFormula): string {
if (!('type' in formula)) return String(formula);
switch (formula.type) {
case 'variable':
return (formula as any).name;
case 'modal':
const op = (formula as any).operator === 'necessary' || (formula as any).operator === '□' ? '□' : '◇';
return `${op}${this.formatFormula((formula as any).operand)}`;
case 'unary':
return `¬${this.formatFormula((formula as any).operand)}`;
case 'binary':
const f = formula as any;
const left = this.formatFormula(f.left);
const right = this.formatFormula(f.right);
let operator = f.operator;
if (operator === 'and') operator = '∧';
else if (operator === 'or') operator = '∨';
else if (operator === 'implies') operator = '→';
else if (operator === 'iff') operator = '↔';
return `(${left} ${operator} ${right})`;
default:
return String(formula);
}
}
}
