Logikai nyelvek.

Néhány matematikai diszciplína (struktúra) logikai nyelve.

Minden esetben adott az illető diszciplína meghatározásához hozzátartozik egy nem logikai jelkészlet,  
a tárgyalási univerzum U, vagy indivíduumhalmaz, 
az univerzumon értelmezett legszükségesebb 
(alap)relációk (logikai függvények Un{i,h})és 
(alap)műveletek (matematikai függvények, UnU). 
Ezek az illető diszciplínában az egyszerű állítások leírásának eszközei. 

A logikai jelkészlet:az indivíduum változók, a logikai összekötőjelek és a kvantorok. Kiegészítő elemek az elválasztójelek.

Példák.
1. Az elemi aritmetika logikai nyelve (Ar. nyelv).
(Univerzum: N0 )

ábécé:
Műveletek jelei:
0-változós (konstans)			0
1-változós (rákövetkezés)		s(x)
2-változós	(összeadás, szorzás) 	+, *.
Alaprelációk jelei:
2-változós:					=, 
Összefoglalva: Az N0-on értelmezett relációk és műveletek jelei 
(=,  ; s, *, +, 0) alkotják az Ar nyelv ábécéjének  “logikán kívüli” (speciális) részét.

- Indivíduum változók: x, y,...
- Logikai műveletek: , , , 
- Kvantorok: 	    ,  
alkotják az Ar nyelv ábécéjének  “logikai” részét. 
Elválasztójelek: ( ) ,

Szintaxis:
Matematikai leképezéseket leíró kifejezések a termek. Az s, *, +, 0, univerzumelemek és az indivíduum változók felhasználásával az aritmetikában ismert módon állnak elő.

Logikai leképezéseket leíró kifejezések a formulák. Atomi formulák: x=y, xy. Ezekből a , , ,  és a ,  felhasználásával állítjuk elő a formulákat. 

Példák :
Termek: x, x+y, x*y+z.
Formulák:
x=y		atomi
x*s(s(0))  x+s(s(0))	atomi
x=y x*s(s(0))= y*s(s(0)) összetett

Szemantika:
A (=,  ; s, *, +, 0) és a , , ,  jelek értéktábláinak ismeretében, a lehetséges változókiértékelések mellett kiszámítjuk a kifejezés helyettesítési értékét, azt hozzárendeljük az egyes változókiértékelésekhez megadva ezzel azt a függvénykapcsolatot amit a kifejezés jelent.

Logikai leképezések (nem alaprelációk) leírása - formalizálása:
xy =def  x=y
xy =def z(y+z)=x
x<y =def xy  xy
x osztója y-nak: xy =def  x0  z(x*z)=y
x prímszám =def x0  xs(0)  z(zx  (z=s(0)  z=x)
Elsőrendű az a nyelv amelyben az univerzumot befutó indivíduumváltozóra lehet a kvantorokat alkalmazni. 
Másodrendű az a nyelv nyelv amelyben az univerzumon definiálható összes logikai és matematikai függvények halmazát befutó változóra lehet a kvantorokat alkalmazni. 
Kifejezőerő.!!!

 2. A részhalmaz logikai nyelv (Részh. nyelv).
Univerzum: P(H), egy halmaz hatványhalmaza.

ábécé:
Műveletek jelei:
1-változós (komplementer)	x.
2-változós	(metszet, unió) , .
Alaprelációk jelei:
2-változós:		
Változók: x, y,...
Összefoglalva: P(H) ( ; x, , ) a részhalmaz nyelv ábécéjének  “logikán kívüli” része.

- Indivíduum változók: x, y,...
- Logikai műveletek: , , , 
- Kvantorok: ,  
A nyelv ábécéjének  “logikai” része. 
Elválasztójelek: ( ) ,

Szintaxis:
Matematikai leképezéseket leíró kifejezések a termek. Az (x, , ) jelek, univerzumelemek és  változók felhasználásával a halmazelméletben ismert módon állnak elő.
Logikai leképezéseket leíró kifejezések a formulák. Atomi formula:  xy. Ebből a , , ,  és a ,  felhasználásával állítjuk elő a formulákat. 
Példák :
Termek: xy, xyz, xx.
Formulák:
xy		atomi
Néhány fontosabb nem alapreláció formalizálása:
x=y =def xy  yx
xy =def  x=y
xy =def xy   xy
Műveletek definiálása logikai leképezésekkel -formalizálása.
x = yz =def xy   xz  v(vy   vz  vx)

A háromdimemziós Euklideszi geometria logikai nyelve (geom nyelv).
Univerzum: E a háromdimemziós Euklideszi tér pontjai, egyenesei, síkjai. Tehát itt három “fajtájú” univerzumelem létezik. 
{A, B,...}=UP a tér pontjait, 
{p, q, ...}= UE a tér egyeneseit és 
{a, b, ...} = US a tér síkjait jelölik.
Ennek megfelelően E= UP  UE  US .
Alapműveleteket nem definiálunk.
Alaprelációk; 2-változósak, és definíciójukban szerepel, hogy melyik fajta univerzumelemek kerülhetnek az argumentumokba.
-  A=B, argumentumok csak pontok lehetnek. UP  UP {i.h}
-  Az illeszkedés relációt, pont - egyenes illetve pont sík viszonylatában definiáljuk:
1) Bq, UP  UE {i.h}, pont illeszkedik egyenesre,
2) Ba, UP  US {i.h}, pont illeszkedik síkra.
Az ábécé logikán kívüli része:
A=B, Bq, Ba jelekből áll.
A többi reláció már ezeket a relációkat felhasználható formulákkal leírható.
Például:
Egyenes illeszkedik síkra pa.
pa. =def A(Ap Aa)

- a nyelv logikai része megegyezik a többi nyelvével.
- a nyelvek “logikán kívüli” része: univerzum megnevezett elemei az elemek fajtájának megjelölésével, a relációk és műveletek, amelyeket aritásuk és fajtájuk jellemezhet
	univerzum, 	alaprelációk		alapműveletek	argumentumszámok
	N0  		( =, .;		 s, *, +, 0)		(2, 2;  1;  2,  2, 0)
:	P(H) 		( ; 			x, , )		( 2;  1,  2,  2)
	UP ,UE ,US	( =, Bq, Ba;		    )		( 2, 2, 2;   -   )

Összefoglalva. 
 = <Tp, Kn, Fn, Pr >, amennyiben a konstansokra megkülönböztető jelölést vezetünk be,  
Tp ={1, 2, …} – indivíduum fajtákra utaló szimbólumok halmaza, 
Kn ={c1, c2, …} – konstans szimbólumok halmaza, 
Fn ={ f1, f2, …, fk} – függvény szimbólumok halmaza (véges, esetleg üres), 
Pr ={ P1, P2, …, Pn } – predikátum szimbólumok halmaza (véges, nem üres)
A típus megadása többfajtájú esetben:
m-változós függvény szimbólum esetén a(z indivíduum) fajták egy m+1 elemű vektora. (i,1,  i,2, …,  i,m+1)
m-változós predikátum szimbólum esetén a(z indivíduum) fajták egy m elemű vektora. (i,1,  i ,2, …,  i ,m)
A geom nyelv megadása ebben a stílusban.
 = <Tp, Kn, Fn, Pr >,
