Der Beweiskalkül für die Quantorenlogik

Schlussregeln

Fallunterscheidung, FU: \frac{{(φ → ψ) \atop (¬φ → ψ)}}{ψ}

Widerspruch, Wid: \frac{{(¬φ → ψ) \atop (¬φ → ¬ψ)}}{φ}

Modus Ponens, MP: \frac{{φ \atop (φ → ψ)}}{ψ}

Allregel, ∀ : für alle S-Terme t \frac{∀xφ}{φ\frac{t}{x}}

Identitätsregel, ≡: für alle S-Terme t \overline{t ≡ t}

Substitutionsregel, Sub: für alle S-Terme s, t \frac{\begin{matrix}φ & \frac{s}{x} \\ s ≡ t \end{matrix}}{φ\frac{t}{x}}

\underline{Texte} Eine Folge T_{0}, …, T_{n−1} ist ein Text gdw es für jedes i < n einen Ausdruck φ_{i} ∈ L^{S} gibt mit:

T_{i} = φ_{i} [ “ es gilt φ_{i} ” ], oder T_{i} => φ_{i} [ “ angenommen φ_{i} ” ], oder T_{i} =< φ_{i} [ “ also φ_{i} ” ], oder T_{i} =>.

Ordne dem Text lokale Voraussetzungen V_{i}, Zeiger z_{i}; und Mengen B_{i} belegter Variablen zu:

V_{o} = ∅, z_{0} = −∞, B_{0} = ∅,

T_{i} = φ_{i} impliziert V_{i+1} = V_{i} ∪ {φ_{i}}, z_{i+1} = z_{i}, B_{i+1} = B_{i} ∪ Fr(φ_{i}), T_{i} => φ_{i} impliziert V_{i+1} = V_{i} ∪ {φ_{i}}, z_{i+1} = i, B_{i+1} = B_{i} ∪ Fr(φ_{i}), T_{i} =< φ_{i} impliziert V_{i+1} = V_{z_{i}} ∪ {φ_{i}}, z_{i+1} = z_{z_{i}}, B_{i+1} = B_{z_{i}} ∪ Fr(φ_{i}), T_{i} => impliziert V_{i+1} = V_{i} , z_{i+1} = i , B_{i+1} = B_{i}.

\underline{Beweise} Ein Text T_{0}, …, T_{n−1} mit V_{i}, z_{i}, B_{i} wie oben ist ein Beweis gdw für i < n und φ_{i} ∈ L^{S} gilt:

1. T_{i} = φ_{i} impliziert, dass φ_{i} ∈ V_{i} oder dass es ψ_{0}, …, ψ_{l−1} ∈ V_{i} gibt, so

dass \frac{ψ_{0} … ψ_{l−1}}{φ_{i}} Instanz einer Schlussregel ist.

2. T_{i} =< φ_{i} impliziert, dass z_{i} ≥ 0 [eine >-Klammer wird geschlossen ].

3. T_{i} =< φ_{i} und T_{z_{i}} => φ_{z_{i}} impliziert, dass es Ausdrücke X , ψ ∈ L^{S}, paarweise verschiedene Variablen x_{0}, …, x_{l−1} und paarweise verschiedene Variablen y_{0}, …, y_{l−1} gibt, so dass φ_{z_{i}} = X \frac{y_{0}...y_{l−1}}{x_{0}...x_{l−1}} , φ_{i−1} = ψ \frac{y_{0}...y_{l−1}}{x_{0}...x_{l−1}} , φ_{i} = ∀x_{0} … ∀x_{l−1}(X → ψ) und y_{0}, …, y_{l−1} ∉ B_{z_{i}} ∪ Fr(X) ∪ Fr(ψ).

4. T_{i} =< φ_{i} und T_{z_{i}} => impliziert, dass es einen Ausdruck ψ ∈ L^{S}, paarweise verschiedene Variablen x_{0}, …, x_{l−1} und paarweise verschiedene Variablen y_{0}, …, y_{l−1} gibt, so dass φ_{i−1} = ψ \frac{y_{0}...y_{l−1}}{x_{0}...x_{l−1}} , φ_{i} = ∀x_{0} … ∀x_{l−1}ψ und y_{0}, …, y_{l−1} ∉ B_{z_{i}} ∪ Fr(ψ).

Z_{i} : > X \frac{y⃗}{x⃗}  >
⋮  ⋮
i − 1 : ψ\frac{y⃗}{x⃗}  ψ\frac{y⃗}{x⃗}
i  : < ∀x⃗(X → ψ) < ∀x⃗ψ

T_{0}, …, T_{n−1} ist ein Beweis von φ gdw T_{n−1} = φ und z_{n−1} = −∞. Notation, Beispiel 0 : > 1 : > v_{0} ≡ v_{1}. 2 : (v_{0} ≡ v_{3})\frac{v_{1}}{v_{3}} nach 1. 3 : > v_{1} ≡ v_{2}. 4 : (v_{0} ≡ v_{3})\frac{v_{2}}{v_{3}} nach (Sub), 2,3. 5 : v_{0} ≡ v_{2} nach 4. 6 : < (v_{1} ≡ v_{2} → v_{0} ≡ v_{2}) 7 : < (v_{0} ≡ v_{1} → (v_{1} ≡ v_{2} → v_{0} ≡ v_{2})) 8 : < ∀v_{0}∀v_{1}∀v_{2}(v_{0} ≡ v_{1} → (v_{1} ≡ v_{2} → v_{0} ≡ v_{2})) 9 : ∀v_{0}∀v_{1}∀v_{2}(v_{0} ≡ v_{1} → (v_{1} ≡ v_{2} → v_{0} ≡ v_{2})) nach 8.

Das gleiche Beispiel in der Mizar-MSE-Sprache:

environ
        reserve x,y,z for set;
begin
        a: now let x,y,z;
                b: now assume b1: x=y;
                        c: now assume c1: y=z;
                        thus x=z by b1,c1;
                        end;
                        thus y=z implies x=z by c;
                end;
                thus x=y implies (y=z implies x=z) by b;
        end;
        for x,y,z holds x=y implies (y=z implies x=z) by a;

Dieser Beweis wir von Mizar-MSE als korrekt akzeptiert:

!! MIZAR-MSE UNIX version 2.2 Dep of Comp Sci, Univ of Alberta !!
environ
        reserve x,y,z for set;
begin
        a: now let x,y,z;
                b: now assume b1: x=y;
                        c: now assume c1: y=z;
                        thus x=z by b1,c1;
                        end;
                        thus y=z implies x=z by c;
                end;
                thus x=y implies (y=z implies x=z) by b;
        end;
        for x,y,z holds x=y implies (y=z implies x=z) by a;
!!
!! Thanks, OK
!! ----------

In dem Mizar-Kalkül kann auch das Behauptung-Beweis-Format benutzt werden, und übliche Abkürzungen sind möglich:

environ
        reserve x,y,z for set;
begin
Transitivity: for x,y,z holds x=y implies (y=z implies x=z)
proof
        let x,y,z;
        assume b1: x=y;
        assume c1: y=z;
        thus x=z by b1,c1;
end