A matematikai logika alkalmazásszemléletű tárgyalása

Főoldal > TAMOP 4.2.5 Pályázat könyvei > Könyvek > Természettudományok > Matematika

A matematikai logika alkalmazásszemléletű tárgyalása

Pásztorné Varga Katalin, Várterész Magda, Sági Gábor

Panem Kft.

Beágyazás

Gentzen-stílusú kalkulusok

A bizonyításelméletben az eldöntésprobléma megoldásához szükséges levezetés megkonstruálása nagyon kényelmetlen. Gyakran a legegyszerűbb formula levezetése is igen hosszadalmas, és ami még nagyobb probléma, a levezetések általában nem hasonlítanak a matematikában szokásos érvelésekre.

Hogy a gyakorlatban is hatékonyan lehessen a bizonyításelmélet eldöntésproblémáját megoldani, a levezetési sémákra vonatkozó speciális segédszabályok egész rendszerét dolgozták ki. Segítségükkel a bizonyításelméleti levezethetőség igazolható a levezetés tényleges megkonstruálása nélkül. A segédszabályok ugyanakkor szoros analógiát mutatnak a szokásos matematikai érvelés gyakorlatával is, ami könnyűvé teszi a levezethetőség igazolását. Ezen szabályok rendszerét nevezik a természetes levezetés technikájának, amit az irodalom Gentzen nevéhez köt ([63]).

A természetes levezetés technikája mellett Gentzen kidolgozott egy másik – ún. szekventekkel dolgozó – kalkulust is. Gentzen szekventkalkulusa is igen kényelmesen használható az eldöntésprobléma megoldására, mivel a levezetési szabályok egyszerűen és a levezetendő szekventben szereplő formulák szerkezete által meghatározott sorrendben alkalmazhatók.

A természetes levezetés technikája

Legyenek $Γ$ és $Δ$ ítéletlogikai formulák tetszőleges – esetleg üres – halmazai, $A, B$ és $C$ pedig ítéletlogikai formulák. Jelöljük a fejezetben egyszerűen a $Γ \cup Δ$ halmazt $Γ, Δ$ -val és a $Γ \cup {A}$ -t is $Γ, A$ -val. A 6.6. és a 6.7. táblázatokba gyűjtöttük össze a természetes levezetés technikájának ítéletlogikai szabályait. A levezetési szabályok szekvenciákat tartalmaznak – egy kivételével – vonallal elválasztva. A vonal alatt egy, a vonal felett pedig egy vagy két szekvencia található. A szekvencia egy formulahalmazból valamely formulának az ítéletkalkulusban való levezethetőségére vonatkozó állítást jelöl. Egy természetes technikai szabály is mindig egy állítást jelöl: ha adva van(nak) a vonal feletti szekvenciá(ka)t megalapozó ítéletkalkulusbeli levezetés(ek), akkor megkonstruálható a vonal alatti szekvenciát megalapozó levezetés is.

A strukturális szabályok igazolása nagyon egyszerű. Az azonosság törvényét – egyedül itt nincs vonal – például az $A$ egyetlen formulából álló levezetés bizonyítja. A bővítés, a szűkítés és a felcserélés szabálya esetén a vonal feletti szekvenciát megalapozó levezetés egyúttal a vonal alatti szekvenciát megalapozó levezetés is. Vizsgáljuk meg most a vágás szabályát. A dedukciós tétel szerint ha $Δ, A ⊢_{0} B$ , akkor $Δ ⊢_{0} A \supset B$ . Ekkor viszont a $Γ ⊢_{0} A$ -t és a $Δ, A ⊢_{0} B$ -t igazoló levezetések konkatenációja megalapozza $Γ, Δ ⊢_{0} B$ -t. A felsorolt strukturális szabályokat gyakran alkalmazzák a levezetések létezésének igazolása során külön hivatkozás nélkül is.

Table 6.6. A természetes levezetés technikájának strukturális szabályai

az azonosság törvénye
$Γ, A ⊢_{0} A$
a bővítés szabálya	a szűkítés szabálya
$\frac{Γ ⊢_{0} A}{Γ, B ⊢_{0} A}$	$\frac{Γ, B, B, Δ ⊢_{0} A}{Γ, B, Δ ⊢_{0} A}$
a felcserélés szabálya	a vágás szabálya
$\frac{Γ, B, C, Δ ⊢_{0} A}{Γ, C, B, Δ ⊢_{0} A}$	$\frac{Γ ⊢_{0} A Δ, A ⊢_{0} B}{Γ, Δ ⊢_{0} B}$

A természetes levezetés technikájának vannak ún. logikai szabályai is. Az ítéletlogika minden logikai összekötőjeléhez két szabályt fogunk kapcsolni, egy ,,bevezető” szabályt ( $b$ -szabály) és egy ,,alkalmazó” szabályt ( $a$ -szabály). A bevezető szabály arra vonatkozik, hogyan igazolható egy negációs, egy konjunkciós, egy diszjunkciós, illetve egy implikációs formula levezethetősége. A alkalmazó szabály pedig arra, hogyan kell bánni bizonyos negációs, konjunkciós, diszjunkciós, illetve implikációs formulákkal egy szekvencia megalapozása során.

Table 6.7. A természetes levezetés technikájának logikai szabályai

$(\supset b)$	$\frac{Γ, A ⊢_{0} B}{Γ ⊢_{0} A \supset B}$	$(\supset a)$	$\frac{Γ ⊢_{0} A Γ ⊢_{0} A \supset B}{Γ ⊢_{0} B}$
$(\land b)$	$\frac{Γ ⊢_{0} A Γ ⊢_{0} B}{Γ ⊢_{0} A \land B}$	$(\land a)$	$\frac{Γ, A, B ⊢_{0} C}{Γ, A \land B ⊢_{0} C}$
$(\lor b)$	$\frac{Γ ⊢_{0} A}{Γ ⊢_{0} A \lor B} \frac{Γ ⊢_{0} B}{Γ ⊢_{0} A \lor B}$	$(\lor a)$	$\frac{Γ, A ⊢_{0} C Γ, B ⊢_{0} C}{Γ, A \lor B ⊢_{0} C}$
$(\neg b)$	$\frac{Γ, A ⊢_{0} B Γ, A ⊢_{0} \neg B}{Γ ⊢_{0} \neg A}$	$(\neg a)$	$\frac{Γ ⊢_{0} \neg \neg A}{Γ ⊢_{0} A}$

A logikai szabályok igazolása sem nehéz. Bebizonyítunk néhányat, a többit az olvasóra bízzuk.

Az implikáció bevezetésének szabálya épp a dedukciós tétel.
Az implikációt alkalmazó szabály: Ha adottak a $Γ ⊢_{0} A$ és a $Γ ⊢_{0} A \supset B$ állításokat megalapozó levezetések, a kettő konkatenációja után alkalmazható a modus ponens, és így épp $B$ -nek egy, a $Γ$ -ból való levezetését állítottuk elő.
A diszjunkció bevezetése: Ha adott $Γ$ -ból $A$ -nak a levezetése, akkor az $A \supset A \lor B$ axiómát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk a $Γ$ -ból az $A \lor B$ egy levezetését.
A diszjunkció alkalmazása: Ha adottak a $Γ, A ⊢_{0} C$ és a $Γ, B ⊢_{0} C$ állításokat megalapozó levezetések, akkor a dedukciós tétel miatt megkonstruálhatók a $Γ ⊢_{0} A \supset C$ és a $Γ ⊢_{0} B \supset C$ állításokat megalapozó levezetések is. Ezt a két levezetést konkatenáljuk, és írjuk le az $(A \supset C) \supset ((B \supset C) \supset (A \lor B \supset C))$ axiómát. Kétszer alkalmazva a modus ponenst megalapoztuk, hogy $Γ ⊢_{0} A \lor B \supset C$ . Írjuk be a levezetésbe a vonal alatti szekvenciából az $A \lor B$ hipotézist, és ha most újból alkalmazzuk a modus ponenst, megkapjuk a $Γ, A \lor B ⊢_{0} C$ -t megalapozó levezetést.

6.2.1. PÉLDA. Lássuk be a természetes levezetés technikájával, hogy

$⊢_{0} A \supset (\neg A \supset B) .$

A bizonyítás során a természetes levezetés technikai szabályait ,,felülről lefelé” használtuk fel:

$1.$	$A, \neg A, \neg B ⊢_{0} A$	[ az azonosság törvénye alapján ]
$2.$	$A, \neg A, \neg B ⊢_{0} \neg A$	[ az azonosság törvénye alapján ]
$3.$	$A, \neg A ⊢_{0} \neg \neg B$	[ 1-ből és 2-ből $(\neg b)$ ]
$4.$	$A, \neg A ⊢_{0} B$	[ 3-ból $(\neg a)$ ]
$5.$	$A ⊢_{0} \neg A \supset B$	[ $(\supset b)$ ]
$6.$	$⊢_{0} A \supset (\neg A \supset B)$	[ $(\supset b)$ ]

A gyakorlatban a természetes technikai szabályokat inkább ,,alulról felfelé” szoktuk alkalmazni: amikor igazolni kell egy vonal alatti állítást, elegendő bebizonyítani, hogy a vonal feletti állítások igazak. Ekkor világosan látható, hogy a felsorolt szabályok elég jól tükrözik a matematikusok által széles körben használt bizonyítási módszereket.

Például a diszjunkció alkalmazása megfelel az esetelemzés módszerének. Ha le kell vezetni $A \lor B$ -ből $C$ -t, akkor az esetelemzés a következőképpen történik: ha $A \lor B$ igaz, akkor vagy $A$ , vagy $B$ igaz, ezért elegendő két esetet megvizsgálni. Külön-külön le kell vezetni $A$ -ból $C$ -t és $B$ -ből $C$ -t.
A negáció bevezetése a matematikai gyakorlatban az indirekt bizonyítás, azaz az ellentmondáshoz való visszavezetés módszere. Hogy bebizonyítsuk $\neg A$ -t, elegendő – feltéve, hogy $A$ teljesül – ellentmondáshoz jutni, vagyis egy $B$ -t kiválasztva $A$ -ból levezetni $B$ -t és $\neg B$ -t is.

6.2.2. PÉLDA. Konstruáljuk meg a 6.2.1. példabeli

$⊢_{0} A \supset (\neg A \supset B)$

levezetést a természetes levezetés technikáját ,,alulról felfelé” alkalmazva. Ha alkalmazzuk kétszer az implikáció bevezetésének szabályát, az

$A, \neg A ⊢_{0} B$

bizonyítandó állítást kapjuk. Felhasználva a negáció alkalmazásának a szabályát az

$A, \neg A ⊢_{0} \neg \neg B$

megalapozandó szekvenciát nyerjük. Ezután a negáció bevezetésének szabályával visszavezethetjük a kérdést arra, vajon levezethető-e az $A, \neg A, \neg B$ hipotézisekből valamely formula és annak negáltja is. E hipotézisekből viszont az azonosság törvénye miatt $A$ és $\neg A$ is levezethető.

6.2.3. PÉLDA. Igazoljuk, hogy

$⊢_{0} (A \supset B \supset C) \supset B \supset \neg C \supset \neg A .$

Alkalmazva az implikáció bevezetésének a szabályát háromszor, megkapjuk az egyszerűbb bizonyítandó szekvenciát:

$A \supset B \supset C, B, \neg C ⊢_{0} \neg A .$

A negáció bevezetésének a szabályát felhasználva, elegendő $A$ -t hozzácsatolni a szekvencia feltételeihez és valamilyen ellentmondást levezetni. Belátjuk, hogy a hipotézisekből levezethető $C$ és $\neg C$ . Mivel $\neg C$ szerepel a hipotézisek között, az azonosság törvénye szerint teljesül, hogy

$A \supset (B \supset C), B, \neg C, A ⊢_{0} \neg C .$