Geom nyelv = <{pont, egyenes, sík}, {}, {}, {A=B, Bq, Ba,}>,
Típus/ szignatúra:			 [ ; (pont, pont), (pont, egyenes), (pont, sík)] 

 = <Tp, Fn, Pr >, amennyiben a konstansokat mint 0-argumentumos függvényeket tekintjük.
A matematikai struktúrák nagyrésze egyfajtájú (lásd Ar, Részh.). Ez azt jelenti, hogy a Tp, Fn és Pr halmazban egyfajtájú elemek szerepelnek. Ez jelölési egyszerűsítést tesz lehetővé de a logika tárgyalását nem befolyásolja, hiszen a nyelv matematika specifikus (nem logikai) része az egyszerű állításmegfogalmazás eszköze, így a többfajtájú esetben árnyaltabb a matematika specifikus rész. A logika tárgyalásához a jelölési egyszerűsítés előnyei miatt az egyfajtájú nyelvet választjuk mint az egyszerű állításmegfogalmazás szimbolikus eszközét. Ez a nyelv: L= < Fn, Pr >, azzal a megjegyzéssel, hogy L-hez tartozik az indivídiuumváltozók halmaza, amelyeknek a típusa megegyezik az univerzum elemeinek típusával.

Egy másik jelölésrendszerben a matematikai struktúra a következő:
   univerzum     alaprelációk	alapműveletek (jelei)
S= U               (R1, R2,..., Rn;     o1, o2,..., ok)
         		   ( r1, r2,  ..., rn;       s1, s2, ..., sk) a struktúra típusa
mint a relációk és a műveletek argumentumszámai.

Példák struktúrákra.
1. Boole  algebra
     a)  univerzum:P(H), relációk: =, , műveletek: , ,   .
	P(H)( =, ,; , ,  )
	         (2,  2 ;  2,  2,  1)  típus
     b) univerzum: {i,h}, reláció , műveletek , ,  .
	{i,h}( ; , ,  )
	         ( 2 ; 1,  2,  2 )  típus
2. Elemi aritmetika
            univerzum: N0, relációk: =,  , műveletek: 0, 1, +, *
	N0(=,  ; 0, 1, +, *)
	    (2, 2; 0, 0, 2, 2)

A formalizált vagy egyfajtájú L mat. log. nyelv ábécéje és a matematikai struktúra közötti kapcsolat. Elsőrendű és másodrendű nyelvi elemek.

struktúra
	mat. log. nyelv
ábécé	jelölés	minőség		rend		
az U univerzum elemei	individuum változók	x, y, xk, ...,
	logikai				
alapműveletek.
arg. számok(0,1...)  	függvény szimbólumok
arg. számok(0,1...) 	f, g, fr,	
logikán				
alaprelációk
arg. szám.(1,2...)	predikátum szimbólumok
arg. szám.(1,2...) 	P, Q, Ps, ...	kívüli	0.			
	az egyenlőség
predikátum	=			1.		
	logikai 
összekötőjelek	, , , , 	logikai			2.	
	kvantorok	, 					
	predikátum (halmaz) változók	Xn, Yn, ...					

Az így tekintett L formalizált nyelv esetén a szimbólumok és a struktúrák alkotóelemeinek megfeleltetése szemléletes.  
Az L nyelv egy megadási módja:
           predikátum   függvény    szimbólumok
      L (P1, P2,..., Pn;  f1, f2,..., fk)
         ( r1, r2,  ..., rn;  s1, s2, ..., sk)  Az L nyelv típusa.
Egy S struktúra nyelvét (ha van ilyen) az alaprelációk és az alapműveletek jeleinek (azonosítóinak) felsorolásával adjuk meg. Ebben az esetben a jelek megnevezik az alaprelációkat és az alapműveleteket
relációk	 műveletek jelei
S= U(R1, R2,..., Rn; o1, o2,..., ok)
         ( r1, r2,  ..., rn;  s1, s2, ..., sk) a struktúra típusa

Az elsőrendű logika szintaxisa:

Szintaxis - jól formált kifejezések előállításának szabályai

Term  - matematikai leképezés szimbolizálása

1. Egy indivíduum változó x jól formált term (jft)
2. Ha f egy n-változós függvényszimbólum és t1, t2, ..., tn  jft-ek, akkor 
f(t1, t2, ..., tn)  jft.
3. Minden jft az 1., 2 véges sokszori alkalmazásával áll elő.

Formula  - logikai leképezés szimbolizálása
1. . Ha P egy n változós predikátumszimbólum és t1, t2, ..., tn  jft-ek, akkor 
P(t1, t2, ..., tn) jól formált formula (jff). (atomi formula, primformula)
2. Ha A, B  jff-ák, akkor (A)  jff.,	(zárójeles)
A,  (negációs formula)  jff.		(negációs formula)
(AB) (konjunkciós formula)  jff., 	(konjunkciós formula)
(AB) diszjunkciós formula)  jff., 	(diszjunkciós formula)
(AB) (implikációs formula)  jff., 	(implikációs formula)
[(AB) (ekvivalencia formula)  jff.	(ekvivalencia formula), ha  eleme a nyelvnek.]
----------------------------------------------------------------------------0-rendű formulák 
3. xA, xA   jff-ák. (kvantált formula, primformula)
---------------------------------------------------------------------------1. rendű formulák
4. Minden jff az 1., 2., és 3. szabály véges sokszori alkalmazásával áll elő.

Megjegyzés: A szintaxis szabályai azt sugallják, hogy az argumentum formulák zárójelbe tett formulák. A szükségtelen zárójeleket azonban elhagyhatjuk a szabályok szerint előállított formulákból (52,53 old.)
A továbbiakban feltételezzük, hogy a formula nem teljesen zárójelezett.
Részformula, közvetlen részformula, hatáskör:
Egy formula legszűkebb részformulája egy logikai szavára nézve, az illető logikai szótól jobbra lévő (1 változós esetben) / jobbra és balra lévő . (2 változós esetben) részformula, amely az első alacsonyabb prioritású logikai szónál zárul. Ez más néven a logikai szó hatásköre.

A teljes prioritási sorrend (csökkenő): , , , , , . (logikai szavak)
A kvantorok ,   prioritása a legerősebb. A ,  hatásköre a legszűkebb részformula jobbra. Azaz xA közvetlen részformulája. Más szóval a x, y hatásköre tőle jobbra a legközelebbi kétváltozós logikai műveletig tart. A kvantor a mellete álló változóra vonatkozik.

A  hatásköre a A közvetlen részformulája, hasonlóan a kvantorokéhoz.

