Sign in

Libre University uses your GitHub account. Signing in is only needed to sit a final test, so the score is kept on your profile.

Assumptions, conditional proof and reductio

The previous lesson ended with a system that could take conditionals, disjunctions and negations apart and had no way to build any of them, so it could not even derive PP.

Everything missing has one cause. To prove a conditional you must reason from its antecedent without believing it. To prove a negation you must assume the thing you are denying and watch it fail. To use a disjunction you must take each case in turn. All three are suppositions, and a supposition is dangerous: whatever is proved under it is proved only under it, and letting such a line escape would let anything be proved from nothing. The bookkeeping that keeps suppositions in their place is what this lesson adds, and with it the system becomes complete.

Suppositions and discharge

A subproof begins with an assumption, made freely and with no justification, and runs until it is closed. Lines inside it are written shifted to the right, and here they carry a bar. When the subproof is closed, the assumption is discharged: it is no longer in force, and the conclusion drawn from it survives only in a form that mentions it explicitly.

The scope rule is absolute. Once a subproof is closed, none of its lines may be cited again, and only the conclusion the closing rule produces remains available. A line proved under an assumption depends on that assumption, and dragging it out into the main proof would be exactly the error of treating a supposition as a fact.

Everything else stays as before. Lines are numbered, each carries its justification, and a checker verifies the derivation without needing to know how it was found.

Conditional proof

Conditional introduction (I): assume φ, derive ψ, close the subproof, and write φψ, citing the range of lines.

That is what a mathematician means by "suppose x is even" at the start of a proof, and it is why the technique is called conditional proof. Its soundness is the conditional's table read from the other side: the conditional can only fail when the antecedent is true and the consequent false, and the subproof shows that if the antecedent holds the consequent follows, so that row is unreachable.

From PQ and QR, derive PR, which is hypothetical syllogism proved rather than assumed.

#FormulaJustification
1PQpremise
2QRpremise
3Passumption
4Q1, 3, E
5R2, 4, E
6PR3-5, I

Line 6 is the first line in the whole subject that depends on no assumption beyond the premises, having been built out of lines that did. Note also that P, Q and R never had to be true: the derivation shows what would follow if P were.

Subproofs nest, which is how a conditional with a conditional inside it gets proved. From no premises at all, derive P(Q(PQ)).

#FormulaJustification
1Passumption
2│ │ Qassumption
3│ │ PQ1, 2, I
4Q(PQ)2-3, I
5P(Q(PQ))1-4, I

Line 3 cites line 1, which is legitimate because the outer subproof is still open there. The reverse never is: after line 5 nothing may cite lines 1 to 4.

Example. Derive PP from no premises.

#FormulaJustification
1Passumption
2PP1-1, I

Two lines, and the subproof does no work at all: assume P, and P is immediately available, so the conditional follows. The tautology that defeated the previous lesson's system falls out the moment assumptions are allowed.

Now you. Derive P(QR) from the single premise (PQ)R.

Answer
#FormulaJustification
1(PQ)Rpremise
2Passumption
3│ │ Qassumption
4│ │ PQ2, 3, I
5│ │ R1, 4, E
6QR3-5, I
7P(QR)2-6, I

This is the exportation equivalence of the fifth lesson, now derived instead of tabulated.

Reductio ad absurdum

Negation introduction (¬I): assume φ, derive a contradiction, close the subproof, and write ¬φ. A contradiction here means any formula together with its negation, or the symbol used to mark that they have both appeared.

The reasoning is that a set of true statements cannot contain a contradiction, so if adding φ produced one, φ was not true. This is reductio ad absurdum, in use since Euclid, and the twelfth lesson of Mathematical Foundations used it to show that no fraction squares to 2.

From PQ and P¬Q, derive ¬P.

#FormulaJustification
1PQpremise
2P¬Qpremise
3Passumption
4Q1, 3, E
5¬Q2, 3, E
64, 5
7¬P3-6, ¬I

The mirror-image rule is the one that makes the system classical. Indirect proof, or negation elimination: assume ¬φ, derive a contradiction, and conclude φ. Strictly this is ¬I followed by double negation elimination, and it is worth naming separately because it is the standard way to prove something positive that resists a direct attack.

One further rule follows from contradiction and is worth stating because it startles people: from , anything at all may be inferred. This is ex falso quodlibet, and it is the derivation-level version of the third lesson's result that an inconsistent set entails everything. The system is not being reckless; it is recording that once your premises contradict each other, they have stopped constraining anything.

Example. Derive ¬Q from ¬(PQ) and P.

#FormulaJustification
1¬(PQ)premise
2Ppremise
3Qassumption
4PQ2, 3, I
51, 4
6¬Q3-5, ¬I