Tehát már csak az

$A \supset (B \supset C), B, \neg C, A ⊢_{0} C$

szekvenciát kellene megalapozni. Ehhez alkalmazva az implikáció alkalmazásának a szabályát például az

$A \supset (B \supset C), B, \neg C, A ⊢_{0} B$

és az

$A \supset (B \supset C), B, \neg C, A ⊢_{0} B \supset C$

állításokat kell bizonyítani. Az első az azonosság törvénye alapján igaz. A második szekvencia megalapozását újból az implikáció alkalmazása szabályának felhasználásával kíséreljük meg. A bizonyítandó

$A \supset (B \supset C), B, \neg C, A ⊢_{0} A$

és

$A \supset (B \supset C), B, \neg C, A ⊢_{0} A \supset (B \supset C)$

szekvenciákat az azonosság törvénye igazolja. Ezzel befejeztük a feladat megoldását.

6.2.4. PÉLDA. Ebben a példában azt bizonyítjuk be, hogy $⊢_{0} A \lor \neg A$ . Első ötletünk az, hogy alkalmazzuk a diszjunkció bevezetésének a szabályát. Ekkor vagy a $⊢_{0} A$ , vagy a $⊢_{0} \neg A$ szekvenciát kellene megalapoznunk, ami nyilvánvaló, hogy nem megy. Próbálkozzunk másképp. $⊢_{0} A \lor \neg A$ helyett – alkalmazva a negáció alkalmazásának a szabályát – igazoljuk a

$⊢_{0} \neg \neg (A \lor \neg A)$

szekvenciát. Most felhasználva a negációnak a bevezetését, mutassuk meg, hogy a $\neg (A \lor \neg A)$ hipotézis ellentmondáshoz vezet. Megalapozható ugyanis például

$\neg (A \lor \neg A) ⊢_{0} \neg A és \neg (A \lor \neg A) ⊢_{0} \neg \neg A .$

Az első szekvencia igazolását visszavezethetjük (negáció bevezetésével) a következő két szekvenciára:

$\neg (A \lor \neg A), A ⊢_{0} \neg (A \lor \neg A) és \neg (A \lor \neg A), A ⊢_{0} A \lor \neg A .$

A bal oldali szekvencia az azonosság törvénye miatt nyilvánvaló, a jobb oldali a $\neg (A \lor \neg A), A ⊢_{0} A$ szekvenciából (azonosság törvénye) nyerhető diszjunkció bevezetésével. Hasonlóan bizonyítható a

$\neg (A \lor \neg A) ⊢_{0} \neg \neg A$

szekvencia az alábbiak segítségével:

$\neg (A \lor \neg A), \neg A ⊢_{0} \neg (A \lor \neg A) és \neg (A \lor \neg A), \neg A ⊢_{0} A \lor \neg A .$

6.2.5. PÉLDA. Most lássuk be, hogy $\neg A \lor B, C \supset \neg B, A ⊢_{0} \neg C$ . A negáció bevezetésének a szabályát alkalmazva a

$\neg A \lor B, C \supset \neg B, A, C ⊢_{0} A és \neg A \lor B, C \supset \neg B, A, C ⊢_{0} \neg A$

szekvenciák megalapozhatóságának igazolására vezetjük vissza a bizonyítást. Az első szekvencia az azonosság törvénye. A második bizonyításához a diszjunkció alkalmazásának szabályát használjuk, így a

$\neg A, C \supset \neg B, A, C ⊢_{0} \neg A és B, C \supset \neg B, A, C ⊢_{0} \neg A$

szekvenciák megalapozhatóságát kell bizonyítanunk. Az első itt is az azonosság törvénye. A második szekvencia igazolása pedig a vágás szabálya felhasználásával visszavezethető a

$C \supset \neg B, C ⊢_{0} \neg B és \neg B, B, A ⊢_{0} \neg A$

szekvenciák megalapozhatóságának bizonyítására. Az első szekvencia esetén az implikáció alkalmazásának a szabályával már az azonosság törvényét kapjuk:

$C \supset \neg B, C ⊢_{0} C \supset \neg B és C \supset \neg B, C ⊢_{0} C .$

A második esetben pedig a negáció bevezetésével ellentmondáshoz jutunk:

$\neg B, B, A ⊢_{0} B és \neg B, B, A ⊢_{0} \neg B .$

Felvetődhet az a kérdés is, hogy ha egy formulahalmazból az ítéletkalkulusban levezethető egy formula, akkor ezt be tudjuk-e mindig bizonyítani csupán a természetes levezetés technikájával. Tegyük fel, hogy a $Γ ⊢_{0} B$ szekvenciát a $D_{1}, D_{2}, \dots, D_{m}$ $(m \geq 1)$ levezetés megalapozta. Ekkor minden $j = 1,2, \dots, m$ -re $D_{j}$ vagy hipotézis, vagy axiómaformula, vagy van olyan $1 \leq s, t \leq j$ , hogy a $D_{s}$ és a $D_{t}$ formulákból modus ponenssel állt elő.

Ha $D_{j}$ hipotézis, azaz eleme a $Γ$ formulahalmaznak, akkor a $Γ ⊢_{0} D_{j}$ az azonosság törvénye.
Ha $D_{j}$ az (A1)–(A10) axiómasémákból nyert formula, akkor $⊢_{0} D_{j}$ bizonyítható természetes technikával (ezeket a bizonyításokat az olvasóra bízzuk), így – a bővítés szabálya alapján – $Γ ⊢_{0} D_{j}$ is bizonyítható természetes technikával.
Tegyük végül fel, hogy $D_{j}$ a modus ponenssel állt elő a $D_{s}$ és a $D_{t}$ formulákból. Ha a $Γ ⊢_{0} D_{s}$ és a $Γ ⊢_{0} D_{t}$ szekvenciák megalapozhatók természetes technikával, akkor az implikáció alkalmazásának a szabályával a $Γ ⊢_{0} D_{j}$ -t is bizonyítottuk.

Tehát a levezetés minden $D_{j}$ formulája esetén $Γ ⊢_{0} D_{j}$ bizonyítható természetes technikával.

A predikátumkalkulus eldöntésproblémájának megoldásakor is alkalmazhatjuk a természetes technikát. Mivel ha $Γ ⊢_{0} A$ , akkor $Γ ⊢ A$ is, így a természetes levezetés technikájának ítéletlogikai szabályait használhatjuk. Nyilvánvaló azonban, hogy további logikai szabályokra is szükség van. A 6.8. táblázatban megadunk két kvantort bevezető és két kvantort alkalmazó szabályt. Ezekkel a szabályokkal egészítjük ki a természetes technikai szabálygyűjteményünket. Most a 6.6., a 6.7. és a 6.8. táblázatokban legyenek $Γ$ és $Δ$ egy rögzített elsőrendű logikai nyelv formuláinak tetszőleges – esetleg üres – halmazai, $A, B$ és $C$ formulák, $x$ változó és $t$ pedig tetszőleges term a nyelvben.

Table 6.8. A természetes levezetés technikájának kvantoros szabályai

$(\forall b)$	$\frac{Γ ⊢ A}{Γ ⊢ \forall x A} (x \notin Par (Γ))$	$(\forall a)$	$\frac{Γ ⊢ \forall x A}{Γ ⊢ [A (x ∥ t)]}$
$(\exists b)$	$\frac{Γ ⊢ [A (x ∥ t)]}{Γ ⊢ \exists x A}$	$(\exists a)$	$\frac{Γ, A ⊢ B}{Γ, \exists x A ⊢ B} (x \notin Par (Γ, B))$

Igazoljuk a természetes levezetés technikájának kvantoros szabályait is:

Az univerzális kvantor bevezetésének szabálya éppen az általánosítás szabálya (6.1.44. tétel).
Az univerzális kvantor alkalmazásának szabálya: Ha adott a $Γ ⊢ \forall x A$ szekvenciát megalapozó levezetés, akkor a $\forall x A \supset [A (x ∥ t)]$ axiómát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk $[A (x ∥ t)]$ egy levezetését $Γ$ -ból.
Az egzisztenciális kvantort bevezető szabály: Ha adott a $Γ ⊢ [A (x ∥ t)]$ szekvenciát megalapozó levezetés, akkor írjuk be az $[A (x ∥ t)] \supset \exists x A$ axiómát a levezetésbe, és alkalmazzuk a modus ponenst. Így $Γ$ -ból levezettük $\exists x A$ -t.
Az egzisztenciális kvantor alkalmazásának szabálya: Ha adott a $Γ, A ⊢ B$ szekvenciát megalapozó levezetés, akkor a dedukciós tétel miatt megkonstruálható a $Γ ⊢ A \supset B$ szekvenciát megalapozó levezetés is. Ebből az általánosítás szabálya miatt – mivel $x \notin Par (Γ)$ – $Γ ⊢ \forall x (A \supset B)$ adódik. Ha most a levezetésbe beírjuk a $\forall x (A \supset B) \supset (\exists x A \supset B)$ axiómát (lényeges, hogy $x \notin Par (B)$ ), alkalmazhatjuk a modus ponenst. Ezzel megkapjuk a $\exists x A \supset B$ egy levezetését $Γ$ -ból. A dedukciós tétel újbóli alkalmazásával pedig igazoltuk, hogy $Γ, \exists x A ⊢ B$ .

6.2.6. PÉLDA. A természetes levezetés technikája segítségével példánkban bebizonyítjuk, hogy $\exists x A ⊢ \neg \forall x \neg A$ . A hipotézis egy egzisztenciálisan kvantált formula, tehát az egzisztenciális kvantort alkalmazó szabály szerint elég igazolni, hogy $A ⊢ \neg \forall x \neg A$ , hisz $x \notin Par (\neg \forall x \neg A)$ . A jobb oldali negáció miatt érdemes alkalmazni a negáció bevezetést: alapozzuk meg az

$A, \forall x \neg A ⊢ A és az A, \forall x \neg A ⊢ \neg A$

szekvenciákat. Az első az azonosság törvénye. A második igazolása az univerzális kvantort alkalmazó szabály segítségével vezethető vissza az $A, \forall x \neg A ⊢ \forall x \neg A$ szekvenciára, ami szintén az azonosság törvénye.

6.2.7. PÉLDA. Most pedig a $\neg \forall x \neg A ⊢ \exists x A$ szekvenciát fogjuk természetes technikával megalapozni. A negáció alkalmazása szerint próbáljuk meg ehhez a $\neg \forall x \neg A ⊢ \neg \neg \exists x A$ -t bizonyítani. Negáció bevezetésével a

$\neg \forall x \neg A, \neg \exists x A ⊢ \neg \forall x \neg A és a \neg \forall x \neg A, \neg \exists x A ⊢ \forall x \neg A$

szekvenciák igazolására vezethetjük vissza a feladatot. Az első szekvencia most is az azonosság törvénye. A második igazolásához használjuk fel az univerzális kvantor bevezetésének szabályát, és lássuk be, hogy $\neg \forall x \neg A, \neg \exists x A ⊢ \neg A$ . Újból a negáció bevezetése segítségével folytatva a levezetést kapjuk, hogy a

$\neg \forall x \neg A, \neg \exists x A, A ⊢ \neg \exists x A és a \neg \forall x \neg A, \neg \exists x A, A ⊢ \exists x A$

szekvenciákat kellene megalapozni. Az első szekvencia megint az azonosság törvénye. A második az egzisztenciális kvantor bevezetésének szabálya alapján a $\neg \forall x \neg A, \neg \exists x A, A ⊢ [A (x ∥ x)]$ szekvencia megalapozásával igazolható, ami pedig az azonosság törvénye.

Végül az olvasóra bízzuk annak belátását, hogy ha a predikátumkalkulusban egy formula levezető valamely formulahalmazból, akkor – a predikátumkalkulusbeli levezetés tényleges megkonstruálása nélkül – csak a természetes levezetés technikáját alkalmazva is be lehet ezt bizonyítani.