A , ,  hatásköre az (AB) közvetlen részformulái.  
Egy adott logikai szóhoz tartozó legszűkebb részformula éppen a hozzátartozó közvetlen részformula(k).
Egy formula zárójeles részformulája egyetlen egység a formula szerkezetének vizsgálata esetén. Az , ,  műveletek 2 változósak. A “, ,  lánc” formulák nem jff.-ák ezért zárójelezéssel biztosítani kell ezt. Ha megengedünk “lánc” formulákat, akkor meg kell állapodni egy zárójelezési módban. Az implikációs lánc formula esetén jobbról balra zárójelezés kötelező: 

B1(B2(B3(B4B5)))

A formula minősítése arra a logikai műveletre utal amelyet alkalmazva a közvetlen részformulákra a teljes formula előáll. (Amelynek a hatásköre a teljes formula.) 
A következő formula implikációs formula.
A C B  C A C.

Közvetlen részformulák

Aláhúzva a legszűkebb részformulák az első -re nézve: 
A C B  C A C.

A kvantor leköti azt a hatáskörébe eső változót, amelyre a kvantor vonatkozik.
Egy formula zárt, ha minden változója kötött.

Egy formula nyitott, ha legalább egy indivíduum változónak van legalább egy szabad előfordulása.

Egy formula kvantormentes, ha nem tartalmaz kvantort.

Def. Alapkifejezés a változót nem tartalmazó L kifejezés (alapterm ahol a változókba konstansszimbólumot helyettesítettünk, alapformula).
Alapatom az argumentumok konstanszimbólumok, vagy interpretációban univerzumelem nevek.!!!

1. rendű nyelven állítások.
Alapformula: 1. rendű nyelven írt 0. rendű állítást szimbolizál
Zárt formula 1. rendű állítást szimbolizál
Nem zárt formula (nyitott) logikai leképezést szimbolizál
Az elsőrendű logika szemantikája az L egy I interpretációja (máshol  L-értékelés)
Informális definíció
1. Választunk egy a nyelvvel azonos típusú struktúrát.Ez az I. Ezzel interpretáljuk a nyelvet (a fv. szimbólumok a megfelelő alapműveleteket, a pred. szimbólumok a megfelelő alaprelációkat jelentik majd).
2. A kifejezés szabad változóinak egy kiértékelését az interpretáló struktúra univerzumán jelölje . és A kifejezés helyettesítési értékét minden  kiértékelésre kiszámítjuk.

Formális definíció: K egy kifejezés, KI jelöli a kifejezés értékét az I interpretáció és  változókiértékelés esetén. ( L-értékelését).
Termek
1. x I   U (a struktúra univerzuma)
2. f(t1, t2, …, tn)  I= f I  (t1 I, t2 I, …, tn I)

Formulák
1. P(t1, t2, …, tn)  I = i, ha (t1 I, t2 I, …, tn I)PI igaz halmazának
2. A I = i, ha A I = h
3. AB I = i, ha A I = i és B I = i, 
   AB I = i, ha A I = i, vagy B I = i, 
   AB I = i, ha A I = h vagy B I = i
4. xA I = i, ha A I (x/a)=i, minden aU-ra
    xA I = i, ha A I (x/a)=i, legalább egy aU-ra

Egy formula komponensformulái azok a részformulák, amelyeket logikai műveletekkel összekapcsolva megkapjuk a formulát. Egy formula prímkomponensei azok a komponensformulák, amelyeknek már nincs komponensük. Itéletlogikai formula esetén prímkomponensek az ítéletváltozók. Elsőrendű formula esetén prímkonponens lehet az atomi formula és a kvantált formula.
Egy formula helyettesítési értékeit prímkomponenseinek igazságértékei alapján számítjuk ki. A prímformula helyettesítési értékeit az interpretáló struktúra relációinak és műveleteinek értéktáblái és az indivíduum változók értékei alapján kapjuk meg.

Egy 1. rendű formula értéktáblájában az első sorba a formula nem kötött változói, a primkomponensek és a formula kerülnek. Mivel a fomula (és így a primformulák is) sok esetben nem zárt, ezért az indivíduum változók kiértékelése után válnak állításokká. 
Az indivíduum változók alá az interpretáló stuktúra univerzuma alapján előálló lehetséges  kiértékelései , a  primformulák alá a megfelelő helyettesítési értékek kerülnek. A formula alatt a prímformulák értékeinek megfelelő helyettesítési értékek találhatók.

Példa.
Legyen az interpretáló struktura: U={d, e, f}, PI (x)=i, ha x=e, QI (x,y)=i, ha x,y az (d, d),(f, d), (e, d) (e, e) (e, f) értékpárok valamelyike.
A formula	 xP(x)yQ(w,y)P(v) zQ(w,z)
A primformulák:  xP(x), y(Q(w,y), P(v), zQ(w,z)). A szabad indivíduum 
változók   v, w.

