Umformungsregeln für Quantoren in der Prädikatenlogik

Hier kommen die Umformungsregeln für Quantoren. Grundregeln und Anwendung auf kompliziertere Beispiele.

Beachte immer, dass einige Umformungen äquivalenz Umformungen sind, und andere dagegen einfache Schlussfolgerungen.
Die Regeln lassen sich nicht nur auf eine gesamte Aussage sondern auch auf Teilausdrücke anwenden (bei den einfachen Schlussfolgerung dort, wo der Kontext ein Schliessen erlaubt)
Für die hier angegebenen Umformungen/Schlussfolgerungen verwende ich ⇒ ⇐ ⇔ , im Gegensatz zu → ← ↔ für Junktoren innerhalb der Ausdrücke.
 ⇔ usw. binden syntaktisch schwächer als die Quantoren und diese schwächer als die normalen Junktoren. a⇔b⇔c  steht für (a⇔b)∧ (b⇔c)
Die Bezeichner φ,ψ, ... stehen für beliebige Ausdrücke, in denen aber keine der evtl. vorangehend quantifizierten Variablen des umzuformenden Teilausdrucks frei vorkommt. Ausdrücke, in denen etwa die Variablen x und z frei vorkommen bezeichne ich mit φ(x,z)

Die Regeln für Quantoren kann man sich im Prinzip aus aussagenlogischen Regeln plausibel machen, wenn man sich vorstellt, dass
∀x:φ(x) bedeutet: φ(x1) ∧ φ(x2) ∧ φ(x3) ... sowie
∃x:φ(x) bedeutet: φ(x1) ∨ φ(x2) ∨ φ(x3) ....  und
ausserdem aussagenlogische Regeln wie (¬a ∧ ¬b ∧ ¬c ...) = ¬(a∨b∨c ...) auch für beliebig (auch unendlich)  viele Teile abc.. gelten.
Mache Autoren schreiben auch ⋀ bzw. ⋁ statt ∀ bzw. ∃.

Alle Quantorenregeln lassen sich aus diesen 4 Regeln ableiten:
∀x:φ⇔φ⇔∃x:φ;  ∀x:φ(x)⇒φ(a)⇒∃x:φ(x)

Kurzschreibweisen für Quantifizierung über Mengen:
∀x∊A:φ(x)  =  ∀x:x∊A → φ(x)
∃x∊A:φ(x)  =  ∃x:x∊A ∧ φ(x)

Die hier angegebenen Umformungsregeln gelten dann immer auch direkt für die Kurzschreibweisen, wenn A nicht leer ist,  d.h man kann in den Regeln  statt ∀x: bzw ∃x austauschen mit ∀x∊A bzw ∃x∊A . Die Kurzschreibweisen brauchen also für die Anwendung der Regeln nicht expandiert werden. Allgemeiner kann statt x∊A auch stehen: x mit der Eigenschaft A. Auch wenn die expandierte Form vorliegt wie "∀x:x∊A → (...)" kann man so tun, als ob dies ein einzelner Quantor ist und sein Gegenstück ist dann "∃x:x∊A ∧ (...) ". Einige Regeln gelten aber nicht, wenn A leer ist. Bei leerer Menge A ist ∀x∊A: ... immer wahr und ∃x∊A: .... immer falsch.
Die Regeln, die auch bei leerer Trägermenge gelten, sind hier mit einem · markiert.

∀x:φ(x) ⇒ ∃x:φ(x) ∀x∊A:φ(x) ⇒ ∃x∊A:φ(x)    gilt nur , wenn A nicht leer ist.
Siehe dazu auch noch im Abschitt "Bedingte Quantoren" am Ende des Papiers.

Dualität von ∀ und  ∃
∃x:φ(x)  ⇔ ¬∀x:¬φ(x) · ∀x:φ(x)  ⇔ ¬∃x:¬φ(x) ·  ¬∃x:φ(x)  ⇔ ∀x:¬φ(x) · ¬∀x:φ(x)  ⇔ ∃x:¬φ(x) ·
Die Anwendung bei mehreren hintereinanderstehenden Quantoren sieht so aus:
¬∀x:∃y:∀z:φ(x,y,z)      ⇔
  ∃x:∀y:∃z:¬φ(x,y,z)
d.h man kann das ¬ durch mehrere Quantoren hindurchschieben und jeder Quantor wird dabei umgedreht.

