5. World 5: Classical Logic🔗

One more rule, which is different from all the others: it has no input.

Tertium non datur (TND, “a third is not given”, the law of the excluded middle): for every statement A, you may use A ∨ (A → ⊥), “A is true or it is false”.

With the rules so far, this cannot be proved. Logic without it is called intuitionistic, logic with it classical. In Lean, TND is Classical.em; Lean's proofs then use classical logic. Usually you use TND together with ∨E: “Either A holds, or it does not. In the first case …”

Later in this world comes a second rule, the proof by contradiction (RAA, in Lean by_contra): to prove A, assume A → ⊥ and derive ⊥.

Noch eine Regel, die anders ist als alle anderen: Sie hat keinen Eingang.

Tertium non datur (TND, „ein Drittes gibt es nicht“, der Satz vom ausgeschlossenen Dritten): Für jede Aussage A darfst du A ∨ (A → ⊥) verwenden, „A ist wahr oder falsch“.

Mit den bisherigen Regeln lässt sich das nicht beweisen. Logik ohne diese Regel heißt intuitionistisch, Logik mit ihr klassisch. In Lean heißt TND Classical.em; Leans Beweise verwenden dann klassische Logik. Meist verwendest du TND zusammen mit ∨E: „Entweder gilt A, oder nicht. Im ersten Fall …“

Später in dieser Welt kommt eine zweite Regel dazu, der Widerspruchsbeweis (RAA, in Lean by_contra): Um A zu beweisen, nimm A → ⊥ an und leite ⊥ her.

Just the new rule.

Nur die neue Regel.

The converse of level 7 of the previous world. Distinguish the cases B and B → ⊥.

Die Umkehrung von Level 7 der letzten Welt. Unterscheide die Fälle B und B → ⊥.

If not both are true, then one of them is false.

Wenn nicht beide wahr sind, ist eine von beiden falsch.

Double negation: if A is not false, it is true.

Doppelte Negation: Wenn A nicht falsch ist, ist es wahr.

An implication as an “or”.

Eine Implikation als „oder“.

New: a proof by contradiction (RAA, in Lean by_contra h). To prove A, assume A → ⊥ (the purple hypothesis) and derive ⊥. It is what you just proved by hand with TND: from (A → ⊥) → ⊥ follows A.

Neu: ein Widerspruchsbeweis (RAA, in Lean by_contra h). Um A zu beweisen, nimm A → ⊥ an (die lila Annahme) und leite ⊥ her. Das ist, was du gerade von Hand mit TND bewiesen hast: Aus (A → ⊥) → ⊥ folgt A.

Tertium non datur, but without the TND block, only with proof by contradiction (RAA). Level 4 went the other way, from TND to ((A → ⊥) → ⊥) → A: the two principles are equally strong.

Tertium non datur, aber ohne den TND-Baustein, nur mit dem Widerspruchsbeweis (RAA). Level 4 ging den umgekehrten Weg, von TND zu ((A → ⊥) → ⊥) → A: Beide Prinzipien sind gleich stark.

Two implications.

Zwei Implikationen.

Peirce's law: no ⊥ in it, and still it needs TND.

Das Gesetz von Peirce: kein ⊥ darin, und trotzdem braucht es TND.

Level 3, with three parts.

Level 3, mit drei Teilen.

Sheet 01-e. Classical: distinguish the cases P and ¬P.

Blatt 01-e. Klassisch: Unterscheide die Fälle P und ¬P.

A statement that follows from its own negation holds.

Eine Aussage, die aus ihrer eigenen Negation folgt, gilt.

An implication as a disjunction.

Eine Implikation als Disjunktion.

One of the two implications always holds. Distinguish the cases for Q.

Eine der beiden Implikationen gilt immer. Unterscheide die Fälle für Q.

The implication distributes over ∨, but only classically. Distinguish the cases for A.

Die Implikation verteilt sich über ∨, aber nur klassisch. Unterscheide die Fälle für A.

The final level: if the implication is false, then A is true and B is false.

Das letzte Level: Wenn die Implikation falsch ist, ist A wahr und B falsch.