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

Chapter 6. A logika szintaktikus tárgyalása

Bizonyításelmélet

Az ítéletlogikában a szemantikus eldöntésprobléma megoldásakor a vizsgált ítéletlogikai formuláról el kell tudni dönteni azt, hogy tautológia-e, esetleg azt, hogy kielégíthetetlen-e. A döntéshez egy $n$ -változós formula esetén a formula összes – $2^{n}$ különböző – interpretációjában szükséges lehet a formula vizsgálata. Ez akkor is kezelhetetlen feladat, ha a ,,lusta” kiértékeléssel dolgozunk. Az elsőrendű logika vonatkozásában ugyanez a feladat annak a kérdésnek az eldöntése, hogy egy elsőrendű formula logikailag igaz-e (logikai törvény-e). Mivel a megszámlálható univerzum esetén a lehetséges modellek száma kontinuum, az esetek végignézése szóba sem jöhet. Ezért olyan módszereket kerestek, amelyek a formula szintaktikai jellegzetességeit használják ki, és egy olyan szintaktikus eldöntésproblémára adnak döntési eljárást, amely megoldása az eredeti szemantikus eldöntésprobléma megoldását vonja maga után.

Egy ilyen döntési eljárás során ,,adatokból” – egy formulából vagy egy formulahalmazból – kiindulva az eljárás lépései során formulák egy sorozatát állítjuk elő. Ezt a formulasorozatot levezetésnek nevezzük. Az eljáráshoz levezetési szabályok tartoznak, amelyek formulákból új formulát alkotva lehetővé teszik a levezetés előállítását. Minden döntési eljárás esetén adott egy ún. megállási feltétel. Ez általában egy meghatározott formula megjelenése a levezetésben vagy a levezetés speciális szerkezetűvé válása. Egy konkrét döntési eljárás esetén az a kérdés, hogy ,,adott bemenet mellett elérhető-e a megállási feltétel” úgy is tekinthető, mint a döntési eljáráshoz tartozó (szintaktikus) eldöntésprobléma. Ezen döntési eljárásokat kalkulusoknak szokás nevezni. Az alábbiakban a döntési eljárások két fontos tulajdonságát fogalmazzuk meg.

6.1.1. DEFINÍCIÓ.

Azt mondjuk, hogy egy kalkulus helyes, ha a szintaktikus eldöntésproblémára adott igen válaszból következik, hogy a szemantikus eldöntésproblémára is igen a válasz.
Egy kalkulus teljes, ha minden olyan esetben, amikor a szemantikus eldöntésproblémára igen a válasz, a döntési eljárás a szintaktikus eldöntésproblémára adott igen válasszal eléri a megállási feltételt.

Ha a logika alapproblémájának a tételbizonyítás megoldását tekintjük, akkor a logika tárgyalásának tekinthető bármely kalkulus, amely mögött következményfogalom és (vagy) eldöntésprobléma áll. Ezért mondhatjuk azt, hogy a

logika = nyelv + kalkulus.

A logika ilyen felépítését (szintaktikus következményfogalom, szintaktikus eldöntésprobléma) szokták a logika értékmentes tárgyalásának is nevezni, mivel logikai igazságértékeket, igazságtáblát nem használ. Az alábbiakban áttekintjük a legismertebb kalkulusokat.

Az ítéletkalkulus

Nézzük meg, hogyan lehet felépíteni az ítéletlogikát szemantikai fogalmak nélkül, tisztán szintaktikai eszközökkel. Az ítéletkalkulus, más néven az ítéletlogika bizonyításelméleti tárgyalása Hilbert nevéhez fűződik. Az ítéletkalkulusban néhány kitüntetett szerkezetű ítéletlogikai formulát, ún. axiómasémát, valamint egy levezetési szabályt rögzítünk. Az axiómasémák tautológiák, és ha bennük az ítéletváltozókat tetszőleges ítéletlogikai formulával helyettesítjük, a 4.3.5. tétel szerint újból tautológiákat kapunk. Az axiómasémákból formulahelyettesítéssel állnak elő az axiómaformulák, röviden axiómák. Mivel minden tautológia ugyanazt a logikai műveletet írja le, egyes szerzők úgy tekintik, hogy a bizonyításelméletben az axiómák halmaza az összes tautológia. Ekkor azonban problematikus annak eldöntése, hogy egy formula – szerkezetét tekintve – axióma-e. Az axiómák a nyelvben felhasznált logikai műveletek tulajdonságait írják le. A ${\neg, \supset}$ funkcionálisan teljes művelethalmaz, ezért egy logikai nyelv ábécéjébe elegendő csak ezt a két műveletet betenni. Egy ilyen nyelv esetén a kiválasztott axiómasémáknak csak e két műveletnek megfelelő logikai összekötőjeleket kell tartalmazniuk.

Table 6.1. Az ítéletkalkulus axiómasémái

(A1)	$X \supset (Y \supset X)$
(A2)	$(X \supset (Y \supset Z)) \supset ((X \supset Y) \supset (X \supset Z))$
(A3)	$(\neg X \supset Y) \supset ((\neg X \supset \neg Y) \supset X)$

Az ítéletkalkulus három axiómasémája alapján helyettesítéssel kapjuk az axiómaformulákat.

6.1.2. MEGJEGYZÉS. Az (A1) axiómaséma a 4.3.6. tételben bizonyított ,,bővítés előtaggal”, az (A2) az ,,implikációlánc”, az (A3) a ,,reductio ad absurdum” tautológia. Az (A3) axiómaséma helyett szoktak más sémát is használni, például a kontrapozíciót kifejező $(\neg X \supset \neg Y) \supset (Y \supset X)$ sémát.

Egy levezetési szabály ítéletlogikai formulákból új ítéletlogikai formulát állít elő. Azt mondjuk, hogy a levezetési szabály helyes, ha a levezetett formula szemantikus következménye azoknak a formuláknak, amelyekből levezettük. Az ítéletkalkulus levezetési szabálya – a modus ponens vagy leválasztási szabály – a 4.4.12. tételből ismert $({X \supset Y, X}, Y)$ helyes következtetési formához kötődik.

Table 6.2. Az ítéletkalkulus levezetési szabálya

(MP)	${X \supset Y, X} ⊢_{0} Y$

A leválasztási szabály – (MP) – segítségével a következőképpen állíthatunk elő formulát: ha rendelkezésünkre áll egy implikációs formula: $A \supset B$ és ennek bal oldali közvetlen részformulája (előtagja): $A$ is, akkor azt mondjuk, hogy a modus ponenssel előáll a jobb oldali közvetlen részformula (utótag): $B$ .

Az ítéletkalkulus axiómasémáinak és levezetési szabályának rögzítése után bevezetjük a bizonyításelméleti levezetés fogalmát.

6.1.3. DEFINÍCIÓ. Legyen ${A_{1}, A_{2}, \dots}$ formulák tetszőleges, esetleg üres halmaza és $B$ egy formula. Az ${A_{1}, A_{2}, \dots}$ formulahalmazból a $B$ formula ítéletkalkulusbeli levezetése egy olyan $D_{1}, D_{2}, \dots, D_{m}$ $(m \geq 1)$ formulasorozat, ahol minden $j = 1,2, \dots, m$ -re $D_{j}$

vagy eleme az ${A_{1}, A_{2}, \dots}$ formulahalmaznak, azaz ún. feltételformula vagy hipotézis,
vagy valamelyik axiómasémából formulahelyettesítéssel állt elő, azaz axiómaformula,
vagy van olyan $1 \leq s, t \leq j$ , hogy a $D_{s}$ és a $D_{t}$ formulákból a levezetési szabállyal állt elő,

és a formulasorozat utolsó tagja, $D_{m}$ , éppen a $B$ formula.

6.1.4. DEFINÍCIÓ. Azt mondjuk, hogy a $B$ formula az ${A_{1}, A_{2}, \dots}$ formulahalmazból az ítéletkalkulusban levezethető, ha $B$ -nek van az ${A_{1}, A_{2}, \dots}$ formulahalmazból levezetése. Jelölése: ${A_{1}, A_{2}, \dots} ⊢_{0} B$ , amit röviden szekvenciának fogunk nevezni.

A logika szemantikus következményfogalma az igazság fogalmán alapul. Az igazságfogalmat a tényekre alapozzuk. Az ítéletkalkulusbeli levezethetőség az ítéletkalkulus következményfogalma, amelyet szintaktikus következményfogalomnak is neveznek. A szintaktikus következményfogalom definiálásához csak szintaktikai fogalmakat használtunk.

6.1.5. MEGJEGYZÉS. A levezetés fogalmának definíciója biztosítja, hogy a hipotézisek halmazából ezen feltételformulák bármelyike levezethető, egy axiómaformula pedig levezethető bármely hipotézishalmazból, tehát az üres hipotézishalmazból is.

6.1.6. DEFINÍCIÓ. Egy $B$ formula bizonyítható az ítéletkalkulusban, ha van hipotézismentes levezetése (azaz levezethető az üres feltételformula-halmazból). Ebben az esetben a $⊢_{0} B$ jelölést alkalmazzuk.

6.1.7. PÉLDA. Most megmutatjuk, hogy $A \supset A$ bizonyítható az ítéletkalkulusban, azaz megalapozzuk a $⊢_{0} A \supset A$ szekvenciát. A levezetés megszerkesztése során az ,,(A $i$ ) axiómasémából a … formulahelyettesítéssel nyert formula” helyett röviden [ (Ai): … ]-t, a ,,levezetés $i .$ és $j .$ formulájából modus ponenssel állt elő” helyett pedig röviden [ (MP): i,j ]-t írunk. A levezetés a következő:

$1.$	$(A \supset ((A \supset A) \supset A)) \supset ((A \supset (A \supset A)) \supset (A \supset A))$
		$[(A 2) : (X, Y, Z ∥ A, A \supset A, A)]$
$2.$	$A \supset ((A \supset A) \supset A)$	$[(A1) : (X, Y ∥ A, A \supset A)]$
$3.$	$(A \supset (A \supset A)) \supset (A \supset A)$	[ (MP): 1, 2 ]
$4.$	$A \supset (A \supset A)$	$[(A1) : (X, Y \| \| A, A)]$
$5.$	$A \supset A$	[ (MP): 3, 4 ]

6.1.8. MEGJEGYZÉS. A levezetés során felhasznált formulák alakja implikációs lánc. A levezetési szabály az implikációs lánc előtagjának eltávolításával kapott új formulát vezeti be. Ezért kézenfekvő egy formula levezetésének megszerkesztését egy olyan implikációs láncformulával kezdeni, amelynek utolsó formulája a levezetendő formula és az előtag(ok) leválaszthatók. Ezt tettük a fenti példában is.

6.1.9. PÉLDA. Megmutatjuk, hogy a 4.1.21. példa (c) részében a nyomozók sejtését leíró formula levezethető a nyomozás során megállapított tényeket leíró, célszerű alakú formulákból, azaz

${\neg \neg X \supset Y, \neg \neg Y \supset Z, X \lor U, U \supset V \supset Z, \neg Z} ⊢_{0} \neg X .$