Az értéktábla
v	w	P(v)	y(Q(w,y)	zQ(w,z)	xP(x)	xP(x)yQ(w,y)P(v)zQ(w,z)	
d	d	h	y(Q(d,y)=i	zQ(d,z)=h	h	i	
d	e	h	y(Q(e,y)=i	zQ(e,z)=i	h	i	
d	f	h	y(Q(f,y)=i	zQ(f,z)=h	h	i	
e	d	i	y(Q(d,y)=i	zQ(d,z)=h	h	i	
e	e	i	y(Q(e,y)=i	zQ(e,z)=i	h	i	
e	f	i	y(Q(f,y)=i	zQ(f,z)=h	h	i	
f	d	h	y(Q(d,y)=i	zQ(d,z)=h	h	i	
f	e	h	y(Q(e,y)=i	zQ(e,z)=i	h	i	
f	f	h	y(Q(f,y)=i	zQ(f,z)=h	h	i	
Vegyük észre, hogy a prímkomponesek ebben az interpretációban rendre csak a
(h,i,h,h), (h,i,i,h), (i, i,h,h), (i,i,h,h) értékeket vették fel a lehetséges 16 közül.
Definíciók
Egy   I interpretáció  kielégít egy A 1. rendű formulát   (I=A), ha AI értéke i, legalább egy  kiértékelés mellett. Ha az A formula mondat és I =A, akkor azt mondjuk, hogy az interpretáló S struktúra elégíti ki A-t. Ezt S=A-val jelölünk. Azt is mondjuk, hogy S  modellje  A-nak.
Ha L egy I interpretációjára az  F={F1, F2, ..., Fn} formulahalmazban  (Fi zárt) FiI értéke i,  minden 1in-re, akkor I kielégíti F-et. Jelölés: I= F. Azt mondjuk, hogy 
F  kielégíthető ha L–nek van legalább egy I interpretációja, hogy I =F.
Azt mondjuk, hogy egy G formula  logikailag igaz, ha G  igaz  minden lehetséges I interpretációban. (Ez azt jelenti, hogy G  igaz  minden lehetséges interpretáló struktúrában.) Jelölés: = G. 
Láttuk, hogy egy formula prímformulái adott  I-ra 0.- vagy 1. rendű állítások. Mivel a logikai műveletek az állításoknak csak az igazságértékét veszik figyelembe nincs jelentősége annak, hogy megkülönböztessük a 0.- és az 1. rendű állításokat. 
Az a logikai nyelv (a továbbiakban ítéletlogika nyelve vagy 0. rendű logikai nyelv ), amely ezt képes leírni a következő:
ábécé: állítás –ítélet – vagy logikai változók. (X, Z, …) 0-változós predikátum betűk 
	Logikai összekötőjelek: , , , . (egyben prioritási sorrend)
Szintaxis.
1. X ítélet változó jff.
2. Ha A, B  jff-ák, akkor (A)  jff.,	(zárójeles)
A,    jff.	(negációs formula)		
(AB)   jff., 	(konjunkciós formula)	
(AB)   jff., 	(diszjunkciós formula)	
(AB)   jff., 	(implikációs formula)	
3. Minden jff. Az 1, 2 véges sokszori alkalmazásával áll elő.

Szemantika: Az ítéletlogika nyelvének interpretációja egy I :Vv {i, h} függvény 
(az ítéletváltozók kiértékelése = igazságkiértékelés).
Egy n-változós Q formula változói igaz vagy a hamis értéket vehetnek fel, ezek minden értékkombinációjához a formula helyettesítési értéke hozzárendeli az igaz vagy a hamis értéket (igazságtábla). Ez azt jelenti, hogy a Q n-változós formula egy 
{i.h}n {i,h} leképezést ír le.
Egy formula Boole-értékelése (kiértékelése) egy interpretációban BI (A) (szerkezeti rekurzió).
1. ha A primformula: BI (A) legyen I (A).
2. a BI (A) legyen  BI (A).
3. a BI (AB) legyen BI (A)  BI (B)
4. a BI (AB) legyen BI (A)  BI (B)
5. a BI (AB) legyen BI (A)  BI (B)
Amit a formula igazságtáblájával megadhatunk. A fejlécben az ítéletváltozók (prímformulák) és a formula. A sorokban a prímformulák (ítéletváltozók) igazságértékei. 
Az igazságtábla soraiban lévő értékkombinációk/igazságkiértékelések az ítéletlogika nyelvének I interpretációi. I: Vv{i,h}.
Az X, Y, Z változósorrend esetén, amit bázisnak is nevezünk ezt felsorolással megadhatjuk. A formula igaz halmaza / hamis halmaza.

Példa
	X	Y	Z	XYZX	
az	i	i	i	i	
ös	i	i	h	h	
sz	i	h	i	h	
es	i	h	h	h	
in	h	i	i	i	
ter	h	i	h	i	
pre	h	h	i	i	
táció	h	h	h	i	
 
Az összes interpretáció megadható, adott bázis esetén szemantikus fával. 
Definíció. Egy n-változós szemantikus fa egy n-szintű bináris fa, ahol a szintek a bázisbeli változóknak vannak megfeleltetve. Egy X változó szintjén a csúcsokból kiinduló élpárokhoz X, X. cimkéket rendelünk. X jelentése X igaz, X jelentése X hamis. Igy egy n- szintű szemantikus fa ágain az összes (2n ) lehetséges igazságkiértékelés (I interpretáció) megjelenik.

Szemantikus fa az X, Y, Z logikai változókra, mint bázisra.

				X			X
				
			Y	       Y			Y	       Y
					
		Z	  Z 	Z	  Z 	Z	  Z 	Z	  Z
						
		i i i	i i h	i h i	i h h	h i i	h i h	h h i	h h h

Legyen A egy tetszőleges n-változós ítéletlogikai formula. Az általa leírt {i.h}n {i,h} leképezés megadása igazságtáblával a gyakorlati alkalmazásokban kivihetetlen. 
Az ítéletlogika szemantikája a felhasználásorientált tárgyalásban Az igazságértékelés. Ez egy rekurzív módszer arra, hogy egy formulához,az igazságtábla felírása nélkül, hozzárendeljük annak jelentését oly módon, hogy megadjuk minden formulafajtára a Ai és a Ah feltételt amelyeknek pontosan azok az interpretációk tesznek eleget amelyekben  I (A) igaz, illetve hamis. 
A -igazságértékelés szabályai:
1. ha A primformula (ítéletváltozó): akkor a Ai feltételt pontosan azok az interpretációk teljesítik amelyekben  I (A)=i, a Ah feltételt pedig azok amelyekben I (A)=h.
2. a  A i  feltételek pontosan akkor teljesülnek, ha teljesülnek a  Ah feltételek.
3. a  (AB) i  feltételek pontosan akkor teljesülnek, ha teljesülnek a Ai és a  Bi feltételek.
4. a  (AB) i  feltételek pontosan akkor teljesülnek, ha teljesülnek a  Ai vagy a Bi feltételek.
5. a  (AB) i  feltételek pontosan akkor teljesülnek, ha teljesülnek a Ah vagy a  Ai feltételek.
A  (A) h  a  (AB) h , a  (AB) h , és a  (AB) h  feltételek értelemszerűen adódnak.

A -igazságértékelés a formulatípusokhoz adja meg azokat a feltételeket a formula argumentumaira, amelyeket teljesítő interpretációkban a formula értéke igaz illetve hamis lesz.  

A kapott feltételek teljesülésének feltételeit megadva és folytatva az eljárást az eljárás befejeztével az ítéletváltozókra kapott megkapjuk az összes megfelelő interpretációt. (igaz halmaz, hamis halmaz)
Példa. 

		 (XYZX) i, ha				implikációs formula

	Xh		vagy	(YZX) i, ha		diszjunkciós formula
1. értékadás/igazságkiértékelés
konjunkciós formula     (YZ) i,   vagy	  (X) i,  negációs formula
						
2. értékadás	   Yi és Zi 		Xh    3. értékadás

	1. ág			2. ág			3. ág
	X Y Z			X Y Z			X Y Z
	h ~  ~			~  i   i			h ~  ~	

Az igaz halmaz
X	Y	Z	
i	i	i	
h	i	i	
h	i	h	
h	h	i	
h	h	h	
A formula helyettesítési értékének kiszámítása az ítéletváltozók egy adott I igazságkiértékelése mellett. Lusta és mohó stratégia az A helyettesítési értékének kiszámítására. Például az I= X=h,Y=i,Z=i interpretációra az 1. ágon kapott feltételek miatt már az első lépésben kiderül, hogy a formula helyettesítési értéke i.

A hamis halmazt a formula hamissá válás feltételeinek megkeresésével kapjuk.
		 (XYZX) h, ha			 implikációs formula

1. értékadás		Xi	és
		(YZX) h, ha		diszjunkciós formula

			(X) h és
			 (YZ)=h, ha

2. értékadás		Xi és

3. értékadás	     Y h    vagy      Z h

		bal ág		jobb. ág	
		X Y Z		X Y Z		
		 i  h  ~		 i  ~  h		

A hamis halmaz
X	Y	Z	
i	i	h	
i	h	i	
i	h	h	

Definíciók. 
-Kielégíthetőség: Egy I-interpretáció (igazságkiértékelés) kielégít egy formulát, formulahalmazt, ha a formula vagy a formulahalmaz minden eleme igaz I-ben. Ha  van ilyen I-interpretáció, akkor a formula vagy formulahalmaz kielégíthető.
- Kielégíthetetlen egy formula/ formulahalmaz, ha egyetlen I-igazságkiértékelés sem elégít ki.
- Ha egy A formulát minden I-igazságkiértékelés kielégít - tautológia vagy logikai törvény jelőlése =0A.

Azt mondjuk, hogy egy G elsőrendű formula  tautológia(ként viselkedik), ha G  értéke igaz a prímkomponenseinek egymástól függetlenül adott minden igazságértékkombinációra.

A következményfogalom az itéletlogikában és az 1 rendű logikában. Tautológiák és logikailag igaz formulák szerepe.

Tautológikus vagy szemantikus következmény. Azt mondjuk, hogy a G formula  tautológikus következménye az F formulahalmaznak, ha minden olyan I igazságkiértékelésre, amelyre I =0 F akkor I =0 G. Más szóval F=0 G ha az F, G közös igazságtáblája minden olyan sorában, ahol az F elemeinek helyettesítési értéke i(gaz), a G helyettesítési értéke is i(gaz)
Jelölés: F=0 G vagy {F1, F2, ..., Fn}=0 G.
Logikai vagy szemantikus következmény. Azt mondjuk, hogy a G formula  logikai következménye az F formulahalmaznak, ha valahányszor egy  I interpretációra I = F akkor  I = G. Más szóval F= G ha bármely interpretáló struktúrában az F, G közös értéktáblájának minden olyan sorában, ahol az F elemeinek helyettesítési értéke  i(gaz), a G helyettesítési értéke is i(gaz). Jelölés: F= G vagy {F1, F2, ..., Fn}= G.
A következményfogalom alapján, annak eldöntése, hogy F= G megoldható lenne, ha el tudnánk dönteni az  interpretáló struktúrákban az F1, F2, ..., Fn és G-re kapott közös értéktáblák alapján a következőt: Minden interpretáló struktúrában, ahol a közös értéktáblában azokban a sorokban, ahol F1, F2, ..., Fn igaz,  G szintén igaz. – végrehajtható ?? 
Annak eldöntése, hogy F=0 G “csak” annak ellenőrzését jelentené, hogy a közös igazságtábla azon a soraiban, ahol F1, F2, ..., Fn igaz,  G szintén igaz-e. 
2n sor – végrehajtható ?? 

Ha a közös igazságtáblában G kizárólag azokban sorokban (interpretációkban) igaz ahol  F1, F2, ..., Fn igazak, akkor G a legszűkebb következménye F-nek. 

Megjegyzés: 1. rendben ennek minden interpretációban teljesülnie kellene ahhoz, hogy G legszűkebb következménye legyen F-nek. Később látjuk, hogy ez bizonyos esetekben ekvivalens azzal, hogy bizonyos univerzum felett ez minden interpretációban teljesül.
A következő tételek bizonyítása nem különbözik 0. és 1. rendben :

Dedukciós tétel: {F1, F2, ..., Fn}=G {F1, F2, ..., Fn-1}=FnG 

Eldöntésprobléma tétele: {F1, F2, ..., Fn}=G 
= F1(F2(...( Fn-1(FnG))...)). [Vagyis F1(F2(...( Fn-1(FnG))...))  logikailag igaz – érvényes (0 rendben tautológia) ].

Eldöntésprobléma átfogalmazásának tétele: 
{F1, F2, ..., Fn}=G {F1, F2, ..., Fn,G} kielégíthetetlen. Illetve 
{F1, F2, ..., Fn}=G {F1F2 ... FnG} kielégíthetetlen.

Előrekövetkeztetés (szemantikai tartalma): ismert az F feltételhalmaz és keressük F lehetséges következményeit.
(Egy megoldás) Megkeressük F legszűkebb következményét V-t. Következmény minden olyan G formula, amelyre VG tautológia (1. rendben logikailag igaz) vagy V igazhalmaza része G igazhalmazának.

Visszakövetkeztetés: Az F feltételhalmaz és a B következményformula ismeretében eldöntjük, hogy B valóban következménye-e F-nek. Mivel ha F=B, akkor {F.B} kielégíthetetlen, B akkor következménye F-nek, ha valahányszor B hamis az F kielégíthetetlen. 
Kielégíthetők-e a következő formulák?
a) xy(P(x)P(y))
b) xyz(P1(x)(P2(y)P3(z)))
c) yx(P(x)P(y))

Gyakorolni példákat  az előre és a visszakövetkeztetésre.
Megoldani előre és a visszakövetkeztetéssel F=0 D, ahol F={B,CBR} és D= CR,
Megkeresni előrekövetkeztetéssel a {FK,KA,FR,R(HA),A}. formulahalmaz 
a) legszűkebb következményét, 
b) egyetlen literálból álló következményeit.

Megkeresni visszakövetkeztetéssel, hogy a {FK,KA,FR,R(HA),A}. formulahalmaznak következménye-e a K, F, R, A ?
.  Igazolja, hogy az alábbi formulák azonosan igazak
	(PQ)(QP)  -     igazságértékeléssel 
	(PQ)(QP)   - igazságtáblával

Ezek a problémák szemantikailag világosak, de megoldásuk a teljes kipróbálást tételezi fel. Algoritmusokra van szükség a megoldáshoz.

Formulák logikailag ekvivalens átalakításainak elméleti háttere. 
Ítéletlogika.
A hálóra mint algebrai struktúrára két (ekvivalens) definíció ismert.
	a)  U (univerzum/értelmezési tartomány), R rendezési reláció  U(R;)
	b)  U (univerzum/értelmezési tartomány), két kétváltozós művelet. 
U(; , ).

R ésa két hálóművelet ,  kölcsönösen származtathatók egymásból.

	R-ből  ,  mint min(x,y), max(x,y)
	, -alapján R, R definíciója 
ha (x y)=x, akkor xRy vagy R(x,y), itt a  művelet a min(x,y),
ha (x y)=x, akkor xRy vagy R(x,y), itt a  művelet a min(x,y),

1. x y)=yx   2. (x y)=yx	kommutativitás
3. (x y) z= x(yz)  4. (x y) z=x(yz)	asszociativitás
5. x (xy)= x-6. x (xy)= x		elnyelés 
hálóaxiómák
Disztributív háló – 
7. x (yz)= (x y) (x z) 8. x  (yz)= (xy)( xz) 
disztributivitási axiómák is.

Az R, R rendezések közül a háló univerzumán csak az egyiket használjuk. 

Hálódiagram fogalma. 

Ha van minimális O és maximális I elem az univerzumban például az R rendezésre, akkor egy q univerzumelem komplementuma az a v univerzumelem, amelyre q  v=O és q  v=I.. Ha minden univerzumelemnek van legalább egy komplementuma akkor komplementumos hálóról beszélünk. Ha minden univerzumelemnek pontosan egy komplementuma akkor egyértelműen komplementumos hálóról beszélünk. Ha a háló komplementumos és disztributív is, akkor bizonyítható, hogy egyértelműen koplementumos. Ekkor definiálható egy k(x) egyargumentumos művelet mint komplementumképző műveletet, amelyre fennállnak a 
9. x  k(x)=O, 10. x  k(x)=I axiómák.
A komplementumos disztributív hálót Boole algebrának nevezik.
Példák:
Egy H halmaz P(H) hatványhalmaza a rajta értelmezett halmazelméleti metszet, unió, komplementer műveletekre Boole algebra
Az {i, h} halmaz a rajta értelmezett konjunkció, diszjunkció és negáció műveletekre Boole algebra. (Az ítéletlogika Boole algebra)
Következmények:
Logikai műveletekre érvényes azonosságok.
Előkészítő definíciók: literál, azonos alapú literál, különböző literál, elemi konjunkció, -diszjunkció, teljes elemi konjunkció, -diszjunkció, konjunktív és diszjunktív normálforma (KNF, DNF), kitüntetett konjunktív és diszjunktív normálforma (KKNF, KDNF).
DeMorgan szabályok:1. ¬(XY)= XY, 2. (XY)= X¬Y
Bebizonyíthatók az axiómák alapján.

Egyszeűsítési szabályok: 1. (Xd)(Xd)= d, 2. . (Xk) (Xk)=k, ahol d elemi diszjunkció és k elemi konjunkció.

Művelethalmaz funkcionális teljessége.
n-változós formula {i,h}n {i,h} leképezést ír le.
Az a logikai művelethalmaz, amelynek elemeiből és n db változóból tetszőleges {i,h}n {i,h} leképezést leíró formula előállítható, funkcionálisan teljes művelethalmaz.
Algoritmusok egy adott leképezést leíró KKNF és KDNF konstrukciójára.
Az egyszerűsítési szabályokkal 
KKNF és KDNF, valamint KNF és DNF egyszerűsítése. 
Tetszőleges formulák átírása DNF-be és KNF-be.

Definíció. Egy elsőrendű C formula általánosítása az a zárt formula, amely az eredeti formula szabad változóinak univerzális kvantálásával áll elő.
Helyettesítés.
A.
 x egy h term változója, t egy jft. h(x/t) az a term, amelyet t-nek x minden előfordulásába való behelyettesítével kaptunk.
 x az A formula szabad változója, t egy jft.. 
A(x/t) az a formula amelyet t-nek x minden szabad előfordulásába való behelyettesítével kaptunk.
B.
[xi] az L nyelv változóinak, [ti] L-termek egy megszámlálhatóan végtelen sorozata. Az  = [xi]/ [ti] helyettesítés az összes xi/ti helyettesítés szimultán elvégzését jelenti.
Szekvenciális helyettesítés.
Helyettesítések kompozíciója.  és  helyettesítések szekvenciális alkalmazásával kapott szimultán helyettesítés
Probléma a behelyettesített formula -L értékelése eredményezze ugyanazt, mint a 			       formula -L értékelése után kapott formula behelyettesítettje.
Más szóval ugyanazt a leképezést írják le a formulák.
Formálisan: [A(x/t)]   A (x/t)
Ha t eleget tesz ennek a feltételnek, akkor a t termet szabad az x-be helyettesíteni.
- a t term változói nem kerülhetnek kvantor hatáskörébe.

Például y(x=y) esetében a leírt leképezés az   x függvénye
x	y(x=y) - 	
u1	y(u1=y) - h, ha U legalább 2 elemű	
u2	y(u2=y)           “	
u3	...	

Legyen a helyettesítés x/y, akkor a y(x=y) formula 

1. előbb helyettesítünk - y(y=y)
Interpretálunk: (y=y)= i, bármely interpretációban,
 tehát a (y(x=y)( x/y) ) = i bármely interpretációban

2. Előbb interpretálunk és utána helyettesítjük az interpretált termet:
(y(x=y) )( x/y), vagyis a formula y(y=y) lesz, ami hamis.

Elsőrendű logika formuláinak logikailag ekvivalens átalakításai.
Az első a  prenex forma. Jelöle Q bármely kvantort. A Qx1, Qx2,  ..., QxnB formula egy prenex formula. 
Qx1, Qx2,  ..., Qxn a prefixum és B a formula törzse, matrixa. B  kvantormentes formula.
Minden 1. rendű formula átírható prenex formába.
Átírási szabályok

xA=xA	xA=xA       általános  DeMorgan szabályok 

A kvantorkiemelési szabályok
1. xA[x]B=x(A[x]B)
    “        “=      “       “   
2. xA[x]B= x(A[x]B)  
    “       “ =      “      “   
3. xA[x]xB[x]= x(A[x] B[x]) , de   -re nem
4. xA[x] xB[x] = x(A[x] B[x]), de   -re nem.
5. Q1xA[x] Q2xB[x]=Q1xQ2z(A[x]B[x/z])
6. Q1xA[x ] Q2xB[x]= Q1xQ2z(A[x ] B[x/z]).

A prenex formába való átírás algoritmusa.
1. A logikai összekötőjelek átírása , , -ra.
2. A DeMorgan szabályok alkalmazása addig amíg a  hatásköre atomi formula nem lesz.
3. A kvantorkiemelési szabályok alkalmazása addig amíg  minden kvantor a formula elejére nem kerül (ami kvantormentes formula).

Példa.
x (yP(x,y)y (Q(y)P(x,a))) xy(P(x,y)R(x,y)
1. lépés
x (yP(x,y)y(Q(y)P(x,a))) xy(P(x,y)R(x,y))
2. lépés.
x(yP(x,y)y(Q(y)P(x,a)))xy(P(x,y)R(x,y))
x(yP(x,y) y(Q(y)P(x,a))) xy(P(x,y)R(x,y))
x(yP(x,y) y (Q(y)P(x,a))) xy(P(x,y) R(x,y))
x(yP(x,y) y (Q(y)P(x,a))) xy(P(x,y) R(x,y))

3. lépés. kvantorkiemelési szabályok
 x-re 
x(yP(x,y) y (Q(y)P(x,a))  y(P(x,y) R(x,y)))
 y-re először végrehajtjuk az y/y1 helyettesítést a y-al kezdődő első részformulában és az  y/y2  helyettesítést ay al kezdődő második részformulában
x(yP(x,y) y1 (Q(y1)P(x,a))  y2 (P(x,y2) R(x,y2)))
xy(P(x,y) y1 (Q(y1)P(x,a))  y2 (P(x,y2) R(x,y2)))
és végül
xyy1 y2 (P(x,y) (Q(y1)P(x,a))  (P(x,y2) R(x,y2)))
Megkaptuk a  prenex formulát.

Ha a prenex formula törzse KNF-ben vagy DNF-ben van, akkor a formula  prenex konjunktív / prenex diszjunktív formula.
A másik speciális (normal) formula egy 1. rendű formula Skolem formája.
A x1, x2,  ..., xnA  formulát , ahol a prefixumban csak univerzális kvantorok vannak Skolem formulának nevezzük.

Minden 1. rendű formula átírható Skolem formába.
Először átírjuk a formulát prenex formába. Azután bevezetjuk a Skolem függvényeket és elimináljuk az egzisztenciális kvantorokat.
Tekintsük az első egzisztenciális kvantort a prefixumban, legyen ez xj. Ha a formula igaz, akkor az x1, x2, ..., xj-1 változók minden értékkombinációjához létezik legalább egy értéke az xj változónak amelyre a formula értéke i. Ezt a tényt az  
 f(x1, x2, ..., xj-1 ) =xj   függvénnyel fejezzük ki. Ez a függvény rendeli az xj -hez a megfelelő értéket. Ezt a lépést végrehajtjuk  a soronkövetkező egzisztenciális kvantorra addig amíg, minden egzisztenciális kvantort nem elimináltunk.
Pl. xyP(x,y)	Skolem alak: xP(x,f(x))
Interpretációk
Minden emberhez van olyan nő, aki az anyja. Skolem fv. anyja(x).
Egy sokszög minden csúcsához van legalább egy hozzá legközelebbi csúcs. Skolem fv. legközelebbi(x).
Minden számhoz van nála eggyel nagyobb szám. Skolem fv.s(x), a rákövetkezési fv..
Eldönthető függvényosztály.

Döntési algoritmus, levezető eljárás egy olyan algoritmus, amely adott input adatokkal dolgozik, azokat a megfelelő szabályok szerint használja fel, a levezetési szabály szerint alakítja át és akkor áll meg amikor a kitűzött célt elérte.  A megállással egy kétesélyes döntés egyik kimenetét igazolja. Azonban, ha az algoritmus nem éri el a kitűzött célt az nem feltétlenül jelenti azt, hogy az algoritmus meghozta a másik kimenetre a döntést.

A logika szintaktikai alapokon való felépítése.
0. rendű logika - ítélet vagy állításlogika bizonyításelméleti felépítése (Hilbert rendszer).
 (Elmélet – egy L formalizált nyelv és egy F formulahalmaz)
(Elmélet - egy axiomatizált struktúra)

Szintaktikus következményfogalon, eldöntésprobléma, előre- és visszakövetkeztetés

Definíciók:
Az ítéletkalkulust leíró nyelvben itt a logikai összekötőjelekből csak a ,  párt használjuk.
Axiómák (axiómasémák) megadják a műveletek tulajdonságait.
1. ABA
2. (ABC) (AB) AC
3. (AB) (AB) A

Kapcsolat a szemantikával: 
Ezek az axiómák tautológiák / logikai törvények.
Tétel: Legyen G egy formula, G(X/S) az a formula, amit G-ből X változójának egy S formulával való behelyettesítésével kaptuk. Ha G tautológia, akkor G(X/S) is az.
Következmény: Az axiómákból behelyettesítéssel kapott formulák is logikai törvények - axiómának tekinthetők.
Tétel: {AB, A}=0B

-Bizonyításelméleti levezetés fogalma. G-nek F-ből való levezetése.
-Levezetési szabály  modus ponens  -  leválasztási szabály.
-Egy G formula az F={F1, F2, ..., Fn} formulahalmazból levezethető 
F={F1, F2, ..., Fn}0G

Tulajdonságok

- Egy G formula bármely F feltételhalmazból levezethető - G bizonyítható 0G.
- Egy F={F1, F2, ..., Fn} formulahalmaz ellentmondásos (inkonzisztens), ha F0G és F0 G
- Egyébként az F={F1, F2, ..., Fn} formulahalmaz nem ellentmondásos (konzisztens)

Példa levezetésre / bizonyításra: 0AA, {B, B}0A, (A tetszőleges) 

Tételek
Tétel: Két levezetés konkatenációja is levezetés. Ha F-ből levezethető G1 és S-ből levezethető G2, akkor a két levezetés konkatenációja az FS-ből való levezetés.

Tétel: Ha F- ből levezethető G1 és S- ből levezethető G2,  valamint, {G1, G2}- ből levezethető A, akkor az FS- ből levezethető A.

Tétel (Dedukciós): Az {F1, F2, ..., Fn}0G  akkor és   csak akkor, ha 
0F1(F2(...( Fn-1(FnG))...)). 
Ez az eldöntésprobléma a bizonyításelméletben.

Tétel: Ha  {F1, F2, ..., Fn}0G  akkor {F1, F2, ..., Fn}=0G. (Helyesség)

Tétel: Ha F- ből levezethető G, akkor az F  { G} ellentmondásos.

Tétel: Ha  {F1, F2, ..., Fn}ellentmondásos, akkor kielégíthetetlen.

(em)Tétel: Legyen A egy formula és F egy konzisztens formulahalmaz, ekkor
a) F A ellentmondásos, akkor és csak akkor, ha F0A.
b) F,A ellentmondásos, akkor és csak akkor, ha F0A. 
Bizonyítás:
a) Ha F, A ellentmondásos, akkor F, A0B és F, A0B. A dedukciós tétel miatt F0AB és F0AB. A két levezetés konkatenációját folytatva a 3. axióma (AB)(AB)A alakjával, majd a AB és a AB leválasztásával megkapjuk az A levezetését F-ből. 
Ha F0 A, akkor F A ellentmondásos, mivel F, A0A és 
F, A0A.