Hinzufügen und entfernen von Quantoren
φ  ⇔ ∀x: φ  φ ⇔ ∃x:φ wenn x in φ nicht frei vorkommt.
Man darf Ausdrücken also beliebig einen Quantor mit einer neuen Variablen voranstellen, und darf Quantoren entfernen, wenn ihre Variable im inneren Ausdruck nicht vorkommt. (φ ⇒ ∃x∊A:φ und φ ⇐ ∀x∊A:φ gelten nur wenn A≠∅).

Einsetzen der Quantorvariable
∀x:φ(x) ⇒ φ(a) ∃x:φ(x) ⇐ φ(a) a ist ein beliebig gewählter Ausdruck der den selben Typ hat wie x
Wenn wir die Regel anwenden, um x durch a zu ersetzen, darf a global definierte Symbole und Quantorvariablen des Ausdrucks, die hier gültig sind, benutzen. Wenn a Funktionssymbole benutzt, muss sicher sein dass die Argumente im Wertebereich der Funktion liegen; sonst: ∀x:φ(x) ⇒ b∊dom f → φ(f(b)) , ∃x:φ(x) ⇐ b∊dom f ∧ φ(f(b))
Zusammengenommen mit dem Hinzufügen von Quantoren funktioniert auch etwa
∀x:φ(x) ⇒ ∀a:∀b:∀c:φ(ψ(a,b,c))     ; ψ(a,b,c) hat selben Typ wie x; anstelle der ∀'s rechts könnten auch ∃ oder gemischt stehen.
Die ∀ rechts könnten wir auch später wegen (∀⇒∃) umwandeln.
Das funktioniert auch umgekehrt, also z.B. ∃x:∃y:φ(x*y) ⇒ ∃z:φ(z)
Der eingesetzte Term darf also auch neue, freie Variablen enthalten. Für jede dieser Variablen wird dann ein Quantor gleichen Typs an die Stelle des Quantors gesetzt, dessen Variable ersetzt wurde. Siehe dazu auch weiter unter im Abschnitt Einsetzen mit Äquivalenz.
Bei  ∀x∊A:φ(x) darf x nur durch Elemente von A ersetzt werden, anderfalls gillt aber auch ⇒a∊A→φ(a).
∀x:φ(x) ⇒ ∀a:∀b:φ(ψ(a,b)) ∃x:φ(x) ⇐ ∃a:∃b:φ(ψ(a,b))

Herausnehmen und hereinholen von Ausdrücken
a ist ein Ausdruck , in dem x nicht vorkommt.
(∀x:φ(x))∧a  ⇔ ∀x:φ(x)∧a (∃x:φ(x))∧a  ⇔ ∃x:φ(x)∧a ·
(∀x:φ(x))∨a  ⇔ ∀x:φ(x)∨a · (∃x:φ(x))∨a  ⇔ ∃x:φ(x)∨a
(∀x:φ(x))→a  ⇔ ∃x:φ(x)→a (∃x:φ(x))→a  ⇔ ∀x:φ(x)→a ·
(∀x:φ(x))←a  ⇔ ∀x:φ(x)←a · (∃x:φ(x))←a  ⇔ ∃x:φ(x)←a

Die Grundregeln sind hier die in den oberen beiden Zeilen. Daraus lassen sich die anderen Zeilen herleiten
Die Regeln kann man für jeden Junktor j aufstellen , für den sich a j b schreiben lässt als x∧y bzw x∨y, mit x = a oder ¬a und y = b oder ¬b.
Das sind alle effktiv zweistelligen Junktoren ausser ↔ und xor.  Immer wenn auf der Seite des Quantors x bzw y eine Negation erfordert, muss der Quantor umgedreht werden. Wir nennen dies für später eine "negative Seite" des Junktors. Beispiel:
(∀x:φ(x))→a  ⇔   ¬(∀x:φ(x))∨a  ⇔    (∃x:¬φ(x))∨a ⇔   ∃x:(¬φ(x) ∨ a)  ⇔  ∃x:φ(x)→a

Mit den Regeln kann man Ausdrücke von ausserhalb in den Quantor hereinholen und Teilausdrücke innerhalb des Quantors, die sich nicht auf die Variable beziehen, herausnehmen. (Regeln von links nach rechts bzw von recht nach links lesen)
Die Anwendung auf mehrere hintereinanderstende Quantoren sieht so aus:
∀x:∃y:∀z φ(x,y,z)→a  ⇔  (∃x:∀y:∃z:φ(x,y,z))→a
Allgemeiner Tipp: Zusammenhängende gleiche Quantoren können auch immer wie ein grosser Quantor angesehen werden. Bei denen der bisherigen Regeln, die mit ⇔ arbeiten, dürfen auch Ketten die aus verschiedenen Quantoren bestehen, wie ein grosser Quantor betrachtet werden.