Először kiküszöböljük a $\lor$ -t. $X \lor U$ helyett bevezetjük a vele tautologikusan ekvivalens $\neg X \supset U, \neg U \supset X$ formulákat a feltételhalmazba. A levezetés:

$1.$	$(\neg \neg X \supset Y) \supset ((\neg \neg X \supset \neg Y) \supset \neg X)$	[ (A3) ]
$2.$	$\neg \neg X \supset Y$	[ hipotézis ]
$3.$	$(\neg \neg X \supset \neg Y) \supset \neg X$	[ (MP): 1, 2 ]
$4.$	$(\neg \neg Y \supset Z) \supset ((\neg \neg Y \supset \neg Z) \supset \neg Y)$	[ (A3) ]
$5.$	$\neg \neg Y \supset Z$	[ hipotézis ]
$6.$	$(\neg \neg Y \supset \neg Z) \supset \neg Y$	[ (MP): 4, 5 ]
$7.$	$\neg Z \supset (\neg \neg Y \supset \neg Z)$	[ (A1) ]
$8.$	$\neg Z$	[ hipotézis ]
$9.$	$\neg \neg Y \supset \neg Z$	[ (MP): 7, 8 ]
$10.$	$\neg Y$	[ (MP): 6, 9 ]
$11.$	$\neg Y \supset (\neg \neg X \supset \neg Y)$	[ (A1) ]
$12.$	$\neg \neg X \supset \neg Y$	[ (MP): 10, 11 ]
$13.$	$\neg X$	[ (MP): 3, 12 ]

6.1.10. DEFINÍCIÓ. A $D_{1}, D_{2}, \dots, D_{m_{1}}$ és a ${D^{'}}_{1}, {D^{'}}_{2}, \dots, {D^{'}}_{m_{2}}$ formulasorozatok konkatenációján a $D_{1}, D_{2}, \dots, D_{m_{1}}, {D^{'}}_{1}, {D^{'}}_{2}, \dots, {D^{'}}_{m_{2}}$ formulasorozatot értjük.

6.1.11. LEMMA. Ha a $d_{1}$ és $d_{2}$ rendre a $Γ_{1}$ és a $Γ_{2}$ hipotézishalmazokból való levezetés, akkor a két levezetés konkatenációja egy – a $Γ_{1} \cup Γ_{2}$ hipotézishalmazból való – levezetés.

BIZONYÍTÁS. A $d_{1}$ és $d_{2}$ levezetések konkatenációjával kapott formulasorozat tetszőleges $D$ eleme

vagy hipotézisként került valamelyik levezetésbe, tehát $D \in Γ_{1} \cup Γ_{2}$ ,
vagy axiómasémából állt elő a két levezetés valamelyikében, akkor a konkatenációban is axiómaformula,
vagy a modus ponenssel állt elő két őt megelőző formulából a két levezetés valamelyikében, akkor (mivel a formulák sorrendjét a levezetésekben nem változtattuk meg) a konkatenált formulasorozatban ugyanez a szerepe.

Tehát a konkatenáció egy levezetés, ahol a hipotézishalmaz $Γ_{1} \cup Γ_{2}$ . $⋄$

Definiáltuk a szintaktikus következményfogalmat, amely rokonítható a szemantikus következményfogalommal. Definiáltuk a bizonyíthatóságot, mint egy ítéletlogikai formula tulajdonságát. Most megvizsgáljuk, hogy a szemantikus eldöntésprobléma megfogalmazásához szükséges dedukciós tétel formai megfelelője bebizonyítható-e.

6.1.12. TÉTEL. (DEDUKCIÓS TÉTEL.) Legyenek $A_{1}, A_{2}, \dots, A_{n}, B$ $(n \geq 1)$ tetszőleges ítéletlogikai formulák. ${A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}} ⊢_{0} B$ pontosan akkor, ha ${A_{1}, A_{2}, \dots, A_{n - 1}} ⊢_{0} A_{n} \supset B$ .

BIZONYÍTÁS. Jelölje $Γ$ az ${A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}}$ , $Γ'$ pedig az ${A_{1}, A_{2}, \dots, A_{n - 1}}$ formulahalmazt.

Először azt bizonyítjuk be, hogy ha $Γ ⊢_{0} B$ , akkor $Γ' ⊢_{0} A_{n} \supset B$ . $Γ ⊢_{0} B$ azt jelenti, hogy $B$ -nek van levezetése $Γ$ -ból. Legyen ez a levezetés $D_{1}, D_{2}, \dots, D_{m} = B$ . A bizonyítás a következő lépésekből áll:

Írjuk a levezetésben szereplő formulák elé az $A_{n} \supset$ szimbólumsorozatot. Így az $A_{n} \supset D_{1}, A_{n} \supset D_{2}, \dots, A_{n} \supset D_{m} = A_{n} \supset B$ formulasorozatot kapjuk.
Lássuk be, hogy minden $k$ -ra $(1 \leq k \leq m)$ létezik $A_{n} \supset D_{k}$ -nak $Γ'$ -ből való levezetése.
1. Legyen $D_{k}$ axiómaformula, ekkor $A_{n} \supset D_{k}$ bizonyítható. A levezetés:

$1.$	$D_{k} \supset A_{n} \supset D_{k}$	[ (A1) ]
$2.$	$D_{k}$	[ axiómaformula ]
$3.$	$A_{n} \supset D_{k}$	[ (MP): 1, 2 ]

Legyen $D_{k} (\neq A_{n})$ eleme a $Γ$ -nak, ekkor $A_{n} \supset D_{k}$ levezethető $Γ'$ -ből. A levezetés:

$1.$	$D_{k} \supset A_{n} \supset D_{k}$	[ (A1) ]
$2.$	$D_{k}$	[ hipotézis ]
$3.$	$A_{n} \supset D_{k}$	[ (MP): 1, 2 ]

Legyen $D_{k} = A_{n}$ . Az $A_{n} \supset A_{n}$ szekvenciának a 6.1.7. példában megadtuk a bizonyítását.
Legyen $D_{k}$ az első olyan (eddig még nem vizsgált) formula az eredeti levezetésben, amely modus ponense $D_{t}, D_{s} = D_{t} \supset D_{k}$ levezetésbeli formuláknak $(s, t \leq k)$ . Ez azt jelenti, hogy már igazoltuk, hogy $Γ'$ -ből az $A_{n} \supset D_{t} \supset D_{k}$ , valamint az $A_{n} \supset D_{t}$ formula levezethető:

$⋮$
$i .$	$A_{n} \supset D_{t} \supset D_{k}$
$⋮$
$j .$	$A_{n} \supset D_{t}$
$⋮$
$w .$	$(A_{n} \supset D_{t} \supset D_{k}) \supset (A_{n} \supset D_{t}) \supset A_{n} \supset D_{k}$ [ (A2) ]
$(w + 1) .$	$(A_{n} \supset D_{t}) \supset A_{n} \supset D_{k}$	[ (MP): i, w ]
$(w + 2) .$	$A_{n} \supset D_{k}$	[ (MP): j, (w+1) ]

Indukcióval könnyen bizonyítható, hogy $Γ' ⊢_{0} A_{n} \supset D_{k}$ akkor is, ha $D_{k}$ tetszőleges – nem feltétlen az első – olyan formula az eredeti levezetésben, amelyet modus ponenssel nyertünk.

Az $A_{n} \supset D_{k}$ formulák elé $(1 \leq k \leq m)$ beírjuk azok levezetését a $Γ'$ -ből. Ezzel $Γ'$ -ből való levezetések konkatenációját kapjuk, ami a $Γ'$ -ből való levezetése az $A_{n} \supset B$ formulának.

2. Most pedig azt bizonyítjuk, hogy ha $Γ' ⊢_{0} A_{n} \supset B$ , akkor $Γ ⊢_{0} B$ . A feltétel szerint $Γ' ⊢_{0} A_{n} \supset B$ . Legyen ez a levezetés

$D_{1}, D_{2}, \dots, D_{m - 1}, A_{n} \supset B .$

Írjuk a levezetés végére az $A_{n}$ formulát és a két utolsó formula modus ponensét. Ez éppen a $B$ egy levezetése $Γ$ -ból:

$D_{1}, D_{2}, \dots, D_{m - 1}, A_{n} \supset B, A_{n}, B$

Ezzel a dedukciós tételt bebizonyítottuk. $⋄$

6.1.13. TÉTEL. (AZ ELDÖNTÉSPROBLÉMA TÉTELE.)

Legyenek $A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}, B$ (n $\geq 1)$ tetszőleges ítéletlogikai formulák. ${A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}} ⊢_{0} B$ pontosan akkor, ha

$⊢_{0} A_{1} \supset A_{2} \supset \dots \supset A_{n - 1} \supset A_{n} \supset B .$

BIZONYÍTÁS. ${A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}} ⊢_{0} B$ -re $n$ -szer alkalmazva a dedukciós tételt egyik irányban, és $⊢_{0} A_{1} \supset A_{2} \supset \dots \supset A_{n - 1} \supset A_{n} \supset B$ -re $n$ -szer alkalmazva a dedukciós tételt visszafelé, a tétel mindkét irányú állítása könnyen adódik. $⋄$

6.1.14. MEGJEGYZÉS. Mivel egy formulahalmazban a formulák sorrendje tetszőleges, a 6.1.13. tétel kimondható úgy is, hogy ${A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}} ⊢_{0} B$ akkor és csak akkor, ha $⊢_{0} A_{i_{1}} \supset A_{i_{2}} \supset \dots \supset A_{i_{n}} \supset B$ , ahol $i_{1}, i_{2}, \dots, i_{n}$ az $1,2, \dots, n$ számok tetszőleges permutációja.

A 6.1.13. tétel azt mondja ki, hogy a következő két állítás ekvivalens:

Az ${A_{1}, A_{2}, \dots, A_{n}}$ formulahalmazból a $B$ formula levezethető.
Az $A_{1} \supset A_{2} \supset \dots \supset A_{n} \supset B$ formula bizonyítható.

Tehát annak eldöntéséhez, hogy egy $B$ formula az adott feltételek mellett tétel-e, el kell tudni dönteni, hogy a megfelelő ítéletlogikai formula bizonyítható-e. Ez az ítéletkalkulus eldöntésproblémája. Az eldöntésprobléma megoldása itt is az automatikus tételbizonyítást jelenti. A bizonyításelméleti levezetés célja (megállási feltétele) az, hogy a levezetés során előálljon a levezetendő formula. A levezetés definíciója miatt az ítéletkalkulusban eldöntésproblémának nem csak azt tekintjük, hogy bizonyítható-e egy adott formula, hanem azt is, hogy levezethető-e feltételformulák valamely halmazából a formula.

6.1.15. TÉTEL. (AZ ÍTÉLETKALKULUS HELYESSÉGE.)

Legyenek $A_{1}, A_{2}, \dots, B$ ítéletlogikai formulák. Ha ${A_{1}, A_{2}, \dots} ⊢_{0} B$ , akkor ${A_{1}, A_{2}, \dots} ⊨_{0} B$ .