Szekventkalkulusok

6.2.8. DEFINÍCIÓ. (A SZEKVENTEK SZINTAXISA) Legyenek $Γ$ és $Δ$ ítéletlogikai formulák tetszőleges, véges, nemrendezett sorozatai. Ekkor a $(Γ, Δ)$ párt szekventnek nevezzük és $Γ \to Δ$ -val jelöljük.

Megengedjük, hogy a $(Γ, Δ)$ szekventben akár $Γ$ , akár $Δ$ egyetlen formulát se tartalmazzon. Ha a $Γ$ sorozat üres, a szekventet $\to Δ$ -val, ha a $Δ$ sorozat üres, $Γ \to$ -lal jelöljük. Mindkét formulasorozat is lehet üres, ekkor a szekvent üres szekvent, amit $\to$ jelöl. Ha $Γ$ az $A_{1}, A_{2}, \dots, A_{n}$ és $Δ$ a $B_{1}, B_{2}, \dots, B_{m}$ (nemrendezett) formulasorozat, továbbá $A$ és $B$ ítéletlogikai formulák, akkor $A, Γ \to Δ, B$ -t írunk, ha az $A, A_{1}, A_{2}, \dots, A_{n} \to B_{1}, B_{2}, \dots, B_{m}, B$ szekventre akarunk hivatkozni.

Az ítéletlogika nyelvének rögzített interpretációja esetén terjesszük ki a Boole-értékelést szekventekre is.

6.2.9. DEFINÍCIÓ. (A SZEKVENTEK SZEMANTIKÁJA.) Legyen $ℐ$ az ítéletlogika nyelvének egy interpretációja, $ℬ_{ℐ}$ pedig $ℐ$ -beli Boole-értékelés. Legyen $ℬ_{ℐ} (Γ \to Δ)$ pontosan akkor $i$ igazságértékű, ha van olyan $A$ a $Γ$ formulasorozatban, hogy $ℬ_{ℐ} (A) = h$ vagy van olyan $B$ a $Δ$ formulasorozatban, hogy $ℬ_{ℐ} (B) = i$ . Egyébként rendeljen $ℬ_{ℐ}$ a $Γ \to Δ$ szekventhez $h$ igazságértéket.

Figyeljük meg, hogy a definíció alapján

$ℬ_{ℐ} (\to) = h$ ,

$ℬ_{ℐ} (\to B) = ℬ_{ℐ} (B)$ ,

$ℬ_{ℐ} (A \to) = ℬ_{ℐ} (\neg A)$ ,

$ℬ_{ℐ} (A \to B) = ℬ_{ℐ} (A \supset B)$ ,

$ℬ_{ℐ} (A_{1}, A_{2} \to B_{1}, B_{2}) = ℬ_{ℐ} (A_{1} \land A_{2} \supset B_{1} \lor B_{2})$ ,

és így tovább. Azaz a szekventek szemantikája szerint írhatjuk általánosan azt, hogy

$\begin{array}{l} ℬ_{ℐ} (A_{1}, A_{2}, \dots, A_{n} \to B_{1}, B_{2}, \dots, B_{m}) = \\ = ℬ_{ℐ} (⊤ \land A_{1} \land A_{2} \land \dots \land A_{n} \supset B_{1} \lor B_{2} \lor \dots \lor B_{m} \lor ⊥) . \end{array}$

Gondolhatunk tehát a $Γ \to Δ$ szekventre úgy is, mint speciális alakú formulára: implikációra, melyben az implikáció bal oldalán a $Γ$ sorozat formuláinak konjunkciós, a jobb oldalán a $Δ$ sorozat formuláinak diszjunkciós láncformulája áll. Továbbá ha a szekventben $Γ$ üres, az implikáció bal oldalán a $⊤$ tautológiát, ha $Δ$ üres, az implikáció jobb oldalán a $⊥$ kielégíthetetlen formulát kell elképzelni.

Két szekventkalkulust adunk meg. Az első Gentzen strukturális szabályokat is tartalmazó kalkulusa (G-kalkulus; 6.9. táblázat), a második pedig Curry strukturális szabályoktól mentes kalkulusa (C-kalkulus; 6.10. táblázat).

Table 6.9. A G-kalkulus

axiómaséma
$X \to X$
levezetési szabályok
$(\to s z)$	$(s z \to)$
$\frac{Γ \to Δ, X, X}{Γ \to Δ, X}$	$\frac{X, X, Γ \to Δ}{X, Γ \to Δ}$
$(\to b)$	$(b \to)$
$\frac{Γ \to Δ}{Γ \to Δ, X}$	$\frac{Γ \to Δ}{X, Γ \to Δ}$
$(\to \supset)$	$(\supset \to)$
$\frac{X, Γ \to Δ, Y}{Γ \to Δ, (X \supset Y)}$	$\frac{Γ \to Δ, X Y, Γ \to Δ}{(X \supset Y), Γ \to Δ}$
$(\to \land)$	$(\land \to)$
$\frac{Γ \to Δ, X Γ \to Δ, Y}{Γ \to Δ, (X \land Y)}$	$\frac{X, Γ \to Δ}{(X \land Y), Γ \to Δ} \frac{Y, Γ \to Δ}{(X \land Y), Γ \to Δ}$
$(\to \lor)$	$(\lor \to)$
$\frac{Γ \to Δ, X}{Γ \to Δ, (X \lor Y)} \frac{Γ \to Δ, Y}{Γ \to Δ, (X \lor Y)}$	$\frac{X, Γ \to Δ Y, Γ \to Δ}{(X \lor Y), Γ \to Δ}$
$(\to \neg)$	$(\neg \to)$
$\frac{X, Γ \to Δ}{Γ \to Δ, \neg X}$	$\frac{Γ \to Δ, X}{\neg X, Γ \to Δ}$

Table 6.10. A C-kalkulus

axiómaséma
$X, Γ \to Δ, X$
levezetési szabályok
$(\to \supset)$	$\frac{X, Γ \to Δ, Y}{Γ \to Δ, (X \supset Y)}$	$(\supset \to)$	$\frac{Γ \to Δ, X Y, Γ \to Δ}{(X \supset Y), Γ \to Δ}$
$(\to \land)$	$\frac{Γ \to Δ, X Γ \to Δ, Y}{Γ \to Δ, (X \land Y)}$	$(\land \to)$	$\frac{X, Y, Γ \to Δ}{(X \land Y), Γ \to Δ}$
$(\to \lor)$	$\frac{Γ \to Δ, X, Y}{Γ \to Δ, (X \lor Y)}$	$(\lor \to)$	$\frac{X, Γ \to Δ Y, Γ \to Δ}{(X \lor Y), Γ \to Δ}$
$(\to \neg)$	$\frac{X, Γ \to Δ}{Γ \to Δ, \neg X}$	$(\neg \to)$	$\frac{Γ \to Δ, X}{\neg X, Γ \to Δ}$

A szekventkalkulusokban – hasonlóan az ítéletkalkulushoz – axióma(szekvent)séma segítségével egy-egy kitüntetett szerkezetű szekventet, valamint néhány levezetési szabályt rögzítünk. Az axiómasémák és a levezetési szabályok száma a természetes levezetés technikájára emlékeztet minket: egy-egy axiómaséma található a kalkulusokban, és minden logikai összekötőjelhez két levezetési szabályunk van. Az axiómasémákból formulahelyettesítéssel állnak elő az axiómaszekventek, egy levezetési szabály pedig szekvent(ek)ből új szekventet állít elő. Például a $(\to \land)$ szabály segítségével a következőképpen állíthatunk elő szekventet: ha rendelkezésünkre állnak a $Γ \to Δ, A$ és a $Γ \to Δ, B$ szekventek, akkor azt mondjuk, hogy a $(\to \land)$ levezetési szabállyal előáll a $Γ \to Δ, (A \land B)$ szekvent.

A szekventkalkulusok megadása után bevezetjük a szekventkalkulusbeli bizonyíthatóság fogalmát. Ehhez most szemléletes utat választunk: a bizonyítás során ún. levezetésfát készítünk szekventekből a kalkulusok alapján. Megjegyezzük, hogy a bizonyításelméletben is dolgozhattunk volna hasonló módon. Legyen K vagy a G-kalkulus, vagy a C-kalkulus.

6.2.10. DEFINÍCIÓ. A K-kalkulusbeli levezetésfa és a levezetésfa magassága a következő:

A K-kalkulus minden axiómaszekventje egy (egyetlen szekventből álló) levezetésfa, ez a szekvent lesz a levezetésfa gyökere. A levezetésfa magassága 1.
Ha $D$ $m$ magasságú olyan K-kalkulusbeli levezetésfa, amelynek gyökere valamely K-kalkulusbeli levezetési szabályban épp vonal feletti szekvent, akkor a levezetési szabállyal a vonal alatti $S$ szekventet előállítva

$\frac{D}{S}$

is K-kalkulusbeli levezetésfa, ahol az $S$ szekvent a kapott levezetésfa gyökere, és a levezetésfa magassága $m + 1$ .

Ha $D_{1}$ és $D_{2}$ rendre $m_{1}$ és $m_{2}$ magasságú olyan K-kalkulusbeli levezetésfák, melyek gyökerei valamely K-kalkulusbeli levezetési szabályban épp vonal feletti szekventek, akkor előállítva a levezetési szabállyal a vonal alatti $S$ szekventet,

$\frac{D_{1} D_{2}}{S}$

is levezetésfa a $K$ -kalkulusban, amelyben az $S$ szekvent lesz a levezetésfa gyökere, és a levezetésfa magassága $\max (m_{1}, m_{2}) + 1$ .

Minden levezetésfa az 1–3. szabályok véges sokszori alkalmazásával áll elő.

6.2.11. PÉLDA. A C-kalkulusban az alábbi fa 3 magasságú levezetésfa, melynek gyökere a $\to A \supset (B \supset A)$ szekvent:

A szekventek mellett zárójelek között megadtuk azt a levezetési szabályt, melyet alkalmazva a szekvent előállt.

A G-kalkulusban a fa nem levezetésfa, hisz a G-kalkulusban $A, B \to A$ nem axiómaszekvent.

6.2.12. DEFINÍCIÓ. Azt mondjuk, hogy az $S$ szekvent a K-kalkulusban bizonyítható, ha van olyan K-kalkulusbeli levezetésfa, melynek $S$ a gyökere. Jelölése: $⊢_{K} S$ .

6.2.13. PÉLDA.

Az $A \land B \to B \land A$ szekvent a G-kalkulusban az alábbi – 3 magasságú – levezetésfával bizonyítható:

A $\to (A \land B \supset C) \supset (A \supset (B \supset C))$ szekvent a C-kalkulusban a következő – 6 magasságú – levezetésfával bizonyítható:

A gyakorlatban a szekventkalkulusok levezetési szabályait is ,,alulról felfelé” szoktuk alkalmazni: amikor bizonyítani szeretnénk egy $S$ szekventet, megpróbáljuk a bizonyító levezetésfát a gyökeréből ( $S$ -ből) kiindulva ,,alulról felfelé” haladva felépíteni. Ehhez keresni kell az épülő levezetésfa minden nem axiómaszekvent leveléhez olyan levezetési szabályt a kalkulusban, mely segítségével a levél előállhat, és a levezetési szabálynak megfelelő vonal feletti szekvent(ek)et be kell írni a készülő levezetésfába ezen levél szülőjeként (szüleiként).

A két kalkulus ismeretében felmerülhet a kérdés: vajon a két kalkulus ekvivalens-e, azaz minden olyan szekvent, amelyik bizonyítható a G-kalkulusban bizonyítható-e a C-kalkulusban is és fordítva, minden olyan szekvent, amelyik bizonyítható a C-kalkulusban bizonyítható-e a G-kalkulusban is.

