Kontextbasiertes Schliessen    -kurzgefasst-

Hier untersuchen wir den Aufbau von Beweisketten, und wie wir in einer Kette von einem Schritt zum nächsten gelangen können. Ziel ist, die möglichen Umformungen von Aussagen möglicht voll auszuschöpfen, um kurze Beweisketten erhalten zu können.

Beweisketten
A ⇔ ... ⇔ ... ⇔ B         beweist A↔ B.
A ⇔ w
beweist A
A ⇔ f
beweist ¬A
A ⇒ ... ⇒ ... ⇒ B beweist A → B
A ⇐ ... ⇐ ... ⇐ B beweist A ← B
A ⇐ w  ; w ⇒ A
beweist A
A ⇒ f    ; f  ⇐ A
beweist ¬A
A ⇒ w  und A ⇐ f
beweisen nichts
in der Kette dürfen auch ⇔ vorkommen, aber keine Pfeile in die Gegenrichtung.

(⇔ , ⇒ , ⇐ sind transitiv;   (w→a)↔a , (a→f)↔¬a , a→w , f→a sind Tautologien).
Es gilt auch (a→b) ↔ (¬a←¬b).
Wir betrachten also auch Beweisketten mit ⇐ Richtung; manchmal lässt sich der Beweis schneller finden, wenn die zu beweisende Aussage am Anfang steht.

A⇒B lässt sich auch beweisen, in dem wir A (temporär) zu den bekannten Sätzen hinzufügen, und dann B beweisen. (Φ→(A→B)) ↔ ((Φ∧A)→B)

Äquivalenzketten:
Formeln A↔B , oder A=B erlauben  (Formeln = bereits bewiesene Sätze/Definitionen)
.... A ....  ⇔ .... B ....
also beliebige Teilausdrücke sind ersetzbar
Beispiel:  Formel ∀u∀v: u*v = v*u erlaubt z=(a+1)*4 ⇔ z=4*(a+1). (eingesetzt u=(a+1); v=4)
Es kommen immer diejenigen Formeln in Frage, wo links oder rechts von ⇔ bzw. = ein Ausdruck steht, der bei passender Einsetzung zu A wird und den gleichen Typ hat wie A.
Da '=' auch transitiv ist können Aussagen der Gestalt u=v auch durch eine Kette u = ... = v bewiesen werden. (Anstelle von u=v ⇔ ... ⇔ v=v ⇔ wahr).

Folgerungsketten:
Formel A→B erlaubt
A ⇒ B und B ⇐ A
aber nicht immer in Teilausdrücken:
     a<4 ⇒ a<5, aber  aus a<4↔x=3 folgt nicht a<5↔x=3
Beispiele:
∀b: b-b=0 ⇒ 5-5=0; wegen der Regel (∀x:φ(x))→φ(a)
a>b∧b>c ⇒ a>c;  bei bekanntem Satz ∀u,v,w:u>v∧v>w→u>w .