Auch lassen sich damit seperat stehende Quantoren so anordnen, dass sie hintereinander stehen:
(∀x:φ(x)) ∨ (∀y:ψ(y)) ⇔ ∀x:(φ(x) ∨ ∀y:ψ(y))  ⇔ ∀x:∀y: φ(x)∨ψ(y).
Für andere Junktoren als ∨ gilt wieder, dass ein Quantor umgedreht werden muss, wenn der Junktor an dessen Position "negativ" ist, z.B.
(∀x:φ(x)) → (∀y:ψ(y)) ⇔ ∃x:∀y: φ(x)→ψ(y).
Bei längeren Ausdrucksketten lassen sich die Quantoren auch in einem Schritt nach vorn ziehen:
( (∀x:φ(x)) → (∀y:ψ(y)) ) → (∀z:χ(z)) ⇔ ∀x:∃y:∀z:(φ(x)→ψ(y))→χ(z)
Dabei wird ∀x 2* umgedreht, weil er 2* auf der linken Seite von → steht. ∀y wird 1* umgedreht.
Die Reihenfolge der Quantoren, die vorn angekommen sind kann beliebig gewählt werden.

In (A) j1 (B) j2 (C) j3 (D) ; (A usw. Sind Ausdrücke die mit Quantoren beginnen können; j sind beliebige Junktoen ausser ↔ und xor; es dürfen zusätzliche Klammern stehen), dürfen wir jeden der Quantoren beliebig weit nach vorn (genauergesagt in Richtung zu Wurzel) schieben, und jedes mal, wenn er dabei eine negative Junktorseite überquert, wird er umgedreht. Umgekehrt dürfen wir in Q:(a j1 b j2 c ...) den Quantor Q zu einem beliebigen der a,b,c hinschieben, mit den selben Regeln fürs Umdrehen, solange die übrigbleibenden a,b,c dabei nicht die Quantorvariable enthalten.
Die Regeln "¬∀ = ∃¬" ergeben sich auch aus diesem Prinzip, wenn wir ¬ als einstelligen Junktor mit negativer Seite auffassen.

Für ↔ und xor gibt es hier keine einfache Umformung. Es kann zuerst a↔b zerlegt werden nach (a→b)∧(b→a) oder (a∧b)∨(¬a∧¬b)
Dann ergibt sich (∀x:φ(x))↔a ⇔ ∀x:∃y:(φ(x)→a)∧(a→φ(y))  ⇔ ∀x:∃y:(φ(x)∧a)∨(¬φ(y)∧¬a))  
bzw                    ∀x:(φ(x)↔a) ⇔ ((∃x:φ(x))→a ) ∧ (a→(∀y:φ(y)))

Bei ∀∊A ... muss man aufpassen dass A nicht leer sein darf, andernfalls, gelten nur die Regeln mit · , das sind die wo ∀ ein ∨ überquert oder ∃ ein ∧ überquert.

Vertauschen von Quantoren
Hintereinanderstehende gleichartige Quantoren dürfen vertauscht werden.
∀x:∀y:φ(x,y) ⇔ ∀y:∀x:φ(x,y) · ∃x:∃y:φ(x,y) ⇔ ∃y:∃x:φ(x,y) ·
daher darf auch in Ketten hintereinanderstehenden gleichartiger Quantoren beliebig vertauscht werden. Es gillt ausserdem : 
∃x:∀y:φ(x,y) ⇒ ∀y:∃x:φ(x,y) · aber die Umkehrung gilt nicht.
auch hier kann wieder mehrfach angewendet werden , wie ∃x:∀y:∃z: ∀t:φ(x,y,z,t)⇒∀x:∀t: ∃y: ∃z:φ(x,y,z,t),  d.h bei vorwärts Schliessen dürfen die ∀ beliebig nach vorn geschoben werden. Beim rückwärts Schliessen können die ∃  nach vorn geschoben werden (bzw die ∀ nach hinten).