6.2.14. DEFINÍCIÓ. Jelölje K₁ a G- és C-kalkulusok egyikét, és K₂ a másikat. Azt mondjuk, hogy egy a K₁-kalkulusbeli

$\frac{S_{1}}{S_{2}}$

levezetési szabály elérhető a K₂-kalkulusból, ha minden olyan esetben, amikor $⊢_{K_{2}} S_{1}$ , akkor $⊢_{K_{2}} S_{2}$ is. Hasonlóan, egy a K₁-kalkulusbeli

$\frac{S_{1} S_{2}}{S_{3}}$

levezetési szabály elérhető a K₂-kalkulusból, ha minden olyan esetben, amikor $⊢_{K_{2}} S_{1}$ és $⊢_{K_{2}} S_{2}$ , akkor $⊢_{K_{2}} S_{3}$ is.

6.2.15. LEMMA. A $C$ -kalkulus axiómái bizonyíthatók a $G$ -kalkulusban, azaz tetszőleges $A$ formula és $Γ, Δ$ formulasorozat esetén $⊢_{G} A, Γ \to Δ, A$ .

BIZONYÍTÁS. Az állítás bizonyításához megmutatjuk, hogyan kell megkonstruálni a szóban forgó G-kalkulusbeli levezetésfát. Tegyük fel, hogy $Γ$ az $A_{1}, A_{2}, \dots, A_{n}$ és $Δ$ a $B_{1}, B_{2}, \dots, B_{m}$ formulasorozat.

Ezzel a lemmát bebizonyítottuk. $⋄$

6.2.16. LEMMA. A $C$ -kalkulus minden levezetési szabálya elérhető a $G$ -kalkulusból.

BIZONYÍTÁS. Vegyük észre, hogy a C-kalkulus $(\to \supset)$ , $(\supset \to)$ , $(\to \land)$ , $(\lor \to)$ , $(\to \neg)$ , $(\neg \to)$ levezetési szabályai a G-kalkulusnak is levezetési szabályai, így a 6.2.14. definíció szerint ezek nyilván elérhetők a G-kalkulusból. A $(\land \to)$ és $(\to \lor)$ levezetési szabályok esetén pedig megkonstruáljuk a levezetésfát.

Tegyük fel először, hogy az $A, B, Γ \to Δ$ szekvent bizonyítható a G-kalkulusban. Ez azt jelenti, hogy van olyan G-beli levezetésfa, melynek gyökere $A, B, Γ \to Δ$ . Építsük tovább a levezetésfát G-ben:

Tehát az $A \land B, Γ \to Δ$ szekvent is bizonyítható a G-kalkulusban.

Tegyük fel most, hogy a $Γ \to Δ, A, B$ szekvent bizonyítható a G-kalkulusban. Ez azt jelenti, hogy van olyan G-beli levezetésfa, melynek gyökere $Γ \to Δ, A, B$ . Építsük tovább most is a levezetésfát G-ben:

Tehát a $Γ \to Δ, A \lor B$ szekvent is bizonyítható a G-kalkulusban.

Ezzel a lemmát bebizonyítottuk. $⋄$

6.2.17. TÉTEL. Ha egy $S$ szekvent bizonyítható a $C$ -kalkulusban, akkor bizonyítható a $G$ -kalkulusban is, azaz ha $⊢_{C} S$ , akkor $⊢_{G} S$ .

BIZONYÍTÁS. A bizonyítás a C-kalkulusbeli levezetésfa magassága szerinti indukcióval történik.

(alaplépés:) Ha $S$ a C-kalkulusban $1$ magasságú levezetésfával bizonyítható, akkor $S$ a C-kalkulusban axióma. De ekkor a 6.2.15. lemma miatt $⊢_{G} S$ .

(indukciós feltevés:) Ha $S$ a C-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható, akkor $⊢_{G} S$ .

(indukciós lépések:) Legyen most $S$ a C-kalkulusban $k + 1$ magasságú levezetésfával bizonyítható. Ekkor $S$ valamely C-kalkulusbeli levezetési szabály alkalmazásával állt elő vagy egy $D$ , vagy egy $D_{1}$ és egy $D_{2}$ legfeljebb $k$ magasságú C-kalkulusbeli levezetésfá(k)ból. Az indukciós feltevés szerint tehát ezen levezetésfa (levezetésfák) gyökere (gyökerei) bizonyítható(ak) a G-kalkulusban. A 6.2.16. lemma szerint pedig a G-kalkulusból minden C-kalkulusbeli levezetési szabály elérhető, tehát az is, amelyik segítségével C-ben a $D$ vagy a $D_{1}$ és a $D_{2}$ levezetésfá(k)ból előállítottuk az $S$ szekventet. Tehát $S$ bizonyítható a G-kalkulusban is.

Ezzel a tételt bebizonyítottuk. $⋄$

Most rátérünk a 6.2.17. tétel megfordításának vizsgálatára. A következő állítás triviális, hisz a G-kalkulus axiómasémájából nyert szekventek a C-kalkulus szerint is axiómaszekventek:

6.2.18. LEMMA. A $G$ -kalkulus axiómái bizonyíthatók a $C$ -kalkulusban, azaz tetszőleges $A$ formula esetén $⊢_{C} A \to A$ .

6.2.19. LEMMA. A $G$ -kalkulus minden levezetési szabálya elérhető a $C$ -kalkulusból.

BIZONYÍTÁS. A G-kalkulus $(\to \supset)$ , $(\supset \to)$ , $(\to \land)$ , $(\lor \to)$ , $(\to \neg)$ , $(\neg \to)$ levezetési szabályai a C-kalkulusnak is levezetési szabályai, így ezek nyilván elérhetők a C-kalkulusból.

Bizonyítsuk most be, hogy a G -kalkulus $(b)$ levezetési szabályai – nem magasabb levezetésfával – elérhetők a C-kalkulusból. Tegyük fel hogy $⊢_{C} Γ \to Δ$ . A bizonyítás a C-kalkulusbeli levezetésfa magassága szerinti indukcióval történik.
(alaplépés:) Ha $Γ \to Δ$ a C-kalkulusban 1 magasságú levezetésfával bizonyítható, akkor $Γ \to Δ$ a $C$ -kalkulusban axióma, azaz a $Γ$ és a $Δ$ formulasorozatban van közös formula. De ekkor az $A, Γ \to Δ$ és a $Γ \to Δ, A$ is axióma, tehát $1$ magasságú levezetésfával bizonyítható.
(indukciós feltevés:) Ha $Γ \to Δ$ a C-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható, akkor $⊢_{C} A, Γ \to Δ$ és $⊢_{C} Γ \to Δ, A$ is legfeljebb $k$ magasságú levezetésfával bizonyítható.
(indukciós lépések:) Legyen most $Γ \to Δ$ a $C$ -kalkulusban $k + 1$ magasságú levezetésfával bizonyítható. Ekkor $Γ \to Δ$ valamely C-kalkulusbeli levezetési szabály alkalmazásával állt elő vagy egy $D$ , vagy egy $D_{1}$ és egy $D_{2}$ legfeljebb k magasságú C-kalkulusbeli levezetésfá(k)ból.
Tegyük fel, hogy a $(\land \to)$ levezetési szabály alkalmazásával állt elő $Γ \to Δ$ , tehát a $Γ$ formulasorozatban szerepel valamilyen $B$ és $C$ formulák konjunkciója. Jelölje $Γ'$ a $Γ$ -beli formulák $B \land C$ nélküli sorozatát. Az indukciós feltevés szerint, mivel $B, C, Γ' \to Δ$ $k$ magasságú levezetésfával bizonyítható volt C-ben,

$A, B, C, Γ' \to Δ, illetve B, C, Γ' \to Δ, A$

legfeljebb $k$ magasságú levezetésfával bizonyítható C-ben. Innen a $(\land \to)$ szabállyal

$A, B \land C, Γ' \to Δ, tehát A, Γ \to Δ,$

illetve

$B \land C, Γ' \to Δ, A, tehát Γ \to Δ, A$

C-beli bizonyíthatósága is adódik legfeljebb $k + 1$ magasságú levezetésfával.

A többi C-beli levezetési szabály esetén a $(b)$ levezetési szabályok elérhetőségének a bizonyítását az olvasóra hagyjuk.

Be kellene még bizonyítani, hogy a G-kalkulus $(s z)$ levezetési szabályai is elérhetők a C-kalkulusból. A bizonyítás hasonló az előzőhöz, ezért nem közöljük.
Vizsgáljuk azonban meg a G-beli $(\land \to)$ levezetési szabály elérhetőségét. Tegyük fel, hogy $⊢_{C} A, Γ \to Δ$ . Mivel $(b \to)$ elérhető C-ből, $⊢_{C} A, B, Γ \to Δ$ . Erre a szekventre alkalmazva a C-beli $(\land \to)$ levezetési szabályt kapjuk, hogy $⊢_{C} A \land B, Γ \to Δ$ .
A $(\to \lor)$ levezetési szabály elérhetősége hasonló módon látható be.

Ezzel a lemmát bebizonyítottuk. $⋄$

6.2.20. TÉTEL. Ha az $S$ szekvent a $G$ -kalkulusban bizonyítható, bizonyítható a $C$ -kalkulusban is, azaz ha $⊢_{G} S$ , akkor $⊢_{C} S$ .

BIZONYÍTÁS. A bizonyítás a G-kalkulusbeli levezetésfa magassága szerinti indukcióval történik.

(alaplépés:) Ha $S$ a G-kalkulusban $1$ magasságú levezetésfával bizonyítható, akkor $S$ a $G$ -kalkulusban axióma. De ekkor a 6.2.18. lemma miatt $⊢_{C} S$ .

(indukciós feltevés:) Ha $S$ a G-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható, akkor $⊢_{C} S$ .

(indukciós lépések:) Legyen most $S$ a G-kalkulusban $k + 1$ magasságú levezetésfával bizonyítható. Ekkor $S$ valamely G-kalkulusbeli levezetési szabály alkalmazásával állt elő vagy egy $D$ , vagy egy $D_{1}$ és egy $D_{2}$ legfeljebb $k$ magasságú G-kalkulusbeli levezetésfá(k)ból. Az indukciós feltevés szerint tehát ezen levezetésfa (levezetésfák) gyökere (gyökerei) bizonyítható(ak) a C-kalkulusban. A 6.2.19. lemma szerint pedig a C-kalkulusból minden G-kalkulusbeli levezetési szabály elérhető, tehát az is, amelyik segítségével G-ben a $D$ vagy a $D_{1}$ és a $D_{2}$ levezetésfá(k)ból előállítottuk az $S$ szekventet. Tehát $S$ bizonyítható a C-kalkulusban is.

Ezzel a tétel bizonyítást nyert. $⋄$

Ezzel bebizonyítottuk, hogy a G-kalkulus és a C-kalkulus ekvivalens egymással. Így a továbbiakban, amikor nem fontos, hogy éppen melyik kalkulust használjuk, egyszerűen szekventkalkulusról fogunk beszélni.

6.2.21. DEFINÍCIÓ. Azt mondjuk, hogy egy szekventkalkulusbeli

$\frac{S_{1}}{S_{2}}$

levezetési szabály megfordítható, ha minden olyan esetben, amikor az $S_{2}$ szekvent bizonyítható, akkor az $S_{1}$ szekvent is bizonyítható. Hasonlóan, egy

$\frac{S_{1} S_{2}}{S_{3}}$

levezetési szabály megfordítható, ha minden olyan esetben, amikor az $S_{3}$ szekvent bizonyítható, akkor $S_{1}$ és $S_{2}$ is bizonyíthatók.

6.2.22. LEMMA. A $C$ -kalkulus levezetési szabályai megfordíthatók.

