Proof Strategies and Advanced Techniques

In previous posts of this thread, we introduced formal proof techniques in propositional logic, discussing natural deduction, Hilbert-style proofs, and the fundamental concepts of soundness and completeness. Now, we turn to advanced proof strategies that enhance our ability to construct and analyze proofs efficiently. In particular, we will explore proof by contradiction and resolution, two powerful techniques frequently used in mathematics, logic, and computer science.

Proof by Contradiction

Proof by contradiction (also known as reductio ad absurdum) is a fundamental method in mathematical reasoning. The core idea is to assume the negation of the statement we wish to prove and show that this leads to a contradiction. If the assumption results in an impossible situation, we conclude that our original statement must be true.

Formalization in Propositional Logic

Proof by contradiction can be expressed formally as:

\((\neg P \vdash (Q \land \neg Q)) \vdash P\).

This means that if assuming \(\neg P\) leads to a contradiction (\(Q\land \neg Q\)), then \(\neg P\) must be false, so \(P\) holds. This formulation captures the essence of proof by contradiction: by demonstrating that an assumption results in a logical impossibility, we conclude that the assumption must have been incorrect.In propositional logic, suppose we wish to prove a formula \(P\).

Proof by contradiction consists of the following steps:

1. Assume \(\neg P\) (i.e., assume that \(P\) is false).
2. Using inference rules, derive a contradiction—i.e., derive a formula of the form \(Q \land \neg Q\), where \(Q\) is some proposition.
3. Since a contradiction is always false, the assumption \(\neg P\) must also be false.
4. Therefore, \(P\) must be true.

This follows from the principle of the excluded middle in classical logic, which states that for any proposition \(P\), either \(P\) or \(\neg P\) must be true.

Example in Propositional Logic

Let us prove that if \(P \rightarrow Q\) and \(\neg Q\) hold, then \(\neg P\) must also hold:

1. Assume the negation of the desired conclusion: Suppose \(P\) is true.
2. Use the given premises:
   • We know that \(P \rightarrow Q\) is true.
   • By Modus Ponens, since \(P\) is true, we must have \(Q\) as true.
   • However, we are also given that \(\neg Q\) is true, meaning that \(Q\) must be false.
3. Contradiction: Since \(Q\) is both true and false, we reach a contradiction.
4. Conclusion: Since our assumption \(P\) led to a contradiction, we conclude that \(\neg P\) must be true.

This establishes the validity of Modus Tollens: If \(P→Q\) is true and \(\neg Q\) is true, then \(\neg P\) is also true.

Applied Example

To illustrate how proof by contradiction works in an applied setting, consider proving that \(2\sqrt{2}\) is irrational.

We define the following propositions:

• \(R\): “\(2\sqrt{2}\) is irrational.”
• \(E_p\): “\(p\) is even.”
• \(E_q\): “\(q\) is even.”

1. Assume the opposite: Suppose that \(R\) is false, meaning \(2\sqrt{2}\) is rational and can be written as a fraction \(\frac{p}{q}\) in lowest terms, where \(p\) and \(q\) are integers with no common factors other than \(1\).
2. Square both sides: \(2 = \frac{p^2}{q^2}\), which implies \(2q^2 = p^2\).
3. Conclude that \(p^2\) is even: Since \(2q^2 = p^2\), \(p^2\) is divisible by \(2\), which means \(p\) must also be even. That is, \(E_p\) holds.
4. Write \(p\) as \(p=2k\) for some integer \(k\), then substitute: \(2q^2 = (2k)^2 = 4k^2\), so \(q^2 = 2k^2\).
5. Conclude that \(q^2\) is even, which implies that \(q\) is even, i.e., \(E_q\) holds.
6. Contradiction: Both \(p\) and \(q\) are even, contradicting the assumption that \(\frac{p}{q}\) was in lowest terms. That is, we have derived \(E_p \land E_q\), which contradicts the assumption that \(\neg (E_p \land E_q)\) held under \(R\).
7. Conclusion: Since assuming \(\neg R\) led to a contradiction, we conclude that \(R\) must be true. Therefore, \(2\sqrt{2}\) is irrational.

Proof by contradiction is a widely used technique, particularly in theoretical mathematics, number theory, and logic.

Resolution

Resolution is a proof technique commonly used in automated theorem proving and logic programming. It is based on the idea of refutation: to prove that a statement is true, we assume its negation and derive a contradiction using a systematic process.

Resolution operates within conjunctive normal form (CNF), where statements are expressed as a conjunction of disjunctions (i.e., sets of clauses). The resolution rule allows us to eliminate variables step by step to derive contradictions.

The Resolution Rule:

If we have two clauses:

• \(P \lor A\)
• \(\neg P \lor B\)

We can resolve them to infer a new clause:

• \(A \lor B\)

By eliminating \(P\), we combine the remaining parts of the clauses.

Example:

Suppose we have the following premises:

1. “Alice studies or Bob is happy.” \(S \lor H\)
2. “Alice does not study or Bob goes to the gym.” \(\neg S \lor G\)
3. “Bob does not go to the gym.” \(\neg G\)

We wish to determine whether Bob is happy (i.e., prove \(H\)).

Step 1: Apply Resolution

• From (2) and (3), resolve on \(G\): \(\neg S \lor G\) and \(\neg G\) produce \(\neg S\).
• From (1) and \(\neg S\), resolve on \(S\): \(S \lor H\) and \(\neg S\) produce \(H\).

Thus, we have derived \(H\), proving that Bob is happy.

Summary

• Proof by contradiction is a classical method that assumes the negation of a statement and derives a contradiction, proving that the statement must be true.
• Resolution is a formal proof technique used in logic and computer science, particularly in automated reasoning.

Both methods are powerful tools in mathematical logic, each serving distinct purposes in different areas of theoretical and applied reasoning.

Next Steps

Now that we have covered fundamental and advanced proof techniques in propositional logic, in the next post of this thread I will talk about the Limitations of Propositional Logic.