Skip to main content
Back to path

Welcome to a Grasp lesson

Create a free account to keep studying and create your own study path.

Lesson 4

Formal Proofs in Propositional Logic

Recommended resources

Welcome to the next lesson in our journey through Discrete Mathematics. In our previous session, we built a crucial skill: translating complex English statements into the precise language of First-Order Logic using predicates and quantifiers. This allows us to capture the meaning of arguments with mathematical rigor. Now, we will learn how to use these logical statements to formally prove or disprove claims.

Today's lesson focuses on constructing formal proofs for logical arguments. This is the heart of mathematical reasoning and a skill frequently tested in GATE. You will learn the "rules of the game" for logic—the valid steps you can take to move from a set of given facts (premises) to a new, logically certain conclusion. We will cover fundamental inference rules like modus ponens and modus tollens, the powerful resolution rule, and two major proof strategies: direct proof and proof by contradiction.

1. The Anatomy of a Formal Proof

Before we start building proofs, we must understand what they are. A formal proof is not a vague essay; it's a structured sequence of statements, starting from a set of assumptions (hypotheses) and ending with a conclusion, where every step is justified by a pre-established rule of logic.

To formalize this, we'll watch a short segment that lays out the definitions of a theorem, a proof, and the valid components you can use to construct one.

BM3. Formal Proofs

This video from MathDoctorBob provides the foundational vocabulary for our lesson. It defines what a proof is and what constitutes a valid step within one.

Please watch the following two segments: First, focus on the definition of a theorem and proof. Understand that a theorem is true if the hypotheses logically imply the conclusion. Next, review the list of valid statements in a proof. These are your building blocks: hypotheses, tautologies, logical equivalences (which we studied in lesson 1.2), and rules of inference.

In essence, a proof is a logical chain. You start with your given hypotheses and apply rules of inference to derive new, true statements. You continue this process until you arrive at the desired conclusion.

2. The Toolkit: Rules of Inference

Rules of inference are the templates for valid logical deduction. They are your primary tools for building the steps of a proof. Each rule is a simple, tautological implication that allows you to deduce a conclusion from a set of premises.

The following video from Neso Academy provides a concise tour of the most common inference rules you'll need for GATE.

Rules of Inference - Definition & Types of Inference Rules

This video serves as a reference guide to the fundamental rules of inference. As you watch, I'll list the key rules below. For each rule, the video gives its formal definition and a simple example.

Watch the explanations for each of the following rules. You can navigate the video using its chapter markers or by looking for the title of each rule on the screen. Modus Ponens (The Law of Detachment): If P is true and P → Q is true, then Q must be true. Modus Tollens: If P → Q is true and Q is false (¬Q), then P must be false (¬P). Hypothetical Syllogism: If P → Q and Q → R, then P → R. This is like a chain rule for implications. Disjunctive Syllogism: If P ∨ Q is true and P is false (¬P), then Q must be true. Addition: If P is true, then P ∨ Q is true for any statement Q. Simplification: If P ∧ Q is true, then P is true (and Q is also true). Conjunction: If P is true and Q is true, then P ∧ Q is true. Resolution: If P ∨ Q and ¬P ∨ R are both true, then Q ∨ R must be true. The P and ¬P "cancel out". We will revisit this powerful rule later.

These rules are the bedrock of logical arguments. Let's now see how to assemble them into a complete proof.

3. Strategy 1: Direct Proof

The most straightforward proof strategy is the direct proof. You start with your hypotheses, apply the rules of inference step by step, and march directly toward the conclusion.

Let's walk through an example.
Theorem: Given the hypotheses P, P → Q, and Q → R, prove the conclusion R.

This argument structure is a chain of reasoning. The MathDoctorBob video demonstrates how to formalize this.

BM3. Formal Proofs

This segment demonstrates a simple and clear direct proof using the rules we just learned.

Watch the walkthrough of this first proof example. Notice the structure: List all hypotheses. Use Modus Ponens on P and P → Q to derive Q. Use Modus Ponens again on the newly derived Q and the hypothesis Q → R to derive R. Since R is the conclusion, the proof is complete. The English analogy provided makes the logical flow intuitive: "If I wake up late, I miss the bus. If I miss the bus, I walk to school. I woke up late. Therefore, I walk to school."

Direct proofs for more complex theorems follow the same pattern, though they may require more steps and a wider variety of rules. The key is to see the premises and the conclusion and try to find a path between them using your toolkit of inference rules.

4. Strategy 2: Proof by Contradiction