∧,∨ stören dabei nicht;   sei a→a+; a←a-; b→b+; b←b-.   dann gilt
a∧b ⇒ a+∧b a∧b ⇐ a-∧b
a∨b ⇒ a+∨b a∨b ⇐ a-∨b
Das Negationszeichen dreht die Folgerung um:
¬a⇐¬(a+) ¬a⇒¬(a-)
Wegen a→b   ↔  ¬a∨b gilt daher
a→b ⇒ a→b+ a→b ⇒ a-→b
a→b ⇐ a+→b a→b ⇐ a→b-
Quantoren stören den Ablauf nicht.
∀x:a ⇒ ∀x:a+; ∃x:a ⇒ ∃x:a+ etc; auch wenn x in a frei vorkommt und die Voraussetzung ∀x:a(x)→a+(x) gilt.
Jeder Teilaussage a lässt sich ein Schliessungsvorzeichen zuordnen; wenn man alle → in ¬x∨y wandelt und dann zählt, wieviele Negationszeichen zwischen a und der Wurzel des Satzbaums liegen. Gerade Anzahl = + ; ungerade Anzahl = -. Teilaussagen unterhalb eines ↔ haben kein Vorzeichen. Dort ist keine Ersetzung a nach a+ möglich.   Beispiel:
a→((b→c)→d) ⇒ a→((b+→c)→d,  weil b 2x negativ (links vom →)
(+)∧(+)     (+)∨(+)    (-)→(+)     ¬(-).
Wenn wir unterhalb ↔ arbeiten wollen können wir vorher umformen mit a↔b ⇔ a→b ∧ a←b
Für das Einsetzen von Werten / Teilausdrücken in Quantorvariablen in unser Aussage ergibt sich:
Das Verfahren in diesem Abschnitt ergibt sich aus den Tautologien (a→b)→((a∧c)→(b∧c)) , (a→b)→((a∨c)→(b∨c)) , (a→b) ↔ (¬a←¬b).

Standartrepertoire fur ↔ Regeln: Aussagenlogische Tautologien und einfache prädikatenlogische Tautologien
Standartrepertoire fur → Regeln: Aussagenlogische Folgerungen und einfache prädikatenlogische Folgerungen, z.B ∀x:φ(x)  ⇒ φ(a)

Einsetzen in Quantoren
Mit den Regeln  (∀x:φ(x)) → φ(a)  und  φ(a) → (∃x:φ(x)) ergibit sich aus dem obigen Abschitt:
Einsetzen in ∀ gibt ⇒/⇐ und in ∃ gibt ⇐/⇒ bei +/- Vorzeichen.     Beispiel: ∀x:x-x=0 ⇒ 5-5=0.
Bei bedingten Quantoren wie ∀x∈A:φ(x) dürfen wir nur Objekte einsetzen, die ∈A a sind, bzw. wenn das unklar ist müssen wir vorher expandieren mit ∀x∈A:φ(x) ≡ ∀x:x∈A→φ(x) bzw. ∃x∈A:φ(x) ≡ ∃x:x∈A∧φ(x).
Wir dürfen für die Quantorvariable beliebige Terme einsetzen, die syntaktisch korrekt sind und den gleichen Typ haben wie die Variable; dabei dürfen auch Variablen aus vorangehenden Quantoren, die hier noch im Wirkungsbereich sind, benutzt werden.
Wichtig aber: das so bezeichnete Objekt muss auch existieren. a/b ist syntaktisch korrekt, aber wenn b=0, dann existiert so ein Objekt nicht. Bei zusammengestzten Termen die Funktionssymbole (oder operatoren) enthalten existiert das Objekt dann, wenn die parameter der Funktionen im Definitionsbereich liegen. Wenn wir nicht genau wissen, ob das der Fall ist können wir dies als Bedingung voranstellen:
bei + vorzeichen ∀x:φ(x) ⇒ a∈dom f → φ(f(a)) ∃x:φ(x) ⇐ a∈dom f ∧φ(f(a))
bei - vorzeichen ¬∀x:φ(x) ⇐ ¬(a∈dom f → φ(f(a))) ¬∃x:φ(x) ⇒ ¬(a∈dom f ∧φ(f(a)))

Folgerung durch wahr einsetzen
Angenommen wir haben habe folgende Formel:
∀a,b: a≤b∧b≤a→a=b (*) (antisymmetrie von ≤); und unsere Aussage lautet:
∀x: m≤x.     (m ist kleinstes Element). Wir wollen jetzt mit Hilfe von (*) etwas folgern.
Aber a≤b steht nicht allein links von →, daher können wir die Formel so direkt nicht benutzen.
Wenn wir wissen, dass (*) sich auch schreiben lässt als ∀a,b:a≤b→(b≤a→a=b) können wir weitermachen, und erhalten
⇒ ∀x: x≤m→x=m.   (m ist ein minimales Element)
Wenn wir das in einem kompliziertern Fall nicht sehen, dann können wir so vorgehen: nach der Bindung a=m,b=x ersetzen wir m≤x in der Formel durch wahr. Das Resultat ist dann auch x≤m→x=m.  Wenn wir rüchwärts folgern wollen (⇐), dann können wir die Startaussage in der Formel  durch falsch ersetzen, und die Negation des Resultats ist dann eine ⇐ Folgerung.  In diesem konkreten Beispiel kommt dabei allerdings nur die Tautologie ⇐ f  dabei heraus.

Einfache Folgerungen
Einige Aussagenlogische Tautologien erlauben auch Hinzufügen und Weglassen von Aussagen:
a∧b⇒a      a⇒a∨b     a⇒ (b→a)    etc. ;
sowie das Abschwächen von Junktoren:
(a↔b)⇒(a→b)     (a∧b)⇒a∨b  etc.
Die nächsten Methoden ergeben äquivalenz Folgerungen:
Wegen a∧a⇔a und a∨a⇔a dürfen wir auch Teilaussagen verdoppeln, bzw bei Folgerungen das Original stehen lassen: a⇒a+∧a, etc.
Wir dürfen jederzeit bekannte wahre Aussagen hinzufügen (z.B bereits bewiesene Sätze) entsprechend a∧w⇔a ; w→a⇔a.

Formeln und Einsetzen
Allgemeingültige Formeln/Sätze werden oft verschieden abgekürzt aufgeschrieben:
∀a∊R:∀b∊R:a+b=b+a;   ∀a:∀b:a+b=b+a;   a+b=b+a;  
Dabei wird, wenn aus dem Zusammenhang bekannt, schonmal die Angabe des Typs (R) oder die Allquantoren weggelassen.
Vorsicht aber, wenn die Formel innerhalb eines Typs nur für einen begrenzten Wertebereich gilt; z.B a = a*b/b ohne die Einschränkung b≠0.Das kann zu Widersprüchen führen:  2 = 2*0/0 = 0/0 = 1*(0/0) = 1*0/0 = 1 .  Daher besser: b≠0 → a = a*b/b   (die Formel ohne b≠0 lässt sich auch nicht herleiten, wenn in der Definition von / die Bedingung b≠0 mit eingebaut ist).
Wenn beim Einsetzen in eine Formel darin freie Variable übrig bleiben, können wir für diese entweder einen beliebigen Ausdruck (des Typs) einsetzen, oder
einen Quantor mit in unser Aussage übernehmen. Der Quantor muss an eine beliebige Stelle kommen die ein + oder - Schliessungsvorzeichen hat und wird bei + zu ∀ und bei - zu ∃.
z.B Formel ∀a∀b:a=a+b-b
3*x =y  ⇔ (3*x)+7-7 = y
3*x =y  ⇔ ∀b: (3*x)+b-b = y

Gleichheitsregel
a=b ⇒ f(a) = f(b) ;   a=c∧b=d ⇒ f(a,b) = f(c,d) ; etc. ;ausserdem: a=b↔b=a; a=b∧b=c→a=c
'f' ist ein beliebiger Funktionsausdruck, z.B. u=v ⇒ 3*(u+1)=3*(v+1).

Seitenausdrücke
Wir wollen A durch etwas anderes ersetzen in  .... X .... A ....  .
Wenn X=falsch → (A bedeutungslos), dann kann X als wahr unterstellt werden;
Wenn X=wahr  → (A bedeutungslos), dann kann X als falsch unterstellt werden.
z.B. x=y ∧ x>4  ⇔ x=y ∧ y>4,   weil x=y bei Bearbeitung von x>4 als wahr unterstellt werden kann.
(w) ∧ (w)   ;    (f) ∨ (f)    ,    (w) → (f)     (= was kann für diesen Teil unterstellt werden , wenn der andere Teil bearbeitet wird)
Dabei kann man vom aktuellen Ausdruck bis zur Wurzel hochgehen und alle diese Seiten ausdrücke mit einbeziehen.
Quantoren stören nicht;  ↔ erlaubt keine seiten-unterstellung, aber hält die Kette zur Wurzel nicht auf.
Die Seitenausdrücke, können dann (evtl. negiert) so eingesetzt werden, wie die bereits bewiesenen Sätze; oder sie können auch mit ∧ zur aktuellen Teilaussage hinzugefügt werden.
Das ergibt sich auch durch die Tautologien (a∧b)↔(a∧(b∧a)) , sowie (a∨b)↔(a∨(b∧¬a)). Man sollte aber nicht 2 Umformungen dieser Art auf einmal vornehmen, um Schreibarbeit zu sparen, denn a∨b ist nicht gleich (a∧¬b)∨(b∧¬a).
Noch ein Beispiel: Gegeben: ∀a,b,c: a<b∧b<c→a<c
((u<v)∧z)→(v<w∧t)  ⇒ ((u<v)∧z)→(u<w∧t). Bei Bearbeitung von v<w kann das u<v als wahr angenommen werden. Wir könnten es mit ∧ neben unser v<w stellen und dann die gegebene Formel anwenden. Wir könnten auch das als wahr unterstellte u<v in die Formel einsetzen (für a<b) dann durch dort wahr ersetzen, dann bleibt die Formel ∀c:v<c→u<c übrig, und dann diese anwenden.
Weiteres Beispiel: a∧(b∧a) ⇔ a∧(b∧wahr); die Methode hilft also auch bei aussagenlogischen Vereinfachungen, wenn ein Teilausdruzck mehrfach vorkommt: z.B (a→(a↔b)) ⇔ (a→(w↔b)) ⇔ a→b.

Fallunterscheidungen
Das Prinzip der Seitenausdrücke ist auch bei Fallunterscheidungen gut anwendbar.
a ⇔ (c→a) ∧ (¬c→a) bzw. a ⇔ (c∧a)∨(¬c∧a).
in den erhaltenen Formeln können wir dann bei Bearbeitung von a links unterstellen dass c wahr ist und rechts dass c falsch ist.
Allgemeiner gillt auch (c∨d) ⇒ (a⇔ (c→a) ∧ (d→a) ⇔ (c∧a) ∨ (d∧a) ).
c und d brauchen sich also nicht auszuschliessen, es braucht bloss c∨d wahr zu sein. Analog mit mehr als 2 Bedingungen.

Wiederverwenden von Folgengliedern
In der Beweisfolge A ⇒ B ⇒ C ⇒ ...  dürfen wir auch im nächsten Schritt alle Vorgänger in der Kette als wahr unterstellen, also etwa anwenden wie einen bereits bekannten Satz, oder mit ∧ irgendwo hinzufügen. Streng genommen ist das nächte Folgenglied dann keine Folgerung aus seinem Vorgänger allein sondern benutzt auch die anderen mit. Beim Aufschreiben kann man das durch eine gestrichelte Line zum Hilfsvorgänger kennzeichnen. Wir dürfen auch die Folgerung bei einem früheren Folgenglied anstelle des letzten fortsetzen. Beispiel:
∃x:φ(x)∧ψ(x) ⇒ ∃x:φ(x) ⇒ ∃x:ψ(x) ⇒  (∃x:φ(x)) ∧ (∃x:ψ(x)).    (1⇒2;1⇒3;2+3⇒4)
In der Folge A ⇐ B ⇐ C ⇐ ... dürfen wir die Vorgänger als falsch unterstellen.
Besteht die Kette zum Hilfsvorgänger nur aus ⇔, dann dürfen wir uns entscheiden, ob wir diese als ⇒ oder ⇐ interpretieren, bekommen dann aber auch nur eine ⇒ bzw. ⇐ Folgerung, und keine Äquivalenz.

Beweismethoden
Unsere Beweisketten lassen sich auf mehrere Arten verwenden  Viele Beweismethoden ergeben sich durch aussagenlogische Tautologien; z.B
(¬a→f) ⇔ a ; ((a∧¬b)→f) ⇔ (a→b)  (Beweis durch Kontraposition, Widerspruch) , oder   (a→b)∧(¬a→b) ⇔ b (Fallunterscheidung), (a↔b) ⇔ (a→b)∧(b→a) ⇔ (a→b)∧(¬a→¬b) (Äquivalenz durch einzelne Implikationen beweisen);  (a↔b) ∧ (a↔c) ⇔ (a→b)∧(b→c)∧(c→a) (Ringschluss).
Hier ein paar Vorschläge, für die Auswahl der Beweisskette in Abhängigkeit von der Struktur der zu beweisenden Aussage (nach voranstehenden Allquantoren):
(⇒ : Folgerungsketten; A! : unterstelle A als wahr)
A A⇐w ;   ¬A⇒f
A→B A⇒B;  ¬B⇒¬A;  A!,B⇐w;  A!,¬B⇒f;  ¬B!, A⇒f
A∨B ¬A→B;    ¬B→A
A∧B A und B einzeln
A↔B A⇒B und B⇒A;    A⇔B
Anstelle von 'w' kann auch ein bereits bewiesener Satz stehen.

Gleichartigkeit verschiedener Beweisketten
An diesem Beispiel soll gezeigt werden, das bei unterschiedlichem Aufbau der Beweiskette oft trotzdem die selben Umformungen stattfinden.
Beispiel:  Beweis von A→B mit
(1) A→B A+→B ... B→B wahr
(2) ¬(A→B) ¬(A+→B) ... ¬(B→B) falsch
(3) A A+ ... B
In allen 3 Beweisen wird A schrittweise so verändert, dass es zu B wird. Da in (1) das A links von → steht ergeben sich daher immer ⇐ Folgerungen, wo sich in (3) ⇒ Folgerungen ergeben. Es werden die selben Umformungen vorgenommen; (3) ist weniger zu schreiben. (2) ist Beweis durch Widerspruch
(4) A→B A→B- ... A→wahr wahr
(5) A gegeben B B- ... wahr
(6) A gegeben ¬B ¬(B-) ... falsch
In diesen Beweisen wird B über B- auf wahr hingeführt. Da in (4) das A als Seitenausdruck links vom Pfeil zu B steht dürfen wir A als wahr unterstellen und daher sind die selben Umformungen möglich wie in (5), wo A als gegeben gesetzt wird.