Proof Techniques in Propositional Logic

In the previous post, we explored the semantics of propositional logic using truth tables to determine the truth values of logical expressions. While truth tables are useful for evaluating small formulas, they become impractical for complex logical statements. Instead, formal proof techniques allow us to establish the validity of logical statements using deductive reasoning. This post introduces key proof methods in propositional logic, compares different proof systems, and discusses the fundamental notions of soundness and completeness.

Deductive Reasoning Methods

Deductive reasoning is the process of deriving conclusions from a given set of premises using formal rules of inference. Unlike truth tables, which exhaustively list all possible cases, deductive reasoning allows us to derive logical conclusions step by step.

A valid argument in propositional logic consists of premises and a conclusion, where the conclusion logically follows from the premises. If the premises are true, then the conclusion must also be true.

Common rules of inference include:

1. Modus Ponens (MP): If \(P \rightarrow Q\) and P are both true, then \(Q\) must be true.
   • Example:
     • Premise 1: If it is raining, then the ground is wet. (\(P \rightarrow Q\))
     • Premise 2: It is raining. (\(P\))
     • Conclusion: The ground is wet. (\(Q\))
2. Modus Tollens (MT): If \(P \rightarrow Q\) is true and \(Q\) is false, then \(P\) must be false.
   • Example:
     • Premise 1: If it is raining, then the ground is wet. (\(P \rightarrow Q\))
     • Premise 2: The ground is not wet. (\(\neg Q\))
     • Conclusion: It is not raining. (\(\neg P\))
3. Hypothetical Syllogism (HS): If \(P \rightarrow Q\) and \(Q \rightarrow R\) are true, then \(P \rightarrow R\) is also true.
4. Disjunctive Syllogism (DS): If \(P \lor Q\) is true and \(\neg P\) is true, then \(Q\) must be true.

These inference rules form the basis of formal proofs, where a conclusion is derived using a sequence of valid steps.

Formal Notation for Proofs

When working with formal proofs, we often use the notation (\(\vdash\)) to indicate that a formula is provable from a given set of premises. Specifically, if \( S \) is a set of premises and \( P \) is a formula, then:

\[
S \vdash P
\]

means that \( P \) is provable from \( S \) within a proof system.

It is important to distinguish between \(\vdash\) and \(\rightarrow\), as they represent fundamentally different concepts:

• The symbol \( P \rightarrow Q \) is a propositional formula that asserts a logical relationship between two statements. It states that if \( P \) is true, then \( Q \) must also be true.
• The symbol \( S \vdash P \) expresses provability: it states that \( P \) can be derived as a theorem from the premises \( S \) using a formal system of inference rules.

In other words, \( \rightarrow \) is a statement about truth, while \( \vdash \) is a statement about derivability in a formal system.

For example, Modus Ponens can be expressed formally as:

\[
P, (P \rightarrow Q) \vdash Q.
\]

This notation will be useful in later discussions where we analyze formal proofs rigorously.

Natural Deduction vs. Hilbert-Style Proofs

There are multiple systems for structuring formal proofs in propositional logic. The two primary approaches are Natural Deduction and Hilbert-Style Proof Systems.

Natural Deduction

Natural Deduction is a proof system that mimics human reasoning by allowing direct application of inference rules. Proofs in this system consist of a sequence of steps, each justified by a rule of inference. Assumptions can be introduced temporarily and later discharged to derive conclusions.

Key features of Natural Deduction:

• Uses rules such as Introduction and Elimination for logical connectives (e.g., AND introduction, OR elimination).
• Allows assumption-based reasoning, where subproofs are used to establish conditional statements.
• Proofs resemble the step-by-step reasoning found in mathematical arguments.

However, natural language statements remain ambiguous, which can lead to confusion. For instance, “If John studies, he will pass the exam” might not specify if passing the exam is solely dependent on studying. Later, when dealing with mathematical statements, we will ensure that all ambiguity is removed.

Example proof using Natural Deduction:

1. Assume “If the traffic is bad, I will be late” (\(P \rightarrow Q\))
2. Assume “The traffic is bad” (\(P\))
3. Conclude “I will be late” (\(Q\)) by Modus Ponens.

Hilbert-Style Proof Systems

Hilbert-style systems take a different approach, using a minimal set of axioms and inference rules. Proofs in this system involve applying axioms and the rule of detachment (Modus Ponens) repeatedly to derive new theorems.

Key features of Hilbert-Style Proofs:

• Based on a small number of axioms (e.g., axioms for implication and negation).
• Uses fewer inference rules but requires more steps to construct proofs.
• More suitable for metamathematical investigations, such as proving soundness and completeness.

Example of Hilbert-style proof:

1. Axiom: “If it is sunny, then I will go to the park” (\(P \rightarrow Q\))
2. Axiom: “If I go to the park, then I will be happy” (\(Q \rightarrow R\))
3. Using Hypothetical Syllogism: “If it is sunny, then I will be happy” (\(P \rightarrow R\))

While Hilbert-style systems are theoretically elegant, they are less intuitive for constructing actual proofs. Natural Deduction is generally preferred in practical applications.

Soundness and Completeness

A well-designed proof system should ensure that we only derive statements that are logically valid and that we can derive all logically valid statements. The concepts of soundness and completeness formalize these requirements and play a fundamental role in modern logic.

Soundness guarantees that the proof system does not allow us to derive false statements. If a proof system were unsound, we could deduce incorrect conclusions, undermining the entire logical structure of mathematics. Completeness, on the other hand, ensures that the proof system is powerful enough to derive every true statement within its domain. Without completeness, there would be true logical statements that we could never formally prove.

These properties are especially important in mathematical logic, automated theorem proving, and computer science. Soundness ensures that logical deductions made by computers are reliable, while completeness ensures that all provable truths can be algorithmically verified, given enough computational resources.

Since this is an introductory course, we will not formally define these concepts. However, informally we can state them as follows:

1. Soundness: If a formula can be proven in a formal system, then it must be logically valid (i.e., true in all possible interpretations).
   • This ensures that our proof system does not prove false statements.
   • Informally, if a statement is provable, then it must be true.
2. Completeness: If a formula is logically valid, then it must be provable within the formal system.
   • This guarantees that our proof system is powerful enough to prove all true statements.
   • Informally, if a statement is true in all interpretations, then we should be able to prove it.

Gödel’s Completeness Theorem states that propositional logic is both sound and complete—everything that is true can be proven, and everything that can be proven is true. However, the proof of this theorem is beyond the scope of this course.

Next Steps

Now that we have introduced formal proof techniques in propositional logic, the next step is to explore proof strategies and advanced techniques, such as proof by contradiction and resolution, which are particularly useful in automated theorem proving and logic programming.