Sometimes, a direct path from premises to conclusion is hard to find. In these cases, an indirect approach can be much more effective. The most powerful indirect method is proof by contradiction (or reductio ad absurdum).

The logic is as follows:

  1. To prove a conclusion C, you start by assuming the opposite, ¬C.
  2. You add ¬C to your list of hypotheses.
  3. Using this expanded set of statements, you apply the rules of inference until you derive a contradiction—a statement that is always false, like P ∧ ¬P.
  4. Since your initial assumptions led to an absurdity, one of them must be false. Because the original hypotheses are taken as given, the one that must be false is your new assumption, ¬C.
  5. If ¬C is false, then C must be true. The proof is complete.

Let's see the formal justification and an example of this method.

BM3. Formal Proofs

This video first explains the logical basis for proof by contradiction and then applies it to the same theorem we proved directly.

First, watch the segment explaining the logic of contradiction. The key is the logical equivalence: H → C is equivalent to (H ∧ ¬C) → False. Proving that the hypotheses plus the negated conclusion lead to a contradiction is the same as proving the original theorem. Next, see this method in action as the video re-proves the same theorem from before using proof by contradiction. Notice the steps: Assume ¬R (the negation of the conclusion). Use Modus Tollens on ¬R and Q → R to get ¬Q. Use Modus Tollens again on ¬Q and P → Q to get ¬P. Combine ¬P with the original hypothesis P to form the contradiction P ∧ ¬P. Since we reached a contradiction, our assumption ¬R must be false, so R is true.

For many problems in theoretical computer science, especially those involving proofs of non-existence (e.g., "the halting problem is undecidable"), proof by contradiction is the standard and most natural approach.

5. The Resolution Rule Revisited

The Resolution rule deserves special attention because it is a generalization of many other rules and is the foundation for most modern automated theorem provers. For GATE, questions involving resolution are common.

The rule states:

You find a literal and its negation in two different clauses (in CNF) and combine the rest of the clauses.

This single rule is surprisingly powerful. For instance, it can simulate Modus Ponens:

  • Premise 1: P (which is P ∨ F, where F is False)
  • Premise 2: P → Q (which is ¬P ∨ Q)
  • Applying resolution on P and ¬P gives F ∨ Q, which simplifies to Q.

Proof by Resolution Refutation

This is the practical application of proof by contradiction using the resolution rule.

  1. Convert all your premises into Conjunctive Normal Form (CNF). (We covered this in lesson 1.2).
  2. Negate the conclusion you want to prove and convert it to CNF as well.
  3. Combine all these CNF clauses into one big set.
  4. Repeatedly apply the resolution rule to pairs of clauses in the set to generate new clauses.
  5. If you ever derive the empty clause (which represents a contradiction, F), the proof is complete. You have successfully "refuted" the negated conclusion, which means the original conclusion must be true.

Example: Prove R from premises P, P → Q, Q → R.

  1. Premises in CNF:
    • P
    • ¬P ∨ Q
    • ¬Q ∨ R
  2. Negated Conclusion in CNF: ¬R
  3. Set of Clauses: {P, ¬P ∨ Q, ¬Q ∨ R, ¬R}
  4. Apply Resolution:
    • Resolve P and ¬P ∨ Q to get Q.
    • Now our set is {P, ¬P ∨ Q, ¬Q ∨ R, ¬R, Q}.
    • Resolve Q and ¬Q ∨ R to get R.
    • Now our set is {..., Q, R}.
    • Resolve R and ¬R to get the empty clause (contradiction!).

Since we derived the empty clause, the original conclusion R is proven to be a valid deduction.

Conclusion

In this lesson, we have built a formal framework for constructing logical arguments. You now have the essential tools and strategies to validate logical statements, a fundamental skill for many areas of computer science and a high-yield topic for the GATE exam.

Here are the key takeaways:

  • A formal proof is a sequence of statements, each justified by a hypothesis or a rule of inference, that leads from premises to a conclusion.
  • Rules of inference like Modus Ponens and Modus Tollens are the valid deductive steps.
  • A direct proof builds a step-by-step chain from the hypotheses directly to the conclusion.
  • A proof by contradiction assumes the conclusion is false and shows that this assumption leads to a logical impossibility.
  • Resolution is a powerful, general rule that can be used systematically to prove theorems by refutation, forming the basis of automated reasoning systems.

We have now concluded our deep dive into logic. The rigorous, step-by-step thinking you've honed here will be invaluable as we move into the next topic of this module: Sets and Relations. There, we will apply these same principles of formal reasoning to prove properties about collections of objects and the relationships between them.