3. World 3: Disjunction🔗

Three new rules, for disjunction (∨, “or”):

∨-introduction comes in two forms: ∨I₁ makes A ∨ B from A, ∨I₂ makes A ∨ B from B.
∨-elimination (∨E) is a case distinction. From A ∨ B you may conclude C if you can prove C twice: once using the local hypothesis A, once using B. Each hypothesis (a blue dot with a purple ring) sits next to the input it belongs to, and may only be used to prove that input.

In Lean, ∨I₁ and ∨I₂ are Or.inl and Or.inr, and ∨E is Or.elim.

Drei neue Regeln, für die Disjunktion (∨, „oder“):

Die ∨-Einführung gibt es in zwei Formen: ∨I₁ macht aus A die Aussage A ∨ B, ∨I₂ macht aus B die Aussage A ∨ B.
Die ∨-Beseitigung (∨E) ist eine Fallunterscheidung. Aus A ∨ B darfst du C folgern, wenn du C zweimal beweisen kannst: einmal mit der lokalen Annahme A, einmal mit B. Jede Annahme (ein blauer Punkt mit lila Ring) sitzt neben dem Eingang, zu dem sie gehört, und darf nur für diesen Eingang verwendet werden.

In Lean heißen ∨I₁ und ∨I₂ Or.inl und Or.inr, und ∨E heißt Or.elim.

Your first ∨. One of the two assumptions is enough.

Dein erstes ∨. Eine der beiden Annahmen genügt.

B need not be true at all.

B muss gar nicht wahr sein.

And from the other side.

Und von der anderen Seite.

Either way.

So oder so.

Your first ∨E: prove B ∨ A in the case A and in the case B.

Dein erstes ∨E: Beweise B ∨ A im Fall A und im Fall B.

∨E is a case distinction. From A ∨ B, prove the goal twice: in the compartment ?1 ⇒ ?3 with the hypothesis A, and in ?2 ⇒ ?3 with the hypothesis B.

∨E ist eine Fallunterscheidung. Aus A ∨ B beweist du das Ziel zweimal: im Fach ?1 ⇒ ?3 mit der Annahme A und im Fach ?2 ⇒ ?3 mit der Annahme B.

A ∨ B ∨ C means A ∨ (B ∨ C). One case distinction inside another.

A ∨ B ∨ C bedeutet A ∨ (B ∨ C). Eine Fallunterscheidung in einer anderen.

“And” is stronger than “or”.

„Und“ ist stärker als „oder“.

Sheet 01-c. P ∨ Q ∨ R means P ∨ (Q ∨ R).

Blatt 01-c. P ∨ Q ∨ R bedeutet P ∨ (Q ∨ R).

Any one of the three will do.

Irgendeine der drei genügt.

Associativity of ∨: the other direction of level 6.

Assoziativität von ∨: die andere Richtung von Level 6.

Absorption, one direction: in both cases you have P.

Absorption, eine Richtung: In beiden Fällen hast du P.

In Lean, ∧ binds more strongly than ∨: A ∧ B ∨ C is (A ∧ B) ∨ C.

In Lean bindet ∧ stärker als ∨: A ∧ B ∨ C ist (A ∧ B) ∨ C.

Distribute C.

Verteile C.

Distributivity, the direction back.

Distributivität, die Richtung zurück.

The other distributive law, back. Two case distinctions, one inside the other.

Das andere Distributivgesetz, zurück. Zwei Fallunterscheidungen, eine in der anderen.

A ∨ B → C means (A ∨ B) → C.

A ∨ B → C bedeutet (A ∨ B) → C.

And back.

Und zurück.

Take apart, then distinguish the cases. S is not needed.

Zerlegen, dann die Fälle unterscheiden. S wird nicht gebraucht.

Weaken a disjunction on both sides at once.

Schwäche eine Disjunktion auf beiden Seiten zugleich ab.

The final level of the world.

Das letzte Level der Welt.