3.3 Constructing formal proofs in FOL

First-order logic (FOL) proofs build on propositional logic by introducing predicates, quantifiers, and variables. This allows for more complex reasoning about relationships between objects and properties in a given domain.

Constructing FOL proofs involves translating natural language arguments into formal notation, then applying inference rules to derive conclusions. Key strategies include direct proofs, indirect proofs, and goal-oriented approaches like working backwards from the conclusion.

Translating Arguments into FOL Proofs

Key Components of FOL Proofs

• FOL proofs consist of a sequence of well-formed formulas (wffs)
  • Each wff is either a premise, an assumption introduced by a subproof, or follows from previous wffs by an inference rule
  • Premises are the starting points of the argument, assumptions are temporary statements used in subproofs, and derived statements follow logically from the premises and assumptions
• Translation from natural language to FOL involves identifying the logical structure of the argument
  • Identify premises, conclusion, and any hidden assumptions necessary for the argument to be valid
  • Break down complex statements into simpler propositions connected by logical operators
  • Ensure that the formal representation captures the intended meaning and logical relationships of the natural language argument

Representing Arguments in FOL

• Predicates, constants, and variables must be carefully chosen to accurately represent the entities and relationships described in the natural language argument
  • Predicates represent properties or relations (is_red(x), loves(x, y))
  • Constants represent specific objects or individuals (alice, bob)
  • Variables represent arbitrary objects in the domain of discourse (x, y, z)
• Quantifiers (universal and existential) are used to express the scope of the variables in the argument
  • Universal quantifier (∀): asserts that a statement holds for all objects in the domain (∀x is_human(x) → is_mortal(x))
  • Existential quantifier (∃): asserts that a statement holds for at least one object in the domain (∃x is_prime(x) ∧ is_even(x))
• Logical connectives (conjunction, disjunction, implication, and negation) are used to capture the logical relationships between the propositions in the argument
  • Conjunction (∧): asserts that both propositions are true (is_red(x) ∧ is_round(x))
  • Disjunction (∨): asserts that at least one of the propositions is true (is_student(x) ∨ is_teacher(x))
  • Implication (→): asserts that if the first proposition is true, then the second proposition must also be true (is_human(x) → is_mortal(x))
  • Negation (¬): asserts that a proposition is not true (¬is_even(3))

Strategies for Constructing Proofs

Direct and Indirect Proof Strategies

• The direct proof strategy starts with the premises and applies inference rules to derive the conclusion step by step
  • Begin with the given premises and assumptions
  • Apply inference rules to derive new statements that logically follow from the previous statements
  • Continue this process until the conclusion is derived
• The indirect proof strategy assumes the negation of the conclusion and derives a contradiction, thereby proving the original conclusion by reductio ad absurdum
  • Assume the negation of the conclusion as a new premise
  • Derive a contradiction (a statement that is always false, such as P ∧ ¬P) using the premises, assumptions, and inference rules
  • Since a contradiction is derived, the assumed negation of the conclusion must be false, implying that the original conclusion is true

Goal-Oriented Strategies

• Working backwards from the conclusion involves considering what premises and inference rules would be needed to derive the conclusion, and then working towards those subgoals
  • Identify the conclusion to be proved
  • Consider what premises or derived statements could be used to directly infer the conclusion using an inference rule
  • Work backwards, identifying the premises or subgoals needed to derive those statements, until the given premises are reached
• Proof by cases considers different possible scenarios and shows that the conclusion holds in each case
  • Identify the different cases or scenarios relevant to the argument (P, ¬P)
  • Prove the conclusion holds for each case separately
  • Conclude that the conclusion holds in general, since it holds for all possible cases
• Proof by contradiction assumes the negation of the conclusion and derives a contradiction with the premises or known facts
  • Assume the negation of the conclusion
  • Derive a contradiction using the premises, assumptions, and inference rules
  • Conclude that the original conclusion must be true, since its negation leads to a contradiction

Inference Rules and Proof Techniques in FOL

Propositional Inference Rules

• Modus ponens (→-elimination): If P and P→Q are true, then Q is true
  • Example: If "Socrates is a man" (P) and "If Socrates is a man, then Socrates is mortal" (P→Q) are true, then "Socrates is mortal" (Q) is true
• Modus tollens (MT): If P→Q and ¬Q are true, then ¬P is true
  • Example: If "If it is raining, then the ground is wet" (P→Q) and "The ground is not wet" (¬Q) are true, then "It is not raining" (¬P) is true
• Hypothetical syllogism (HS): If P→Q and Q→R are true, then P→R is true
  • Example: If "If I study hard, I will pass the exam" (P→Q) and "If I pass the exam, I will graduate" (Q→R) are true, then "If I study hard, I will graduate" (P→R) is true
