6. World 6: Equivalence and Truth🔗

Two more connectives, and four new rules:

P ↔ Q (“P if and only if Q”) is an equivalence. ↔-introduction (↔I) proves it from the two implications P → Q and Q → P. ↔-elimination uses it: ↔E₁ forwards, from P to Q, and ↔E₂ backwards, from Q to P. In Lean: Iff.intro, Iff.mp and Iff.mpr.
⊤ (“true”, in Lean True) always holds: ⊤-introduction (⊤I) proves it, without an input. In Lean: trivial.

In Lean, ↔ binds less strongly than →: P → Q ↔ R means (P → Q) ↔ R. Here such brackets are shown anyway. The levels come from the Lean course; the last ones need TND.

Zwei weitere Verknüpfungen und vier neue Regeln:

P ↔ Q („P genau dann, wenn Q“) ist eine Äquivalenz. Die ↔-Einführung (↔I) beweist sie aus den zwei Implikationen P → Q und Q → P. Die ↔-Beseitigung verwendet sie: ↔E₁ vorwärts, von P nach Q, und ↔E₂ rückwärts, von Q nach P. In Lean: Iff.intro, Iff.mp und Iff.mpr.
⊤ („wahr“, in Lean True) gilt immer: Die ⊤-Einführung (⊤I) beweist es, ohne Eingang. In Lean: trivial.

In Lean bindet ↔ schwächer als →: P → Q ↔ R bedeutet (P → Q) ↔ R. Hier werden solche Klammern trotzdem gezeigt. Die Levels stammen aus dem Lean-Kurs; die letzten brauchen TND.

Your first ↔I: an equivalence is two implications.

Dein erstes ↔I: Eine Äquivalenz besteht aus zwei Implikationen.

↔E₁ uses an equivalence forwards.

↔E₁ verwendet eine Äquivalenz vorwärts.

… and ↔E₂ backwards.

… und ↔E₂ rückwärts.

No assumptions. Each direction is an →I.

Keine Annahmen. Jede Richtung ist ein →I.

Symmetry of ↔.

Symmetrie von ↔.

Transitivity of ↔.

Transitivität von ↔.

↔ really is a conjunction of two implications.

↔ ist wirklich eine Konjunktion zweier Implikationen.

The puzzle from world 2, with a new goal.

Das Rätsel aus Welt 2, mit einem neuen Ziel.

Replace P by Q inside a conjunction.

Ersetze P durch Q in einer Konjunktion.

⊤ (in Lean True) always holds: ⊤I proves it, with no input.

⊤ (in Lean True) gilt immer: ⊤I beweist es, ganz ohne Eingang.

⊤ (in Lean True) always holds: the block ⊤I proves it, without any input.

⊤ (in Lean True) gilt immer: Der Block ⊤I beweist es, ganz ohne Eingang.

An assumption that always holds tells you nothing.

Eine Annahme, die immer gilt, sagt nichts.

In Lean: ¬True ↔ False.

In Lean: True ↔ ¬False.

¬P says exactly that P is false.

¬P sagt genau, dass P falsch ist.

Both sides are false.

Beide Seiten sind falsch.

Commutativity of ∨, both directions.

Kommutativität von ∨, beide Richtungen.

Absorption. Here P ∨ P ∧ Q means P ∨ (P ∧ Q).

Absorption. Hier bedeutet P ∨ P ∧ Q dasselbe wie P ∨ (P ∧ Q).

De Morgan: ¬(P ∨ Q) ↔ ¬P ∧ ¬Q.

Distributivity, both directions.

Distributivität, beide Richtungen.

The other distributive law. Lemmas from world 3 may help.

Das andere Distributivgesetz. Hilfssätze aus Welt 3 können helfen.

Classical: double negation, both directions.

Klassisch: doppelte Negation, beide Richtungen.

The De Morgan law that needs TND.

Das De-Morgan-Gesetz, das TND braucht.

An implication is a disjunction in disguise.

Eine Implikation ist eine verkleidete Disjunktion.

Negating an implication.

Eine Implikation verneinen.

If A and B are not equivalent, then A is equivalent to the opposite of B. One direction needs the cases for A.

Wenn A und B nicht äquivalent sind, dann ist A zum Gegenteil von B äquivalent. Eine Richtung braucht die Fälle für A.

The final level: every statement is equivalent to B or to its opposite. The level before helps.

Das letzte Level: Jede Aussage ist zu B oder zu seinem Gegenteil äquivalent. Das Level davor hilft.