b) Ha F,A ellentmondásos, akkor mivel minden ami F,A-ból levezethető az F,A-ból is levezethető, tehát, ha F,A ellentmondásos, akkor F,A  is az. Használva a tétel a) részét A helyett A-ra F0A.  Ha F0A, akkor F,A ellentmondásos, mivel F ,A0A és F ,A0A. 

Tétel (Kalmár): Egy k-változós G formula igazságtáblájának minden sorában  X1’,X2’,...,Xk’0G’
Tétel: Ha X1’,X2’,...,Xk’0G’ és X1’,X2’,...,Xk’0G’ ,akkor X2’,...,Xk’0G’
Tétel: Ha G tautológia, akkor G bizonyítható. (Gyenge teljesség).

Tétel: Ha{F1, F2, ..., Fn}=0G, akkor  {F1, F2, ..., Fn}0G. (Teljesség) 
Biz: Gödel féle gondolatmenet
A) Ha {F1, F2, ..., Fn}=0G, akkor {F1, F2, ..., Fn} { G} kielégíthetetlen.     
B) Ha {F1, F2, ..., Fn} { G} ellentmondásos (inkonzisztens), akkor {F1, F2, ..., Fn}0G. 
Azt tudjuk, hogy az ellentmondásos formulahalmaz kielégíthetetlen. Ha meg tudjuk mutatni, hogy a kielégíthetetlenség mint szemantikus tulajdonság és az inkonzisztencia mint szintaktikus tulajdonság a formulahalmazok halmazát ugyanúgy osztja két diszjunkt részre, akkor a bizonyítás a következő lenne:
Ha{F1, F2, ..., Fn}=0G, akkor {F1, F2, ..., Fn} { G} kielégíthetetlen. Ha egy formulahalmaz kielégíthetetlen, akkor ellentmondásos (inkonzisztens) is.
Ha {F1, F2, ..., Fn} { G} ellentmondásos (inkonzisztens), akkor {F1, F2, ..., Fn}0G. 

