8. World 8: Quantifiers🔗

Statements about objects: P a says that the object a has the property P, R a b that a and b are in the relation R. Four new rules:

∀-elimination (∀E): from ∀ x, ?1 x you get ?1 ?2 for any object ?2. In Lean: h a.
∀-introduction (∀I): to prove ∀ x, ?1 x, prove ?1 c₁ for its eigenvariable c₁, an arbitrary object. In Lean: fun c₁ => ….
∃-introduction (∃I): from ?1 ?2 for some object ?2 you get ∃ x, ?1 x. In Lean: ⟨a, …⟩.
∃-elimination (∃E): from ∃ x, ?1 x you may conclude ?2 if you can prove it with the hypothesis ?1 c₁, where the eigenvariable c₁ is the object that exists. In Lean: Exists.elim h (fun c₁ h₁ => …).

An eigenvariable must stay arbitrary: it may not appear in the conclusion of its block, nor in an assumption that the proof uses. If it does, its block gets a ⚠. As in Lean with Inhabited, there is always at least one object; an object that is not determined appears in Lean as default.

Aussagen über Objekte: P a sagt, dass das Objekt a die Eigenschaft P hat, R a b, dass a und b in der Beziehung R stehen. Vier neue Regeln:

∀-Beseitigung (∀E): Aus ∀ x, ?1 x bekommst du ?1 ?2 für ein beliebiges Objekt ?2. In Lean: h a.
∀-Einführung (∀I): Um ∀ x, ?1 x zu beweisen, beweise ?1 c₁ für seine Eigenvariable c₁, ein beliebiges Objekt. In Lean: fun c₁ => ….
∃-Einführung (∃I): Aus ?1 ?2 für ein Objekt ?2 bekommst du ∃ x, ?1 x. In Lean: ⟨a, …⟩.
∃-Beseitigung (∃E): Aus ∃ x, ?1 x darfst du ?2 folgern, wenn du es mit der Annahme ?1 c₁ beweisen kannst; die Eigenvariable c₁ ist das Objekt, das existiert. In Lean: Exists.elim h (fun c₁ h₁ => …).

Eine Eigenvariable muss beliebig bleiben: Sie darf weder in der Folgerung ihres Blocks vorkommen noch in einer Annahme, die der Beweis verwendet. Sonst bekommt ihr Block ein ⚠. Wie in Lean mit Inhabited gibt es immer mindestens ein Objekt; ein Objekt, das nicht festgelegt ist, erscheint in Lean als default.

Your first ∀E: what holds for all x holds for a.

Dein erstes ∀E: Was für alle x gilt, gilt auch für a.

For two objects.

Für zwei Objekte.

Your first ∃I: a is an example.

Dein erstes ∃I: a ist ein Beispiel.

∃I: to prove ∃ x, P x, give an example. From P a you get ∃ x, P x.

∃I: Um ∃ x, P x zu beweisen, gib ein Beispiel an. Aus P a bekommst du ∃ x, P x.

No object is named. Here (as in Lean with Inhabited) there is always at least one.

Kein Objekt hat einen Namen. Hier gibt es (wie in Lean mit Inhabited) immer mindestens eines.

A does not depend on x.

A hängt nicht von x ab.

Your first ∃E. Its eigenvariable c₁ is the object that exists; its hypothesis is A.

Dein erstes ∃E. Seine Eigenvariable c₁ ist das Objekt, das existiert; seine Annahme ist A.

∃E: from ∃ x, A you may use the hypothesis A about an object c₁ that exists, the block's eigenvariable. Nothing else is known about c₁: it must not appear in the goal.

∃E: Aus ∃ x, A darfst du die Annahme A über ein Objekt c₁ verwenden, das existiert, die Eigenvariable des Blocks. Sonst ist über c₁ nichts bekannt: Es darf nicht im Ziel vorkommen.

Your first ∀I: prove A ∧ P c₁ for an arbitrary c₁.

Dein erstes ∀I: Beweise A ∧ P c₁ für ein beliebiges c₁.

∀I: to prove ∀ x, A ∧ P x, prove A ∧ P c₁ for an arbitrary object c₁, the block's eigenvariable. Arbitrary means: c₁ must not appear in an assumption that you use.

∀I: Um ∀ x, A ∧ P x zu beweisen, beweise A ∧ P c₁ für ein beliebiges Objekt c₁, die Eigenvariable des Blocks. Beliebig heißt: c₁ darf in keiner Annahme vorkommen, die du verwendest.

Two ∀ statements into one.

Zwei ∀-Aussagen werden eine.

A case distinction, and in each case an ∃E.

Eine Fallunterscheidung, und in jedem Fall ein ∃E.

Here ∀ x, P x → A means ∀ x, (P x → A).

Hier bedeutet ∀ x, P x → A dasselbe wie ∀ x, (P x → A).

First ∀E, then →E.

Erst ∀E, dann →E.

Swap two ∀.

Vertausche zwei ∀.

Swap two ∃.

Vertausche zwei ∃.

∃∀ gives ∀∃. (The other way round it does not work: try it, and watch the ⚠.)

Aus ∃∀ folgt ∀∃. (Umgekehrt geht es nicht: Probiere es, und achte auf das ⚠.)

In Lean: from ∀ x, P x follows ¬∃ x, ¬P x.

In Lean: Aus ∀ x, P x folgt ¬∃ x, ¬P x.

If no object has P, then every object lacks it. This direction needs no TND.

Wenn kein Objekt P hat, dann fehlt es jedem. Diese Richtung braucht kein TND.

And back, also without TND: “there is none” and “every one is not” are the same.

Und zurück, ebenfalls ohne TND: „es gibt keines“ und „jedes nicht“ sind dasselbe.

The other pair needs classical logic: if no object lacks P, every object has it. For P c₁, assume the opposite (RAA).

Das andere Paar braucht klassische Logik: Wenn keinem Objekt P fehlt, hat jedes Objekt P. Für P c₁ nimm das Gegenteil an (RAA).

The levels before went without TND or RAA: (∃ x, P x) → ⊥ and ∀ x, P x → ⊥ say the same. With the opposite put the other way round, (∃ x, P x → ⊥) → ⊥ and ∀ x, P x, one direction needs classical logic: from “no object lacks P” one only gets P c₁ by contradiction.

Die Levels davor gingen ohne TND oder RAA: (∃ x, P x) → ⊥ und ∀ x, P x → ⊥ sagen dasselbe. Mit der Verneinung andersherum, (∃ x, P x → ⊥) → ⊥ und ∀ x, P x, braucht eine Richtung klassische Logik: Aus „keinem Objekt fehlt P“ bekommt man P c₁ nur durch einen Widerspruch.

Classical too: if not every object lacks P, then one has it, though no one says which.

Ebenfalls klassisch: Wenn nicht jedem Objekt P fehlt, dann hat es eines, auch wenn keiner sagt, welches.

Classical: if not all x have P, then one does not. Use TND twice.

Klassisch: Wenn nicht alle x die Eigenschaft P haben, dann eines nicht. Verwende TND zweimal.

A does not depend on x, so it can be taken out of the ∀. Distinguish the cases for A.

A hängt nicht von x ab, also kann man es aus dem ∀ herausziehen. Unterscheide die Fälle für A.

If A holds, take the object that A gives; if not, any object will do.

Wenn A gilt, nimm das Objekt, das A liefert; wenn nicht, tut es jedes Objekt.

The final level, and a hard one. Distinguish the cases ∀ x, P x and its negation.

Das letzte Level, und ein schweres. Unterscheide die Fälle ∀ x, P x und seine Negation.