import { BaseLogicSystem } from './base.js';
import { DeonticParser } from '../parsers/deonticParser.js';
import { DeonticValidator } from '../validators/deonticValidator.js';
import { LogicResult, DeonticFormula, SolutionStep, InputFormat } from '../types.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.systems.deontic;
export class DeonticLogicSystem extends BaseLogicSystem {
private parser: DeonticParser;
private validator: DeonticValidator;
constructor() {
super();
this.parser = new DeonticParser();
this.validator = new DeonticValidator();
}
validate(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
const worlds = this.validator.generateExampleWorlds();
const isValid = this.validator.validate(formula, worlds);
const principles = this.validator.checkDeonticPrinciples(formula);
return {
system: 'deontic',
message: `The formula "${input}" is ${isValid ? 'valid' : 'not valid'} in the deontic model.`,
details: {
system: 'deontic',
formalizedInput: input,
analysis: {
isValid,
fallacies: [],
explanation: this.generateExplanation(formula, worlds, isValid, principles)
}
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error validating deontic logic:', error);
return {
code: 'DEONTIC_VALIDATION_ERROR',
message: error instanceof Error ? error.message : 'Failed to validate deontic formula',
system: 'deontic',
status: 'error' as const,
details: {
system: 'deontic'
}
} as LogicResult;
}
}
formalize(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
const formalized = this.formulaToString(formula);
return {
system: 'deontic',
message: 'Input formalized successfully.',
details: {
system: 'deontic',
formalizedInput: formalized,
originalInput: input
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error formalizing deontic logic:', error);
return {
code: 'DEONTIC_FORMALIZATION_ERROR',
message: error instanceof Error ? error.message : 'Failed to formalize deontic input',
system: 'deontic',
status: 'error' as const,
details: {
system: 'deontic'
}
} as LogicResult;
}
}
visualize(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
const scenarios = this.validator.generateScenarios();
const visualization = this.generateDeonticVisualization(formula, scenarios);
return {
system: 'deontic',
message: 'Visualization generated successfully.',
details: {
system: 'deontic',
formalizedInput: input,
visualization
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error visualizing deontic logic:', error);
return {
code: 'DEONTIC_VISUALIZATION_ERROR',
message: error instanceof Error ? error.message : 'Failed to visualize deontic formula',
system: 'deontic',
status: 'error' as const,
details: {
system: 'deontic'
}
} as LogicResult;
}
}
solve(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
const steps = this.generateDeonticProof(formula);
return {
system: 'deontic',
message: 'Deontic analysis completed successfully.',
details: {
system: 'deontic',
formalizedInput: input,
solution: {
steps,
conclusion: 'Deontic analysis completed.'
}
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error solving deontic logic:', error);
return {
code: 'DEONTIC_SOLVING_ERROR',
message: error instanceof Error ? error.message : 'Failed to solve deontic formula',
system: 'deontic',
status: 'error' as const,
details: {
system: 'deontic'
}
} as LogicResult;
}
}
private formulaToString(formula: DeonticFormula): string {
switch (formula.type) {
case 'atom':
return formula.name;
case 'negation':
return `¬${this.formulaToString(formula.operand)}`;
case 'and':
return `(${this.formulaToString(formula.left)} ∧ ${this.formulaToString(formula.right)})`;
case 'or':
return `(${this.formulaToString(formula.left)} ∨ ${this.formulaToString(formula.right)})`;
case 'implication':
return `(${this.formulaToString(formula.left)} → ${this.formulaToString(formula.right)})`;
case 'deontic':
if (formula.operator === 'OB' || formula.operator === 'PM') {
// Special handling for conditional deontic operators
if (formula.operand.type === 'implication') {
return `${formula.operator}(${this.formulaToString(formula.operand.left)}|${this.formulaToString(formula.operand.right)})`;
}
}
return `${formula.operator}(${this.formulaToString(formula.operand)})`;
default:
return '?';
}
}
private generateExplanation(
formula: DeonticFormula,
worlds: any[],
isValid: boolean,
principles: any[]
): string {
let explanation = `Deontic Logic Analysis of: ${this.formulaToString(formula)}\n\n`;
// Explain deontic operators
explanation += 'Deontic Operators:\n';
explanation += ' O(p) - It is obligatory that p\n';
explanation += ' P(p) - It is permitted that p\n';
explanation += ' F(p) - It is forbidden that p\n';
explanation += ' OB(p|q) - p is obligatory given q\n';
explanation += ' PM(p|q) - p is permitted given q\n';
explanation += ' IM(p) - It is impermissible that p\n\n';
// Show worlds
explanation += 'Deontic Worlds:\n';
worlds.forEach(world => {
explanation += ` World ${world.id}:\n`;
explanation += ` Obligations: {${Array.from(world.obligations).join(', ')}}\n`;
explanation += ` Permissions: {${Array.from(world.permissions).join(', ')}}\n`;
explanation += ` Facts: {${Array.from(world.facts).join(', ')}}\n`;
explanation += ` Ideal: ${Array.from(world.obligations).every(o => world.facts.has(o)) ? 'Yes' : 'No'}\n`;
});
explanation += `\nResult: ${isValid ? 'VALID' : 'INVALID'}\n`;
// Show principles
if (principles.length > 0) {
explanation += '\nDeontic Principles:\n';
principles.forEach(p => {
explanation += ` ${p.principle}: ${p.holds ? '✓' : '✗'} - ${p.explanation}\n`;
});
}
return explanation;
}
private generateDeonticVisualization(formula: DeonticFormula, scenarios: any[]): string {
let viz = `
Deontic Logic Visualization
===========================
Formula: ${this.formulaToString(formula)}
Deontic Relationships:
`;
// Create a simple diagram
viz += '\n┌─────────────────────────────────────┐\n';
viz += '│ DEONTIC MODALITIES │\n';
viz += '├─────────────────────────────────────┤\n';
viz += '│ │\n';
viz += '│ OBLIGATORY ──implies──> PERMITTED│\n';
viz += '│ O(p) ────────> P(p) │\n';
viz += '│ │\n';
viz += '│ FORBIDDEN = NOT PERMITTED │\n';
viz += '│ F(p) = ¬P(p) │\n';
viz += '│ │\n';
viz += '│ OBLIGATORY = NOT PERMITTED NOT │\n';
viz += '│ O(p) = ¬P(¬p) │\n';
viz += '│ │\n';
viz += '└─────────────────────────────────────┘\n\n';
// Show example scenarios
viz += 'Example Scenarios:\n';
viz += '==================\n\n';
scenarios.forEach(scenario => {
viz += `${scenario.name}:\n`;
viz += ` Obligations: ${scenario.obligations.join(', ')}\n`;
viz += ` Permissions: ${scenario.permissions.join(', ')}\n`;
viz += ` Forbidden: ${scenario.forbiddens.join(', ')}\n\n`;
});
// Add standard deontic principles
viz += 'Standard Deontic Principles:\n';
viz += '============================\n';
viz += '1. D Axiom: O(p) → P(p)\n';
viz += ' (What is obligatory is permitted)\n\n';
viz += '2. Consistency: ¬(O(p) ∧ O(¬p))\n';
viz += ' (No contradictory obligations)\n\n';
viz += '3. Deontic Duality: F(p) ↔ O(¬p)\n';
viz += ' (Forbidden = Obligatory not)\n\n';
viz += '4. Permission Duality: P(p) ↔ ¬O(¬p)\n';
viz += ' (Permitted = Not obligatory not)\n';
return viz;
}
private generateDeonticProof(formula: DeonticFormula): SolutionStep[] {
const steps: SolutionStep[] = [];
let index = 1;
steps.push({
index: index++,
statement: `Given deontic formula: ${this.formulaToString(formula)}`,
rule: 'Given',
justification: 'Initial deontic formula'
});
// Analyze the formula type
if (formula.type === 'deontic') {
switch (formula.operator) {
case 'O':
steps.push({
index: index++,
statement: 'O(p) means "It is obligatory that p"',
rule: 'Definition',
justification: 'Deontic obligation operator'
});
steps.push({
index: index++,
statement: 'By D axiom: O(p) → P(p)',
rule: 'D Axiom',
justification: 'What is obligatory is permitted'
});
break;
case 'P':
steps.push({
index: index++,
statement: 'P(p) means "It is permitted that p"',
rule: 'Definition',
justification: 'Deontic permission operator'
});
steps.push({
index: index++,
statement: 'P(p) ↔ ¬O(¬p)',
rule: 'Permission Duality',
justification: 'Permitted = Not obligatory not'
});
break;
case 'F':
steps.push({
index: index++,
statement: 'F(p) means "It is forbidden that p"',
rule: 'Definition',
justification: 'Deontic prohibition operator'
});
steps.push({
index: index++,
statement: 'F(p) ↔ O(¬p)',
rule: 'Deontic Duality',
justification: 'Forbidden = Obligatory not'
});
break;
case 'OB':
steps.push({
index: index++,
statement: 'OB(p|q) means "p is obligatory given q"',
rule: 'Definition',
justification: 'Conditional obligation'
});
steps.push({
index: index++,
statement: 'If q holds, then O(p) must hold',
rule: 'Conditional Semantics',
justification: 'Conditional obligation evaluation'
});
break;
}
}
// Add relevant deontic theorems
steps.push({
index: index++,
statement: 'Key Deontic Theorem: ¬(O(p) ∧ O(¬p))',
rule: 'Consistency',
justification: 'Cannot have contradictory obligations'
});
steps.push({
index: index++,
statement: 'Von Wright\'s Paradox: O(p) → O(p ∨ q)',
rule: 'Deontic Paradox',
justification: 'If p is obligatory, then p or q is obligatory'
});
return steps;
}
}