BIZONYÍTÁS. Bebizonyítjuk, hogy a $(\to \supset)$ szabály megfordítható, a többi C-kalkulusbeli levezetési szabály megfordíthatóságának bizonyítását az olvasóra bízzuk. Tegyük fel tehát, hogy $⊢_{C} Γ \to Δ, A \supset B$ . A C-kalkulusbeli levezetésfa magassága szerinti indukcióval bizonyítjuk, hogy $⊢_{C} A, Γ \to Δ, B$ .

(alaplépés:) Ha $Γ \to Δ, A \supset B$ a C-kalkulusban $1$ magasságú levezetésfával bizonyítható, akkor a C-kalkulusban $Γ \to Δ, A \supset B$ axiómaszekvent, azaz van közös formula $Γ$ -ban és $Δ, A \supset B$ -ben. Két eset lehetséges:

Az axiómaszekvent $C, Γ' \to Δ', C, A \supset B$ alakú. Ekkor az $A, C, Γ' \to Δ', C, B$ szekvent is axiómaszekvent.
Az axiómaszekvent $A \supset B, Γ' \to Δ, A \supset B$ alakú. Ekkor az $A, A \supset B, Γ' \to Δ, B$ szekventet kell bizonyítanunk, ami az

$A, Γ' \to Δ, B, A és az A, B, Γ' \to Δ, B$

axiómaszekventekből az $(\supset \to)$ szabállyal áll elő.

(indukciós feltevés:) Ha $Γ \to Δ, A \supset B$ a C-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható, akkor $⊢_{C} A, Γ \to Δ, B$ .

(indukciós lépések:) Tegyük fel, hogy $Γ \to Δ, A \supset B$ a C-kalkulusban $k + 1$ magasságú levezetésfával bizonyítható, tehát valamely levezetési szabály alkalmazásával állt elő egy vagy két legfeljebb $k$ magasságú levezetésfából. Az alkalmazott levezetési szabály a C-kalkulus $(\to \supset)$ , $(\supset \to)$ , $(\to \land)$ , $(\land \to)$ , $(\to \lor)$ , $(\lor \to)$ , $(\to \neg)$ , $(\neg \to)$ szabályai közül valamelyik lehet. Ha ez a levezetési szabály

éppen a $(\to \supset)$ szabály és ezzel a $Γ \to Δ, A \supset B$ szekventet az $A, Γ \to Δ, B$ szekventből vezettük le, akkor nyilván $A, Γ \to Δ, B$ is bizonyítható,
egyébként valamely $Γ' \to Δ', A \supset B$ (és $Γ ″ \to Δ ″, A \supset B$ ) alakú szekvent(ek)ből nyertük $Γ \to Δ, A \supset B$ -t. Ekkor az indukciós feltételezés miatt $⊢_{C} A, Γ' \to Δ', B$ (és $⊢_{C} A, Γ ″ \to Δ ″, B$ ). Erre (ezekre) a szekvent(ek)re alkalmazva azt a levezetési szabályt, aminek az eredménye az eredeti levezetésben $Γ \to Δ, A \supset B$ volt, nyerjük a kívánt levezetést.

Ezzel a lemmát bebizonyítottuk. $⋄$

A C-kalkulus levezetési szabályainak megfordíthatósága azt jelenti, hogy amikor egy szekvent bizonyítása során ,,alulról felfelé” próbáljuk megkonstruálni a levezetésfát, lényegtelen, hogy az alkalmazható levezetési szabályok közül melyiket választjuk. Ugyanakkor a G-kalkulus nem minden levezetési szabálya megfordítható, így a bizonyítás során – a levezetési szabályok ügyetlen alkalmazási sorrendje esetén – bizonyítható szekventek esetén is elakadhatunk: a készülő levezetésfa valamely levele nem axiómaszekvent, még sincs olyan levezetési szabály, mely alkalmazásával létrejöhetett volna.

6.2.23. PÉLDA. A 6.2.13. pont első példájában bizonyított $A \land B \to B \land A$ szekvent esetén ha ,,alulról felfelé” haladva először nem a $(\to \land)$ szabályt, hanem a $(\land \to)$ szabályt alkalmazzuk, akkor vagy az $A \to B \land A$ , vagy a $B \to B \land A$ szekventhez jutunk. A következő lépésben a $(\to \land)$ szabályt alkalmazhatjuk: az első esetben az $A \to B$ és az $A \to A$ , a második esetben pedig a $B \to B$ és a $B \to A$ szekventeket nyerjük. Egyik esetben sem lehet folytatni a bizonyítást, pedig mindkét esetben az egyik szekvent nem axióma.

A következő lemma azt bizonyítja, hogy a szekventkalkulusban is használható a vágás szabálya.

6.2.24. LEMMA. Ha $⊢_{C} Γ \to Δ, A$ és $⊢_{C} A, Γ \to Δ$ , akkor $⊢_{C} Γ \to Δ$ .

BIZONYÍTÁS. Nevezzük a bizonyítás során jónak az $A$ formulát, ha amikor $⊢_{C} Γ \to Δ, A$ és $⊢_{C} A, Γ \to Δ$ , akkor $⊢_{C} Γ \to Δ$ is. A szerkezeti indukció elve segítségével igazolni fogjuk, hogy minden ítéletlogikai formula jó.

(alaplépés:) Legyen $A$ prímformula. Tegyük fel, hogy $⊢_{C} Γ \to Δ, A$ és $⊢_{C} A, Γ \to Δ$ . Az első szekvent levezetésfájának a magassága szerinti indukcióval bebizonyítjuk, hogy $A$ jó.

(alaplépés:) Legyen a $Γ \to Δ, A$ szekventet bizonyító levezetésfa magassága 1, tehát $Γ \to Δ, A$ axióma. Két eset lehetséges:

Ha $A, Γ \to Δ$ is axiómaszekvent, akkor $Γ \to Δ$ is az, tehát bizonyítható.
Ha $A, Γ \to Δ$ nem axiómaszekvent, akkor $Γ = A, Γ'$ , és így ez a szekvent $A, A, Γ' \to Δ$ alakú. Alkalmazva az $(s z \to)$ szabályt $A, Γ' \to Δ$ bizonyíthatóságát kapjuk, ami a bizonyítandó $Γ \to Δ$ szekvent.

(indukciós feltevés:) Tegyük fel, hogy ha $Γ \to Δ, A$ és $A, Γ \to Δ$ bizonyíthatók, és $Γ \to Δ, A$ levezetésfája legfeljebb $k$ magasságú ( $A$ prímformula), akkor a $Γ \to Δ$ szekvent is bizonyítható.

(indukciós lépések:) Tegyük fel, hogy a $Γ \to Δ, A$ $k + 1$ magasságú, levezetésfával bizonyítható és az $A, Γ \to Δ$ szekvent is bizonyítható.

Ha $A, Γ \to Δ$ axiómaszekvent, akkor $A, Γ \to Δ', A$ alakú, mivel feltehető, hogy $Γ$ -nak és $Δ$ -nak nincs közös formulája, hisz $Γ \to Δ, A$ nem axiómaszekvent (1-nél magasabb levezetésfával bizonyítható). Tehát a $Γ \to Δ, A$ szekvent $Γ \to Δ', A, A$ alakú. Alkalmazva a $(\to s z)$ szabályt kapjuk, hogy $Γ \to Δ$ bizonyítható.
Egyébként, mivel $A$ prímformula, a szekventeket ugyanazon levezetési szabály alkalmazásával nyertük:
- vagy rendre valamely $Γ' \to Δ', A$ és $A, Γ' \to Δ'$ szekventekből,
- vagy az elsőt valamely $Γ' \to Δ', A$ és $Γ ″ \to Δ ″, A$ , a másodikat pedig $A, Γ' \to Δ'$ és $A, Γ ″ \to Δ ″$ szekventpárokból.

Az indukciós feltevés miatt $Γ' \to Δ'$ , illetve $Γ' \to Δ'$ és $Γ ″ \to Δ ″$ bizonyítható. Az így nyert szekventre, illetve szekventekre nyilván alkalmazható az a levezetési szabály, amit az eredeti levezetésfákban az utolsó lépésben alkalmaztunk. Az alkalmazás eredménye a $Γ \to Δ$ szekvent, tehát ez a szekvent is bizonyítható.

Tehát a prímformulák jók.

(indukciós lépések:) Tegyük fel, hogy az $A$ ítéletlogikai formula jó. Bebizonyítjuk, hogy $\neg A$ is jó. Ekkor ugyanis ha

$⊢_{C} Γ \to Δ, \neg A és ⊢_{C} \neg A, Γ \to Δ,$

mivel a $(\to \neg)$ és $(\neg \to)$ levezetési szabályok megfordíthatók,

$⊢_{C} A, Γ \to Δ és ⊢_{C} Γ \to Δ, A .$

De $A$ jó, ezért fennáll $⊢_{C} Γ \to Δ$ is.

Legyenek most $A$ és $B$ jók, és igazoljuk, hogy $A \land B$ is jó. Ha

$⊢_{C} Γ \to Δ, A \land B és ⊢_{C} A \land B, Γ \to Δ,$

mivel a $(\to \land)$ és $(\land \to)$ levezetési szabályok megfordíthatók, így

$⊢_{C} Γ \to Δ, A, ⊢_{C} Γ \to Δ, B és ⊢_{C} A, B, Γ \to Δ .$

Mivel a $(b \to)$ levezetési szabály elérhető a C-kalkulusban, és $⊢_{C} Γ \to Δ, A$ , így $⊢_{C} B, Γ \to Δ, A$ is. Továbbá mivel $A$ jó,

$⊢_{C} B, Γ \to Δ, A és ⊢_{C} A, B, Γ \to Δ$

esetén $⊢_{C} B, Γ \to Δ$ . Ebből, $⊢_{C} Γ \to Δ, B$ -ből és mert $B$ is jó, adódik, hogy $⊢_{C} Γ \to Δ$ is fennáll. Tehát $A \land B$ is jó.

Hasonlóan $A \lor B$ és $A \supset B$ jóságát is be lehet bizonyítani.

Így a lemma bizonyítást nyert. $⋄$

Most foglalkozzunk azzal az izgalmas kérdéssel a szekventkalkulusok kapcsán, hogy ekvivalensek-e az ítéletkalkulussal, azaz vajon igaz-e az, hogy egy $\to A$ szekvent akkor és csak akkor bizonyítható a szekventkalkulusban, amikor az $A$ formula bizonyítható az ítéletkalkulusban. Ha ugyanis a szekventkalkulusok ekvivalensek az ítéletkalkulussal, akkor ezek a kalkulusok is helyes és teljes kalkulusok. Megjegyezzük, hogy a szekventkalkulusok helyességének és teljességének ezen az úton történő bizonyításakor nem használjuk fel közvetlenül a szekventek szemantikáját.

Vezessük be a következő jelölést: ha $Γ$ az $A_{1}, A_{2}, \dots, A_{n}$ és $Δ$ a $B_{1}, B_{2}, \dots, B_{m}$ (nemrendezett) formulasorozat, akkor a $⊤ \land A_{1} \land A_{2} \land \dots \land A_{n}$ formulára $(\land Γ)$ -val és a $B_{1} \lor B_{2} \lor \dots \lor B_{m} \lor ⊥$ formulára $(\lor Δ)$ -val fogunk hivatkozni.

6.2.25. TÉTEL. (A SZEKVENTKALKULUS HELYESSÉGE.) Ha a $Γ \to Δ$ szekvent bizonyítható a $C$ -kalkulusban, akkor a $(\land Γ) \supset (\lor Δ)$ formula bizonyítható az ítéletkalkulusban, azaz ha $⊢_{C} Γ \to Δ$ , akkor $⊢_{0} (\land Γ) \supset (\lor Δ)$ .

