/**
* Propositional Logic Explanation Generator
* Generates detailed explanations for propositional logic proofs
* Part of simplified Phase 4d Implementation
*/
import {
SolutionStep
} from '../types.js';
import {
ProofContext
} from '../types-explanations.js';
import { BaseExplanationGenerator } from './BaseExplanationGenerator.js';
/**
* Explanation generator for propositional logic.
*/
export class PropositionalExplanationGenerator extends BaseExplanationGenerator {
// Map of natural deduction rules to their explanations
private readonly ruleExplanations: Record<string, string> = {
'Modus Ponens': 'Modus Ponens (or implication elimination) allows us to deduce Q if we know both P → Q and P.',
'Modus Tollens': 'Modus Tollens allows us to deduce ¬P if we know both P → Q and ¬Q.',
'Conjunction Introduction': 'Conjunction Introduction allows us to deduce P ∧ Q if we know both P and Q individually.',
'Conjunction Elimination': 'Conjunction Elimination allows us to deduce P or Q individually if we know P ∧ Q.',
'Disjunction Introduction': 'Disjunction Introduction allows us to deduce P ∨ Q if we know either P or Q.',
'Disjunction Elimination': 'Disjunction Elimination (or case analysis) allows us to deduce R if we know P ∨ Q, P → R, and Q → R.',
'Implication Introduction': 'Implication Introduction allows us to deduce P → Q if we can derive Q from the assumption P.',
'Biconditional Introduction': 'Biconditional Introduction allows us to deduce P ↔ Q if we can derive both P → Q and Q → P.',
'Biconditional Elimination': 'Biconditional Elimination allows us to deduce either P → Q or Q → P if we know P ↔ Q.',
'Negation Introduction': 'Negation Introduction allows us to deduce ¬P if assuming P leads to a contradiction.',
'Negation Elimination': 'Negation Elimination allows us to deduce P if we know ¬¬P.',
'Double Negation': 'Double Negation allows us to eliminate or introduce double negations (P ⟷ ¬¬P).',
'Contraposition': 'Contraposition states that P → Q is logically equivalent to ¬Q → ¬P.',
'De Morgan\'s Law': 'De Morgan\'s Laws state that ¬(P ∧ Q) ⟷ (¬P ∨ ¬Q) and ¬(P ∨ Q) ⟷ (¬P ∧ ¬Q).',
'Law of Excluded Middle': 'The Law of Excluded Middle states that P ∨ ¬P is a tautology.',
'Material Implication': 'Material Implication states that P → Q is logically equivalent to ¬P ∨ Q.',
'Identity': 'The Identity rule states that P always implies P.',
'Premise': 'A premise is an initial statement assumed to be true, from which further conclusions are derived.'
};
// Common logical symbols and their explanations
private readonly symbolExplanations: Record<string, string> = {
'∧': 'Logical AND (conjunction). P ∧ Q is true only when both P and Q are true.',
'∨': 'Logical OR (disjunction). P ∨ Q is true when either P or Q (or both) are true.',
'→': 'Logical implication. P → Q is false only when P is true and Q is false.',
'↔': 'Logical biconditional. P ↔ Q is true when P and Q have the same truth value.',
'¬': 'Logical negation. ¬P is true when P is false, and false when P is true.',
'⊢': 'Turnstile symbol, indicating that the right-hand side can be derived from the left-hand side.',
'⊨': 'Double turnstile symbol, indicating that the right-hand side is a logical consequence of the left-hand side.',
'≡': 'Logical equivalence. P ≡ Q means that P and Q have the same truth value under all interpretations.'
};
// Truth table templates for common propositional forms
private readonly truthTableTemplates: Record<string, string> = {
'conjunction': 'P | Q | P ∧ Q\n--+---+------\nT | T | T\nT | F | F\nF | T | F\nF | F | F',
'disjunction': 'P | Q | P ∨ Q\n--+---+------\nT | T | T\nT | F | T\nF | T | T\nF | F | F',
'implication': 'P | Q | P → Q\n--+---+------\nT | T | T\nT | F | F\nF | T | T\nF | F | T',
'biconditional': 'P | Q | P ↔ Q\n--+---+------\nT | T | T\nT | F | F\nF | T | F\nF | F | T',
'negation': 'P | ¬P\n--+---\nT | F\nF | T'
};
protected getLogicSystemName(): string {
return 'propositional logic';
}
protected getRuleExplanations(): Record<string, string> {
return this.ruleExplanations;
}
protected getSymbolExplanations(): Record<string, string> {
return this.symbolExplanations;
}
protected getSpecificExplanation(step: SolutionStep, context: ProofContext): string {
const dependencies = this.getDependencies(step);
if (dependencies.length === 0) {
return 'This step introduces a new logical element based on previous reasoning.';
}
// Get the dependent steps
const dependentSteps = dependencies.map(depIndex => {
return context.previousSteps.find(s => s.index === depIndex);
}).filter(Boolean);
// Generate explanation based on the rule
switch (step.rule) {
case 'Modus Ponens':
if (dependentSteps.length === 2) {
return `We have "${dependentSteps[0]?.statement}" (which has the form P → Q) and "${dependentSteps[1]?.statement}" (which corresponds to P). By Modus Ponens, we can conclude Q, which is "${step.statement}".`;
}
break;
case 'Conjunction Introduction':
if (dependentSteps.length === 2) {
return `We have established "${dependentSteps[0]?.statement}" and "${dependentSteps[1]?.statement}" separately. By Conjunction Introduction, we can combine them to get "${step.statement}".`;
}
break;
case 'Conjunction Elimination':
if (dependentSteps.length === 1) {
return `From the conjunction "${dependentSteps[0]?.statement}", we can extract one of its components, "${step.statement}".`;
}
break;
case 'Disjunction Introduction':
if (dependentSteps.length === 1) {
return `Since we have established "${dependentSteps[0]?.statement}", we can add any statement using OR to get "${step.statement}".`;
}
break;
}
// Default explanation
if (dependentSteps.length === 1) {
return `This follows from step ${dependencies[0]} by applying the ${step.rule} rule.`;
} else {
return `This follows from steps ${dependencies.join(' and ')} by applying the ${step.rule} rule.`;
}
}
protected generateSystemSpecificVisualization(step: SolutionStep, context: ProofContext): string {
// For propositional logic, we generate ASCII truth tables or parse trees
if (step.rule === 'Tautology' || step.rule === 'Contradiction') {
return this.generateTruthTable(step.statement);
}
// Generate a simple parse tree
return this.generateParseTree(step.statement);
}
protected getRuleExample(rule: string): string {
switch (rule) {
case 'Modus Ponens':
return "Example:\nPremise 1: P → Q (If it rains, the ground will be wet)\nPremise 2: P (It rains)\nConclusion: Q (The ground is wet)\n\n";
case 'Modus Tollens':
return "Example:\nPremise 1: P → Q (If it rains, the ground will be wet)\nPremise 2: ¬Q (The ground is not wet)\nConclusion: ¬P (It does not rain)\n\n";
case 'Conjunction Introduction':
return "Example:\nPremise 1: P (It is sunny)\nPremise 2: Q (It is warm)\nConclusion: P ∧ Q (It is sunny and warm)\n\n";
case 'Conjunction Elimination':
return "Example:\nPremise: P ∧ Q (It is sunny and warm)\nConclusion 1: P (It is sunny)\nConclusion 2: Q (It is warm)\n\n";
case 'Disjunction Introduction':
return "Example:\nPremise: P (It is sunny)\nConclusion: P ∨ Q (It is sunny or it is raining)\n\n";
case 'Disjunction Elimination':
return "Example:\nPremise 1: P ∨ Q (Either it's sunny or it's raining)\nPremise 2: P → R (If it's sunny, we'll go to the park)\nPremise 3: Q → R (If it's raining, we'll go to the museum)\nConclusion: R (We'll either go to the park or to the museum)\n\n";
case 'Implication Introduction':
return "Example:\nAssumption: P (Assume it's raining)\nDerived: Q (The ground is wet)\nConclusion: P → Q (If it rains, the ground will be wet)\n\n";
case 'Double Negation':
return "Example:\nPremise: ¬¬P (It is not the case that it is not raining)\nConclusion: P (It is raining)\n\n";
default:
return "";
}
}
protected getHistoricalContext(rule: string): string {
switch (rule) {
case 'Modus Ponens':
case 'Modus Tollens':
return "Historical Context: These rules were first formalized by ancient Stoic logicians, particularly Chrysippus (c. 279-206 BCE), and later incorporated into Aristotelian logic. They form the foundation of deductive reasoning in classical logic.\n\n";
case 'De Morgan\'s Law':
return "Historical Context: Named after Augustus De Morgan (1806-1871), a British mathematician and logician who formalized these rules, although they were known implicitly before him. They are fundamental to modern Boolean algebra and digital circuit design.\n\n";
case 'Law of Excluded Middle':
return "Historical Context: This principle dates back to Aristotle's Metaphysics and has been a cornerstone of classical logic. However, it is rejected in intuitionistic logic and some other non-classical logics.\n\n";
default:
return "";
}
}
protected assessRuleDifficulty(rule: string): number {
switch (rule) {
// Basic rules
case 'Premise':
case 'Identity':
case 'Double Negation':
case 'Conjunction Introduction':
case 'Conjunction Elimination':
return 1;
// Intermediate rules
case 'Modus Ponens':
case 'Disjunction Introduction':
case 'Negation Elimination':
case 'Material Implication':
return 2;
// More challenging rules
case 'Modus Tollens':
case 'Contraposition':
case 'De Morgan\'s Law':
case 'Biconditional Introduction':
case 'Biconditional Elimination':
return 3;
// Advanced rules
case 'Disjunction Elimination':
case 'Implication Introduction':
case 'Negation Introduction':
return 4;
// Complex reasoning
case 'Proof by Contradiction':
case 'Proof by Cases':
case 'Mathematical Induction':
return 5;
// Default moderate difficulty
default:
return 3;
}
}
protected getSystemSpecificDetails(step: SolutionStep, context: ProofContext): string {
let details = '';
// Get relevant truth table
const truthTable = this.getRelevantTruthTable(step.statement, step.rule);
if (truthTable) {
details += `\n\nRelevant truth table:\n\`\`\`\n${truthTable}\n\`\`\`\n`;
}
// Add formal validity explanation
details += `\n\n${this.getValidityExplanation(step, context)}`;
return details;
}
protected generateProofStrategy(steps: SolutionStep[], context: ProofContext): string {
// Look for patterns in the steps to determine the proof strategy
const rules = steps.map(step => step.rule);
if (rules.includes('Proof by Contradiction')) {
return 'This proof uses the method of proof by contradiction (reductio ad absurdum). It assumes the negation of what we want to prove and derives a contradiction, thus establishing the original statement.';
}
if (rules.includes('Proof by Cases')) {
return 'This proof uses the method of proof by cases (disjunction elimination). It considers different possible scenarios and shows that the conclusion follows in each case.';
}
if (rules.includes('Disjunction Elimination') && rules.includes('Implication Introduction')) {
return 'This proof involves conditional reasoning and case analysis. It establishes conditional relationships and then uses them to analyze different possible scenarios.';
}
if (rules.filter(r => r === 'Modus Ponens').length > 1) {
return 'This proof uses a chain of implications, applying Modus Ponens multiple times to derive the conclusion from the premises.';
}
// Default strategy description
return 'This proof uses standard propositional logic rules to derive the conclusion from the premises. It follows a direct proof approach, establishing each step based on previous steps.';
}
protected generateKeyInsights(steps: SolutionStep[], context: ProofContext): string[] {
const insights: string[] = [];
// Add general insight about propositional logic
insights.push(
"Propositional logic focuses on the relationships between complete statements, using logical connectives (AND, OR, NOT, etc.) to build complex statements."
);
// Add insight about key rules used
const uniqueRules = new Set(steps.map(step => step.rule));
if (uniqueRules.size > 0) {
insights.push(
`This proof makes essential use of ${Array.from(uniqueRules).filter(r => r !== 'Premise').slice(0, 3).join(', ')}, showcasing how these rules work together to establish logical consequences.`
);
}
// Add insight about structure
if (steps.length > 5) {
insights.push(
"This proof demonstrates how complex logical arguments can be broken down into simple, incremental steps."
);
}
// Add insight about tautologies if relevant
if (steps.some(step => step.rule === 'Tautology')) {
insights.push(
"Tautologies (statements that are always true) play a key role in this proof. They provide logical certainties that help establish the conclusion."
);
}
return insights;
}
protected generateAlternativeApproaches(steps: SolutionStep[], context: ProofContext): string[] {
const alternatives: string[] = [];
// Suggest direct proof if current proof is by contradiction
if (steps.some(step => step.rule === 'Proof by Contradiction')) {
alternatives.push(
"Direct Proof: Instead of assuming the negation and deriving a contradiction, one could try to build a direct sequence of steps from the premises to the conclusion."
);
} else {
// Suggest proof by contradiction if current proof is direct
alternatives.push(
"Proof by Contradiction: One could assume the negation of the conclusion and derive a contradiction with the premises."
);
}
// Suggest truth table method
alternatives.push(
"Truth Table Method: Instead of a formal proof, one could construct a truth table to verify that the premises logically entail the conclusion under all possible interpretations of the atomic propositions."
);
// Suggest alternative rule sequences
alternatives.push(
"Alternative Rule Sequence: The same conclusion could be derived using different combinations of logical rules, potentially resulting in a more elegant or shorter proof."
);
return alternatives;
}
/**
* Get a relevant truth table for a statement or rule.
* @param statement The logical statement
* @param rule The rule applied
* @returns ASCII truth table
*/
private getRelevantTruthTable(statement: string, rule: string): string | null {
// Check for specific connectives in the statement
if (statement.includes('∧')) {
return this.truthTableTemplates.conjunction;
} else if (statement.includes('∨')) {
return this.truthTableTemplates.disjunction;
} else if (statement.includes('→')) {
return this.truthTableTemplates.implication;
} else if (statement.includes('↔')) {
return this.truthTableTemplates.biconditional;
} else if (statement.includes('¬')) {
return this.truthTableTemplates.negation;
}
// Check for rules associated with specific connectives
if (rule.includes('Conjunction')) {
return this.truthTableTemplates.conjunction;
} else if (rule.includes('Disjunction')) {
return this.truthTableTemplates.disjunction;
} else if (rule.includes('Implication') || rule === 'Modus Ponens' || rule === 'Modus Tollens') {
return this.truthTableTemplates.implication;
} else if (rule.includes('Biconditional')) {
return this.truthTableTemplates.biconditional;
} else if (rule.includes('Negation') || rule === 'Double Negation') {
return this.truthTableTemplates.negation;
}
return null;
}
/**
* Get an explanation of the validity of a step.
* @param step The solution step
* @param context The proof context
* @returns Explanation of validity
*/
private getValidityExplanation(step: SolutionStep, context: ProofContext): string {
// This is a simplified implementation
return `This step is formally valid according to the rules of propositional logic. The rule "${step.rule}" ensures that if the premises are true, the conclusion must also be true.`;
}
/**
* Generate a simplified ASCII truth table for a statement.
* @param statement The logical statement
* @returns ASCII truth table
*/
private generateTruthTable(statement: string): string {
// This is a simplified implementation that would be replaced
// with actual truth table generation logic
return `Truth Table for "${statement}":\n` +
`(This would be generated dynamically based on the statement)`;
}
/**
* Generate a simplified ASCII parse tree for a statement.
* @param statement The logical statement
* @returns ASCII parse tree
*/
private generateParseTree(statement: string): string {
// This is a simplified implementation that would be replaced
// with actual parse tree generation logic
return `Parse Tree for "${statement}":\n` +
`(This would be generated dynamically based on the statement)`;
}
}