Manchmal ist auch der Umkehrschluss zur obigen Regel möglich, nämlich dann wenn x und y unterhalb der Quantoren unabhängig vorkommen.
∃x:∀y:φ(x) j ψ(y) ⇔ ∀y:∃x:φ(x) j ψ(y),  wenn a j b = (*a∨*b)  oder (*a∧*b) mit * = optionales ¬ .; also alle ausser ↔ und xor
(Ergibt sich durch die Regeln zum herein- und herausholen von Ausdrücken)

Vereinigen und aufteilen von Quantoren
(∀x:φ(x)) ∧ (∀y:ψ(y)) ⇔ ∀x:∀y:φ(x)∧ψ(y) ⇔     ∀z:φ(z)∧ψ(z) · (∃x:φ(x)) ∨ (∃y:ψ(y)) ⇔ ∃x:∃y:φ(x)∨ψ(y) ⇔      ∃z:φ(z)∨ψ(z) ·
(∀x:φ(x) ) → (∃y:ψ(y)) ⇔ ∃x:∃y:φ(x)→ψ(y)  ⇔ ∃z:φ(z)→ψ(z) · ← weitere ergeben sich durch Einsetzetn von ¬ in eine Seite von ∧ // ∨
Funktioniert nur mit den hier angegebenen Verknüpfungen; nicht , wenn man etwa ∧ durch ∨ ersetzt.
Bei ∀x∊M: ... klappt es nur, wenn die beiden Quantoren die gleichen Einschränkungen haben. Anderfalls kann man vorher Umwandeln nach ∀x: x∊M → (...). Es gilt auch (∀x∊A:φ(x)) ∧ (∀y∊B:ψ(y)) ⇒ ∀z∊A∩B:φ(z)∧ψ(z), sowie mit  ∃,∨,∪,⇒.  (wegen (a→b)∧(c→d)⇒(a∧c)→(b∧d); nur ⇒, kein ⇔ ).
In Kombination mit den anderen Regeln für das nach vorn ziehen von Quantoren, kann man also bei günstigem Junktor immer gleich vereinigen:
(∀x:∃y:∀z:φ(x,y,z)) ∧ (∀x:∃y:∀z:ψ(x,y,z)) ⇔ ∀x:∃y1:∃y2:∀z:φ(x,y1,z)∧ψ(x,y2,z).
Vorsicht evtl. bei bedingten Quantoren; wenn etwa anstatt ∀z steht ∀z∊f(y), dann muss vor dem Zusammenfassen der z's expandiert werden, weil sie ja sonst von verschiedenen y's abhängen. Wenn uns ⇒ genügt, können wir auch ∀z∊f(y1)∩f(y2) schreiben.

Formeln wie (∀x: φ(x))∨(∀y:ψ(y)) ⇔ ∀x:∀y:φ(x)∨ψ(y) ⇒ ∀x:φ(x)∨ψ(x) , oder allgemeiner ∀x:∀y:φ(x,y) ⇒ ∀x:φ(x,x) und Qx:∃y:φ(x,y) ⇐ Qx:φ(x,x) enstehen , indem man einfach für ∀y bzw. ∃y      x einsetzt.
Ein paar nützliche davon sind:
∀z:φ(z)∨ψ(z) ⇐ (∀x:φ(x)) ∨ (∀y:ψ(y))· ∃z:φ(z)∧ψ(z) ⇒ (∃x:φ(x)) ∧ (∃y:ψ(y))· ∀z:φ(z)→ψ(z) ⇐ (∃x:φ(x)) → (∀y:ψ(y))·

Auch noch erwähnenswert sind folgende:
∀x:a(x)→b(x) ⇒ (∀x:a(x) ⇒ ∀x:b(x))· ∀x:a(x)↔b(x) ⇒ (∀x:φ(a(x)) ⇔ ∀x:φ(b(x)))·
∀x:a(x)→b(x) ⇒ (∃x:a(x) ⇒ ∃x:b(x))· ∀x:a(x)↔b(x) ⇒ (∃x:φ(a(x)) ⇔ ∃x:φ(b(x)))·
Sie stehen im Zusammenhang mit Tatsache, dass bei allgemeingültigen Folgerungs/Äquivalenz -beziehungen die Folgerung/Äquivalenz auch auf den Unterknoten eines Quantors angewendet werden darf.