The shape is worth memorising, since it is how nearly every negative conclusion is reached: assume the positive version, build the thing that was denied, and collect the contradiction.

Now you. Derive ¬P from P(Q¬Q).

Answer
#FormulaJustification
1P(Q¬Q)premise
2Passumption
3Q¬Q1, 2, E
4Q3, E
5¬Q3, E
64, 5
7¬P2-6, ¬I

Argument by cases

Disjunction elimination (E): given φψ, if a subproof assuming φ reaches χ and another assuming ψ also reaches χ, then χ follows.

This is the rule the previous lesson could not state, and it is the one that makes a disjunction useful rather than merely true. Its soundness is direct: any row making the disjunction true makes at least one disjunct true, and either way χ comes out true.

From PQ, PR and QR, derive R.

#FormulaJustification
1PQpremise
2PRpremise
3QRpremise
4Passumption
5R2, 4, E
6Qassumption
7R3, 6, E
8R1, 4-5, 6-7, E

Everyday reasoning uses this constantly without naming it. A doctor who says the pain is either a strain or a stress fracture, and that either way the treatment is rest, has argued by cases, and the conclusion holds without ever settling which case is real.

Proving what looks unprovable

With assumptions available, tautologies can be derived from no premises whatever, and the case worth working through is the law of excluded middle, P¬P, since there is nothing to start from and no obvious first move.

#FormulaJustification
1¬(P¬P)assumption
2│ │ Passumption
3│ │ P¬P2, I
4│ │ 1, 3
5¬P2-4, ¬I
6P¬P5, I
71, 6
8¬¬(P¬P)1-7, ¬I
9P¬P8, ¬¬E

The despised disjunction introduction of the previous lesson does the work twice, at lines 3 and 6, which is what it is for. And line 9 is where the system commits itself: intuitionistic logic, developed by Brouwer and formalised by Heyting around 1930, keeps every other rule here and rejects double negation elimination, with the result that P¬P is not provable in it. That is not a fringe position, since it corresponds to demanding a construction rather than a mere absence of contradiction, and it is the logic underlying proof assistants. Classical logic, used throughout this course, accepts line 9.

Example. Derive (PQ)(PR) from P(QR).

Argue by cases on the premise. If P, then PQ and PR both follow by disjunction introduction, so the conjunction follows. If QR, then Q gives PQ and R gives PR, so the conjunction follows again. Both cases reach the same formula, so disjunction elimination delivers it. That is the distribution law of the fifth lesson, proved rather than tabulated, and the proof works for reasons a reader can follow, which the table never gave.

Now you. Show, in outline, how to derive ¬P¬Q from ¬(PQ).

Answer

Indirect proof. Assume ¬(¬P¬Q). Assume P: then assume Q, giving PQ and a contradiction with the premise, so ¬Q, so ¬P¬Q by I, contradicting the outer assumption. So ¬P, which gives ¬P¬Q again and contradicts the outer assumption once more. Therefore the outer assumption fails and ¬P¬Q follows by double negation elimination. The shape is the same as the excluded middle derivation, which is no accident: this half of De Morgan is not provable intuitionistically either.

Soundness and completeness

There are now two relations between premises and conclusion. Γφ says no valuation makes the premises true and the conclusion false. Γφ says a derivation exists. One is about tables, the other about writing lines on a page, and there is no reason in advance for them to agree.

They agree exactly, and the two halves have names.

Soundness: if Γφ then Γφ. Every derivable conclusion is genuinely entailed. The proof is an induction on the length of the derivation, and the work is the check already done for each rule as it was introduced: no rule takes you from true lines to a false one, so nothing false can be reached. Soundness is what makes a derivation worth anything, since without it the rules could prove nonsense.

Completeness: if Γφ then Γφ. Every valid argument has a derivation. This one is not obvious at all, since it says that a fixed handful of rules suffices for every valid argument in the language, including ones nobody has thought of. Emil Post established it for propositional logic in 1921, and Gödel proved the far harder version for predicate logic in 1929, which the eleventh lesson returns to.

Together they say and pick out the same pairs, so the semantic notion of validity and the syntactic notion of provability coincide. That licenses the practical habit of using whichever is easier: a countermodel to show invalidity, a derivation to show validity, and no worry that the two methods might disagree.

Propositional logic is therefore finished, and its limits are exact: sound, complete, and decidable by a table that is exponentially large. What it cannot do is see inside an atom. "All men are mortal, Socrates is a man, so Socrates is mortal" is three unrelated letters to it, and the most famous valid argument in the subject comes out invalid. Fixing that means breaking sentences open, and it is the next lesson.