4. World 4: Falsity and Negation
The statement ⊥ (“falsity”) can never be true; in Lean it is called False. One new rule:
-
⊥-elimination (⊥E): from
⊥you may conclude anything. (In Lean:False.elim.)
There is no extra rule for negation: “not A” is written A → ⊥, “from A follows something
impossible”. Lean writes ¬A for it, and ¬A really is defined as A → False. So to prove
A → ⊥ you use →I, and A → ⊥ together with A gives ⊥ by →E.
Die Aussage ⊥ („Falsum“) kann nie wahr sein; in Lean heißt sie False. Eine neue Regel:
-
⊥-Beseitigung (⊥E): Aus
⊥darfst du alles folgern. (In Lean:False.elim.)
Für die Negation gibt es keine eigene Regel: „nicht A“ wird A → ⊥ geschrieben, „aus A folgt
etwas Unmögliches“. Lean schreibt dafür ¬A, und ¬A ist tatsächlich als A → False definiert.
Um A → ⊥ zu beweisen, verwendest du also →I, und A → ⊥ zusammen mit A ergibt ⊥ mit →E.
From something impossible, anything follows.
Aus etwas Unmöglichem folgt alles.
Two goals, one assumption.
Zwei Ziele, eine Annahme.
An “or” with something impossible.
Ein „oder“ mit etwas Unmöglichem.
And back: one of the two cases cannot happen.
Und zurück: Einer der beiden Fälle kann nicht eintreten.
No new rule needed.
Keine neue Regel nötig.
No assumptions at all.
Gar keine Annahmen.
If A implies B, then “not B” implies “not A”. Here (B → ⊥) → A → ⊥ means
(B → ⊥) → (A → ⊥).
Wenn A die Aussage B impliziert, dann impliziert „nicht B“ auch „nicht A“. Hier bedeutet
(B → ⊥) → A → ⊥ dasselbe wie (B → ⊥) → (A → ⊥).
If neither A nor B …
Wenn weder A noch B …
… and back.
… und zurück.
If one of the two is false, then not both are true.
Wenn eine der beiden falsch ist, dann sind nicht beide wahr.
Three negations are as good as one.
Drei Negationen sind so gut wie eine.
Case by case.
Fall für Fall.
Chain the implications.
Verkette die Implikationen.
Three cases this time.
Diesmal drei Fälle.
From a contradiction, anything follows.
Aus einem Widerspruch folgt alles.
Sheet 01-d. In Lean: P → ¬¬P.
Blatt 01-d. In Lean: P → ¬¬P.
P and ¬P never hold together.
P und ¬P gelten nie zusammen.
If P implies both Q and ¬Q, then P is false.
Wenn P sowohl Q als auch ¬Q impliziert, ist P falsch.
Sheet 01-f: one of the two, and not the second.
Blatt 01-f: eines von beiden, und das zweite nicht.
If P holds and Q does not, then P → Q is false.
Wenn P gilt und Q nicht, ist P → Q falsch.
The final level of the world: it is impossible that both A and “not A” are false. Note
A ∨ (A → ⊥) → ⊥ means (A ∨ (A → ⊥)) → ⊥.
Das letzte Level der Welt: Es ist unmöglich, dass sowohl A als auch „nicht A“ falsch
sind. Beachte: A ∨ (A → ⊥) → ⊥ bedeutet (A ∨ (A → ⊥)) → ⊥.