BIZONYÍTÁS. Tegyük fel, hogy $⊢_{C} Γ \to Δ$ . A C-kalkulusbeli levezetésfa magassága szerinti indukcióval bizonyítjuk be, hogy $⊢_{0} (\land Γ) \supset (\lor Δ)$ . Az egyes indukciós lépésekben $(\land Γ) \supset (\lor Δ)$ ítéletkalkulusbeli bizonyíthatóságát természetes technikával igazoljuk.

(alaplépés:) Ha $Γ \to Δ$ a C-kalkulusban 1 magasságú levezetésfával bizonyítható, akkor a C-kalkulusban $Γ \to Δ$ axiómaszekvent, azaz van közös formula $Γ$ -ban és $Δ$ -ban. Jelölje ezt a formulát $A$ , így a szekvent $A, Γ' \to Δ', A$ alakú. De ekkor az $A \land (\land Γ') \supset (\lor Δ') \lor A$ formula ítéletkalkulusbeli bizonyíthatóságához a dedukciós tétel miatt elég az $A \land (\land Γ') ⊢_{0} (\lor Δ') \lor A$ szekvenciát megalapozni. Innen a konjunkció bevezetése és a diszjunkció alkalmazása szabályokkal visszavezethetjük a feladatot a $A, (\land Γ') ⊢_{0} A$ szekvencia megalapozására, ez viszont az azonosság törvénye.

(indukciós feltevés:) Ha $Γ \to Δ$ a C-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható, akkor $⊢_{0} (\land Γ) \supset (\lor Δ)$ .

(indukciós lépések:) Tegyük fel, hogy $Γ \to Δ$ a C-kalkulusban $k + 1$ magasságú levezetésfával bizonyítható, tehát valamely levezetési szabály alkalmazásával áll elő egy vagy két legfeljebb $k$ magasságú levezetésfából. Ha ez a levezetési szabály a

$(\to \supset)$ szabály volt, a $Γ \to Δ$ szekvent $Γ \to Δ', A \supset B$ alakú, és egy $k$ magasságú levezetésfával levezetett $A, Γ \to Δ', B$ szekventből nyertük. Az indukciós feltevés szerint ekkor $⊢_{0} A \land (\land Γ) \supset (\lor Δ') \lor B$ . Lássuk be, hogy $⊢_{0} (\land Γ) \supset (\lor Δ') \lor (A \supset B)$ is. Az implikáció bevezetésével a $(\land Γ) ⊢_{0} (\lor Δ') \lor (A \supset B)$ szekvencia megalapozására vezethető vissza a bizonyítás. Ekkor a vágás szabályát alkalmazva kapjuk, hogy a

$(\land Γ) ⊢_{0} (\lor Δ') \lor \neg A \lor B és a (\lor Δ') \lor \neg A \lor B ⊢_{0} (\lor Δ') \lor (A \supset B)$

szekvenciákat elég bizonyítanunk.

Az első szekvencia megalapozásához az indukciós feltevésünk szerint elég az

$A \land (\land Γ) \supset (\lor Δ') \lor B, (\land Γ) ⊢_{0} (\lor Δ') \lor \neg A \lor B$

szekvenciát a vágás szabályával megalapozni. A negáció alkalmazás és bevezetés után az

$A \land (\land Γ) \supset (\lor Δ') \lor B, (\land Γ), \neg ((\lor Δ') \lor \neg A \lor B)$

hipotézisből fogjuk az $A$ és $\neg A$ formulákat levezetni. Az $A$ levezetéséhez újból a negáció alkalmazásával és bevezetésével az

$A \land (\land Γ) \supset (\lor Δ') \lor B, (\land Γ), \neg ((\lor Δ') \lor \neg A \lor B), \neg A$

formulákból, $\neg A$ levezetéséhez pedig a negáció bevezetésével az

$A \land (\land Γ) \supset (\lor Δ') \lor B, (\land Γ), \neg ((\lor Δ') \lor \neg A \lor B), A$

formulákból a $((\lor Δ') \lor \neg A \lor B)$ és $\neg ((\lor Δ') \lor \neg A \lor B)$ ellentmondást lehet könnyen levezetni.

A második szekvencia megalapozásához a diszjunkció alkalmazásának szabálya szerint a

$(\lor Δ') ⊢_{0} (\lor Δ') \lor (A \supset B),$