BIZONYÍTÁS. Jelölje $Γ$ az ${A_{1}, A_{2}, \dots}$ formulahalmazt. A tétel feltétele miatt adott a $D_{1}, D_{2}, \dots, D_{m} = B$ levezetés. Indukcióval megmutatjuk, hogy a levezetés minden $D_{k}$ $(1 \leq k \leq m)$ formulája tautologikus következménye a hipotézisek halmazának, azaz $Γ ⊨_{0} D_{k}$ .

Tetszőleges axiómaformula, illetve $Γ$ tetszőleges eleme nyilvánvalóan szemantikus következménye $Γ$ -nak és $D_{1}$ (a levezetés első formulája) csak axiómaformula vagy $Γ$ -beli hipotézis lehet.
Tegyük most fel, hogy minden $(n \leq k)$ -ra igazoltuk már, hogy $Γ ⊨_{0} D_{n}$ .
Ha most $D_{k + 1}$ axiómaformula vagy hipotézis, akkor az előzők szerint $Γ ⊨_{0} 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 $Γ ⊨_{0} D_{s}$ és $Γ ⊨_{0} D_{s} \supset D_{k + 1}$ adódik. A modus ponensre vonatkozó 4.3.6. szemantikus tétel miatt ${D_{s}, D_{t}} ⊨_{0} D_{k + 1}$ , a 4.4.3. tétel miatt pedig $Γ ⊨_{0} D_{k + 1}$ .

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

6.1.16. DEFINÍCIÓ. Azt mondjuk, hogy az $A$ és a $B$ formula bizonyíthatóan ekvivalensek, ha ${A} ⊢_{0} B$ és ${B} ⊢_{0} A$ .

Ez a szemantikus tárgyalásnál definiált tautologikus ekvivalenciafogalom bizonyításelméleti megfelelője. A dedukciós tételből könnyen adódik, hogy ez pontosan akkor áll fenn, ha $⊢_{0} A \supset B$ és $⊢_{0} B \supset A$ . A 6.1.17. példa mutatja, hogy $A$ és $\neg \neg A$ bizonyíthatóan ekvivalensek.

6.1.17. PÉLDA.

A ${\neg \neg A} ⊢_{0} A$ szekvenciát megalapozó levezetés:

$1.$	$\dots$
$⋮$
$5.$	$\neg A \supset \neg A$	[ 6.1.7. példa ]
$6.$	$(\neg A \supset \neg A) \supset ((\neg A \supset \neg \neg A) \supset A)$	[ (A3) ]
$7.$	$(\neg A \supset \neg \neg A) \supset A$	[ (MP): 5, 6 ]
$8.$	$\neg \neg A \supset (\neg A \supset \neg \neg A)$	[ (A1) ]
$9.$	$\neg \neg A$	[ hipotézis ]
$10.$	$\neg A \supset \neg \neg A$	[ (MP): 8, 9 ]
$11.$	$A$	[ (MP): 7, 10 ]

A ${\neg \neg A} ⊢_{0} A$ szekvenciához hasonlóan ${\neg \neg \neg A} ⊢_{0} \neg A$ is megalapozható. Ebből a dedukciós tétel miatt következik, hogy $⊢_{0} \neg \neg \neg A \supset \neg A$ , azaz van hipotézismentes levezetése a $\neg \neg \neg A \supset \neg A$ formulának. Így az ${A} ⊢_{0} \neg \neg A$ szekvenciát igazoló levezetés:

$⋮$
$i .$	$\neg \neg \neg A \supset \neg A$	[ (a) + dedukció tétel ]
$(i + 1) .$	$(\neg \neg \neg A \supset A) \supset ((\neg \neg \neg A \supset \neg A) \supset \neg \neg A)$	[ (A3) ]
$(i + 2) .$	$A \supset (\neg \neg \neg A \supset A)$	[ (A1) ]
$(i + 3) .$	$A$	[ hipotézis ]
$(i + 4) .$	$\neg \neg \neg A \supset A$	[ (MP): $(i + 2)$ , $(i + 3)$ ]
$(i + 5) .$	$(\neg \neg \neg A \supset \neg A) \supset \neg \neg A$	[ (MP): $(i + 1)$ , $(i + 4)$ ]
$(i + 6) .$	$\neg \neg A$	[ (MP): $i$ , $(i + 5)$ ]

A következő példákban néhány további, az ítéletkalkulusban alapvető levezetést adunk meg.

6.1.18. PÉLDA. Megmutatjuk először, hogy ${A \supset B} ⊢_{0} \neg \neg A \supset B$ . Ehhez a dedukciós tétel miatt elég bizonyítani, hogy ${A \supset B, \neg \neg A} ⊢_{0} B$ . Ha ugyanis az ${A \supset B, \neg \neg A} ⊢_{0} B$ levezetést elő tudjuk állítani, akkor van levezetése az ${A \supset B} ⊢_{0} \neg \neg A \supset B$ szekvenciának is.

$1.$	$\neg \neg A$	[ hipotézis ]
$⋮$
$11.$	$A$	[ 6.1.17. példa (a) része ]
$12.$	$A \supset B$	[ hipotézis ]
$13.$	$B$	[ (MP): 11, 12 ]

6.1.19. PÉLDA. Bizonyítsuk be, hogy ${A \supset B} ⊢_{0} \neg B \supset \neg A$ . A 6.3. táblázat két levezetést tartalmaz. A bal oldali az $A \supset B$ és $\neg B$ hipotézisekből $\neg A$ -t vezeti le, a jobb oldali levezetésben pedig megmutatjuk, hogy $\neg A$ levezetéséből hogyan szerkeszthetjük meg – a dedukciós tétel bizonyításánál felhasznált módszerrel – a $\neg B \supset \neg A$ levezetését. Az első és az utolsó lépést kidolgoztuk, a második a 6.1.7. példa alapján megy, a többit az olvasóra bízzuk.

6.1.20. DEFINÍCIÓ. Azt mondjuk, hogy egy ${A_{1}, A_{2}, \dots}$ formulahalmaz ellentmondásos, ha van olyan $A$ formula, hogy ${A_{1}, A_{2}, \dots}$ -ből $A$ is, és $\neg A$ is levezethető. Egyébként ${A_{1}, A_{2}, \dots}$ ellentmondástalan.

Az ellentmondásosság egy másik szokásos definíciója: Egy ${A_{1}, A_{2}, \dots}$ formulahalmaz ellentmondásos, ha ${A_{1}, A_{2}, \dots}$ -ből tetszőleges $B$ formula levezethető. A 6.1.21. példa bizonyítja, hogy ha az ${A_{1}, A_{2}, \dots}$ formulahalmazból levezethető valamely $A$ formula és $A$ negáltja is, akkor tetszőleges $B$ formula is levezethető belőle.

6.1.21. PÉLDA. Az ${A, \neg A}$ formulahalmazból tetszőleges $B$ formula levezethető. A levezetés:

$1.$	$(\neg B \supset A) \supset ((\neg B \supset \neg A) \supset B)$	[ (A3) ]
$2.$	$A \supset (\neg B \supset A)$	[ (A1) ]
$3.$	$A$	[ hipotézis ]
$4.$	$\neg B \supset A$	[ (MP): 2, 3 ]
$5.$	$(\neg B \supset \neg A) \supset B$	[ (MP): 1, 4 ]
$6.$	$\neg A \supset (\neg B \supset \neg A)$	[ (A1) ]
$7.$	$\neg A$	[ hipotézis ]
$8.$	$\neg B \supset \neg A$	[ (MP): 6, 7 ]
$9.$	$B$	[ (MP): 5, 8 ]

Table 6.3. Levezetés generálása adott levezetésből

			1.	$(\neg B \supset (\neg \neg A \supset \neg B)) \supset (\neg B \supset (\neg B \supset (\neg \neg A \supset \neg B)))$
			2.	$\neg B \supset (\neg \neg A \supset \neg B)$
1.	$\neg B \supset (\neg \neg A \supset \neg B)$	[(A1)]	3.	$\neg B \supset (\neg B \supset (\neg \neg A \supset \neg B))$
			$⋮$
2.	$\neg B$	[hipotézis]	8.	$\neg B \supset \neg B$
			$⋮$
3.	$\neg \neg A \supset \neg B$	[(MP): 1, 2]	11.	$\neg B \supset (\neg \neg A \supset \neg B)$
			$⋮$
4.	$(\neg \neg A \supset B) \supset ((\neg \neg A \supset \neg B) \supset \neg A)$	[(A3)]	14.	$\neg B \supset (\neg \neg A \supset B) \supset ((\neg \neg A \supset \neg B) \supset \neg A)$
			$⋮$
5.	$A \supset B$	[hipotézis]	17.	$\neg B \supset (A \supset B)$
$⋮$			$⋮$
			$⋮$
i.	$\neg \neg A \supset B$	[6.18. példa]	j.	$\neg B \supset (\neg \neg A \supset B)$
			$⋮$
(i+1).	$(\neg \neg A \supset \neg B) \supset \neg A$	[(MP): 4, i]	(j+3).	$\neg B \supset ((\neg \neg A \supset \neg B) \supset \neg A)$
			(j+4).	$(\neg B \supset (\neg \neg A \supset \neg B) \supset \neg A) \supset (\neg B \supset (\neg \neg A \supset \neg B)) \supset (\neg B \neg A)$
			(j+5).	$(\neg B \supset (\neg \neg A \supset \neg B)) \supset (\neg B \supset \neg A)$
(i+2).	$\neg A$	[(MP): 3, (i+1)]	(j+6).	$\neg B \supset \neg A$

6.1.22. TÉTEL. Legyen ${A_{1}, A_{2}, \dots}$ egy formulahalmaz és $B$ egy ítéletlogikai formula.

${A_{1}, A_{2}, \dots, \neg B}$ pontosan akkor ellentmondásos, ha ${A_{1}, A_{2}, \dots} ⊢_{0} B$ .
${A_{1}, A_{2}, \dots, B}$ pontosan akkor ellentmondásos, ha ${A_{1}, A_{2}, \dots} ⊢_{0} \neg B$ .

BIZONYÍTÁS.

Nyilvánvaló, hogy ${A_{1}, A_{2}, \dots} ⊢_{0} B$ esetén az ${A_{1}, A_{2}, \dots, \neg B}$ formulahalmaz ellentmondásos ( $B$ és $\neg B$ is levezethető ${A_{1}, A_{2}, \dots, \neg B}$ -ből). Fordítva, ha az ${A_{1}, A_{2}, \dots, \neg B}$ formulahalmazról tudjuk, hogy ellentmondásos, akkor valamely $C$ formulára

${A_{1}, A_{2}, \dots, \neg B} ⊢_{0} C és {A_{1}, A_{2}, \dots, \neg B} ⊢_{0} \neg C .$

A dedukciós tétel miatt

${A_{1}, A_{2}, \dots} ⊢_{0} \neg B \supset C és {A_{1}, A_{2}, \dots} ⊢_{0} \neg B \supset \neg C .$

Konkatenáljuk ezt a két levezetést és írjuk a végére az (A3) axióma