Azt nem tudjuk közvetlenül belátni, hogy ha egy formulahalmaz kielégíthetetlen, akkor ellentmondásos (inkonzisztens) is. E helyett belátjuk azt, hogy ha egy formulahalmaz ellentmondásmentes (konzisztens), akkor kielégíthető.
(max.konz). Tétel. Az F formulahalmaz maximális konzisztens (bármely új formula hozzávétele estén a formulahalmaz már inkonzisztens), akkor és csak akkor ha teljesülnek az alábbi feltételek:
a) F konzisztens
b) Bármely A formulára vagy AF vagy AF. 
Bizonyítás. 
  Ha F maximális konzisztens, akkor az 
a) a feltétel miatt teljesül. 
A b) igazolására tegyük fel, hogy van olyan A, hogy sem A, sem  A nem eleme F-nek. Ekkor a maximalitási feltétel miatt F,A is és F, A is inkonzisztens. Ez a (em.) tétel miatt azt jelenti, hogy rendre F0A és F0A, ami ellentmond annak, hogy F konzisztens.  
 Ha a) és b) teljesül, akkor minden olyan G formulahalmaz inkonzisztens, amelynek F valódi része. Legyen G a A-val bővebb mint B. Ekkor, mivel AF, FG és AG, következésképen AG, tehát G inkonzisztens. 