$\neg A ⊢_{0} (\lor Δ') \lor (A \supset B)$

és a

$B ⊢_{0} (\lor Δ') \lor (A \supset B)$

szekvenciákat kell igazolni, amit mindhárom esetben a diszjunkció bevezetésének ügyes felhasználása után egyszerű megtenni.

A többi levezetési szabály esetén a bizonyítás hasonló, így az olvasóra hagyjuk.

Ezzel bebizonyítottuk a C-kalkulus és egyúttal a G-kalkulus helyességét. $⋄$

Természetesen a szekventkalkulusok helyességét bizonyíthattuk volna a szekventek szemantikájának közvetlen felhasználásával is. Megmutattuk ugyanis, hogy a szekventek tulajdonképpen speciális alakú formulák, továbbá könnyű belátni, hogy minden szekventkalkulusbeli levezetési szabály olyan, hogy a vonal alatti szekvent mint formula szemantikus következménye a vonal feletti szekvent(ek)nek mint formulá(k)nak. Egy axiómaszekvent pedig tautológia, így a szekventkalkulusban bizonyítható szekventek mind tautológiák. Most rátérünk a szekventkalkulusok teljességének bizonyítására.

6.2.26. LEMMA. Ha $A$ az ítéletkalkulus axiómája, akkor $\to A$ bizonyítható a $C$ -kalkulusban.

BIZONYÍTÁS. A bizonyítást konstruktív módon végezzük el, az ítéletkalkulus (A1)–(A10) axiómasémáiból előállított axiómák esetén rendre megkonstruáljuk a megfelelő szekvent C-kalkulusbeli levezetését.

Az (A1)-ből előállított axióma esetén a levezetés:

Az (A2)-ből előállított axióma esetén a levezetés:

3-10. Az (A3)–(A10)-ből előállított axiómák esetén a levezetések megadását az olvasóra hagyjuk.

A lemmát így bizonyítottnak tekinthetjük. $⋄$

6.2.27. LEMMA. Az ítéletkalkulus levezetési szabálya, a modus ponens, elérhető a $C$ -kalkulusból, azaz ha $⊢_{C} \to A$ és $⊢_{C} \to A \supset B$ , akkor $⊢_{C} \to B$ .

BIZONYÍTÁS. Tegyük fel, hogy $⊢_{C} \to A$ és $⊢_{C} \to A \supset B$ . Ha $⊢_{C} \to A$ , mivel $(\to b)$ elérhető a C-kalkulusban, így $⊢_{C} \to A, B$ is. Továbbá ha $⊢_{C} \to A \supset B$ , a $(\to \supset)$ levezetési szabály megfordíthatósága miatt $⊢_{C} A \to B$ is. Ekkor alkalmazva a szekventkalkulus vágás szabályát (6.2.24. lemma) kapjuk, hogy $⊢_{C} \to B$ . $⋄$

6.2.28. TÉTEL. (A SZEKVENTKALKULUS TELJESSÉGE.) Ha $B$ bizonyítható az ítéletkalkulusban, akkor $\to B$ bizonyítható a $C$ -kalkulusban, azaz ha $⊢_{0} B$ , akkor $⊢_{C} \to B$ .

BIZONYÍTÁS. Tegyük fel, hogy $⊢_{0} B$ , tehát adott a $D_{1}, D_{2}, \dots, D_{m} = B$ levezetés. Megmutatjuk, hogy a levezetés minden $D_{k}$ $(1 \leq k \leq m)$ formulája esetén $⊢_{C} \to D_{k}$ .

$D_{1}$ axiómaformula, ezért a 6.2.26. lemma szerint $⊢_{C} \to D_{1}$ .
Tegyük most fel, hogy minden $(n \leq k)$ -ra igazoltuk már, hogy $⊢_{C} \to D_{n}$ .
Ha most $D_{k + 1}$ axiómaformula, akkor a 6.2.26. lemma szerint $⊢_{C} \to D_{k + 1}$ . Ha $D_{k + 1}$ modus ponenssel állt elő $D_{s}$ -ből és $D_{t} = D_{s} \supset D_{k + 1}$ -ből, akkor $s, t \leq k$ miatt az indukciós feltételből $⊢_{C} \to D_{s}$ és $⊢_{C} \to D_{s} \supset D_{k + 1}$ adódik. A 6.2.27. lemma miatt innen $⊢_{C} \to D_{k + 1}$ .

Ezzel pedig bizonyítottuk a C-kalkulus, természetesen egyúttal a G-kalkulus teljességét is. $⋄$

Az elsőrendű logika is tárgyalható a szekventkalkulusok segítségével. Megadjuk az elsőrendű szekventek szintaxisát és szemantikáját, majd a szekventkalkulusok kvantoros szabályait.

6.2.29. DEFINÍCIÓ. (AZ ELSŐRENDŰ SZEKVENTEK SZINTAXISA.)

Legyenek $Γ$ és $Δ$ egy $ℒ [V_{v}]$ elsőrendű logikai nyelv formuláinak tetszőleges, véges, nemrendezett sorozatai. Ekkor a $(Γ, Δ)$ párt elsőrendű szekventnek (röviden szekventnek) nevezzük és $Γ \to Δ$ -val jelöljük.

6.2.30. DEFINÍCIÓ. (AZ ELSŐRENDŰ SZEKVENTEK SZEMANTIKÁJA.)

Legyen $ℐ$ az $ℒ [V_{v}]$ nyelv egy interpretációja és $κ$ egy $ℐ$ -beli változókiértékelés. Legyen $| Γ \to Δ |^{ℐ, κ}$ pontosan akkor $i$ igazságértékű, ha van olyan $A$ formula a $Γ$ formulasorozatban, hogy $| A |^{ℐ, κ} = h$ , vagy van olyan $B$ formula a $Δ$ formulasorozatban, hogy $| B |^{ℐ, κ} = i$ . Egyébként $| Γ \to Δ |^{ℐ, κ}$ legyen $h$ igazságértékű.

Az elsőrendű szekventek szemantikája alapján világos, hogy tetszőleges $ℐ$ interpretáció és $κ$ változókiértékelés mellett – hasonlóan az ítéletlogikai szekventekhez –

$\begin{array}{l} | A_{1}, A_{2}, \dots, A_{n} \to B_{1}, B_{2}, \dots, B_{m} |^{ℐ, κ} = \\ = | ⊤ \land A_{1} \land A_{2} \land \dots \land A_{n} \supset B_{1} \lor B_{2} \lor \dots \lor B_{m} \lor ⊥ |^{ℐ, κ} . \end{array}$

Most mindkét szekventkalkulust kiegészítve kvantoros levezetési szabályokkal megkapjuk az elsőrendű szekventkalkulusokat. A levezetésfa és a szekventkalkulusbeli bizonyíthatóság fogalmát módosítás nélkül használjuk.

Table 6.11. A G-kalkulus kvantoros levezetési szabályai

$(\forall \to)$	$\frac{[A (x ∥ t)], Γ \to Δ}{\forall x A, Γ \to Δ}$	$(\to \forall)$	$\frac{Γ \to Δ, A}{Γ \to Δ, \forall x A} (x \notin Par (Γ, Δ))$
$(\exists \to)$	$\frac{A, Γ \to Δ}{\exists x A, Γ \to Δ} (x \notin Par (Γ, Δ))$	$(\to \exists)$	$\frac{Γ \to Δ, [A (x ∥ t)]}{Γ \to Δ, \exists x A}$

Table 6.12. A C-kalkulus kvantoros levezetési szabályai

$(\forall \to)$	$\frac{[A (x ∥ t)], \forall x A, Γ \to Δ}{\forall x A, Γ \to Δ}$	$(\to \forall)$	$\frac{Γ \to Δ, A}{Γ \to Δ, \forall x A} (x \notin Par (Γ, Δ))$
$(\exists \to)$	$\frac{A, Γ \to Δ}{\exists x A, Γ \to Δ} (x \notin Par (Γ, Δ))$	$(\to \exists)$	$\frac{Γ \to Δ, [A (x \| \| t)], \exists x A}{Γ \to Δ, \exists x A}$

6.2.31. PÉLDA. A $\neg \exists x P (x) \lor R \to \forall x (P (x) \supset R)$ szekvent (ahol $x \notin Par (R)$ ) a C-kalkulusban a következő levezetésfával bizonyítható:

6.2.32. LEMMA. A $C$ -kalkulus és a $G$ -kalkulus kvantoros levezetési szabályai kölcsönösen elérhetők egymásból.

BIZONYÍTÁS. A $(\to \forall)$ és az $(\exists \to)$ levezetési szabályok megegyeznek, így csak az $(\forall \to)$ és a $(\to \exists)$ levezetési szabályok kölcsönös elérhetőségét kell bizonyítani.

A C-kalkulusbeli $(\forall \to)$ levezetési szabály G-ből elérhető, ha fennáll, hogy amikor a G-kalkulusban bizonyítható az $[A (x ∥ t)], \forall x A, Γ \to Δ$ szekvent, akkor bizonyítható G-ben a $\forall x A, Γ \to Δ$ is. Tegyük fel, hogy

$⊢_{G} [A (x ∥ t)], \forall x A, Γ \to Δ,$

azaz van olyan G-beli levezetésfa, melynek gyökere $[A (x ∥ t)], \forall x A, Γ \to Δ$ . Építsük tovább a levezetésfát G-ben:

A C-kalkulusbeli $(\to \exists)$ levezetési szabály G-ből való elérhetősége hasonlóan bizonyítható.

A G-kalkulusbeli $(\forall \to)$ és $(\to \exists)$ levezetési szabályok C-ből való elérhetőségéhez először be kell látni, hogy az $(s z)$ és $(b)$ levezetési szabályok az elsőrendű esetben is elérhetőek C-ből. A $(b)$ levezetési szabályok ebben az esetben is nem magasabb levezetési fával érhetők el. A bizonyítások menete hasonló a 6.2.19. lemmabelihez, hosszadalmas voltuk miatt nem közöljük.

Tegyük fel, hogy a $⊢_{C} [A (x | | t)], Γ \to Δ$ . De C-ből elérhető a $(b)$ levezetési szabály, így C-ben bizonyítható a $[A (x | | t)], \forall x A Γ \to Δ$ szekvent is. Erre alkalmazva a $(\forall \to)$ C-beli szabályt, a bizonyítani kívánt szekventet nyerjük.

A $(\to \exists)$ levezetési szabály C-ből való elérhetősége hasonlóan bizonyítható.

Ezzel a lemmát bebizonyítottuk. $⋄$

A 6.2.32. lemma alapján mondhatjuk, hogy a 6.2.17. és a 6.2.20. tételek érvényben maradnak az elsőrendű szekventek esetén is, tehát az elsőrendű G-kalkulus és C-kalkulus is ekvivalensek egymással.

6.2.33. TÉTEL. Egy elsőrendű $S$ szekvent a $G$ -kalkulusban pontosan akkor bizonyítható, ha bizonyítható a $C$ -kalkulusban is, azaz $⊢_{G} S$ akkor és csak akkor, ha $⊢_{C} S$ .

Jelölje most $[(Γ (y ∥ t)] \to [Δ (y ∥ t)]$ azt a szekventet, amit a $Γ \to Δ$ -ból úgy nyerünk, hogy $Γ$ -ban és $Δ$ -ban minden formulában szabályosan elvégezzük az $(y ∥ t)$ formális helyettesítést.

6.2.34. LEMMA. Ha a $Γ \to Δ$ szekvent bizonyítható a $C$ -kalkulusban, akkor a $[(Γ (y ∥ t)] \to [Δ (y | | t)]$ szekvent is bizonyítható $C$ -ben ugyanolyan magasságú levezetésfával.

BIZONYÍTÁS. Tegyük fel, hogy $⊢_{C} Γ \to Δ$ . A levezetésfa magassága szerinti indukcióval bizonyítunk.

(alaplépés:) Ha $Γ \to Δ$ a C-kalkulusban 1 magasságú levezetésfával bizonyítható, akkor a C-kalkulusban $Γ \to Δ$ axiómaszekvent, azaz van közös formula $Γ$ -ban és $Δ$ -ban, legyen ez $A$ . Ekkor az

$[A (y ∥ t)], [Γ' (y ∥ t)] \to [Δ' (y ∥ t)], [A (y ∥ t)]$

szekvent is axiómaszekvent, tehát 1 magasságú levezetésfával bizonyítható.

(indukciós feltevés:) Ha $Γ \to Δ$ a C-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható, akkor $[Γ (y ∥ t)] \to [Δ (y ∥ t)]$ is a C-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható.

(indukciós lépések:) Legyen most $Γ \to Δ$ a C-kalkulusban $k + 1$ magasságú levezetésfával bizonyítható. Tegyük fel, hogy az utolsó lépésben

a $(\to \supset)$ levezetési szabályt alkalmaztuk. Ebben az esetben a szekvent $Γ \to Δ', A \supset B$ alakú, és az $A, Γ \to Δ', B$ szekvent $k$ magasságú levezetésfával bizonyítható. Az indukciós feltevés szerint tehát

$[A (y ∥ t)], [Γ (y ∥ t)] \to [Δ' (y ∥ t)], [B (y ∥ t)]$

szintén $k$ magasságú levezetésfával bizonyítható. Erre a szekventre alkalmazva a $(\to \supset)$ levezetési szabályt az

$[Γ (y ∥ t)] \to [Δ' (y ∥ t)], [A (y ∥ t)] \supset [B (y ∥ t)]$

szekventet nyerjük $k + 1$ magasságú levezetésfával.

az $(\exists \to)$ levezetési szabályt alkalmaztuk. Ilyen esetben a szekvent $\exists x A, Γ' \to Δ$ alakú, ahol $x \notin Par (Γ', Δ)$ , és az $A, Γ' \to Δ$ szekvent $k$ magasságú levezetésfával bizonyítható. Az indukciós feltevés szerint tehát

$[A (y ∥ t)], [Γ' (y ∥ t)] \to [Δ (y ∥ t)]$

szintén $k$ magasságú levezetésfával bizonyítható. Mivel a kötött változó szabályosan végrehajtott átnevezésével mindig elérhetjük, hogy az eredeti szekventben az egzisztenciális kvantorunk által kötött változó ne csak a $Γ'$ és $Δ$ -beli paraméterektől különbözzön, hanem a $t$ -beli változóktól és magától $y$ -tól is, tegyük fel, hogy $x \neq y$ és $x$ nem fordul elő $t$ -ben. Így ha alkalmazzuk az $(\exists \to)$ levezetési szabályt az

$[A (y ∥ t)], [Γ' (y ∥ t)] \to [Δ (y ∥ t)]$

szekventre, $\exists x [A (y ∥ t)] = [(\exists x A) (y ∥ t)]$ miatt a

$[(\exists x A) (y ∥ t)], [Γ' (y ∥ t)] \to [Δ (y ∥ t)]$

szekventet bizonyítjuk éppen $k + 1$ magasságú levezetésfával.

A többi levezetési szabály esetén a bizonyítás ehhez hasonló módon végezhető el.

Így a lemmát bizonyítottnak tekinthetjük. $⋄$

6.2.35. LEMMA. A $C$ -kalkulus kvantoros levezetési szabályai megfordíthatók, sőt a $(\to \forall)$ és az $(\exists \to)$ levezetési szabályok esetén a következő is igaz:

$\frac{Γ \to Δ, \forall x A}{Γ \to Δ, [A (x ∥ t)]} é s \frac{\exists x A, Γ \to Δ}{[A (x ∥ t)], Γ \to Δ}$

BIZONYÍTÁS. Az $(\forall \to)$ és a $(\to \exists)$ levezetési szabályok a $(b)$ szabályok C-kalkulusból való elérhetősége miatt megfordíthatók. A $(\to \forall)$ és az $(\exists \to)$ levezetési szabályok közül az előbbi megfordíthatóságának igazolásával foglalkozunk, a másiké ehhez hasonlóan igazolható.

Tegyük fel tehát, hogy $⊢_{C} Γ \to Δ, \forall x A$ , ahol $x \notin Par (Γ, Δ)$ . A C-kalkulusbeli levezetésfa magassága szerinti indukcióval bizonyítjuk, hogy $⊢_{C} Γ \to Δ, [A (x ∥ t)]$ .

(alaplépés:) Ha $Γ \to Δ, \forall x A$ a C-kalkulusban 1 magasságú levezetésfával bizonyítható, akkor a C-kalkulusban $Γ \to Δ, \forall x A$ axiómaszekvent, azaz van közös formula $Γ$ -ban és $Δ, \forall x A$ -ban. Két eset lehetséges:

Az axiómaszekvent $B, Γ' \to Δ', B, \forall x A$ alakú. Ekkor a

$B, Γ' \to Δ', B, [A (x ∥ t)]$

szekvent is axiómaszekvent.

Az axiómaszekvent $\forall x A, Γ' \to Δ, \forall x A$ alakú. Ekkor a $\forall x A, Γ' \to Δ, [A (x ∥ t)]$ szekventet kell bizonyítanunk, ami az

$[A (x ∥ t)], \forall x A, Γ' \to Δ, [A (x ∥ t)]$

axiómaszekventből az $(\forall \to)$ szabállyal áll elő.

(indukciósfeltevés:) Ha $Γ \to Δ, \forall x A$ a C-kalkulusban legfeljebb $k$ magasságú levezetésfával bizonyítható, akkor $⊢_{C} Γ \to Δ, [A (x ∥ t)]$ .

(indukcióslépések:) Tegyük fel, hogy $Γ \to Δ, \forall x A$ a C-kalkulusban $k + 1$ magasságú levezetésfával bizonyítható, tehát valamely levezetési szabály alkalmazásával áll elő egy vagy két legfeljebb $k$ magasságú levezetésfából. Ha ez a levezetési szabály

éppen a $(\to \forall)$ szabály és ezzel a $Γ \to Δ, \forall x A$ szekventet a $Γ \to Δ, A$ szekventből vezettük le (ekkor nyilván $x \notin Par (Γ, Δ)$ ). Így a 6.2.34. lemma szerint $Γ \to Δ, [A (x ∥ t)]$ is bizonyítható,
egyébként valamely $Γ' \to Δ', \forall x A$ (és $Γ ″ \to Δ ″, \forall x A$ ) alakú szekvent(ek)ből nyertük $Γ \to Δ, \forall x A$ -t. Az indukciós feltevés miatt

$⊢_{C} Γ' \to Δ', [A (x ∥ t)] (és ⊢_{C} Γ ″ \to Δ ″, [A (x | | t)]) .$

Erre (ezekre) a szekvent(ek)re alkalmazva azt a levezetési szabályt, aminek az eredménye az eredeti levezetésben $Γ \to Δ, \forall x A$ volt, nyerjük a kívánt levezetést.

Ezzel a lemmát igazoltuk. $⋄$

Most belátjuk, hogy a 6.2.24. lemma érvényes marad az elsőrendű C-kalkulus esetében is.

6.2.36. LEMMA. Ha $⊢_{C} Γ \to Δ, A$ és $⊢_{C} A, Γ \to Δ$ , akkor $⊢_{C} Γ \to Δ$ .

BIZONYÍTÁS. Folytassuk a 6.2.24. lemma bizonyítását. Tegyük fel, hogy az $A$ elsőrendű formula jó és

$⊢_{C} Γ \to Δ, \exists x A és ⊢_{C} \exists x A, Γ \to Δ .$

Az első levezetésfa magassága szerinti indukcióval bebizonyítjuk, hogy $\exists x A$ is jó.

(alaplépés:) Ha $Γ \to Δ, \exists x A$ és $\exists x A, Γ \to Δ$ a C-kalkulusban bizonyíthatók, mégpedig az első szekvent 1 magasságú levezetésfával, akkor a C-kalkulusban ez axiómaszekvent. Két eset lehetséges:

Ha $\exists x A, Γ \to Δ$ is axiómaszekvent, akkor van közös formula $Γ$ -ban és $Δ$ -ban, tehát $Γ \to Δ$ is axiómaszekvent, azaz bizonyítható.
Amikor csak $Γ \to Δ, \exists x A$ az axiómaszekvent, akkor

$\exists x A, Γ' \to Δ, \exists x A$

alakú, így a másik szekvent $\exists x A, \exists x A, Γ' \to Δ$ alakú. Alkalmazva a C-ből elérhető $(s z \to)$ szabályt a $\exists x A, Γ' \to Δ$ szekventet kapjuk, ami éppen a bizonyítandó $Γ \to Δ$ .

(indukciós feltevés:) Ha $Γ \to Δ, \exists x A$ és $\exists x A, Γ \to Δ$ a C-kalkulusban bizonyíthatók, és $Γ \to Δ, \exists x A$ levezetésfája legfeljebb $k$ magasságú, akkor $⊢_{C} Γ \to Δ$ .

(indukciós lépések:) Ha $Γ \to Δ, \exists x A$ és $\exists x A, Γ \to Δ$ a C-kalkulusban bizonyíthatók, és az első levezetésfa magassága $k + 1$ , akkor a következő esetek lehetségesek:

Ha a $Γ \to Δ, \exists x A$ szekventet bizonyító levezetésfában az utolsó lépésben a $\to \exists$ szabállyal nyertük a szekventet. Ekkor

$Γ \to Δ, [A (x ∥ t)], \exists x A$

legfeljebb $k$ magasságú levezetésfával bizonyítható. A $(\to b)$ szabály elérhető a C-kalkulusban, tehát $\exists x A, Γ \to Δ$ bizonyíthatósága esetén $\exists x A, Γ \to Δ, [A (x ∥ t)]$ is bizonyítható. Az indukciós feltevés alapján ekkor $⊢_{C} Γ \to Δ, [A (x ∥ t)]$ . Mivel pedig $⊢_{C} \exists x A, Γ \to Δ$ , a 6.2.35. lemma miatt $⊢_{C} [A (x ∥ t)], Γ \to Δ$ is. De ha $A$ jó, nyilván $[A (x ∥ t)]$ is jó, tehát $⊢_{C} Γ \to Δ$ .

Ha pedig a $Γ \to Δ, \exists x A$ szekventet bizonyító levezetésfában az utolsó lépésben más szabályt alkalmaztunk, a bizonyítást az olvasóra bízzuk.

Végül azt, hogy $A$ jóságából $\forall x A$ jósága is következik, hasonlóan lehet bizonyítani. $⋄$

6.2.37. TÉTEL. (AZ ELSŐRENDŰ SZEKVENTKALKULUS HELYESSÉGE.)

Ha a $Γ \to Δ$ szekvent bizonyítható az elsőrendű $C$ -kalkulusban, akkor a $(\land Γ) \supset (\lor Δ)$ formula bizonyítható a predikátumkalkulusban, azaz ha $⊢_{C} Γ \to Δ$ , akkor $⊢ (\land Γ) \supset (\lor Δ)$ .

BIZONYÍTÁS. Folytassuk a 6.2.25. tétel bizonyítását. Tegyük fel, hogy $Γ \to Δ$ a C-kalkulusban $k + 1$ magasságú levezetésfával bizonyítható, tehát valamely levezetési szabály alkalmazásával állt elő egy vagy két legfeljebb $k$ magasságú levezetésfából. Legyen az alkalmazott levezetési szabály a C-kalkulus egy kvantoros szabálya. Ha ez a levezetési szabály a

$(\to \forall)$ szabály volt, a $Γ \to Δ$ szekvent $Γ \to Δ', \forall x A$ alakú, és egy $k$ magasságú levezetésfával levezetett $Γ \to Δ', A$ szekventből nyertük ( $x \notin Par (Γ, Δ')$ ). Az indukciós feltevés szerint ekkor $⊢ (\land Γ) \supset (\lor Δ') \lor A$ , amiből a dedukciós tétellel $(\land Γ) ⊢ (\lor Δ') \lor A$ adódik. Lássuk most be, hogy $⊢ (\land Γ) \supset (\lor Δ') \lor \forall x A$ is. Az implikáció bevezetésével a $(\land Γ) ⊢ (\lor Δ') \lor \forall x A$ szekvencia megalapozására vezethető vissza a bizonyítás. A negáció alkalmazásának, majd bevezetésének a szabályaival azt kapjuk, hogy ez a szekvencia a

$(\land Γ), \neg ((\lor Δ') \lor \forall x A) ⊢ \forall x A és a (\land Γ), \neg ((\lor Δ') \lor \forall x A) ⊢ \neg \forall x A$

szekvenciák igazolásával bizonyítható.

Az első szekvencia igazolásához alkalmazzuk az univerzális kvantor bevezetésének szabályát ( $x$ nem paraméter a hipotézisekben) és alapozzuk meg a $(\land Γ), \neg ((\lor Δ') \lor \forall x A) ⊢ A$ szekvenciát. A vágás szabályának alkalmazásával visszavezethetjük a feladatot a

$(\land Γ) ⊢ (\lor Δ') \lor A és (\lor Δ') \lor A, \neg ((\lor Δ') \lor \forall x A) ⊢ A$

szekvenciák bizonyítására. Az első szekvencia az indukciós feltevés szerint megalapozott. A második igazolásához a diszjunkció alkalmazásával a

$(\lor Δ'), \neg ((\lor Δ') \lor \forall x A) ⊢ A és az A, \neg ((\lor Δ') \lor \forall x A) ⊢ A$

szekvenciákat kell megalapozni. Az első szekvencia esetén a negáció alkalmazásának és bevezetésének szabályait felhasználva a

$(\lor Δ'), \neg ((\lor Δ') \lor \forall x A), \neg A$

hipotézisekből levezetjük a $(\lor Δ') \lor \forall x A$ és a $\neg ((\lor Δ') \lor \forall x A)$ ellentmondást. A második szekvencia az azonosság törvénye.

A $(\land Γ), \neg ((\lor Δ') \lor \forall x A) ⊢ \neg \forall x A$ szekvencia igazolásakor felhasználjuk a negáció alkalmazásának és bevezetésének szabályait, és a

$(\land Γ), \neg ((\lor Δ') \lor \forall x A), \forall x A$

hipotézisekből is levezetjük a

$(\lor Δ') \lor \forall x A és a \neg ((\lor Δ') \lor \forall x A)$

ellentmondást.

A többi kvantoros levezetési szabály esetén a tétel bizonyítása hasonló. $⋄$

6.2.38. LEMMA. Ha $A$ a predikátumkalkulus axiómája, akkor $\to A$ bizonyítható az elsőrendű $C$ -kalkulusban.

BIZONYÍTÁS. A bizonyítást konstruktív módon végezzük el, a predikátumkalkulus (C1)–(C15) axiómasémáiból előállított axiómák és ezek általánosításai esetén rendre megkonstruáljuk a megfelelő szekvent C-kalkulusbeli levezetését. A (C1)–(C10) axiómákkal kapcsolatban a levezetésfákat a 6.2.26. lemma bizonyítása adja.

A (C11)-ből előállított axióma esetén a levezetés:

A (C12)-ből előállított axióma esetén a levezetés:

3-5. A (C13)–(C15)-ből előállított axiómák esetén a levezetések megadását az olvasóra hagyjuk.

6. Mivel ha $A$ a predikátumkalkulus (C1)–(C15)-ből előállított axiómája, akkor $\to A$ bizonyítható, így alkalmazva a $(\to \forall)$ szabályt $\to \forall x A$ is bizonyítható. Ezzel beláttuk, hogy az axiómák általánosításainak megfelelő szekventek is bizonyíthatók.

Tehát a lemmát bebizonyítottuk. $⋄$

A 6.2.35. és a 6.2.36. lemmák biztosítják, hogy a 6.2.27. lemma érvényes az elsőrendű C-kalkulusban is, és így a 6.2.38. lemma felhasználásával a következő tétel igazolható a 6.2.28. tétel bizonyításának gondolatmenetével.

6.2.39. TÉTEL. (AZ ELSŐRENDŰ SZEKVENTKALKULUS TELJESSÉGE.)

Ha $B$ bizonyítható a predikátumkalkulusban, akkor $\to B$ bizonyítható az elsőrendű $C$ -kalkulusban, azaz ha $⊢ B$ , akkor $⊢_{C} \to B$ .

Tehát az elsőrendű szekventkalkulusok is helyes és teljes kalkulusok.

Feladatok

6.2.1. FELADAT. A természetes technika segítségével bizonyítsuk be, hogy

$A \lor B \supset C ⊢_{0} (A \supset C) \land (B \supset C)$
$(A \supset C) \land (B \supset C) ⊢_{0} A \lor B \supset C$
$A \supset B \supset C ⊢_{0} A \land B \supset C$
$A \land B \supset C ⊢_{0} A \supset B \supset C$
$A \supset (B \lor C) ⊢_{0} (A \supset B) \lor (A \supset C)$
$(A \supset B) \lor (A \supset C) ⊢_{0} A \supset (B \lor C)$
$\neg (A \supset B) ⊢_{0} \neg A \lor \neg B$
$A \supset B ⊢_{0} \neg A \lor B$

6.2.2. FELADAT. A természetes technika segítségével bizonyítsuk be, hogy

$⊢ \forall x P (x) \supset \exists x P (x)$
$\neg \forall x P (x) \lor R ⊢ \exists x (P (x) \supset R), ahol x \notin Par (R) .$
$\exists x \forall y Q (x, y) ⊢ \forall y \exists x Q (x, y)$
$\forall x \forall y Q (x, y) ⊢ \forall y \forall x Q (x, y)$
$\forall x P (x) \lor \forall x R (x) ⊢ \forall x (P (x) \lor R (x))$
$\exists x (P (x) \land R (x)) ⊢ \exists x P (x) \land \exists x R (x)$

6.2.3. FELADAT. Bizonyítsuk be a következő ítéletlogikai szekventeket a szekventkalkulusban:

$A \lor B \supset C \to (A \supset C) \land (B \supset C)$
$(A \supset C) \land (B \supset C) \to A \lor B \supset C$
$A \supset B \supset C \to A \land B \supset C$
$A \land B \supset C \to A \supset B \supset C$
$A \supset (B \lor C) \to (A \supset B) \lor (A \supset C)$
$(A \supset B) \lor (A \supset C) \to A \supset (B \lor C)$
$\neg (A \supset B) \to \neg A \lor \neg B$
$A \supset B \to \neg A \lor B$

6.2.4. FELADAT. Bizonyítsuk be a következő szekventeket az elsőrendű szekventkalkulusban:

$\to \forall x P (x) \supset \exists x P (x)$
$\neg \forall x P (x) \lor R \to \exists x (P (x) \supset R), ahol x \notin Par (R) .$
$\exists x \forall y Q (x, y) \to \forall y \exists x Q (x, y)$
$\forall x \forall y Q (x, y) \to \forall y \forall x Q (x, y)$
$\forall x P (x) \lor \forall x R (x) \to \forall x (P (x) \lor R (x))$
$\exists x (P (x) \land R (x)) \to \exists x P (x) \land \exists x R (x)$