$(\neg B \supset C) \supset ((\neg B \supset \neg C) \supset B)$

alakját. Majd válasszuk le a két előtagot a konkatenált levezetésben szereplő $\neg B \supset C$ és $\neg B \supset \neg C$ formulákkal, az eredmény ${A_{1}, A_{2}, \dots} ⊢_{0} B$ .

Most is ${A_{1}, A_{2}, \dots} ⊢_{0} \neg B$ -ből az ${A_{1}, A_{2}, \dots, B}$ formulahalmaz ellentmondásossága azonnal következik. Visszafele, ha ${A_{1}, A_{2}, \dots, B}$ ellentmondásos, akkor valamely $C$ formulára

${A_{1}, A_{2}, \dots, B} ⊢_{0} C és {A_{1}, A_{2}, \dots, B} ⊢_{0} \neg C .$

Felhasználva azt, hogy $\neg \neg B ⊢_{0} B$ , megállapíthatjuk, hogy ami levezethető $B$ -ből az levezethető $\neg \neg B$ -ből is. Ebből azt kapjuk, hogy

${A_{1}, A_{2}, \dots, \neg \neg B} ⊢_{0} C és {A_{1}, A_{2}, \dots, \neg \neg B} ⊢_{0} \neg C$

szintén fennáll, azaz ${A_{1}, A_{2}, \dots, \neg \neg B}$ ellentmondásos. Ekkor viszont ${A_{1}, A_{2}, \dots} ⊢_{0} \neg B$ az 1. eset szerint.

Ezzel mindkét állítást bebizonyítottuk. $⋄$

6.1.23. TÉTEL. Ha egy ${A_{1}, A_{2}, \dots}$ formulahalmaz ellentmondásos, akkor kielégíthetetlen.

BIZONYÍTÁS. Jelölje $Γ$ az ${A_{1}, A_{2}, \dots}$ formulahalmazt. Ha $Γ$ ellentmondásos, akkor van olyan $C$ formula, melyre $Γ ⊢_{0} C$ és $Γ ⊢_{0} \neg C$ . Ekkor a 6.1.15. tétel miatt $Γ ⊨_{0} C$ és $Γ ⊨_{0} \neg C$ , azaz ha létezik $Γ$ -t kielégítő interpretáció, akkor az kielégíti $C$ -t is, és $\neg C$ -t is, ami lehetetlen. Tehát nincs olyan interpretáció, ami $Γ$ -t kielégítené. $⋄$

6.1.24. LEMMA. (KALMÁR LÁSZLÓ LEMMÁJA.)

Legyen $A$ tetszőleges ítéletlogikai formula, legyenek az $A$ -ban előforduló ítéletváltozók $X_{1}, X_{2}, \dots, X_{n}$ és legyen $ℐ$ tetszőleges interpretáció. Legyen $j = 1,2, \dots, n$ -re

