Symbolic LogicPredicate Logic: Proofs

Conditional and Indirect Proof with Quantifiers

CP, IP and quantifier negation (QN) work in predicate logic too, as long as each quantifier rule's restrictions are kept.

Not started Jump to practice

Conditional and indirect proof (Nested Subproofs) work in predicate logic too. Combined with the quantifier rules of Proofs with Quantifiers, they prove conclusions that are conditionals or negations, and they often make long proofs short.

Key idea

Use CP to prove a conditional (assume its antecedent) and IP to prove anything by assuming its negation, exactly as before. The quantifier rules keep their restrictions inside subproofs, plus one more: UG may not generalize a variable that is free in an assumption that is still open.

Why it works

Inside a subproof that assumes $Fy$, the variable $y$ is no longer arbitrary: it stands for something assumed to be $F$. Generalizing there would turn "if $y$ is $F$, then …" into a claim about everything, which proves too much. Once the subproof is closed, the assumption has become the antecedent of a conditional, and the variable is arbitrary again, so UG is safe after the CP line.
CP inside a universal proof: UG only after the subproof is closed.

Worked examples

Worked example: CP with quantifiers on both sides

Premise $\forall x(Fx \to Gx)$. Prove $\forall x Fx \to \forall x Gx$.
  1. Assume $\forall x Fx$ (ACP).
  2. UI on the assumption and the premise with $y$: $Fy$, $Fy \to Gy$.
  3. MP: $Gy$. UG: $\forall x Gx$ (allowed: $y$ is not free in the assumption $\forall x Fx$).
  4. CP: $\forall x Fx \to \forall x Gx$.

Answer: Six lines.

Worked example: IP with quantifiers

Premises $\forall x(Fx \to Gx)$ and $\neg \exists x Gx$. Prove $\neg \exists x Fx$.
  1. Assume $\exists x Fx$ (AIP). EI: $Fa$.
  2. UI: $Fa \to Ga$. MP: $Ga$.
  3. QN on premise 2: $\forall x\neg Gx$. UI: $\neg Ga$.
  4. Conj: $Ga \land \neg Ga$. IP: $\neg \exists x Fx$.

Answer: The assumption leads to a contradiction.

Common mistake

Using UG inside a subproof on a variable that is free in the assumption. If line 2 assumes $Fy$, then inside that subproof you may not write $\forall x Gx$ from $Gy$: that would claim everything is $G$ just because the one assumed $F$ thing is. Close the subproof with CP first, then generalize the conditional.

The extra restriction on UG is the only new thing in this lesson. Everything else is the same CP and IP you already know, with quantifier steps inside. It helps to mark, as you go, which variables appear in each open assumption; those are the ones UG must leave alone until the box closes.

EI inside a subproof still needs a new name, one that appears nowhere above it, including in the assumption.

IP is especially handy in predicate logic when the conclusion is a negated quantifier, like $\neg \exists x Fx$: assume the quantifier without the negation, instantiate it, and look for a clash.

  • Conditional conclusion: CP.
  • Negated or stubborn conclusion: IP.
  • Inside the subproof: EI with new names, UI freely.
  • UG only on variables that are not free in an open assumption.

Practice

Pass with 3 right answers, the last 2 in a row. Each right answer earns 3 XP.

Loading practice…

Builds on

Leads to

This is one of the top rungs of Symbolic Logic.

Sources and further reading

  • Patrick J. Hurley and Lori Watson, A Concise Introduction to Logic, 13th ed., section 8.4, Conditional and Indirect Proof
  • forall x: Calgary, an open introduction to formal logic (P. D. Magnus, Tim Button and others; Open Logic Project), chapter on proof strategies for FOL
@teddyrookbook GitHub