Tétel.  Legyen F maximális konzisztens formulahalmaz, ekkor
a) AB F akkor és csak akkor, ha vagy AF vagy BF. 
Bizonyítás:
  Tegyük fel, hogy ABF, de AF vagy BF nem teljesül, tehát AF és BF. De ekkor F,A is és F,B is inkonzisztens, mivel F maximális. A maximalitási feltétel miatt kell hogy  AF és BF legyen, ugyanakkor tudjuk, hogy ABF. Ennek alapján AF miatt F0B és F0 B vagyis F inkonzisztens lenne ellentétben a feltétellel. 
Ha AF vagy BF, akkor a F,A vagy a F,B inkonzisztens. Ebből F,A,B inkonzisztens. Tegyük fel, hogy (AB)F, tehát (AB)F. Ekkor F inkonzisztens lenne, mert AF  miatt F0 AB, de BF is F0 AB. Ezért (AB)F és a maximalitás miatt ABF. 
Tétel. Ha egy F formulahalmaz kielégíthető, akkor konzisztens.
Biz. A helyesség miatt ha F0 A, akkor F=0A.  Ezért F0 A nem lehetséges, mert akkor F kielégíthetetlen lenne. Vagyis F konzisztens.
Tétel. Minden konzisztens G formulahalmazhoz van olyan Maximális konzisztens formulahalmaz F, hogy GF.
Bizonyítás: (Lindenbaum konstrukció)
Legyenek az ítéletlogikai formulák egyetlen 1, 2,… sorozatba rendezve.
G0=G,… Gi=Gi-1 i, ha ezzel Gi konzisztens marad, egyébként Gi=Gi-1.
Belátjuk, hogy az így kapott G0  G1  …Gi  … konzisztens formulahalmaz lánc elemeinek uniója  maximális konzisztens formulahalmaz. 