Einsetzen mit Äquivalenz
Wie oben beschrieben gilt ja:  ∀y:φ(y) ⇒ ∀x:φ(f(x)).   f(x) ist dabei ein "funktionswertiger Ausdruck" über x,  z.B 3*x+1.
Wenn f einen begrenzten "definitionsbereich" hat, dann verstehen wir hier die ∀x als∀x∊def. Bereich.
Die Herleitung aus Elementarregeln ist ∀y:φ(y) ⇔ ∀x∀y:φ(y) ⇒ ∀x:φ(f(x)); also für y wird f(x) eingesetzt.

Manchmal gilt auch die Umkehrung des Pfeils, nämlich dann wenn die Werte von f(x) den ganzen Wertebereich abdecken. Also wenn ∀y:∃x:f(x)=y. Bei über Mengen definierten Funktionen gilt übrigens auch: ∀x∊dom f:φ(f(x)) ⇔ ∀y∊rng f: φ(y). Wenn wir statt y∊rng f schreiben ∃x:f(x)=y, dann gilt das auch für Prädikatenlogische Funktionsausdrücke.
Es gelten folgende Äquivalenzen:
∀y:∃x:f(x)=y ⇒ (∀y:φ(y) ⇔ ∀x:φ(f(x))) ∀y:∃x:f(x)=y ⇒ (∃y:φ(y) ⇔ ∃x:φ(f(x)))
∀x:φ(f(x)) ⇔ ∀y:(∃x:f(x)=y)→φ(y) ∃x:φ(f(x)) ⇔∃y(∃x:f(x)=y)∧φ(y)
∀y:φ(y) ⇔ (∀x:φ(f(x))) ∧ (∀y:(∃x:f(x)=y)∨φ(y)) ∃y:φ(y) ⇔ (∀y:(φ(y)→∃x:f(x)=y) → ∃x:φ(f(x))
Eine Herleitung: ∀y:(∃x:f(x)=y)→φ(y) ⇔ ∀y:∀x:f(x)=y→φ(y) ⇔ ∀y:∀x:f(x)=y→φ(f(x)) ⇔ ∀x:(∃y:f(x)=y)→φ(f(x)) ⇔ ∀x:wahr→φ(f(x))
Statt einer Variable x gilt das auch analog für mehrere , z.b f(a,b,c). Bei bedingten Quantoren gilt: ∀x∊M:φ(f(x)) ⇔ ∀y:(∃x∊M:f(x)=y)→φ(y)

Bedingte Quantoren
Wenn wir einen bedingten Quantor abschwächen wollen (also ∀ ersetzen durch ∃), und vorher expandieren, ergibt sich:
∀x∊A:φ(x) ⇔ ∀x: x∊A→φ(x) ⇒ ∃x: x∊A→φ(x),
was zwar korrekt ist, aber eine schwache Aussage darstellt, denn sie ist bereits dann wahr, wenn es ein x gibt mit ¬x∊A
Auch richtig und spezifischer ist:
∀x∊A:φ(x)  ⇒ (∃x:x∊A) → ∃x∊A:φ(x) ∃x∊A:φ(x)  ⇐ (∃x:x∊A) ∧ ∀x∊A:φ(x)
Wobei dann (∃x:x∊A) oft sofort durch 'wahr' ersetzt werden kann.
Die Herleitung dazu ist wie folgt:
(∃x: x∊A) ∧ ∀x: x∊A→φ(x) ⇔ ∃x∀y:(x∊A)∧(y∊A→φ(y)) ⇒ (einsetzen für y mit x)
∃x:(x∊A)∧(x∊A→φ(x)) ⇔ ∃x: x∊A∧φ(x).
Die beiden Regeln in der Tabelle sind gleichwertig wegen (a∧b)→c ⇔ a→(b→c).
Natürlich darf statt x∊A wieder auch eine beliebige andere Eigenschaft von x stehen.
So gesehen ist es vorteilhaft, die bedingten Quantoren zu verwenden, weil man beim Abschwächen des Quantors weniger Verlust hat. Alternativ dazu könnte man sich auch passende extra Regeln für die expandierte Form überlegen, wie ∀x:ψ(x)→φ(x)  ⇒ (∃x:ψ(x))→∃x: ψ(x)∧φ(x).
Bei anderen selbst ausgedachten Quantoren, wie "Für alle bis auf endlich viele", lassen sich diejenigen Regeln gut verwenden bei denen die Quantoren bloss umgedreht werden. ("es gibt (mindestens) unendlich viele"). Bei anderen Umformungen ist zu bedenken, dass hier die Bedingung nicht von einem einzelnen Objekt abhängt.