/**
* Predicate Logic Explanation Generator
* Generates detailed explanations for predicate 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 predicate logic.
*/
export class PredicateExplanationGenerator extends BaseExplanationGenerator {
// Map of predicate logic rules to their explanations
private readonly ruleExplanations: Record<string, string> = {
'Universal Instantiation': 'Universal Instantiation (UI) allows us to conclude Φ(c) from ∀x Φ(x), where c is any constant in the domain.',
'Universal Generalization': 'Universal Generalization (UG) allows us to conclude ∀x Φ(x) if we can prove Φ(c) for an arbitrary constant c that doesn\'t appear in any assumption.',
'Existential Instantiation': 'Existential Instantiation (EI) allows us to replace ∃x Φ(x) with Φ(c), where c is a new constant not appearing elsewhere in the proof.',
'Existential Generalization': 'Existential Generalization (EG) allows us to conclude ∃x Φ(x) from Φ(c), where c is any constant.',
'Universal Elimination': 'Universal Elimination is another name for Universal Instantiation, allowing us to derive a specific instance from a universally quantified statement.',
'Universal Introduction': 'Universal Introduction is another name for Universal Generalization, allowing us to derive a universally quantified statement from a proof about an arbitrary object.',
'Existential Elimination': 'Existential Elimination is another name for Existential Instantiation, allowing us to reason with a specific instance of an existentially quantified statement.',
'Existential Introduction': 'Existential Introduction is another name for Existential Generalization, allowing us to introduce an existentially quantified statement from a specific instance.',
'Quantifier Negation': 'Quantifier Negation rules state that ¬∀x Φ(x) is equivalent to ∃x ¬Φ(x), and ¬∃x Φ(x) is equivalent to ∀x ¬Φ(x).',
'Instantiate': 'Instantiate a variable in a quantified formula with a specific term.',
'Generalize': 'Generalize from a specific term to a quantified variable.',
'Model Construction': 'Create a formal model with a domain and interpretation that satisfies a given formula.',
'Substitution': 'Replace a variable with a term, ensuring that the term is free for the variable in the formula.',
'Premise': 'A premise is an initial statement assumed to be true, from which further conclusions are derived.'
};
// Common predicate logic symbols and their explanations
private readonly symbolExplanations: Record<string, string> = {
'∀': 'Universal quantifier. ∀x P(x) means "for all x, P(x) is true".',
'∃': 'Existential quantifier. ∃x P(x) means "there exists an x such that P(x) is 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.',
'∧': '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.',
'=': 'Equality. a = b asserts that a and b are the same object.',
'≠': 'Inequality. a ≠ b asserts that a and b are different objects.',
'⊢': '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.'
};
// Common predicate logic patterns and their explanations
private readonly patternExplanations: Record<string, string> = {
'Universal Conditional': 'The pattern ∀x(P(x) → Q(x)) asserts that for all objects, if they have property P, then they also have property Q.',
'Existential Conjunction': 'The pattern ∃x(P(x) ∧ Q(x)) asserts that there exists at least one object that has both properties P and Q.',
'Universal Negation': 'The pattern ∀x ¬P(x) asserts that no object has property P, equivalent to ¬∃x P(x).',
'Existential Negation': 'The pattern ∃x ¬P(x) asserts that there exists at least one object that does not have property P.',
'Nested Quantifiers': 'Expressions with nested quantifiers like ∀x ∃y P(x,y) require careful interpretation. This states that for every x, there exists a y such that P(x,y) holds.',
'Quantifier Order': 'The order of quantifiers matters. ∀x ∃y P(x,y) is generally different from ∃y ∀x P(x,y).'
};
protected getLogicSystemName(): string {
return 'predicate 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 'Universal Instantiation':
if (dependentSteps.length === 1) {
return `From the universally quantified statement "${dependentSteps[0]?.statement}", we substitute a specific value to obtain "${step.statement}".`;
}
break;
case 'Universal Generalization':
if (dependentSteps.length === 1) {
return `Since "${dependentSteps[0]?.statement}" holds for an arbitrary individual, we can generalize to all individuals with "${step.statement}".`;
}
break;
case 'Existential Instantiation':
if (dependentSteps.length === 1) {
return `From the existentially quantified statement "${dependentSteps[0]?.statement}", we introduce a witness constant to get "${step.statement}".`;
}
break;
case 'Existential Generalization':
if (dependentSteps.length === 1) {
return `From the specific instance "${dependentSteps[0]?.statement}", we can assert the existential statement "${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 predicate logic, we generate domain models or parse trees
if (step.rule === 'Model Construction') {
return this.generateModelVisualization(step.statement);
}
// Generate scope visualization for quantified statements
if (step.statement.includes('∀') || step.statement.includes('∃')) {
return this.generateQuantifierScopeVisualization(step.statement);
}
// Generate a simple parse tree
return this.generateParseTree(step.statement);
}
protected getRuleExample(rule: string): string {
switch (rule) {
case 'Universal Instantiation':
return "Example:\nPremise: ∀x P(x) (All objects have property P)\nConclusion: P(a) (Object a has property P)\n\n";
case 'Universal Generalization':
return "Example:\nPremise: P(c) (proven for arbitrary c)\nConclusion: ∀x P(x) (All objects have property P)\n\n";
case 'Existential Instantiation':
return "Example:\nPremise: ∃x P(x) (There exists an object with property P)\nConclusion: P(c) (Object c has property P), where c is a new constant\n\n";
case 'Existential Generalization':
return "Example:\nPremise: P(a) (Object a has property P)\nConclusion: ∃x P(x) (There exists an object with property P)\n\n";
case 'Quantifier Negation':
return "Example:\nPremise: ¬∀x P(x) (Not all objects have property P)\nConclusion: ∃x ¬P(x) (There exists an object that does not have property P)\n\n";
default:
return "";
}
}
protected getHistoricalContext(rule: string): string {
switch (rule) {
case 'Universal Instantiation':
case 'Universal Generalization':
case 'Existential Instantiation':
case 'Existential Generalization':
return "Historical Context: These rules form the core of first-order predicate logic, which was developed in the late 19th and early 20th centuries by logicians like Gottlob Frege, Charles Sanders Peirce, and Bertrand Russell. Predicate logic significantly extended the expressive power of formal logic by introducing quantifiers and variables.\n\n";
case 'Quantifier Negation':
return "Historical Context: The rules for negating quantifiers were formalized in the development of predicate logic. They are central to the duality relationship between universal and existential quantification, which parallels the duality between conjunction and disjunction in propositional logic.\n\n";
default:
return "";
}
}
protected assessRuleDifficulty(rule: string): number {
// Basic rule applications
if (rule === 'Premise' || rule === 'Substitution') {
return 1;
}
// Assess based on specific rules
switch (rule) {
case 'Universal Instantiation':
case 'Existential Generalization':
return 2;
case 'Universal Generalization':
case 'Existential Instantiation':
return 3;
case 'Quantifier Negation':
return 3;
case 'Model Construction':
return 4;
default:
// Default moderate difficulty
return 3;
}
}
protected getSystemSpecificDetails(step: SolutionStep, context: ProofContext): string {
let details = '';
// Add pattern explanations
details += this.getPatternExplanation(step.statement);
// Add formal semantics explanation
details += `\n\n${this.getSemanticsExplanation(step, context)}`;
// Add information about quantifier scope
details += `\n\n${this.getQuantifierScopeExplanation(step.statement)}`;
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('Model Construction')) {
return 'This proof constructs a model to demonstrate the satisfiability of the formulas. It specifies a domain of individuals and interpretations of predicates to make the statements true.';
}
if (rules.includes('Universal Generalization') && rules.includes('Existential Instantiation')) {
return 'This proof uses quantifier manipulation techniques, working with specific instances and then generalizing results. It carefully manages the introduction of new constants and ensures proper generalization.';
}
if (rules.filter(r => r === 'Universal Instantiation').length > 1) {
return 'This proof makes multiple instantiations of universally quantified statements, applying the general principles to specific cases before combining the results.';
}
// Default strategy description
return 'This proof uses standard predicate logic rules to derive the conclusion from the premises. It carefully manages quantifiers and their scope while building a logical chain of reasoning.';
}
protected generateKeyInsights(steps: SolutionStep[], context: ProofContext): string[] {
const insights: string[] = [];
// Add general insight about predicate logic
insights.push(
"Predicate logic extends propositional logic by breaking statements into subjects and predicates, and by introducing quantifiers to make assertions about collections of objects."
);
// Add insight about quantifiers
const hasUniversal = steps.some(step => step.statement.includes('∀'));
const hasExistential = steps.some(step => step.statement.includes('∃'));
if (hasUniversal && hasExistential) {
insights.push(
"This proof demonstrates the interplay between universal (∀) and existential (∃) quantifiers, and how they can be manipulated according to logical rules."
);
} else if (hasUniversal) {
insights.push(
"Universal quantification (∀) plays a key role in this proof, allowing us to reason about all objects in the domain at once."
);
} else if (hasExistential) {
insights.push(
"Existential quantification (∃) is central to this proof, allowing us to assert the existence of objects with specific properties."
);
}
// Add insight about structure
if (steps.length > 5) {
insights.push(
"This proof demonstrates how complex reasoning about quantified statements can be broken down into clear, incremental steps."
);
}
return insights;
}
protected generateAlternativeApproaches(steps: SolutionStep[], context: ProofContext): string[] {
const alternatives: string[] = [];
// Suggest model-theoretic approach if current proof is syntactic
if (!steps.some(step => step.rule === 'Model Construction')) {
alternatives.push(
"Model-Theoretic Approach: Instead of a formal proof, one could construct a model to demonstrate satisfiability or a counterexample to demonstrate invalidity."
);
}
// Suggest different quantifier manipulations
alternatives.push(
"Alternative Quantifier Strategy: The order of quantifier instantiations and generalizations could be changed to produce a different proof structure while reaching the same conclusion."
);
// Suggest translation to propositional logic if domain is finite
alternatives.push(
"Finite Domain Translation: If the domain is finite, the quantified statements could be expanded into conjunctions or disjunctions of propositional statements, allowing for a proof using propositional logic techniques."
);
return alternatives;
}
/**
* Get explanation for common patterns in a statement.
* @param statement The logical statement
* @returns Explanation of the patterns
*/
private getPatternExplanation(statement: string): string {
let explanation = '\nLogical patterns in this statement:\n';
let foundPatterns = false;
// Check for common patterns
for (const [pattern, desc] of Object.entries(this.patternExplanations)) {
switch (pattern) {
case 'Universal Conditional':
if (statement.match(/∀[a-z]\s*\([^)]*→[^)]*\)/)) {
explanation += `- Universal Conditional: ${desc}\n`;
foundPatterns = true;
}
break;
case 'Existential Conjunction':
if (statement.match(/∃[a-z]\s*\([^)]*∧[^)]*\)/)) {
explanation += `- Existential Conjunction: ${desc}\n`;
foundPatterns = true;
}
break;
case 'Universal Negation':
if (statement.match(/∀[a-z]\s*¬/)) {
explanation += `- Universal Negation: ${desc}\n`;
foundPatterns = true;
}
break;
case 'Existential Negation':
if (statement.match(/∃[a-z]\s*¬/)) {
explanation += `- Existential Negation: ${desc}\n`;
foundPatterns = true;
}
break;
case 'Nested Quantifiers':
if (statement.match(/[∀∃][a-z].*[∀∃][a-z]/)) {
explanation += `- Nested Quantifiers: ${desc}\n`;
foundPatterns = true;
}
break;
case 'Quantifier Order':
if (statement.match(/[∀∃][a-z].*[∀∃][a-z]/)) {
explanation += `- Quantifier Order: ${desc}\n`;
foundPatterns = true;
}
break;
}
}
return foundPatterns ? explanation : '';
}
/**
* Get an explanation of the semantics of a step.
* @param step The solution step
* @param context The proof context
* @returns Explanation of semantics
*/
private getSemanticsExplanation(step: SolutionStep, context: ProofContext): string {
// Check for quantifiers in the statement
if (step.statement.includes('∀')) {
return 'The universal quantifier "∀" indicates that the statement must be true for all objects in the domain of discourse. To satisfy this statement, there cannot be any counterexamples.';
} else if (step.statement.includes('∃')) {
return 'The existential quantifier "∃" indicates that there must be at least one object in the domain of discourse for which the statement is true. To satisfy this statement, we only need to find one example.';
}
// Default explanation
return 'The semantics of this statement depend on the interpretation of the predicates and terms in a specific model with a domain of individuals.';
}
/**
* Get an explanation of quantifier scope in a statement.
* @param statement The logical statement
* @returns Explanation of quantifier scope
*/
private getQuantifierScopeExplanation(statement: string): string {
// Check if there are quantifiers in the statement
if (!statement.includes('∀') && !statement.includes('∃')) {
return '';
}
// Basic explanation of scope
let explanation = 'Quantifier Scope: ';
// Check for nested quantifiers
if (statement.match(/[∀∃][a-z].*[∀∃][a-z]/)) {
explanation += 'This statement contains nested quantifiers. The scope of each quantifier extends to the end of the formula or until the closing parenthesis of its subformula. ';
explanation += 'The leftmost quantifier has the widest scope, binding its variable throughout the rest of the formula. ';
// Check for specific patterns
if (statement.match(/∀[a-z].*∃[a-z]/)) {
explanation += 'The pattern "∀x ∃y" indicates that for each x, there may be a different y that satisfies the relation. ';
} else if (statement.match(/∃[a-z].*∀[a-z]/)) {
explanation += 'The pattern "∃x ∀y" indicates that there is a single x that works for all y. This is a stronger statement than "∀y ∃x". ';
}
} else {
// Single quantifier
explanation += 'The scope of the quantifier extends to the end of the formula or until the closing parenthesis of its subformula. ';
explanation += 'All occurrences of the quantified variable within its scope are bound by the quantifier. ';
}
return explanation;
}
/**
* Generate a model visualization for a statement.
* @param statement The logical statement
* @returns ASCII model visualization
*/
private generateModelVisualization(statement: string): string {
// This is a simplified implementation that would be replaced
// with actual model visualization logic
return `Model for "${statement}":\n` +
`Domain: {a, b, c}\n` +
`Interpretation:\n` +
` P(a): true\n` +
` P(b): false\n` +
` P(c): true\n` +
` R(a, b): true\n` +
` R(b, c): true\n` +
` R(a, c): true\n` +
` ...`;
}
/**
* Generate a scope visualization for quantified statements.
* @param statement The logical statement
* @returns ASCII scope visualization
*/
private generateQuantifierScopeVisualization(statement: string): string {
// This is a simplified implementation that would be replaced
// with actual scope visualization logic
return `Quantifier Scope for "${statement}":\n` +
`(Visualization would show nested scopes of quantifiers)`;
}
/**
* Generate a 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` +
`(Visual representation of the formula structure)`;
}
/**
* Get common mistakes associated with a rule.
* @param rule The logical rule
* @returns Description of common mistakes
*/
private getCommonMistakes(rule: string): string {
switch (rule) {
case 'Universal Generalization':
return "Common Mistakes:\n- Attempting to generalize from a specific instance that depends on assumptions about that specific object.\n- Failing to ensure that the constant being generalized is arbitrary and not used in open assumptions.\n\n";
case 'Existential Instantiation':
return "Common Mistakes:\n- Reusing a constant that already appears elsewhere in the proof.\n- Conflating the new constant with existing constants, leading to invalid inferences.\n\n";
case 'Quantifier Negation':
return "Common Mistakes:\n- Incorrectly negating quantifiers without changing the quantifier type.\n- Failing to negate the predicate when changing the quantifier.\n\n";
case 'Universal Instantiation':
return "Common Mistakes:\n- Instantiating with a term that is not free for the variable in the formula.\n- Confusing universal instantiation with universal generalization.\n\n";
default:
return "";
}
}
}