${X^{'}}_{j} ⇌ {\begin{array}{l} X_{j}, & h a ℐ (X_{j}) = i, \\ \neg X_{j} & e g y é b k é n t, \end{array} é s A^{'} ⇌ {\begin{array}{l} A, & h a ℬ_{ℐ} (A) = i, \\ \neg A & e g y é b k é n t . \end{array}$

Ekkor ${{X^{'}}_{1}, {X^{'}}_{2}, \dots, {X^{'}}_{n}} ⊢_{0} A^{'}$ .

BIZONYÍTÁS. Nevezzünk a bizonyítás során egy $A$ ítéletlogikai formulát jónak, ha tetszőleges interpretációban ${{X^{'}}_{1}, {X^{'}}_{2}, \dots, {X^{'}}_{n}} ⊢_{0} A^{'}$ . A szerkezeti indukció elve segítségével igazolni fogjuk, hogy minden formula jó.

(alaplépés:) Ha $A$ prímformula, legyen mondjuk $X$ . $X$ igazságtáblája kétsoros, tehát két szekvenciát kell megalapozni:

$X$	szekvencia	megalapozás
$i$	${X} ⊢_{0} X$	$X$ hipotézis
$h$	${\neg X} ⊢_{0} \neg X$	$\neg X$ hipotézis

Tehát egy prímformula jó.

(indukciós lépések:) Legyen az $A$ formula jó, és legyenek benne az ítéletváltozók $X_{1}, X_{2}, \dots, X_{n}$ . Vizsgáljuk meg $\neg A$ -t. $\neg A$ igazságtáblája $2^{n}$ sort tartalmaz, melyek közül valahányban $A$ alatt $i$ , valahányban pedig $h$ igazságérték szerepel. Mivel $A$ jó, az $A$ alatt $i$ -t tartalmazó sorokbeli interpretációkban az ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} A$ , a többiben pedig az ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg A$ szekvenciák megalapozhatók. Ez utóbbi esetben épp ez volt a célunk, míg az előbbi esetben az ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg \neg A$ levezetés megkonstruálásához az ${A} ⊢_{0} \neg \neg A$ szekvenciát kell megalapozni, amit viszont a 6.1.17. példában már megtettünk:

$X_{1}, \dots, X_{n}$

$A$

$\neg A$

$⋮$

$i$

${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} A$

$h$

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

6.1.17. példa

$⋮$

$h$

${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg A$

$i$

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

$\neg A$ hipotézis

Tehát $\neg A$ is jó.

Legyen most az $A$ és a $B$ formula jó, és legyenek bennük az ítéletváltozók $X_{1}, X_{2}, \dots, X_{n}$ . Vizsgáljuk meg $A \supset B$ -t. $A \supset B$ igazságtáblája is $2^{n}$ sort tartalmaz, melyek közül valahányban $A$ és $B$ alatt is $i$ , néhányban $A$ alatt $i$ , $B$ alatt $h$ , néhányban épp fordítva: $A$ alatt $h$ , $B$ alatt $i$ , a többiben pedig $A$ és $B$ alatt is $h$ igazságérték szerepel. Mivel $A$ jó, az $A$ alatt $i$ -t tartalmazó sorokbeli interpretációkban az ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} A$ , a többiben pedig az ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg A$ , továbbá mivel $B$ is jó, a $B$ alatt $i$ -t tartalmazó sorokbeli interpretációkban az ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} B$ , a többiben pedig az ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg B$ szekvenciák megalapozhatók. Továbbá az (a) és a (c) esetben a

$1.$	$B \supset A \supset B$	[ (A1) ]
$2.$	$B$	[ hipotézis ]
$3.$	$A \supset B$	[ (MP): 1, 2 ]

levezetés megalapozza az $(A \supset B)^{'}$ megfelelő levezetéseit (ugyanis ezekben az esetekben $B^{'} = B$ és $(A \supset B)^{'} = A \supset B$ ).

	$X_{1}, \dots, X_{n}$	$A$	$B$		$A \supset B$
(a)	$⋮$ $⋮$	$i$	$i$	${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} A$ ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} B$	$i$	${A, B} ⊢_{0} A \supset B$
(b)	$⋮$ $⋮$	$i$	$h$	${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} A$ ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg B$	$h$	${A, \neg B} ⊢_{0} \neg (A \supset B)$
(c)	$⋮$ $⋮$	$h$	$i$	${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg A$ ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} B$	$i$	${\neg A, B} ⊢_{0} A \supset B$
(d)	$⋮$ $⋮$	$h$	$h$	${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg A$ ${{X^{'}}_{1}, \dots, {X^{'}}_{n}} ⊢_{0} \neg B$	$i$	${\neg A, \neg B} ⊢_{0} A \supset B$

A (d) esetben az

$1.$	$\neg A \supset \neg B \supset \neg A$	[ (A1) ]
$2.$	$\neg A$	[ hipotézis ]
$3.$	$\neg B \supset \neg A$	[ (MP): 1, 2 ]
$⋮$
$w .$	$A \supset B$	[6.1. 19. példa ]

levezetés megalapozza ${\neg A, \neg B} ⊢_{0} A \supset B$ -t ( $A^{'} = \neg A$ , $B^{'} = \neg B$ , $(A \supset B)^{'} = A \supset B$ ).

A (b) esetben ${A, \neg B} ⊢_{0} \neg (A \supset B)$ fennállását kell belátni ( $A^{'} = A$ , $B^{'} = \neg B$ , $(A \supset B)^{'} = \neg (A \supset B)$ ). Az ${A, \neg B, A \supset B}$ formulahalmaz ellentmondásos, mivel

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

A 6.1.22. tétel miatt ${A, \neg B} ⊢_{0} \neg (A \supset B)$ .

Ezzel beláttuk, hogy az $A \supset B$ formula is jó.

Mivel formuláinkban csak a $\neg$ és a $\supset$ műveleteket engedtük meg, elegendő volt megmutatni az indukciós lépésekben, hogy a tétel fennáll negációs és implikációs formulákra. $⋄$

6.1.25. TÉTEL. Legyenek ${A_{1}, A_{2}, \dots}$ egy formulahalmaz, $B$ és $C$ ítéletlogikai formulák. Ha ${A_{1}, A_{2}, \dots, B} ⊢_{0} C$ és ${A_{1}, A_{2}, \dots, \neg B} ⊢_{0} C$ , akkor ${A_{1}, A_{2}, \dots} ⊢_{0} C$ .

BIZONYÍTÁS. Ha ${A_{1}, A_{2}, \dots, B} ⊢_{0} C$ és ${A_{1}, A_{2}, \dots, \neg B} ⊢_{0} C$ , akkor a 6.1.12. tétel miatt ${A_{1}, A_{2}, \dots} ⊢_{0} B \supset C$ és ${A_{1}, A_{2}, \dots} ⊢_{0} \neg B \supset C$ . A

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

szekvenciákat pedig a 6.1.19. példában megalapoztuk. A $\neg C \supset \neg B$ és a $\neg C \supset \neg \neg B$ formulák levezetései konkatenációjának végére írva az (A3) axiómasémából nyert $(\neg C \supset \neg B) \supset ((\neg C \supset \neg \neg B) \supset C)$ axiómaformulát, két leválasztással megkapjuk, hogy ${A_{1}, A_{2}, \dots} ⊢_{0} C$ . $⋄$

6.1.26. TÉTEL. Legyen $A$ ítéletlogikai formula. Ha $A$ tautológia, akkor $A$ bizonyítható, azaz ha $⊨_{0} A$ , akkor $⊢_{0} A$ .

BIZONYÍTÁS. (Kalmár László gondolatmenete [31].) Legyenek az $A$ formulában előforduló ítéletváltozók $X_{1}, X_{2}, \dots, X_{n}$ . Ha az $A$ formula tautológia, akkor az igazságtábla minden sorában $i$ az értéke, tehát a 6.1.24. lemma szerint minden sorban ${{X^{'}}_{1}, {X^{'}}_{2}, \dots, {X^{'}}_{n}} ⊢_{0} A$ . A 6.1.25. tétel ismételt alkalmazásával sorra kiküszöböljük az összes literált a feltételhalmazból. Minden ${{X^{'}}_{1}, {X^{'}}_{2}, \dots, {X^{'}}_{n}}$ literálhalmazhoz van pontosan egy ${\neg {X^{'}}_{1}, {X^{'}}_{2}, \dots, {X^{'}}_{n}}$ alakú literálhalmaz. Ekkor ${{X^{'}}_{2}, \dots, {X^{'}}_{n}} ⊢_{0} A$ . Ezt folytatva ${{X^{'}}_{2}, \dots, {X^{'}}_{n}}$ -re kapjuk, hogy $⊢_{0} A$ . $⋄$

6.1.27. TÉTEL. (AZ ÍTÉLETKALKULUS GYÖNGE TELJESSÉGE.)

Legyen ${A_{1}, A_{2}, \dots, A_{n}}$ véges formulahalmaz és $B$ tetszőleges formula. Ha ${A_{1}, A_{2}, \dots, A_{n}} ⊨_{0} B$ , akkor ${A_{1}, A_{2}, \dots, A_{n}} ⊢_{0} B$ .

BIZONYÍTÁS. A szemantikus és a szintaktikus dedukciós tétel miatt elegendő azt belátni, hogy ha $⊨_{0} A_{1} \supset A_{2} \supset \dots \supset A_{n} \supset B$ , akkor $⊢_{0} A_{1} \supset A_{2} \supset \dots \supset A_{n} \supset B$ . Feltételeink szerint az $A_{1} \supset A_{2} \supset \dots \supset A_{n} \supset B$ formula tautológia, tehát a 6.1.26. tétel miatt bizonyítható. $⋄$

Az ítéletlogika szemantikus tárgyalása során a formulahalmazok halmazát két diszjunkt részre osztottuk, a kielégíthetetlen és a kielégíthető formulahalmazok halmazára. Az ítéletkalkulus esetén a formulahalmazok halmazának szintén egy diszjunkt osztályozása az ellentmondásos és az ellentmondástalan formulahalmazok halmazára való szétbontás. A logika különböző tárgyalásai esetén a formulahalmazok diszjunkt felbontását eredményező tulajdonságok egységes megnevezése: konzisztencia – inkonzisztencia. Ezek a tulajdonságok – tárgyalásuk során – a tárgyalásmódhoz kötődő megnevezést kapnak. Például szemantikus tárgyalás esetén a konzisztencia (inkonzisztencia) tulajdonságnak a kielégíthetőség (kielégíthetetlenség), a szintaktikus tárgyalások közül a bizonyításelméletben az ellentmondástalanság (ellentmondásosság) a megfelelője. Ha pedig konzisztencia (inkonzisztencia) tulajdonságról beszélünk – egy tárgyalásmód keretei között –, mindig az illető tárgyalásmódbeli megfelelő tulajdonságot értjük rajta.

Érdekes kérdés, hogy a különböző tárgyalásmódok osztályozásai milyen kapcsolatban vannak egymással. Vizsgáljuk most ezt a kapcsolatot szemantikai és bizonyításelméleti tárgyalásmódok esetén. A 6.1.23. tétel szerint minden ellentmondásos formulahalmaz kielégíthetetlen. Ha sikerülne belátni azt, hogy minden ellentmondásmentes formulahalmaz pedig kielégíthető, akkor a kétféle osztályozás eredménye ugyanaz lenne.

6.1.28. DEFINÍCIÓ. Egy $Γ$ formulahalmaz maximális konzisztens (vagy maximális ellentmondásmentes), ha konzisztens (ellentmondásmentes), de tetszőleges $A \notin Γ$ formula esetén $Γ \cup {A}$ már inkonzisztens (ellentmondásos).

6.1.29. TÉTEL. A $Γ$ formulahalmaz akkor és csak akkor maximális konzisztens, ha

$Γ$ konzisztens és
bármely $A$ formulára vagy $A \in Γ$ , vagy $\neg A \in Γ$ .

BIZONYÍTÁS.

Ha $Γ$ maximális konzisztens, akkor $(1)$ – a definíció miatt – teljesül. A $(2)$ tulajdonság igazolásához tegyük fel, hogy van olyan $A$ , hogy sem $A$ , sem $\neg A$ nem eleme $Γ$ -nak. Ekkor a maximalitás miatt $Γ \cup {A}$ és $Γ \cup {\neg A}$ inkonzisztens. Ez a 6.1. 22. tétel miatt azt jelenti, hogy $Γ ⊢_{0} \neg A$ és $Γ ⊢_{0} A$ , vagyis $Γ$ is inkonzisztens, ami ellentmond a feltételnek, tehát a $(2)$ -nek fenn kell állnia.
Ha pedig $Γ$ -ra $(1)$ és $(2)$ is teljesül, akkor minden olyan $Γ'$ formulahalmaz inkonzisztens, amelynek $Γ$ valódi része. Ugyanis legyen $Γ'$ az $A$ formulával bővebb, mint $Γ$ . Ekkor $(2)$ miatt $\neg A \in Γ$ , de $Γ \subset Γ'$ , így $\neg A \in Γ'$ . Tehát $A \in Γ'$ és $\neg A \in Γ'$ , ami azt jelenti, hogy $Γ'$ inkonzisztens.

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

6.1.30. TÉTEL. Legyen $Γ$ maximális konzisztens formulahalmaz.

$A \supset B \in Γ$ pontosan akkor, ha $\neg A \in Γ$ vagy $B \in Γ$ .
$\neg (A \supset B) \in Γ$ pontosan akkor, ha $A \in Γ$ és $\neg B \in Γ$ .

BIZONYÍTÁS.

Ha $A \supset B \in Γ$ , de $\neg A \in Γ$ vagy $B \in Γ$ nem teljesül, akkor $\neg A \notin Γ$ és $B \notin Γ$ . De mivel $Γ$ maximális, egyrészt $Γ \cup \neg A$ is és $Γ \cup B$ is inkonzisztens, másrészt a 6.1.29. tétel szerint $A \in Γ$ és $\neg B \in Γ$ . Ugyanakkor tudjuk, hogy $A \supset B \in Γ$ . Ennek alapján $A \in Γ$ miatt $Γ ⊢_{0} B$ és $\neg B \in Γ$ miatt $Γ ⊢_{0} \neg B$ , vagyis $Γ$ inkonzisztens, ellentétben a feltétellel.

Fordított irányban tegyük most fel, hogy $\neg A \in Γ$ vagy $B \in Γ$ . Mindkét esetben megmutatjuk, hogy $Γ ⊢_{0} A \supset B$ . Ezt elég megmutatni, mert ha $Γ ⊢_{0} A \supset B$ mellett $A \supset B \in Γ$ nem teljesülne, akkor $Γ$ maximalitása miatt $\neg (A \supset B) \in Γ$ , tehát $Γ ⊢_{0} \neg (A \supset B)$ következne, azaz a feltételekkel ellentétben $Γ$ inkonzisztens lenne.

$\neg A \in Γ$ : Ekkor $Γ \cup {A}$ inkonzisztens, tehát bármi levezethető belőle, speciálisan $Γ \cup {A} ⊢_{0} B$ , így a dedukciós tétel miatt $Γ ⊢_{0} A \supset B$ .
$B \in Γ$ : Ebben az esetben a

$1.$	$B \supset (A \supset B)$	[ (A1) ]
$2.$	$B$	[ hipotézis ]
$3.$	$A \supset B$	[ (MP): 1, 2 ]

levezetés igazolja állításunkat.

Tegyük fel, hogy $\neg (A \supset B) \in Γ$ , de $A \in Γ$ és $\neg B \in Γ$ nem teljesül, vagyis $A \notin Γ$ vagy $\neg B \notin Γ$ . Ekkor a maximalitás miatt $\neg A \in Γ$ vagy $B \in Γ$ . Az első állítás bizonyításánál láttuk, hogy ekkor $A \supset B \in Γ$ , ellentétben a feltétellel.

Visszafelé, ha $A \in Γ$ és $\neg B \in Γ$ , ekkor a $Γ \cup {\neg A}$ is, és a $Γ \cup {B}$ is inkonzisztens. Tegyük fel, hogy $\neg (A \supset B) \notin Γ$ , tehát $A \supset B \in Γ$ . Az első állítás bizonyításánál láttuk, hogy ekkor a feltétellel ellentétben $\neg A \in Γ$ vagy $B \in Γ$ lenne.

Ezzel mindkét állítást bebizonyítottuk. $⋄$

6.1.31. TÉTEL. Tetszőleges konzisztens formulahalmaz kiterjeszthető maximális konzisztens formulahalmazzá.

BIZONYÍTÁS. A bizonyítás konstruktív, vagyis előállít egy a tetszőlegesen rögzített $S$ konzisztens formulahalmazt tartalmazó, maximális konzisztens formulahalmazt. A konstrukció Lindenbaum nevéhez fűződik. Jelölje $ℒ_{0}$ az összes ítéletlogikai formulának a halmazát. Az $ℒ_{0}$ megszámlálhatóan végtelen halmaz elemeinek legyen ${A_{1}, A_{2}, \dots}$ egy felsorolása. A konstrukció a következő. Legyen $S_{0}$ az $S$ konzisztens formulahalmaz, és minden $i = 1,2, \dots$ -re ha $S_{i - 1}$ -et már megkonstruáltuk, akkor

$S_{i} ⇌ {\begin{array}{l} S_{i - 1} \cup {A_{i}}, & ha S_{i - 1} \cup {A_{i}} konzisztens, \\ S_{i - 1} & egyébként . \end{array}$

Megmutatjuk, hogy az így kapott $S_{0} \subseteq S_{1} \subseteq \dots$ konzisztens formulahalmazlánc elemeinek uniója egy $Γ$ maximális konzisztens formulahalmaz.

Lássuk be először, hogy $Γ$ konzisztens. Tegyük fel, hogy nem az. Ekkor $Γ$ -ból levezethető valamely $A$ és $\neg A$ is. Legyenek $B_{1}, B_{2}, \dots, B_{j}$ a levezetésekben előforduló $Γ$ -beli formulák. Mivel ezek a levezetések véges sok formulából állnak, van olyan $i$ , hogy ${B_{1}, B_{2}, \dots, B_{j}} \subseteq S_{i}$ . De ez azt jelentené, hogy $S_{i}$ -nek van inkonzisztens részhalmaza, tehát $S_{i}$ inkonzisztens, ellentétben a konstrukcióval. Ez ellentmondás, tehát $Γ$ konzisztens.
Lássuk be ezután, hogy $Γ$ maximális is. Tegyük fel, hogy $Γ'$ konzisztens és $Γ \subseteq Γ'$ . Belátjuk, hogy $Γ = Γ'$ , vagyis ha $A_{k} \in Γ'$ , akkor $A_{k} \in Γ$ is. Tegyük fel, hogy $A_{k} \in Γ'$ , de $A_{k} \notin Γ$ . Konstrukciónk szerint az, hogy $A_{k} \notin Γ$ , azt jelenti, hogy $S_{k - 1} \cup {A_{k}}$ inkonzisztens. Másrészt $S_{k - 1} \subseteq Γ \subseteq Γ'$ és $A_{k} \in Γ'$ , ami miatt $Γ'$ is inkonzisztens volna.

Tehát a tételt igazoltuk. $⋄$

6.1.32. TÉTEL. A maximális konzisztens formulahalmazok kielégíthetők.

BIZONYÍTÁS. Legyen $Γ$ maximális konzisztens formulahalmaz. A 6.1.29. tétel (b) állítása miatt tetszőleges $X$ ítéletváltozó esetén az $X$ és a $\neg X$ literáloknak pontosan az egyike eleme $Γ$ -nak. Tekintsük a következő $ℐ$ interpretációt.

$ℐ (X) ⇌ {\begin{array}{l} i & ha X \in Γ, \\ h & ha \neg X \in Γ . \end{array}$

Megmutatjuk, hogy tetszőleges $A$ formulára $A \in Γ$ akkor és csak akkor, ha $ℬ_{ℐ} (A) = i$ .

(alaplépés:) Ha $A \in Γ$ és az $A$ formula literál, akkor $A = X$ esetén $ℬ_{ℐ} (X) = ℐ (X) = i$ és $A = \neg X$ esetén $ℬ_{ℐ} (\neg X) = \neg ℐ (X) = i$ .

(indukciós lépések:) Tegyük fel, hogy $\neg A \in Γ$ . Ekkor $A \notin Γ Γ$ maximális konzisztenciája (6.1.29. tétel) miatt. Az indukciós feltétel szerint ekkor $ℬ_{ℐ} (A) = h$ . De $ℬ_{ℐ} (\neg A)$ éppen $\neg ℬ_{ℐ} (A)$ , tehát $ℬ_{ℐ} (\neg A) = i$ . Fordítva, legyen $ℬ_{ℐ} (\neg A) = i$ . Ekkor $ℬ_{ℐ} (A) = h$ , az indukciós feltétel szerint viszont így $A \notin Γ$ . A 6.1.29. tétel miatt tehát $\neg A \in Γ$ .

Tegyük fel most, hogy $A \supset B \in Γ$ . Ekkor $Γ$ a 6.1.30. tétel szerint $\neg A \in Γ$ vagy $B \in Γ$ . Az indukciós hipotézis alapján $ℬ_{ℐ} (\neg A) = i$ vagy $ℬ_{ℐ} (B) = i$ , ami azt biztosítja, hogy $ℬ_{ℐ} (A \supset B) = i$ . Fordítva, ha $ℬ_{ℐ} (A \supset B) = i$ , akkor $ℬ_{ℐ} (\neg A) = i$ vagy $ℬ_{ℐ} (B) = i$ . Az indukciós feltétel miatt ebben az esetben $\neg A \in Γ$ vagy $B \in Γ$ , így a 6.1.30. tétel miatt $(A \supset B) \in Γ$ .

Azaz tetszőleges $A \in Γ$ formulára $ℬ_{ℐ} (A) = i$ , így a $ℐ$ kielégíti $Γ$ -t. $⋄$

6.1.33. TÉTEL. Tetszőleges konzisztens formulahalmaz kielégíthető.

BIZONYÍTÁS. A 6.1.31. tétel szerint tetszőleges $S$ konzisztens formulahalmaz kiterjeszthető egy $Γ$ maximális konzisztens formulahalmazzá. A 6.1.32. tétel miatt egy maximális konzisztens formulahalmaz kielégíthető. Egy kielégíthető formulahalmaz minden részhalmaza kielégíthető, ezért – mivel $S \subseteq Γ$ – $S$ is kielégíthető. $⋄$

6.1.34. TÉTEL. Egy formulahalmaz pontosan akkor kielégíthetetlen, ha inkonzisztens.

BIZONYÍTÁS. Beláttuk, hogy ha egy formulahalmaz konzisztens, akkor kielégíthető (6.1.33. tétel). Beláttuk azt is (6.1.23. tétel), hogy ha egy formulahalmaz inkonzisztens, akkor kielégíthetetlen. Ebből következik, hogy egy formulahalmaz akkor és csak akkor inkonzisztens, ha kielégíthetetlen. $⋄$

6.1.35. TÉTEL. (AZ ÍTÉLETKALKULUS TELJESSÉGE.)

Legyen ${A_{1}, A_{2}, \dots}$ tetszőleges, nem feltétlenül véges formulahalmaz és $B$ tetszőleges formula. Ha ${A_{1}, A_{2}, \dots} ⊨_{0} B$ , akkor ${A_{1}, A_{2}, \dots} ⊢_{0} B$ .

BIZONYÍTÁS. (A Gödel-féle gondolatmenet.) Ha ${A_{1}, A_{2}, \dots} ⊨_{0} B$ , akkor a 4.4.4. tétel szerint ${A_{1}, A_{2}, \dots, \neg B}$ kielégíthetetlen. A 6.1.34. tétel miatt a kielégíthetetlen formulahalmazok ellentmondásosak is, tehát ${A_{1}, A_{2}, \dots, \neg B}$ ellentmondásos. A 6.1.22. tétel azt mondja, hogy ha ${A_{1}, A_{2}, \dots, \neg B}$ ellentmondásos, akkor ${A_{1}, A_{2}, \dots} ⊢_{0} B$ . Ezzel a tételt bebizonyítottuk. $⋄$

Azt kaptuk tehát, hogy a szintaktikus és szemantikus következményfogalom azonos egymással, azaz a (szemantikusan) helyes következtetések formálisan bizonyíthatók, valamint hogy minden szintaktikus következmény egyben szemantikus következmény is. Az ítéletkalkulus teljessége azt jelenti, hogy az ítéletlogikát fel lehet építeni szintaktikai alapokon és ez a felépítés ekvivalens a szemantikai alapú felépítéssel. Szokás ezt úgy is fogalmazni, hogy az ítéletlogika minden tautológiája (a bizonyításelmélet eszközeivel) bizonyítható.

Az ítéletlogika nyelvére is felépíthetjük az ítéletkalkulust. Ilyenkor gondoskodunk konjunkciós és diszjunkciós formulákra vonatkozó axiómasémákról, illetve levezetési szabályokról is. Bővítsük ki például az ítéletkalkulus axiómasémáinak rendszerét az (A4)–(A10) axiómasémákkal, és a levezetési szabály továbbra is egyedül a modus ponens legyen.

(A1)	$X \supset (Y \supset X)$
(A2)	$(X \supset (Y \supset Z)) \supset ((X \supset Y) \supset (X \supset Z))$
(A3)	$(\neg X \supset Y) \supset ((\neg X \supset \neg Y) \supset X)$
(A4)	$\neg \neg X \supset X$
(A5)	$X \supset (Y \supset X \land Y)$
(A6)	$X \land Y \supset X$
(A7)	$X \land Y \supset Y$
(A8)	$(X \supset Z) \supset ((Y \supset Z) \supset (X \lor Y \supset Z))$
(A9)	$X \supset X \lor Y$
(A10)	$Y \supset X \lor Y$

A levezetés és a levezethetőség definícióját ne változtassuk. (Természetesen a levezetésben az új kalkulusban mindig leírhatunk egy új axiómasémából nyert formulát is.) Világos, hogy ha ${A_{1}, A_{2}, \dots} ⊢_{0} B$ , akkor az ${A_{1}, A_{2}, \dots}$ hipotézisekből ebben a bővebb axiómaséma-halmazzal rendelkező kalkulusban is levezethető lesz $B$ . Fordítva, ha $B$ a bővebb axiómaséma-halmazzal rendelkező kalkulusban vezethető le az ${A_{1}, A_{2}, \dots}$ hipotézisekből, akkor könnyű belátni, hogy az eredeti kalkulusban is le lehet vezetni $B$ -t (vagy egy vele ekvivalens, csak $\neg$ -t és $\supset$ -t tartalmazó formulát) ${A_{1}, A_{2}, \dots}$ -ből. Az új axiómasémák ugyanis tautológiák, így az ítéletkalkulusban mindegyik bizonyítható, tehát hipotézismentesen levezethető. Így egy az új kalkulusban adott levezetésből mindig előállítható az eredeti kalkulusbeli levezetés úgy, hogy a levezetésben az új axiómaformulák helyére beírjuk a levezetésüket. Tehát a két kalkulusban minden formulahalmazból pontosan ugyanazok a formulák lesznek levezethetők, a két kalkulus ekvivalens.

Egy másik lehetőség az ítéletkalkulusnak az ítéletlogika nyelvéhez illesztésére, hogy új levezetési szabályok bevezetése mellett változatlanul hagyjuk az axiómasémák halmazát. Ekkor az (A4)–(A10) tautológiákat levezetési szabályként használjuk fel. Például $⊢_{0} A \supset A \lor B$ az (A9)-nek megfelelő elemi levezetés, amelyből a dedukciós tétellel azt kapjuk, hogy $A ⊢_{0} A \lor B$ , amit így használhatunk mint levezetési szabályt. A levezetés és a levezethetőség definícióját most se változtassuk. (Természetesen a levezetés során ebben a kalkulusban mindig leírhatunk egy – a már a levezetésben szereplő formulá(k)ból – az új levezetési szabállyal (szabályokkal) nyert formulát is.) Könnyen belátható, hogy egy így nyert kalkulus is ekvivalens az előzőekkel.

A predikátumkalkulus

Az elsőrendű logika bizonyításelméleti tárgyalását mint kalkulust szokás predikátumkalkulusnak vagy logikai függvénykalkulusnak nevezni. Az elsőrendű logika bizonyításelméleti eszközökkel való felépítéséhez bevezetünk elsőrendű formulákat mint ,,alapigazságokat – axiómasémákat” és egy levezetési szabályt, a modus ponenst. Definiáljuk a levezethetőség fogalmát és meghatározzuk, ha lehet, az eldöntésproblémát. Elegendő a $\forall$ kvantort és a $\neg$ , $\supset$ logikai összekötőjeleket bevenni az elsőrendű nyelv ábécéjébe, így az axiómarendszerben a három, az ítéletkalkulusból már ismert sémán kívül az univerzális kvantorra vonatkozó axiómasémák fognak megjelenni. A predikátumkalkulus axiómaformuláit úgy kapjuk, hogy az axiómasémákban az $A, B$ és a $C$ betűk helyére az adott elsőrendű logikai nyelv tetszőleges formuláit, $x$ helyére a nyelv valamely változóját és $t$ helyére a nyelv valamely termjét írjuk, illetve egy így nyert formulát általánosítunk.

Table 6.4. A predikátumkalkulus axiómasémái

(B1)	$A \supset (B \supset A)$
(B2)	$(A \supset (B \supset C)) \supset ((A \supset B) \supset (A \supset C))$
(B3)	$(\neg A \supset B) \supset ((\neg A \supset \neg B) \supset A)$
(B4)	$\forall x A \supset [A (x ∥ t)]$
(B5)	$\forall x (A \supset B) \supset (\forall x A \supset \forall x B)$
(B6)	$A \supset \forall x A$ , ahol $x \notin Par (A)$
(B7)	a (B1)–(B6) axiómák általánosításai

A predikátumkalkulus levezetési szabálya is a modus ponens, az 5.4.13. tételből tudjuk, hogy $({A \supset B, A}, B)$ az elsőrendű logikában is helyes következtetési forma.

Table 6.5. A predikátumkalkulus levezetési szabálya

(MP)	${A \supset B, A} ⊢ B$

A levezetés definíciója formailag megegyezik az ítéletlogikában megadottal, csak most a definícióban hivatkozott axiómaformulák a predikátumkalkulus axiómaformulái.

6.1.36. DEFINÍCIÓ. Legyen ${A_{1}, A_{2}, \dots}$ egy elsőrendű logikai nyelv formuláinak tetszőleges, esetleg üres halmaza és $B$ a nyelv egy formulája. Az ${A_{1}, A_{2}, \dots}$ formulahalmazból a $B$ formula predikátumkalkulusbeli levezetése egy olyan $D_{1}, D_{2}, \dots, D_{m}$ $(m \geq 1)$ formulasorozat, ahol minden $j = 1,2, \dots, m$ -re $D_{j}$

vagy eleme az ${A_{1}, A_{2}, \dots}$ formulahalmaznak, azaz hipotézis,
vagy a (B1)–(B7) axiómasémák szerint nyert formula, azaz axiómaformula,
vagy van olyan $1 \leq s, t \leq j$ , hogy a $D_{s}$ és a $D_{t}$ formulákból levezetési szabállyal állt elő,

és a formulasorozat utolsó tagja, $D_{m}$ , éppen a $B$ formula.

6.1.37. DEFINÍCIÓ. Legyen ${A_{1}, A_{2}, \dots}$ egy elsőrendű logikai nyelv formuláinak tetszőleges, esetleg üres halmaza és $B$ a nyelv egy formulája. Azt mondjuk, hogy $B$ az ${A_{1}, A_{2}, \dots}$ formulahalmazból a predikátumkalkulusban levezethető, ha $B$ -nek van az ${A_{1}, A_{2}, \dots}$ formulahalmazból (predikátumkalkulusbeli) levezetése. Jelölése ${A_{1}, A_{2}, \dots} ⊢ B$ .

A levezethetőség a predikátumkalkulus következményfogalma, amely szintén szintaktikus következményfogalom.

6.1.38. DEFINÍCIÓ. Legyen $B$ egy elsőrendű logikai nyelv formulája. $B$ a predikátumkalkulusban bizonyítható, ha van hipotézismentes levezetése (azaz levezethető az üres feltételformula-halmazból). Ebben az esetben a $⊢ B$ jelölést alkalmazzuk.

6.1.39. PÉLDA. Most megmutatjuk, hogy a $\forall x \forall y Q (x, y) ⊢ Q (x, y)$ szekvencia megalapozható a predikátumkalkulusban.

$1.$	$\forall x \forall y Q (x, y)$	[ hipotézis ]
$2.$	$\forall x \forall y Q (x, y) \supset \forall y Q (x, y)$	[ (B4) ]
$3.$	$\forall y Q (x, y)$	[ (MP): 1, 2 ]
$4.$	$\forall y Q (x, y) \supset Q (x, y)$	[ (B4) ]
$5.$	$Q (x, y)$	[ (MP): 3, 4 ]

Az ítélet- és a predikátumkalkulusban való levezetés definíciója tehát csak abban különbözik egymástól, hogy a predikátumkalkulusban való levezetésben az ítéletkalkulus axiómáin kívül újabb axiómákat is használhatunk. Nyilván előfordulhat az is, hogy a predikátumkalkulusban való levezetésben csak a (B1)–(B3) sémákból – az ítéletkalkulus sémáiból – előállított axiómák szerepelnek. Ha egy $B$ formula predikátumkalkulusbeli levezetése az ${A_{1}, A_{2}, \dots}$ hipotézisekből (vagy hipotézismentesen) ilyen, használjuk a ${A_{1}, A_{2}, \dots} ⊢_{0} B (⊢_{0} B$ ) jelölést. Világos, hogy ha ${A_{1}, A_{2}, \dots} ⊢_{0} B$ , akkor ${A_{1}, A_{2}, \dots} ⊢ B$ , illetve ha $⊢_{0} B$ , akkor $⊢ B$ . Nyilvánvaló az is, hogy ítéletkalkulusnak a levezetéssel kapcsolatos tételei, vagyis azok a tételek, amelyeknek a bizonyításában a levezetés tulajdonságait használjuk ki, a predikátumkalkulusban is érvényesek maradnak. Ezeket a tételeket bizonyítás nélkül adjuk meg.

6.1.40. TÉTEL. (DEDUKCIÓS TÉTEL.)

Legyenek $A_{1}, A_{2}, \dots, A_{n}, B$ (n $\geq 1)$ egy elsőrendű logikai nyelv formulái. ${A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}} ⊢ B$ pontosan akkor, ha ${A_{1}, A_{2}, \dots, A_{n - 1}} ⊢ A_{n} \supset B$ .

6.1.41. TÉTEL. (AZ ELDÖNTÉSPROBLÉMA TÉTELE.)

Legyenek $A_{1}, A_{2}, \dots, A_{n}, B$ (n $\geq 1)$ egy elsőrendű logikai nyelv formulái. ${A_{1}, A_{2}, \dots, A_{n - 1}, A_{n}} ⊢ B$ pontosan akkor, ha $⊢ A_{1} \supset A_{2} \supset \dots \supset A_{n - 1} \supset A_{n} \supset B$ .

6.1.42. TÉTEL. (A PREDIKÁTUMKALKULUS HELYESSÉGE.)

Legyenek $A_{1}, A_{2}, \dots, B$ egy elsőrendű logikai nyelv formulái. Ha ${A_{1}, A_{2}, \dots} ⊢ B$ , akkor ${A_{1}, A_{2}, \dots} ⊨ B$ .

6.1.43. PÉLDA. Bizonyítsuk be a predikátumkalkulusban a $\forall x P (x) \supset \forall y P (y)$ formulát. A dedukciós tétel a predikátumkalkulusban is érvényes, így elég megadni $\forall y P (y)$ levezetését a $\forall x P (x)$ hipotézisből. Ebből a levezetésből a 6.1.12. tétel bizonyításában megtanult módszerrel könnyen megkonstruálható $\forall x P (x) \supset \forall y P (y)$ hipotézismentes levezetése is.

$1.$	$\forall x P (x)$	[ hipotézis ]
$2.$	$\forall x P (x) \supset \forall y \forall x P (x)$	[ (B6) ]
$3.$	$\forall y \forall x P (x)$	[ (MP): 1, 2 ]
$4.$	$\forall y (\forall x P (x) \supset P (y))$	[ (B4) általánosítása ]
$5.$	$\forall y (\forall x P (x) \supset P (y)) \supset (\forall y \forall x P (x) \supset \forall y P (y))$	[ (B5) ]
$6.$	$\forall y \forall x P (x) \supset \forall y P (y)$	[ (MP): 4, 5 ]
$7.$	$\forall y P (y)$	[ (MP): 3, 6 ]

6.1.44. TÉTEL. (AZ ÁLTALÁNOSÍTÁS SZABÁLYA.)

Legyenek $A_{1}, A_{2}, \dots, B$ egy elsőrendű logikai nyelv formulái és $x$ egy olyan változó, hogy $x \notin P a r (A_{i})$ . Ha ${A_{1}, A_{2}, \dots} ⊢ B$ , akkor ${A_{1}, A_{2}, \dots} ⊢ \forall x B$ .

BIZONYÍTÁS. Jelölje $Γ$ az ${A_{1}, A_{2}, \dots}$ formulahalmazt. $Γ ⊢ B$ azt jelenti, hogy $B$ -nek van levezetése $Γ$ -ból. Legyen ez a levezetés $D_{1}, D_{2}, \dots, D_{m} = B$ . A bizonyítás a következő lépésekből áll:

Írjuk a levezetésben szereplő formulák elé a $\forall x$ prefixumot. Így a $\forall x D_{1}, \forall x D_{2}, \dots, \forall x D_{m} = \forall x B$ formulasorozatot kapjuk.
Lássuk be, hogy minden $k$ -ra $(1 \leq k \leq m)$ létezik $\forall x D_{k}$ -nak $Γ$ -ból való levezetése.
1. Legyen $D_{k}$ axiómaformula, ekkor $\forall x D_{k}$ is – (B7) miatt – axiómaformula.
2. Legyen $D_{k}$ eleme a $Γ$ -nak. Ekkor $x \notin Par (D_{k})$ és $\forall x D_{k}$ levezethető $Γ$ -ból. A levezetés:

$1.$	$D_{k} \supset \forall x D_{k}$	[ (B6) ]
$2.$	$D_{k}$	[ hipotézis ]
$3.$	$\forall x D_{k}$	[ (MP): 1, 2 ]

Legyen $D_{k}$ az első olyan (eddig még nem vizsgált) formula az eredeti levezetésben, amely modus ponense $D_{t}, D_{s} = D_{t} \supset D_{k}$ levezetésbeli formuláknak $(s, t \leq k)$ . Ez azt jelenti, hogy már igazoltuk, hogy $Γ$ -ból a $\forall x (D_{t} \supset D_{k})$ , valamint a $\forall x D_{t}$ formula levezethető:

$⋮$
$i .$	$\forall x (D_{t} \supset D_{k})$
$⋮$
$j .$	$\forall x D_{t}$
$⋮$
$w .$	$\forall x (D_{t} \supset D_{k}) \supset (\forall x D_{t}) \supset \forall x D_{k}$	[ (B5) ]
$(w + 1) .$	$\forall x D_{t} \supset \forall x D_{k}$	[ (MP): $i$ , $w$ ]
$(w + 2) .$	$\forall x D_{k}$	[ (MP): $j$ , $(w + 1)$ ]

Indukcióval könnyen bizonyítható, hogy $Γ ⊢ \forall x D_{k}$ akkor is, ha $D_{k}$ tetszőleges – nem feltétlen az első – olyan formula az eredeti levezetésben, amelyet modus ponenssel nyertünk.

A $\forall x D_{k}$ formulák elé $(1 \leq k \leq m)$ beírjuk azok levezetését $Γ$ -ból. Ezzel $Γ$ -ból való levezetések konkatenációját kapjuk, ami a $Γ$ -ból való levezetése a $\forall x B$ formulának.

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

6.1.45. PÉLDA. Bizonyítsuk be a $\forall x P (x) \supset \forall y P (y)$ formulát az általánosítás szabálya (6.1.44. tétel) felhasználásával is. A dedukciós tétel a $\forall x P (x) ⊢ \forall y P (y)$ szekvenciát kell megalapozni, ehhez pedig az általánosítás szabálya miatt elég a $\forall x P (x) ⊢ P (y)$ szekvenciát igazolni.

$1.$	$\forall x P (x)$	[ hipotézis ]
$2.$	$\forall x P (x) \supset P (y)$	[ (B4) ]
$3.$	$P (y)$	[ (MP): 1, 2 ]

Könnyű észrevenni, hogy ebből a levezetésből a 6.1.44. tétel bizonyításában megismert módszerrel is megkonstruálható a 6.1.43. példabeli levezetés.

Most a szemantikus tárgyalásnál definiált logikai ekvivalencia fogalom bizonyításelméleti megfelelőjét definiáljuk:

6.1.46. DEFINÍCIÓ. Azt mondjuk, hogy az $A$ és a $B$ elsőrendű logika formulák bizonyíthatóan ekvivalensek, ha ${A} ⊢ B$ és ${B} ⊢ A$ .

6.1.47. PÉLDA. Igazoljuk, hogy az $R \supset \forall x P (x)$ és a $\forall x (R \supset P (x))$ formulák bizonyíthatóan ekvivalensek ( $x \notin Par (R)$ ).

A $\forall x (R \supset P (x)) ⊢ R \supset \forall x P (x)$ szekvencia megalapozásához a dedukciós tétel miatt elég a $\forall x (R \supset P (x)), R ⊢ \forall x P (x)$ szekvenciát megalapozni, ezt meg az általánosítás szabálya miatt a $\forall x (R \supset P (x)), R ⊢ P (x)$ levezetés megkonstruálásával igazolhatjuk:

$1.$	$\forall x (R \supset P (x))$	[ hipotézis ]
$2.$	$\forall x (R \supset P (x)) \supset (R \supset P (x))$	[ (B4) ]
$3.$	$R \supset P (x)$	[ (MP): 1, 2 ]
$4.$	$R$	[ hipotézis ]
$5.$	$P (x)$	[ (MP): 3, 4 ]

Az $R \supset \forall x P (x) ⊢ \forall x (R \supset P (x))$ szekvencia megalapozásához igazoljuk, hogy $R \supset \forall x P (x) ⊢ R \supset P (x)$ , majd alkalmazzuk az általánosítás szabályát.

$1.$	$\forall x P (x) \supset P (x)$	[ (B4) ]
$2.$	$(\forall x P (x) \supset P (x)) \supset (R \supset (\forall x P (x) \supset P (x)))$	[ (B1) ]
$3.$	$R \supset (\forall x P (x) \supset P (x))$	[ (MP): 1, 2 ]
$4.$	$(R \supset (\forall x P (x) \supset P (x))) \supset ((R \supset \forall x P (x)) \supset (R \supset P (x)))$	[ (B2) ]
$5.$	$(R \supset \forall x P (x)) \supset (R \supset P (x))$	[ (MP): 3, 4 ]
$6.$	$R \supset \forall x P (x)$	[ hipotézis ]
$7.$	$R \supset P (x)$	[ (MP): 5, 6 ]

6.1.48. DEFINÍCIÓ. Azt mondjuk, hogy elsőrendű logikai formulák egy ${A_{1}, A_{2}, \dots}$ halmaza ellentmondásos, ha van olyan $A$ formula, hogy ${A_{1}, A_{2}, \dots}$ -ből $A$ is, és $\neg A$ is levezethető. Egyébként ${A_{1}, A_{2}, \dots}$ ellentmondásmentes.

6.1.49. TÉTEL. Legyen ${A_{1}, A_{2}, \dots}$ egy elsőrendű logikai nyelv formuláinak tetszőleges halmaza és $B$ a nyelv egy formulája.

${A_{1}, A_{2}, \dots, \neg B}$ pontosan akkor ellentmondásos, ha ${A_{1}, A_{2}, \dots} ⊢ B$ .
${A_{1}, A_{2}, \dots, B}$ pontosan akkor ellentmondásos, ha ${A_{1}, A_{2}, \dots} ⊢ \neg B$ .

6.1.50. TÉTEL. Ha egy ${A_{1}, A_{2}, \dots}$ elsőrendű formulahalmaz ellentmondásos, akkor kielégíthetetlen.

6.1.51. TÉTEL. Legyenek ${A_{1}, A_{2}, \dots}$ egy elsőrendű formulahalmaz, $B$ és $C$ elsőrendű logikai formulák. Ha ${A_{1}, A_{2}, \dots, B} ⊢ C$ és ${A_{1}, A_{2}, \dots, \neg B} ⊢ C$ , akkor ${A_{1}, A_{2}, \dots} ⊢ C$ .

6.1.52. TÉTEL. (A PREDIKÁTUMKALKULUS TELJESSÉGE.)

Legyen ${A_{1}, A_{2}, \dots}$ egy elsőrendű logikai nyelv formuláinak tetszőleges (nem feltétlenül véges) halmaza és $B$ tetszőleges formula. Ha ${A_{1}, A_{2}, \dots} ⊨ B$ , akkor ${A_{1}, A_{2}, \dots} ⊢ B$ .

A predikátumkalkulus teljességének bizonyításához meg kell mutatni, hogy minden elsőrendű konzisztens (ellentmondásmentes) formulahalmaz kielégíthető. Ehhez viszont szükség van a következő tételek igazolására:

Tetszőleges elsőrendű konzisztens formulahalmaz kiterjeszthető maximális konzisztens formulahalmazzá.
Egy elsőrendű maximális konzisztens formulahalmaz kielégíthető.

A teljességi tételt Henkin 1949-ben bizonyította be. Ennek a bizonyításnak az ismertetése túlnő a könyv keretein, a szakirodalomban viszont több helyen is megtalálható [7,29,60].

Azt kaptuk tehát, hogy a megadott szintaktikus és szemantikus következményfogalom az elsőrendű logikában is azonos egymással, azaz a (szemantikusan) helyes következtetések formálisan bizonyíthatók, valamint hogy minden szintaktikus következmény egyben szemantikus következmény is. A predikátumkalkulus helyessége és teljessége azt jelenti, hogy az elsőrendű logikát fel lehet építeni szintaktikai alapokon és ez a felépítés ekvivalens a szemantikai alapú felépítéssel.

Legyen $ℒ [V_{ν}]$ egy – az 5.1. fejezetben definiált – elsőrendű logikai nyelv. Az $ℒ [V_{ν}]$ nyelvre is felépíthetjük a predikátumkalkulust. Ilyenkor gondoskodunk konjunkciós, diszjunkciós és egzisztenciálisan kvantált formulákra vonatkozó axiómasémákról is. A levezetési szabály továbbra is a modus ponens legyen.

(C1)	$A \supset (B \supset A)$
(C2)	$(A \supset (B \supset C)) \supset ((A \supset B) \supset (A \supset C))$
(C3)	$(\neg A \supset B) \supset ((\neg A \supset \neg B) \supset A)$
(C4)	$\neg \neg A \supset A$
(C5)	$A \supset (B \supset A \land B)$
(C6)	$A \land B \supset A$
(C7)	$A \land B \supset B$
(C8)	$(A \supset C) \supset ((B \supset C) \supset (A \lor B \supset C))$
(C9)	$A \supset A \lor B$
(C10)	$B \supset A \lor B$
(C11)	$\forall x A \supset [A (x ∥ t)]$
(C12)	$\forall x (B \supset A) \supset (B \supset \forall x A)$ , ahol $x \notin Par (B)$
(C13)	$[A (x ∥ t)] \supset \exists x A$
(C14)	$\forall x (A \supset B) \supset (\exists x A \supset B)$ , ahol $x \notin Par (B)$ .
(C15)	$A \supset \forall x A$ , ahol $x \notin Par (A)$
(C16)	a (C1)–(C15) axiómák általánosításai

A levezetés definícióját módosítsuk úgy, hogy az új kalkulusban a levezetés során mindig leírhassunk egy új axiómasémából nyert formulát is. Be lehet látni, hogy ha ${A_{1}, A_{2}, \dots} ⊢ B$ , akkor az ${A_{1}, A_{2}, \dots}$ hipotézisekből az új kalkulusban is levezethető lesz $B$ . Fordítva, ha $B$ az új kalkulusban vezethető le az ${A_{1}, A_{2}, \dots}$ hipotézisekből, akkor az eredeti kalkulusban is le lehet vezetni $B$ -t (vagy egy vele ekvivalens, csak $\neg, \supset$ és $\forall$ logikai jeleket tartalmazó formulát) ${A_{1}, A_{2}, \dots}$ -ből. Az új axiómasémák ugyanis logikailag igazak, tehát az eredeti predikátumkalkulusban mindegyik bizonyítható, azaz hipotézismentesen levezethető. Így egy az új kalkulusban adott levezetésből mindig előállítható az eredeti kalkulusbeli levezetés úgy, hogy a levezetésben az új axiómaformulák helyére beírjuk a levezetésüket. Tehát a két kalkulusban minden formulahalmazból pontosan ugyanazok a formulák lesznek levezethetők, a két kalkulus ekvivalens.

A 3.3. fejezetben említést tettünk az egyenlőségjeles elsőrendű logikai nyelvről. Ha a nyelvünk ilyen, a kalkulusban megjelennek további, az egyenlőség predikátumra vonatkozó axiómasémák is, melyeket (D7)–(D9)-cel jelölünk. Az egyenlőségjeles predikátumkalkulus axiómasémái például a következők:

(D1)	$A \supset (B \supset A)$
(D2)	$(A \supset (B \supset C)) \supset ((A \supset B) \supset (A \supset C))$
(D3)	$(\neg A \supset B) \supset ((\neg A \supset \neg B) \supset A)$
(D4)	$\forall x A \supset [A (x ∥ t)]$
(D5)	$\forall x (A \supset B) \supset (\forall x A \supset \forall x B)$
(D6)	$A \supset \forall x A$ , ahol $x \notin P a r (A)$
(D7)	$t = t$
(D8)	$t_{1} = t_{n + 1} \supset \dots \supset t_{n} = t_{2 n} \supset f (t_{1}, t_{2}, \dots, t_{n}) = f (t_{n + 1}, t_{n + 2}, \dots, t_{2 n})$
(D9)	$t_{1} = t_{n + 1} \supset \dots \supset t_{n} = t_{2 n} \supset P (t_{1}, t_{2}, \dots, t_{n}) \supset P (t_{n + 1}, t_{n + 2}, \dots, t_{2 n})$
(D10)	a (D1)–(D9) axiómák általánosításai

A levezetési szabálynak megtartjuk a modus ponenst. Be lehet bizonyítani, hogy az egyenlőségjeles predikátumkalkulus is helyes és teljes kalkulus. Ezzel a bizonyítással nem foglalkozunk.

Feladatok

6.1.1. FELADAT. Legyen $Γ$ formulahalmaz, $B$ és $C$ formulák. Igazoljuk, hogy ha $Γ ⊢_{0} B$ és $Γ \cup {B} ⊢_{0} C$ , akkor $Γ ⊢_{0} C$ .

6.1.2. FELADAT. Bizonyíthatók-e a predikátumkalkulusban az alábbi formulák. Ha igen, adjuk meg egy-egy levezetésüket.

$\forall x \forall y Q (x, y) \supset \forall y \forall x Q (x, y)$
$\exists x \forall y Q (x, y) \supset \forall y \exists x Q (x, y)$
$\forall x \exists y Q (x, y) \supset \exists y \forall x Q (x, y)$
$(\forall x P (x) \supset \exists x R (x)) \supset \exists x (P (x) \supset R (x))$