Ugrás a tartalomhoz

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

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

Panem Kft.

Gentzen-stílusú kalkulusok

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 ΓΔ halmazt Γ,Δ-val és a Γ{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 Δ,A0B, akkor Δ0AB. Ekkor viszont a Γ0A-t és a Δ,A0B-t igazoló levezetések konkatenációja megalapozza Γ,Δ0B-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

Γ 0 A Γ , B 0 A

Γ , B , B , Δ 0 A Γ , B , Δ 0 A

a felcserélés szabálya

a vágás szabálya

Γ , B , C , Δ 0 A Γ , C , B , Δ 0 A

Γ 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

( b )

Γ , A 0 B Γ 0 A B

( a )

Γ 0 A Γ 0 A B Γ 0 B

( b )

Γ 0 A Γ 0 B Γ 0 A B

( a )

Γ , A , B 0 C Γ , A B 0 C

( b )

Γ 0 A Γ 0 A B Γ 0 B Γ 0 A B

( a )

Γ , A 0 C Γ , B 0 C Γ , A B 0 C

( ¬ b )

Γ , A 0 B Γ , A 0 ¬ B Γ 0 ¬ A

( ¬ a )

Γ 0 ¬ ¬ 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.

  1. Az implikáció bevezetésének szabálya épp a dedukciós tétel.

  2. Az implikációt alkalmazó szabály: Ha adottak a Γ0A és a Γ0AB á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ő.

  3. A diszjunkció bevezetése: Ha adott Γ-ból A-nak a levezetése, akkor az AAB axiómát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk a Γ-ból az AB egy levezetését.

  4. A diszjunkció alkalmazása: Ha adottak a Γ,A0C és a Γ,B0C állításokat megalapozó levezetések, akkor a dedukciós tétel miatt megkonstruálhatók a Γ0AC és a Γ0BC állításokat megalapozó levezetések is. Ezt a két levezetést konkatenáljuk, és írjuk le az (AC)((BC)(ABC)) axiómát. Kétszer alkalmazva a modus ponenst megalapoztuk, hogy Γ0ABC. Írjuk be a levezetésbe a vonal alatti szekvenciából az AB hipotézist, és ha most újból alkalmazzuk a modus ponenst, megkapjuk a Γ,AB0C-t megalapozó levezetést.

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

0 A ( ¬ A B ) .

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

1.

A , ¬ A , ¬ B 0 A

[ az azonosság törvénye alapján ]

2.

A , ¬ A , ¬ B 0 ¬ A

[ az azonosság törvénye alapján ]

3.

A , ¬ A 0 ¬ ¬ B

[ 1-ből és 2-ből (¬b) ]

4.

A , ¬ A 0 B

[ 3-ból (¬a) ]

5.

A 0 ¬ A B

[ (b) ]

6.

0 A ( ¬ A B )

[ (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 AB-ből C-t, akkor az esetelemzés a következőképpen történik: ha AB 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 ¬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 ¬B-t is.

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

0 A ( ¬ A 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 , ¬ A 0 B

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

A , ¬ A 0 ¬ ¬ 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,¬A,¬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 ¬A is levezethető.

6.2.3. PÉLDA. Igazoljuk, hogy

0 ( A B C ) B ¬ C ¬ A .

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

A B C , B , ¬ C 0 ¬ 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 ¬C. Mivel ¬C szerepel a hipotézisek között, az azonosság törvénye szerint teljesül, hogy

A ( B C ) , B , ¬ C , A 0 ¬ C .

Tehát már csak az

A ( B C ) , B , ¬ 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 ( B C ) , B , ¬ C , A 0 B

és az

A ( B C ) , B , ¬ C , A 0 B 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 ( B C ) , B , ¬ C , A 0 A

és

A ( B C ) , B , ¬ C , A 0 A ( B 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 0A¬A. Első ötletünk az, hogy alkalmazzuk a diszjunkció bevezetésének a szabályát. Ekkor vagy a 0A, vagy a 0¬A szekvenciát kellene megalapoznunk, ami nyilvánvaló, hogy nem megy. Próbálkozzunk másképp. 0A¬A helyett – alkalmazva a negáció alkalmazásának a szabályát – igazoljuk a

0 ¬ ¬ ( A ¬ A )

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

¬ ( A ¬ A ) 0 ¬ A és ¬ ( A ¬ A ) 0 ¬ ¬ A .

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

¬ ( A ¬ A ) , A 0 ¬ ( A ¬ A ) és ¬ ( A ¬ A ) , A 0 A ¬ A .

A bal oldali szekvencia az azonosság törvénye miatt nyilvánvaló, a jobb oldali a ¬(A¬A),A0A szekvenciából (azonosság törvénye) nyerhető diszjunkció bevezetésével. Hasonlóan bizonyítható a

¬ ( A ¬ A ) 0 ¬ ¬ A

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

¬ ( A ¬ A ) , ¬ A 0 ¬ ( A ¬ A ) és ¬ ( A ¬ A ) , ¬ A 0 A ¬ A .

6.2.5. PÉLDA. Most lássuk be, hogy ¬AB,C¬B,A0¬C. A negáció bevezetésének a szabályát alkalmazva a

¬ A B , C ¬ B , A , C 0 A és ¬ A B , C ¬ B , A , C 0 ¬ 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

¬ A , C ¬ B , A , C 0 ¬ A és B , C ¬ B , A , C 0 ¬ 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 ¬ B , C 0 ¬ B és ¬ B , B , A 0 ¬ 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 ¬ B , C 0 C ¬ B és C ¬ B , C 0 C .

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

¬ B , B , A 0 B és ¬ B , B , A 0 ¬ 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 Γ0B szekvenciát a D1,D2,,Dm(m1) levezetés megalapozta. Ekkor minden j=1,2,,m-re Dj vagy hipotézis, vagy axiómaformula, vagy van olyan 1s,tj, hogy a Ds és a Dt formulákból modus ponenssel állt elő.

  1. Ha Dj hipotézis, azaz eleme a Γ formulahalmaznak, akkor a Γ0Dj az azonosság törvénye.

  2. Ha Dj az (A1)–(A10) axiómasémákból nyert formula, akkor 0Dj 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 – Γ0Dj is bizonyítható természetes technikával.

  3. Tegyük végül fel, hogy Dj a modus ponenssel állt elő a Ds és a Dt formulákból. Ha a Γ0Ds és a Γ0Dt szekvenciák megalapozhatók természetes technikával, akkor az implikáció alkalmazásának a szabályával a Γ0Dj-t is bizonyítottuk.

Tehát a levezetés minden Dj formulája esetén Γ0Dj 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 Γ0A, 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

( b )

Γ A Γ x A ( x Par  ( Γ ) )

( a )

Γ x A Γ [ A ( x t ) ]

( b )

Γ [ A ( x t ) ] Γ x A

( a )

Γ , A B Γ , x A B ( x Par  ( Γ , B ) )


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

  1. Az univerzális kvantor bevezetésének szabálya éppen az általánosítás szabálya (6.1.44. tétel).

  2. Az univerzális kvantor alkalmazásának szabálya: Ha adott a ΓxA szekvenciát megalapozó levezetés, akkor a xA[A(xt)] axiómát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk [A(xt)] egy levezetését Γ-ból.

  3. Az egzisztenciális kvantort bevezető szabály: Ha adott a Γ[A(xt)] szekvenciát megalapozó levezetés, akkor írjuk be az [A(xt)]xA axiómát a levezetésbe, és alkalmazzuk a modus ponenst. Így Γ-ból levezettük xA-t.

  4. Az egzisztenciális kvantor alkalmazásának szabálya: Ha adott a Γ,AB szekvenciát megalapozó levezetés, akkor a dedukciós tétel miatt megkonstruálható a ΓAB szekvenciát megalapozó levezetés is. Ebből az általánosítás szabálya miatt – mivel xPar (Γ)Γx(AB) adódik. Ha most a levezetésbe beírjuk a x(AB)(xAB) axiómát (lényeges, hogy xPar (B)), alkalmazhatjuk a modus ponenst. Ezzel megkapjuk a xAB egy levezetését Γ-ból. A dedukciós tétel újbóli alkalmazásával pedig igazoltuk, hogy Γ,xAB.

6.2.6. PÉLDA. A természetes levezetés technikája segítségével példánkban bebizonyítjuk, hogy xA¬x¬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¬x¬A, hisz xPar (¬x¬A). A jobb oldali negáció miatt érdemes alkalmazni a negáció bevezetést: alapozzuk meg az

A , x ¬ A A és az A , x ¬ A ¬ 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,x¬Ax¬A szekvenciára, ami szintén az azonosság törvénye.

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

¬ x ¬ A , ¬ x A ¬ x ¬ A és a ¬ x ¬ A , ¬ x A x ¬ 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 ¬x¬A,¬xA¬A. Újból a negáció bevezetése segítségével folytatva a levezetést kapjuk, hogy a

¬ x ¬ A , ¬ x A , A ¬ x A és a ¬ x ¬ A , ¬ x A , A 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 ¬x¬A,¬xA,A[A(xx)] 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 ΓΔ-val jelöljük.

Megengedjük, hogy a (Γ,Δ) szekventben akár Γ, akár Δ egyetlen formulát se tartalmazzon. Ha a Γ sorozat üres, a szekventet Δ-val, ha a Δ sorozat üres, Γ-lal jelöljük. Mindkét formulasorozat is lehet üres, ekkor a szekvent üres szekvent, amit jelöl. Ha Γ az A1,A2,,An és Δ a B1,B2,,Bm (nemrendezett) formulasorozat, továbbá A és B ítéletlogikai formulák, akkor A,ΓΔ,B-t írunk, ha az A,A1,A2,,AnB1,B2,,Bm,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 (ΓΔ) 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 ΓΔ szekventhez h igazságértéket.

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

( ) = h ,

( B ) = ( B ) ,

( A ) = ( ¬ A ) ,

( A B ) = ( A B ) ,

( A 1 , A 2 B 1 , B 2 ) = ( A 1 A 2 B 1 B 2 ) ,

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

( A 1 , A 2 , , A n B 1 , B 2 , , B m ) = = ( A 1 A 2 A n B 1 B 2 B m ) .

Gondolhatunk tehát a ΓΔ 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 X

levezetési szabályok

( s z )

( s z )

Γ Δ , X , X Γ Δ , X

X , X , Γ Δ X , Γ Δ

( b )

( b )

Γ Δ Γ Δ , X

Γ Δ X , Γ Δ

( )

( )

X , Γ Δ , Y Γ Δ , ( X Y )

Γ Δ , X Y , Γ Δ ( X Y ) , Γ Δ

( )

( )

Γ Δ , X Γ Δ , Y Γ Δ , ( X Y )

X , Γ Δ ( X Y ) , Γ Δ Y , Γ Δ ( X Y ) , Γ Δ

( )

( )

Γ Δ , X Γ Δ , ( X Y ) Γ Δ , Y Γ Δ , ( X Y )

X , Γ Δ Y , Γ Δ ( X Y ) , Γ Δ

( ¬ )

( ¬ )

X , Γ Δ Γ Δ , ¬ X

Γ Δ , X ¬ X , Γ Δ


Table 6.10. A C-kalkulus

axiómaséma

X , Γ Δ , X

levezetési szabályok

( )

X , Γ Δ , Y Γ Δ , ( X Y )

( )

Γ Δ , X Y , Γ Δ ( X Y ) , Γ Δ

( )

Γ Δ , X Γ Δ , Y Γ Δ , ( X Y )

( )

X , Y , Γ Δ ( X Y ) , Γ Δ

( )

Γ Δ , X , Y Γ Δ , ( X Y )

( )

X , Γ Δ Y , Γ Δ ( X Y ) , Γ Δ

( ¬ )

X , Γ Δ Γ Δ , ¬ X

( ¬ )

Γ Δ , X ¬ X , Γ Δ


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 () szabály segítségével a következőképpen állíthatunk elő szekventet: ha rendelkezésünkre állnak a ΓΔ,A és a ΓΔ,B szekventek, akkor azt mondjuk, hogy a () levezetési szabállyal előáll a ΓΔ,(AB) 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ő:

  1. 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.

  2. Ha Dm 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

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.

  1. Ha D1 és D2 rendre m1 és m2 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,

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 (m1,m2)+1.

  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 A(BA) 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,BA 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: KS.

6.2.13. PÉLDA.

  1. Az ABBA szekvent a G-kalkulusban az alábbi – 3 magasságú – levezetésfával bizonyítható:

  1. A (ABC)(A(BC)) 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 K1 a G- és C-kalkulusok egyikét, és K2 a másikat. Azt mondjuk, hogy egy a K1-kalkulusbeli

S 1 S 2

levezetési szabály elérhető a K2-kalkulusból, ha minden olyan esetben, amikor K2S1, akkor K2S2 is. Hasonlóan, egy a K1-kalkulusbeli

S 1 S 2 S 3

levezetési szabály elérhető a K2-kalkulusból, ha minden olyan esetben, amikor K2S1 és K2S2, akkor K2S3 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 GA,ΓΔ,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 A1,A2,,An és Δ a B1,B2,,Bm 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 (), (), (), (), (¬), (¬) 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 () és () levezetési szabályok esetén pedig megkonstruáljuk a levezetésfát.

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

Tehát az AB,ΓΔ szekvent is bizonyítható a G-kalkulusban.

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

Tehát a ΓΔ,AB 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 CS, akkor GS.

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 GS.

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

(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 D1 és egy D2 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 D1 és a D2 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 CAA.

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

BIZONYÍTÁS. A G-kalkulus (), (), (), (), (¬), (¬) 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ΓΔ. A bizonyítás a C-kalkulusbeli levezetésfa magassága szerinti indukcióval történik.

    (alaplépés:) Ha ΓΔ a C-kalkulusban 1 magasságú levezetésfával bizonyítható, akkor ΓΔ a C-kalkulusban axióma, azaz a Γ és a Δ formulasorozatban van közös formula. De ekkor az A,ΓΔ és a ΓΔ,A is axióma, tehát 1 magasságú levezetésfával bizonyítható.

    (indukciós feltevés:) Ha ΓΔ a C-kalkulusban legfeljebb k magasságú levezetésfával bizonyítható, akkor CA,ΓΔ és CΓΔ,A is legfeljebb k magasságú levezetésfával bizonyítható.

    (indukciós lépések:) Legyen most ΓΔ a C-kalkulusban k+1 magasságú levezetésfával bizonyítható. Ekkor ΓΔ valamely C-kalkulusbeli levezetési szabály alkalmazásával állt elő vagy egy D, vagy egy D1 és egy D2 legfeljebb k magasságú C-kalkulusbeli levezetésfá(k)ból.

    Tegyük fel, hogy a () levezetési szabály alkalmazásával állt elő ΓΔ, tehát a Γ formulasorozatban szerepel valamilyen B és C formulák konjunkciója. Jelölje Γ a Γ-beli formulák BC nélküli sorozatát. Az indukciós feltevés szerint, mivel B,C, Γ Δk magasságú levezetésfával bizonyítható volt C-ben,

A , B , C , Γ Δ , illetve B , C , Γ Δ , A

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

A , B C , Γ Δ , tehát A , Γ Δ ,

illetve

B C , Γ Δ , A , tehát Γ Δ , 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 (sz) 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 () levezetési szabály elérhetőségét. Tegyük fel, hogy CA,ΓΔ. Mivel (b) elérhető C-ből, CA,B,ΓΔ. Erre a szekventre alkalmazva a C-beli () levezetési szabályt kapjuk, hogy CAB,ΓΔ.

  • A () 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 GS, akkor CS.

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 CS.

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

(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 D1 és egy D2 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 D1 és a D2 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

S 1 S 2

levezetési szabály megfordítható, ha minden olyan esetben, amikor az S2 szekvent bizonyítható, akkor az S1 szekvent is bizonyítható. Hasonlóan, egy

S 1 S 2 S 3

levezetési szabály megfordítható, ha minden olyan esetben, amikor az S3 szekvent bizonyítható, akkor S1 és S2 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 () 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ΓΔ,AB. A C-kalkulusbeli levezetésfa magassága szerinti indukcióval bizonyítjuk, hogy CA,ΓΔ,B.

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

  • Az axiómaszekvent C, Γ Δ ,C,AB alakú. Ekkor az A,C, Γ Δ ,C,B szekvent is axiómaszekvent.

  • Az axiómaszekvent AB, Γ Δ,AB alakú. Ekkor az A,AB, Γ Δ,B szekventet kell bizonyítanunk, ami az

A , Γ Δ , B , A és az A , B , Γ Δ , B

  • axiómaszekventekből az () szabállyal áll elő.

(indukciós feltevés:) Ha ΓΔ,AB a C-kalkulusban legfeljebb k magasságú levezetésfával bizonyítható, akkor CA,ΓΔ,B.

(indukciós lépések:) Tegyük fel, hogy ΓΔ,AB 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 (), (), (), (), (), (), (¬), (¬) szabályai közül valamelyik lehet. Ha ez a levezetési szabály

  • éppen a () szabály és ezzel a ΓΔ,AB szekventet az A,ΓΔ,B szekventből vezettük le, akkor nyilván A,ΓΔ,B is bizonyítható,

  • egyébként valamely Γ Δ ,AB (és Γ Δ ,AB) alakú szekvent(ek)ből nyertük ΓΔ,AB-t. Ekkor az indukciós feltételezés miatt CA, Γ Δ ,B (és CA, Γ Δ ,B). Erre (ezekre) a szekvent(ek)re alkalmazva azt a levezetési szabályt, aminek az eredménye az eredeti levezetésben ΓΔ,AB 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 ABBA szekvent esetén ha ,,alulról felfelé” haladva először nem a () szabályt, hanem a () szabályt alkalmazzuk, akkor vagy az ABA, vagy a BBA szekventhez jutunk. A következő lépésben a () szabályt alkalmazhatjuk: az első esetben az AB és az AA, a második esetben pedig a BB és a BA 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ΓΔ,A és CA,ΓΔ, akkor CΓΔ.

BIZONYÍTÁS. Nevezzük a bizonyítás során jónak az A formulát, ha amikor CΓΔ,A és CA,ΓΔ, akkor CΓΔ 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ΓΔ,A és CA,ΓΔ. Az első szekvent levezetésfájának a magassága szerinti indukcióval bebizonyítjuk, hogy A jó.

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

  • Ha A,ΓΔ is axiómaszekvent, akkor ΓΔ is az, tehát bizonyítható.

  • Ha A,ΓΔ nem axiómaszekvent, akkor Γ=A, Γ , és így ez a szekvent A,A, Γ Δ alakú. Alkalmazva az (sz) szabályt A, Γ Δ bizonyíthatóságát kapjuk, ami a bizonyítandó ΓΔ szekvent.

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

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

  • Ha A,ΓΔ axiómaszekvent, akkor A,Γ Δ ,A alakú, mivel feltehető, hogy Γ-nak és Δ-nak nincs közös formulája, hisz ΓΔ,A nem axiómaszekvent (1-nél magasabb levezetésfával bizonyítható). Tehát a ΓΔ,A szekvent Γ Δ ,A,A alakú. Alkalmazva a (sz) szabályt kapjuk, hogy ΓΔ bizonyítható.

  • Egyébként, mivel A prímformula, a szekventeket ugyanazon levezetési szabály alkalmazásával nyertük:

    • vagy rendre valamely Γ Δ ,A és A, Γ Δ szekventekből,

    • vagy az elsőt valamely Γ Δ ,A és Γ Δ ,A, a másodikat pedig A, Γ Δ és A, Γ Δ szekventpárokból.

Az indukciós feltevés miatt Γ Δ , illetve Γ Δ és Γ Δ 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 ΓΔ 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 ¬A is jó. Ekkor ugyanis ha

C Γ Δ , ¬ A és C ¬ A , Γ Δ ,

mivel a (¬) és (¬) levezetési szabályok megfordíthatók,

C A , Γ Δ és C Γ Δ , A .

De A jó, ezért fennáll CΓΔ is.

Legyenek most A és B jók, és igazoljuk, hogy AB is jó. Ha

C Γ Δ , A B és C A B , Γ Δ ,

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

C Γ Δ , A , C Γ Δ , B és C A , B , Γ Δ .

Mivel a (b) levezetési szabály elérhető a C-kalkulusban, és CΓΔ,A, így CB,ΓΔ,A is. Továbbá mivel A jó,

C B , Γ Δ , A és C A , B , Γ Δ

esetén CB,ΓΔ. Ebből, CΓΔ,B-ből és mert B is jó, adódik, hogy CΓΔ is fennáll. Tehát AB is jó.

Hasonlóan AB és AB 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 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 A1,A2,,An és Δ a B1,B2,,Bm (nemrendezett) formulasorozat, akkor a A1A2An formulára (Γ)-val és a B1B2Bm formulára (Δ)-val fogunk hivatkozni.

6.2.25. TÉTEL. (A SZEKVENTKALKULUS HELYESSÉGE.) Ha a ΓΔ szekvent bizonyítható a C-kalkulusban, akkor a (Γ)(Δ) formula bizonyítható az ítéletkalkulusban, azaz ha CΓΔ, akkor 0(Γ)(Δ).

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

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

(indukciós feltevés:) Ha ΓΔ a C-kalkulusban legfeljebb k magasságú levezetésfával bizonyítható, akkor 0(Γ)(Δ).

(indukciós lépések:) Tegyük fel, hogy ΓΔ 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

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

( Γ ) 0 ( Δ ) ¬ A B és a ( Δ ) ¬ A B 0 ( Δ ) ( A B )

szekvenciákat elég bizonyítanunk.

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

A ( Γ ) ( Δ ) B , ( Γ ) 0 ( Δ ) ¬ A B

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

A ( Γ ) ( Δ ) B , ( Γ ) , ¬ ( ( Δ ) ¬ A B )

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

A ( Γ ) ( Δ ) B , ( Γ ) , ¬ ( ( Δ ) ¬ A B ) , ¬ A

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

A ( Γ ) ( Δ ) B , ( Γ ) , ¬ ( ( Δ ) ¬ A B ) , A

formulákból a (( Δ )¬AB) és ¬(( Δ )¬AB) ellentmondást lehet könnyen levezetni.

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

( Δ ) 0 ( Δ ) ( A B ) ,

a

¬ A 0 ( Δ ) ( A B )

és a

B 0 ( Δ ) ( A 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 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.

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

  1. 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 CA és CAB, akkor CB.

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

6.2.28. TÉTEL. (A SZEKVENTKALKULUS TELJESSÉGE.) Ha B bizonyítható az ítéletkalkulusban, akkor B bizonyítható a C-kalkulusban, azaz ha 0B, akkor CB.

BIZONYÍTÁS. Tegyük fel, hogy 0B, tehát adott a D1,D2,,Dm=B levezetés. Megmutatjuk, hogy a levezetés minden Dk(1km) formulája esetén CDk.

  1. D 1 axiómaformula, ezért a 6.2.26. lemma szerint CD1.

  2. Tegyük most fel, hogy minden (nk)-ra igazoltuk már, hogy CDn.

  3. Ha most Dk+1 axiómaformula, akkor a 6.2.26. lemma szerint CDk+1. Ha Dk+1 modus ponenssel állt elő Ds-ből és Dt=DsDk+1-ből, akkor s,tk miatt az indukciós feltételből CDs és CDsDk+1 adódik. A 6.2.27. lemma miatt innen CDk+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 [Vv] 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 ΓΔ-val jelöljük.

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

Legyen az [Vv] nyelv egy interpretációja és κ egy -beli változókiértékelés. Legyen |ΓΔ|,κ 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 |ΓΔ|,κ 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 –

| A 1 , A 2 , , A n B 1 , B 2 , , B m | , κ = = | A 1 A 2 A n B 1 B 2 B m | , κ .

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

( )

[ A ( x t ) ] , Γ Δ x A , Γ Δ

( )

Γ Δ , A Γ Δ , x A ( x Par  ( Γ , Δ ) )

( )

A , Γ Δ x A , Γ Δ ( x Par  ( Γ , Δ ) )

( )

Γ Δ , [ A ( x t ) ] Γ Δ , x A


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

( )

[ A ( x t ) ] , x A , Γ Δ x A , Γ Δ

( )

Γ Δ , A Γ Δ , x A ( x Par  ( Γ , Δ ) )

( )

A , Γ Δ x A , Γ Δ ( x Par  ( Γ , Δ ) )

( )

Γ Δ , [ A ( x | | t ) ] , x A Γ Δ , x A


6.2.31. PÉLDA. A ¬xP(x)Rx(P(x)R) szekvent (ahol xPar (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 () és az () levezetési szabályok megegyeznek, így csak az () és a () levezetési szabályok kölcsönös elérhetőségét kell bizonyítani.

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

G [ A ( x t ) ] , x A , Γ Δ ,

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

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

  1. A G-kalkulusbeli () és () levezetési szabályok C-ből való elérhetőségéhez először be kell látni, hogy az (sz) é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)],ΓΔ. De C-ből elérhető a (b) levezetési szabály, így C-ben bizonyítható a [A(x||t)],xAΓΔ szekvent is. Erre alkalmazva a ()C-beli szabályt, a bizonyítani kívánt szekventet nyerjük.

A () 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 GS akkor és csak akkor, ha CS.

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

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

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

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

[ A ( y t ) ] , [ Γ ( y t ) ] [ Δ ( y t ) ] , [ A ( y t ) ]

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

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

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

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

[ A ( y t ) ] , [ Γ ( y t ) ] [ Δ ( y t ) ] , [ B ( y t ) ]

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

[ Γ ( y t ) ] [ Δ ( y t ) ] , [ A ( y t ) ] [ B ( y t ) ]

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

  • az () levezetési szabályt alkalmaztuk. Ilyen esetben a szekvent xA, Γ Δ alakú, ahol xPar ( Γ ,Δ), és az A, Γ Δ szekvent k magasságú levezetésfával bizonyítható. Az indukciós feltevés szerint tehát

[ A ( y t ) ] , [ Γ ( y t ) ] [ Δ ( 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 xy és x nem fordul elő t-ben. Így ha alkalmazzuk az () levezetési szabályt az

[ A ( y t ) ] , [ Γ ( y t ) ] [ Δ ( y t ) ]

szekventre, x[A(yt)]=[(xA)(yt)] miatt a

[ ( x A ) ( y t ) ] , [ Γ ( y t ) ] [ Δ ( 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 () és az () levezetési szabályok esetén a következő is igaz:

Γ Δ , x A Γ Δ , [ A ( x t ) ] é s x A , Γ Δ [ A ( x t ) ] , Γ Δ

BIZONYÍTÁS. Az () és a () levezetési szabályok a (b) szabályok C-kalkulusból való elérhetősége miatt megfordíthatók. A () és az () 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ΓΔ,xA, ahol xPar (Γ,Δ). A C-kalkulusbeli levezetésfa magassága szerinti indukcióval bizonyítjuk, hogy CΓΔ,[A(xt)].

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

  • Az axiómaszekvent B, Γ Δ ,B,xA alakú. Ekkor a

B , Γ Δ , B , [ A ( x t ) ]

szekvent is axiómaszekvent.

  • Az axiómaszekvent xA, Γ Δ,xA alakú. Ekkor a xA, Γ Δ,[A(xt)] szekventet kell bizonyítanunk, ami az

[ A ( x t ) ] , x A , Γ Δ , [ A ( x t ) ]

axiómaszekventből az () szabállyal áll elő.

(indukciósfeltevés:) Ha ΓΔ,xA a C-kalkulusban legfeljebb k magasságú levezetésfával bizonyítható, akkor CΓΔ,[A(xt)].

(indukcióslépések:) Tegyük fel, hogy ΓΔ,xA 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 () szabály és ezzel a ΓΔ,xA szekventet a ΓΔ,A szekventből vezettük le (ekkor nyilván xPar (Γ,Δ)). Így a 6.2.34. lemma szerint ΓΔ,[A(xt)] is bizonyítható,

  • egyébként valamely Γ Δ ,xA (és Γ Δ ,xA) alakú szekvent(ek)ből nyertük ΓΔ,xA-t. Az indukciós feltevés miatt

C Γ Δ , [ A ( x t ) ] ( és C Γ Δ , [ A ( x | | t ) ] ) .

Erre (ezekre) a szekvent(ek)re alkalmazva azt a levezetési szabályt, aminek az eredménye az eredeti levezetésben ΓΔ,xA 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ΓΔ,A és CA,ΓΔ , akkor CΓΔ.

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 Γ Δ , x A és C x A , Γ Δ .

Az első levezetésfa magassága szerinti indukcióval bebizonyítjuk, hogy xA is jó.

(alaplépés:) Ha ΓΔ,xA és xA,ΓΔ 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 xA,ΓΔ is axiómaszekvent, akkor van közös formula Γ-ban és Δ-ban, tehát ΓΔ is axiómaszekvent, azaz bizonyítható.

  • Amikor csak ΓΔ,xA az axiómaszekvent, akkor

x A , Γ Δ , x A

alakú, így a másik szekvent xA,xA, Γ Δ alakú. Alkalmazva a C-ből elérhető (sz) szabályt a xA, Γ Δ szekventet kapjuk, ami éppen a bizonyítandó ΓΔ.

(indukciós feltevés:) Ha ΓΔ,xA és xA,ΓΔ a C-kalkulusban bizonyíthatók, és ΓΔ,xA levezetésfája legfeljebb k magasságú, akkor CΓΔ.

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

  • Ha a ΓΔ,xA szekventet bizonyító levezetésfában az utolsó lépésben a szabállyal nyertük a szekventet. Ekkor

Γ Δ , [ A ( x t ) ] , x A

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

  • Ha pedig a ΓΔ,xA 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 xA jósága is következik, hasonlóan lehet bizonyítani.

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

Ha a ΓΔ szekvent bizonyítható az elsőrendű C-kalkulusban, akkor a (Γ)(Δ) formula bizonyítható a predikátumkalkulusban, azaz ha CΓΔ, akkor (Γ)(Δ).

BIZONYÍTÁS. Folytassuk a 6.2.25. tétel bizonyítását. Tegyük fel, hogy ΓΔ 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

  • ( ) szabály volt, a ΓΔ szekvent Γ Δ ,xA alakú, és egy k magasságú levezetésfával levezetett Γ Δ ,A szekventből nyertük (xPar (Γ, Δ )). Az indukciós feltevés szerint ekkor (Γ)( Δ )A, amiből a dedukciós tétellel (Γ)( Δ )A adódik. Lássuk most be, hogy (Γ)( Δ )xA is. Az implikáció bevezetésével a (Γ)( Δ )xA 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

( Γ ) , ¬ ( ( Δ ) x A ) x A és a ( Γ ) , ¬ ( ( Δ ) x A ) ¬ 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 (Γ),¬(( Δ )xA)A szekvenciát. A vágás szabályának alkalmazásával visszavezethetjük a feladatot a

( Γ ) ( Δ ) A és ( Δ ) A , ¬ ( ( Δ ) 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

( Δ ) , ¬ ( ( Δ ) x A ) A és az A , ¬ ( ( Δ ) 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

( Δ ) , ¬ ( ( Δ ) x A ) , ¬ A

hipotézisekből levezetjük a ( Δ )xA és a ¬(( Δ )xA) ellentmondást. A második szekvencia az azonosság törvénye.

  • A (Γ),¬(( Δ )xA)¬xA szekvencia igazolásakor felhasználjuk a negáció alkalmazásának és bevezetésének szabályait, és a

( Γ ) , ¬ ( ( Δ ) x A ) , x A

hipotézisekből is levezetjük a

( Δ ) x A és a ¬ ( ( Δ ) 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 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.

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

  1. 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 A bizonyítható, így alkalmazva a () szabályt xA 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 B bizonyítható az elsőrendű C-kalkulusban, azaz ha B, akkor CB.

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

  1. A B C 0 ( A C ) ( B C )

  2. ( A C ) ( B C ) 0 A B C

  3. A B C 0 A B C

  4. A B C 0 A B C

  5. A ( B C ) 0 ( A B ) ( A C )

  6. ( A B ) ( A C ) 0 A ( B C )

  7. ¬ ( A B ) 0 ¬ A ¬ B

  8. A B 0 ¬ A B

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

  1. x P ( x ) x P ( x )

  2. ¬ x P ( x ) R x ( P ( x ) R ) , ahol x Par  ( R ) .

  3. x y Q ( x , y ) y x Q ( x , y )

  4. x y Q ( x , y ) y x Q ( x , y )

  5. x P ( x ) x R ( x ) x ( P ( x ) R ( x ) )

  6. x ( P ( x ) R ( x ) ) x P ( x ) x R ( x )

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

  1. A B C ( A C ) ( B C )

  2. ( A C ) ( B C ) A B C

  3. A B C A B C

  4. A B C A B C

  5. A ( B C ) ( A B ) ( A C )

  6. ( A B ) ( A C ) A ( B C )

  7. ¬ ( A B ) ¬ A ¬ B

  8. A B ¬ A B

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

  1. x P ( x ) x P ( x )

  2. ¬ x P ( x ) R x ( P ( x ) R ) , ahol x Par  ( R ) .

  3. x y Q ( x , y ) y x Q ( x , y )

  4. x y Q ( x , y ) y x Q ( x , y )

  5. x P ( x ) x R ( x ) x ( P ( x ) R ( x ) )

  6. x ( P ( x ) R ( x ) ) x P ( x ) x R ( x )