Lássuk be, hogy  konzisztens. Tegyük fel, hogy nem az. Ekkor -ból levezethető A és A is. Legyenek 1, 2, …, q a levezetésekben előforduló -beli formulák. Egyszerű megmutatni, hogy van olyan i, hogy {1, 2, …, q}Gi. De ez azt jelentené, hogy Gi inkonzisztens ellentétben a konstrukcióval, ami ellentmondás.

Lássuk be, hogy  maximális is. Tegyük fel, hogy  konzisztens és . Legyen s, de akkor Gs-1{s } is konzisztens és így Gs= Gs-1{s } is. Vagyis s , tehát .

Tétel: Egy M maximális konzisztens formulahalmaz kielégíthető
Bizonyítás. Legyen a  igazságkiértékelés a következő, ha XM, akkor X=i és h egyébként. Bonyolultság szerinti indukcióval belátható, hogy  kielégíti M-et.
Tétel. Ha G konzisztens, akkor kielégíthető, tehát van olyan  igazságkiértékelés ami kielégíti G-t. 

Biz. A G-t tartalmazó M maximális konzisztens formulahalmaz kielégíthető, így G mint M részhalmaza is kielégíthető.

Előrekövetkeztetés és visszakövetkeztetés a bizonyításelméletben.

Az elsőrendű bizonyításelmélet axiómarendszere.

1-3 a 0-adrendű axiómák.
Az univerzális kvantorra vonatkozó axiómák.
4.x(AB)xAxB.  A, B elsőrendű formulák és x indivíduumváltozó.
5. AxA. Az x nem szabad A-ban
6.xAA(x/t).  a  t  term helyettesítése megengedett x -e.
Az = predikátumra vonatkozó axiómák. ,t1
7. t = t  
8. t1 =tn+1 ... tn =t2nf( t1 ,t2,...,tn)=f(tn+1,tn+2,...,t2n)
9. t1 =tn+1 ... tn =t2nP( t1 ,t2,...,tn)P(tn+1,tn+2,...,t2n)
10. Az 1-9 axiómák általánosításai.

Az axiómák logikailag igazak.
A levezetési szabály a modus ponens.
Következményfogalom, eldöntésprobléma mint nulladrendben.
Helyesség / teljesség u.úgy kezelhető.
Megjegyzés. Az egyenlőségjeles nyelvek esetén a kielégíthetőség és érvényesség vizsgálatánál a kielégíthetőséget csak az = axiómáknak eleget tevő struktúrákban kell vizsgálni.
Az érvényességhez elegendő, ha  formula csak az = axiómáknak eleget tevő struktúrákban azonosan igaz
Ez az egyik legismertebb korlátozó feltétel. A korlátozó feltételek kezelése a logikában, az alkalmazások szempontjából fontos.

Összefoglaló megjegyzés. A bizonyításelméleti levezetésen alapuló eljárás egy szintaktikai alapú kalkulus, amivel megoldjuk a szemantikus eldöntésproblémát. 
A LOGIKA=NYELV + KALKULUS szlogen azt fejezi ki, hogy a logika akkor tekinthető felépítettnek, ha adott egy helyes és teljes szintaktikai alapú algoritmus, ami végül a szemantikus eldöntésproblémát oldja meg.
A logika bizonyításelméleti felépítését 0 rendben ítéletkalkulusnak, 1 rendben logikai függvénykalkulusnak ill. predikátumkalkulusnak nevezik.
A teljesség bizonyítása az illető kalkulus konzisztenciafogalmán alapul.