• Disjunctive syllogism (∨-elimination): If P∨Q and ¬P are true, then Q is true
  • Example: If "Either the suspect is guilty, or the witness is lying" (P∨Q) and "The suspect is not guilty" (¬P) are true, then "The witness is lying" (Q) is true
• Constructive dilemma (CD): If (P→Q)∧(R→S) and P∨R are true, then Q∨S is true
  • Example: If "If it rains, I will bring an umbrella" (P→Q) and "If it is sunny, I will wear sunglasses" (R→S) are true, and "It is either raining or sunny" (P∨R) is true, then "I will either bring an umbrella or wear sunglasses" (Q∨S) is true

Quantifier Inference Rules

• Universal instantiation (UI): If ∀x P(x) is true, then P(c) is true for any constant c
  • Example: If "All humans are mortal" (∀x is_human(x) → is_mortal(x)) is true, then "Socrates is mortal" (is_mortal(socrates)) is true, given that Socrates is a constant representing a human
• Existential generalization (EG): If P(c) is true for some constant c, then ∃x P(x) is true
  • Example: If "Socrates is a philosopher" (is_philosopher(socrates)) is true, then "There exists a philosopher" (∃x is_philosopher(x)) is true
• Existential instantiation (EI): If ∃x P(x) is true, then P(c) is true for some new constant c
  • Example: If "There exists a prime number" (∃x is_prime(x)) is true, then we can introduce a new constant 'p' and assert "p is a prime number" (is_prime(p))
• Universal generalization (UG): If P(c) is true for an arbitrary constant c, then ∀x P(x) is true
  • Example: If we prove that "For an arbitrary triangle t, the sum of the angles of t is 180 degrees" (sum_of_angles(t) = 180), then we can conclude that "For all triangles, the sum of the angles is 180 degrees" (∀x is_triangle(x) → sum_of_angles(x) = 180)

Variable Instantiation and Quantifier Scope in FOL

Variable Instantiation

• Variables in FOL are used to represent arbitrary objects in the domain of discourse
  • Variables are typically represented by lowercase letters (x, y, z)
  • Variables do not have a specific referent until they are instantiated with a constant or a specific object
• Universal instantiation allows the substitution of a constant for a universally quantified variable
  • If a statement holds for all objects in the domain, then it must hold for any specific object
  • Example: From "All humans are mortal" (∀x is_human(x) → is_mortal(x)), we can infer "If Socrates is human, then Socrates is mortal" (is_human(socrates) → is_mortal(socrates))
• Existential instantiation introduces a new constant to represent an object that satisfies an existentially quantified statement
  • If a statement holds for at least one object in the domain, we can introduce a new constant to represent that object and reason about it
  • Example: From "There exists a prime number" (∃x is_prime(x)), we can introduce a new constant 'p' and assert "p is a prime number" (is_prime(p))

Quantifier Scope

• The scope of a quantifier is the portion of the formula it governs
  • The scope of a quantifier determines which variables are bound by the quantifier and which are free
  • Example: In the formula ∀x (P(x) → ∃y Q(x, y)), the scope of ∀x is (P(x) → ∃y Q(x, y)), and the scope of ∃y is Q(x, y)
• Quantifier scope can affect the meaning and validity of a statement
  • Example: ∀x ∃y P(x, y) is not equivalent to ∃y ∀x P(x, y). The first states that for every x, there exists a y such that P(x, y) holds, while the second states that there exists a single y such that for every x, P(x, y) holds
• When instantiating variables, it is crucial to consider the scope of the quantifiers to avoid invalid inferences
  • Existential fallacy: Incorrectly assuming that a statement holds for all objects when it only holds for some
    • Example: From "Some students are tall" (∃x is_student(x) ∧ is_tall(x)), it is invalid to conclude "All students are tall" (∀x is_student(x) → is_tall(x))
  • Illicit universal generalization: Incorrectly generalizing a statement to all objects when it only holds for a specific object
    • Example: From "Socrates is a mortal philosopher" (is_philosopher(socrates) ∧ is_mortal(socrates)), it is invalid to conclude "All philosophers are mortal" (∀x is_philosopher(x) → is_mortal(x))
• Careful management of variable instantiation and quantifier scope is necessary to construct valid FOL proofs and avoid common pitfalls in reasoning
  • Ensure that variables are properly instantiated within the scope of their respective quantifiers
  • Be cautious when generalizing or instantiating statements to avoid invalid inferences
  • Use variable renaming or subscripts to avoid confusion when multiple quantifiers are involved (∀x ∃y P(x, y) vs. ∀x ∃y P(x, y₁))