2. World 2: Implication🔗

Two new rules, for implication:

→-elimination (→E) uses A → B together with A to get B.
→-introduction (→I) proves A → B. It gives you a local hypothesis A: the blue dot with a purple ring on top of the block. Like every blue dot it is something you have, which you may use to prove the block's own input B. Everything that uses the hypothesis must lead back into that input; a dashed box shows this region. Using the hypothesis for anything outside the box is not allowed (⚠).

Zwei neue Regeln, für die Implikation:

→-Beseitigung (→E) macht aus A → B zusammen mit A die Aussage B.
→-Einführung (→I) beweist A → B. Sie gibt dir eine lokale Annahme A: den blauen Punkt mit lila Ring oben am Block. Wie jeder blaue Punkt ist sie etwas, das du hast, und du darfst sie verwenden, um den eigenen Eingang B des Blocks zu beweisen. Alles, was die Annahme verwendet, muss in diesen Eingang zurückführen; ein gestrichelter Kasten zeigt diesen Bereich. Die Annahme außerhalb des Kastens zu verwenden, ist nicht erlaubt (⚠).

Your first →E: from A → B and A you get B.

Dein erstes →E: Aus A → B und A bekommst du B.

Two steps.

Zwei Schritte.

More assumptions than you need.

Mehr Annahmen, als du brauchst.

Is the implication needed at all?

Braucht man die Implikation überhaupt?

Your first →I. Add an →I block for the goal; then use its local hypothesis A (the blue dot with the purple ring), and lead what you get from it into the block's input.

Dein erstes →I. Nimm einen →I-Block für das Ziel; verwende dann seine lokale Annahme A (den blauen Punkt mit dem lila Ring) und führe, was du daraus bekommst, in den Eingang des Blocks.

To prove A → C, use →I. On top it has a compartment ?1 ⇒ ?2: the local hypothesis ?1 (the blue dot with the purple ring) is something you have, but only for proving the input ?2 next to it. Whatever uses it lies in a dashed box.

Um A → C zu beweisen, nimm →I. Oben hat er ein Fach ?1 ⇒ ?2: Die lokale Annahme ?1 (der blaue Punkt mit lila Ring) ist etwas, das du hast, aber nur, um den Eingang ?2 daneben zu beweisen. Was sie verwendet, liegt in einem gestrichelten Kasten.

The hypothesis A may be used more than once.

Die Annahme A darf mehrfach verwendet werden.

No assumptions at all.

Gar keine Annahmen.

Combine ∧ and →.

Kombiniere ∧ und →.

In Lean, A ∧ B → C means (A ∧ B) → C.

In Lean bedeutet A ∧ B → C dasselbe wie (A ∧ B) → C.

The hypothesis need not be used.

Die Annahme muss nicht verwendet werden.

Two →I blocks, one inside the other. A → B → C means A → (B → C).

Zwei →I-Blöcke, einer im anderen. A → B → C bedeutet A → (B → C).

And back.

Und zurück.

Take apart, apply, put together.

Zerlegen, anwenden, zusammensetzen.

If P holds, it holds under any further assumption.

Wenn P gilt, dann auch unter jeder weiteren Annahme.

And the same with the second hypothesis.

Und dasselbe mit der zweiten Annahme.

Modus ponens as a statement of its own.

Der Modus ponens als eigene Aussage.

Supply the premises in the other order.

Liefere die Voraussetzungen in der anderen Reihenfolge.

Transitivity, with no assumptions at all: three →I blocks.

Transitivität, ganz ohne Annahmen: drei →I-Blöcke.

Nothing new, only →I and →E, but the proof of P is needed twice.

Nichts Neues, nur →I und →E, aber der Beweis von P wird zweimal gebraucht.

A puzzle. Not all assumptions are needed: find a path from T to R.

Ein Rätsel. Nicht alle Annahmen werden gebraucht: Finde einen Weg von T nach R.

Three premises one after the other, or all three at once.

Drei Voraussetzungen nacheinander oder alle drei auf einmal.

The final level of the world.

Das letzte Level der Welt.