A tablók módszere – tabló kalkulus – szemantikus tabló – (tábla)
Előkészítő fogalmak
Az ítéletlogika abc-jében a továbbiakban a , , ,  logikai összekötőjelek szerepelnek.
Formula bonyolultsága d(A). (0 rend)
1. X ítéletváltozó: d(X)=0,
2. 	d(A)= d(A)+1,
	d(AB)=d(A)+d(B)+1
	d(AB)=d(A)+d(B)+1
	d(AB)=d(A)+d(B)+1.
Definíció:
Egy formula szerkezeti fája egy olyan bináris fa, amelyben
(i)   Minden levél ítéletváltozó.
(ii)  Minden elágazás nélüli csúcsban egy A alakú formula áll és a rákövetkező csúcsban A.
(iii) Minden elágazásban egy AbB alakú formula áll (b bármelyik bináris logikai művelet) és bal illetve jobb rákövetkezőként A illetve B jelenik meg. 

Példa: [pq(pq)](qp) szerkezeti fája:

 		[pq(pq)](qp)

pq(pq)			(qp)

pq		pq		q	p

p    q	       p	q			   p

	         p		   q

			      q

1. ábra

Definíció:
Legyen  egy igazságkiértékelés (Boole kiértékelés). Egy olyan S formulahalmazt, amely tartalmazza az összes olyan formulát, amelyek egy  igazságkiértékelésre igaz helyettesítési értéket adnak igaz halmaznak nevezzük.  és S kölcsönösen meghatározzák egymást.
Belátható, hogy S a következő tulajdonságokkal bír. 
S1.  {A, A} formulapár pontosan egyike eleme S-nek. Más szóval AS  AS
S2. AB S  AS és BS
S3. AB S  AS vagy BS
S4. AB S  AS vagy BS
Ha egy S formulahalmaz rendelkezik ezekkel a tulajdonságokkal, telített (saturated) vagy igaz halmaznak nevezzük.
A formulák szemantikus tulajdonságai megfogalmazhatók az igaz halmaz segítségével is.
C tautológia, ha C eleme minden igaz halmaznak.
C kielégíthtetlen, ha C egyetlen igaz halmaznak sem eleme.
C kielégíthető, ha van olyan igaz halmaz amelynek C eleme.
Definíció: 
Vezessük be a nyelvbe a "T", "F" szimbólumokat. Jelölt formulának nevezzük a TA, FA kifejezéseket, ahol A jelöletlen formula. (ezek olvasata "TA" - A igaz; "FA" - A hamis.
Egy interpretációban TA igaz, ha A igaz és hamis , ha A hamis és FA igaz, ha A hamis és hamis, ha A igaz.

0 rendű formulák igazságtáblája jelölt és jelöletlen formulaalakok.

		1	2	3	4	5	6	
A	B	AB	(AB)	(AB)	(AB)	AB	AB	
		TAB	FAB	FAB	FAB	TAB	TAB	
i	i	i	h	h	h	i	i	
i	h	h	h	i	i	i	h	
h	i	h	h	h	i	i	i	
h	h	h	i	h	i	h	i	

				2. ábra

Az 1., 2., 3. oszlopokban lévő formulák egyetlen igazságkiértékelésre veszik fel az igaz értéket, tehát az igazzá válásuk a két argumentumra együttesen megadott feltételtől függ. 
A 4., 5., 6. oszlopokban lévő formulák három igazságkiértékelésre veszik fel az igaz értéket, tehát az igazzá válásuk a két argumentumra egymástól függetlenül megadott feltételtől függ.
Például: 
Ha A is és B is igaz, akkor AB igaz. Vagyis {A,B}0 AB.
Ha A igaz vagy ha B igaz, akkor AB igaz. Vagyis {A}0 AB és {B}0 AB
Az 1., 2., 3. oszlopokban lévő formulákat -típusú, 
a 4., 5., 6. oszlopokban lévő formulákat -típusú formuláknak nevezzük.
Az -típusú formulák átalakíthatók 12 alakú fomulává, a -típusú formulák átalakíthatók 12 alakú fomulává. Az 1, 2 az  és a 1, 2 a  típusú formulák közvetlen részformulái. Ez nem mindig esik egybe a formulák eredeti alakjánban lévő közvetlen részformulákkal.
Például: 
(AB) közvetlen részformulája AB, de mint -típusú formulának már A, B a két közvetlen részformulája.

A 3. ábrán lévő táblázat mutatja az egyes formulákhoz tartozó 1, 2  és 1, 2  argumentumokat.

1	2			1	2		
A	B	AB		A	B	(AB)	
A	B	(AB)		A	B	AB	
A	B	(AB)		A	B	AB	
A	A	A					

3. ábra

Tehát, ha 1 is és 2 is igaz, akkor  igaz; {1, 2 }0 .
Ha 1 igaz vagy ha 2 igaz, akkor  igaz; {1}0  és {2}0 
Definíció (az  és  típusba sorolás bevezetésével):
Igaz halmaznak nevezzük az S formulahalmazt, ha a következő tulajdonságokkal bír. Tetszőleges A formulára és  valamint  típusú formulákra:
(0).  {A, A} formulapár pontosan egyike eleme S-nek. Más szóval AS  AS
(1). S  1 S és 2 S
(2). S  1S vagy 2 S
Lefele zártnak nevezünk egy S formulahalmazt, ha a következő tulajdonságokkal bír. Tetszőleges A formulára és  valamint  típusú formulákra:
(1). S  1 S és 2 S
(2). S  1S vagy 2 S
Felfele zártnak nevezünk egy S formulahalmazt, ha a következő tulajdonságokkal bír. Tetszőleges A formulára és  valamint  típusú formulákra:
(1). S  1 S és 2 S
(2). S  1S vagy 2 S
Meg lehet mutatni, hogy az olyan lefele zárt formulahalmaz, amely teljesíti a (0) feltételt is igaz halmaz. Az olyan felfele zárt formulahalmaz, amely teljesíti a (0) feltételt is szintén igaz halmaz.

Analitikus tabló.
Az analitikus tabló a szemantikus tabló egy változata, ahol a tablóépítési szabályokat az  és a  formulatípusokra adjuk meg. A tabló módszer olyan kalkulus, amelynek segítségével el lehet dönteni, hogy egy formula tautológia-e. (Mellékhatásként a bizonyításelmélet teljességét egyszerűbben lehet bizonyítani).

Igazságértékeljük hamisra a pqr  (pq)(pr) formulát a jelölt formulák technikájával.
Ez azt fedi, hogy mindig a megadott jelölt formula igazzá válási feltételeit adjuk meg. Tehát, ha a C formula hamissá válásának feltételeit akarjuk megkapni, akkor azt FC-vel jelöljük és ha a C igazzá válásának feltételeit akarjuk megkapni, akkor azt TC-vel jelöljük.
A formula igazságértékelésének folyamata ily módon a következő.

(1) F[pqr  (pq)(pr)]		
(2) T pqr				
(3) F(pq)(pr)			

(4) Tp					(5) Tqr	
						(6) Tq
						(7) Tr
(8) F(pq)	(9) F(pr)
(10) Fp	(12) Fp		(14) F(pq)	(15) F(pr)
(11) Fq	(13) Fr			(16) Fp	(18) Fp
      X		      X			(17) Fq	(19) Fr
					     X		     X

			4. ábra

A hamissá válás egyetlen feltétele sem teljesült, tehát a formula tautológia.
Vezessünk be tablóépítési (levezetési) szabályokat jelölt formulákra. A tablóépítési szabály a közvetlen tabló előállítás. Jelölt formulák esetén a közvetlen tabló előállítására minden formulára két szabály van. Az egyik ahol a formula T-vel és a másik, ahol F-el jelölt (5. ábra). Az X, Y formulákat literáloknak nevezzük (X, Y ítéletváltozó). Komplemens párnak nevezzük az X, X formulapárt.

	1.	TA		FA	
		FA		TA	
					
	2.	T(AB)		F(AB)	
		TA		FA  FB	
		TB			
					
	3.	T(AB)		F(AB)	
		TA TB		FA	
				FB	
					
	4.	T(AB)		F(AB)	
		FA  TB		TA	
				FB	
		5. ábra
Ezeket a szabályokat egy jelölt formulából kiindulva addig alkalmazzuk, amíg azok ítéletváltozó szintig lebontják a formulát minden ágon, hacsak az ágakon nem jelenik meg komplemens pár. Egy ágat már az első komplemens pár megjelenésénél lezárjuk. 
Jelöletlen formulákra a tablóépítési (levezetési) szabályok hasonlóak. Ott a formula közvetlen tablója a formula típusának (, ) megfelelően az igazzá válás feltételeit adó közvetlen részformulák megadását jelenti. (6. ábra) 
Az  és a  típusú formulákra megfogalmazott tablóépítési szabályok. 
		 típus		 típus	
	1.	A			
		A			
					
	2.	(AB)		 (AB)	
		A		A  B	
		B			
					
	3.	 (AB)		(AB)	
		A		A  B	
		B			
					
	4.	 (AB)		 (AB)	
		A		A  B	
		B			
					
		A típus 	szerint	közösen	
					
		1		12	
		2			
			6. ábra
Ezek a szabályok megadják azt a feltételhalmazt {1, 2}amelynek a kiinduló formula tautológikus következménye ( típus), illetve azt a két formulát (1, 2), amelyek közül bármelyiknek következménye a kiinduló formula ( típus).
Összefoglalva egy formula közvetlen tablója a formula egylépéses kifejtése a megadott szabályok szerint. Egy T tabló közvetlen kiterjesztése a T valamelyik még fel nem dolgozott formulájára a közvetlen tabló előállítása. A formula tablójának építése addig folytatható a kifejtések során kapott formulák feldolgozásával, amíg a fel nem dolgozott formulák mind literálok nem lesznek. Ezt a tablót ábrázolhatjuk fa alakban is, ahol a gyökérhez a vizsgált formulát a belső csúcsokhoz az épen feldolgozott formula alapján kapott {1, 2}formulahalmazt vagy j formulát (j=1,2) rendeljük. Egy csúcsból  típusú formula esetén egy,  típusú formula esetén két él indul ki és a levezetett formulára, formulahalmazra mutat. 
A formula tablójának egy ága teljes, ha a fel nem dolgozott formulák az ágon már literálok. A formula tablója teljes, ha minden ága teljes. A formula tablójának egy ága zárt, ha azon szerepel komplemens pár. A formula tablója zárt, ha minden ága zárt.
A tabló módszer a vizsgált formula teljes tablójának felépítésére alkalmas algoritmus. Az algoritmus megállási feltétele / eldöntésproblémája a tabló lezárása. Azt mondjuk, hogy 
az A formulának létezik (tabló) cáfolata, ha a tablója zárt vagy, hogy 
a B formula bizonyítható tablóval, ha B (jelölt formulákra FB) tablója zárt.
A formulák feldolgozási sorrendje a tablóban nem kötött, így a tabló mérete nem meghatározott. Célszerű először az  típusú formulákat feldolgozni, így a tabló szélessége jelentősen csökkenhet (7., 8. ábra).

(1) F[pqr](pq)(pr)	 típus
				(2) T pqr		 típus
				(3) F (pq)(pr)	 típus
(4) Fp	(2)					   (5) T qr (2)
(6) T(pq)  típus (3)				   (8) T(pq)  típus (3)
(7) F(pr)  típus (3)				   (9) F(pr)  típus (3)
(10) Fp (6)	(11) Tq (6)		(14) Fq (5)			(15) Tr (5)
(12) Tp (7)	(13) Tp (7)	(16) Fp (8)	(17) Tq (8)	(16) Fp (8)	(17) Tq (8)
      X		       X		(20) Tp (9)		X	(21) Tp (9)	(22) Tp (9)
						X				X	(23) Fq (9)
												X
7. ábra (feldolgozás sorszámozás szerint)

(1) F[pqr](pq)(pr)	 típus
				(2) T pqr		 típus (1)
				(3) F (pq)(pr)	 típus (1)
				(4) T(pq)  típus (3)
				(5) F(pr)  típus (3)
				(6) Tp (5)
				(7) Fr (5)
    (8) Fp  (2)			(9) Tqr  típus (2)
         X		(10) Fp (4)	  (11) Tq (4)
				       X		  (12) Fq (9)      (13) Tr (9)
							X		X
8. ábra (feldolgozás  típus előbb stratégiával)

A tabló módszer helyessége és teljessége.
Legyen egy T tabló egy ága  és 0 a  ágon előforduló változók egy igazságkiértékelése - interpretációja. Azt mondjuk, hogy a  ág igaz 0 –ra, ha  minden formulája igaz 0 –ra. A T tabló igaz 0 –ra, ha legalább egy ága igaz 0 –ra. Tekintsük a tabló gyökerében lévő G formula változóinak egy 0 igazságkiértékelését. Ha a G formula helyettesítési értéke igaz 0 –ra, akkor G közvetlen tablója is igaz. Ha a T tabló igaz 0 –ra, akkor a tabló közvetlen kiterjesztése T’ is igaz 0 –ra. A közvetlen kiterjesztés a még igaz ágakat érinti. A T’ igaz 0 –ra, ugyanis ha  típusú formulát dolgoztunk fel egy igaz ágon, akkor {1, 2} jelenik meg így mivel  igaz volt 0 –ra az {1, 2} is igaz lesz, tehát az ág marad igaz. Ha  típusú formulát dolgoztunk fel egy igaz ágon, akkor az elágazásnál egyik ágra 1 a másik ágra 2 kerül.  igaz 0 –ra ezért 1, 2 közül legalább az egyik igaz 0 –ra, vagyis legalább az egyik ág igaz ág lesz.
Abból, hogy egy igaz tabló minden közvetlen kiterjesztése igaz következik, hogy ha a gyökérben lévő G formula igaz egy 0 –ra, akkor a G formula T tablója is igaz 0 –ra. Ha egy T tabló zárt, akkor T nem lehet igaz egyetlen interpretációban sem és így a gyökérben lévő formula kielégíthetetlen.

Tétel. Ha a G formula tablója zárt, akkor G kielégíthetetlen. (tabló módszer helyessége) 
Bizonyítás: Ha egy T tabló zárt, akkor egyetlen ága sem igaz. Mivel a T gyökerében lévő formula  minden ágon szerepel ezért a T gyökerében lévő formula kielégíthetetlen.

Definíció: Hintikka halmaznak nevezik azt a S formulahalmazt, amelyre fennállnak az alábbi tulajdonságok.
H0 - komplemens pár nem fordul elő benne.
H1 - S  1 S és 2 S
H2 -. S  1S vagy 2 S.

Megjegyzés. A Hintikka halmaz lefele zárt formulahalmaz.
Tétel. A Hintikka halmazok kielégíthetők. (Hintikka lemma)
Bizonyítás: Legyen a  igazságkiértékelés a következő. Legyen X igaz, ha X eleme a Hintikka halmaznak és legyen X hamis, ha X eleme a Hintikka halmaznak. A többi ítéletváltozóhoz rendeljünk tetszőlegesen értéket. Bonyolultság szerinti indukcióval belátható, hogy  kielégíti a Hintikka halmazt.

Tétel. Egy tabló bármely teljes nyitott ága kielégíthető.
Bizonyítás: Legyen egy tabló egy teljes nyitott ága  és legyen S a -án előálló formulahalmaz. S-re a következő feltételek teljesülnek:
- Komplemens pár nem szerepel benne.
- S  1 S és 2 S.
- S  1S vagy 2 S.
Tehát S Hintikka halmaz és így kielégíthető.

Tétel. Ha egy G formula kielégíthetetlen, akkor bármely teljes tablója zárt. (teljesség)

Bizonyítás: Tegyük fel, hogy G tablója T nem zárt. Ekkor van legalább egy teljes nyitott ága. Ami azt jelenti, hogy G kielégíthető.

Egy véges (vagy végtelen) formulahalmaz tablója gyökerében az
			F1
			F2
			… 
			Fn ...

Szerepel. A teljes tablót a szokásos módon építjük F1-re. A nyitott ágakat az F2 teljes tablójával folytatjuk és így tovább. Ugyanígy definiálják megszámlálhatóan végtelen formulahalmaz tablóját is.

Definíció. Atomosan zárt tabló, ha minden ága tartalmaz egy atomi formulát (ítéletváltozót) és a negáltját.
Tétel: Ha G kielégíthetetlen, akkor létezik atomosan zárt tablója.
Bizonyítás: Egy olyan zárt ágat, amelyen előfordul egy formula és a negáltja is terjesszük ki addig amíg a fel nem dolgozott formulák atomiak nem lesznek

Elsőrendű analitikus tabló

Annak érdekében, hogy a tárgyalás egyszerűbb legyen az elsőrendű nyelv abc-jében lévő szimbólumok:

Indivíduum változók megszámlálható sorozata.
Indivíduum paraméterszimbólumok megszámlálható sorozata.
Predikátumszimbólumok megszámlálható sorozata minden aritásra.
Logikai összekötőjelek.
Kvantorok.
 Az  és a  típusú formulák mellett két új formulatípus jelenik meg.
xA illetve a xA  -   típus (univerzális típus). Mint jelölt formulák TxA illetve a FxA.
xA illetve a xA  -   típus (egzisztenciális típus). Mint jelölt formulák TxA illetve a FxA
A , (a) a xA, A(x/a) és a , (a) a xA, A(x/a)-t jelenti, ahol az a egy paraméter szimbólum.

A szemantika.
Az interpretáló struktúrákat azok U univerzuma szerint csoportosítva tekintjük. Bevezetjük az “elő interpretáció” fogalmát, ahol a nyelv minden olyan szimbólumát interpretáljuk, amelyhez csak az U ismerete szükséges. Ennek megfelelően
a paraméter interpretációja egy (x) fügvényt jelent, ahol  értelmezési tartománya a nyelv paraméterhalmaza és  értékkészlete az U univerzum.
U formulának nevezzük az olyan 1. rendű formulákat, ahol a paramétereket már interpretáltuk. Vagyis amelyekben paraméter már nem szerepel, de univerzumelem szerepelhet. (Ezek elő interpretált formulák.)
Ha a  és a  mondatokat egy U univerzum felett tekintjük és kU-t használunk, akkor a (k)-t, és a (k) a kU behelyettesítését jelenti.

Egy U feletti bármely interpretációban a következők állnak fenn.
F1:  igaz akkor és csak akkor, ha 1 is és 2 is igaz
F2:  igaz akkor és csak akkor, ha 1 vagy 2 igaz 
F3:  igaz akkor és csak akkor, ha (k) igaz minden kU-ra
F4:  igaz akkor és csak akkor, ha (k) igaz legalább egy kU-ra. 
A fenti tények alapján fennállnak az alábbi kielégíthetőségi szabályok. Adott S egy elsőrendű formulahalmaz. S tartalmaz , , ,  típusú formulákat, paramétereket, de konstansokat nem. S elsőrendben kielégíthető.
G1: Ha S kielégíthető, és S, akkor {S, 1, 2} kielégíthető.
G2: Ha S kielégíthető, és S, akkor {S, 1}és {S, 2} közül legalább az egyik kielégíthető.
G3: Ha S kielégíthető, és S, akkor minden a paraméterre {S, (a)} kielégíthető.
G4: Ha S kielégíthető, és S és a olyan paraméter, amely nem fordul elő S-ben, akkor {S, (a)} kielégíthető.

G4 igazolása: S kielégíthető, és S. S minden paraméteréhez a (x) fügvény már hozzárendelt U-beli értékeket, de (a) még nincs meghatározva, tehát bármely uU hozzárendelhető. A feltételeink szerint S miatt  kielgíthető így van olyan uU érték, hogy (u) igaz.

Tabló szabályok:
		A szabály 		B szabály		C szabály		D szabály	
									
		1		12		(a)		(a)	
		2				a tetsz. paraméter 		a új paraméter	
9. ábra
( formulák közvetlen tablóinak száma a paraméterek számával egyezik meg.)

A C, D szabályok jelölt és jelöletlen formulákra:

		C szabály 		C szabály	
		TxA		FxA	
		TA(x/a)		FA(x/a)	

		C szabály 		C szabály	
		xA		xA	
		A(x/a)		A(x/a)	

		D szabály 		D szabály	
		TxA		FxA	
		TA(x/a)		FA(x/a)	
			megkötéssel		

		D szabály 		D szabály	
		xA		xA	
		A(x/a)		A(x/a)	
			megkötéssel		
10. ábra

A megkötéssel megjegyzés a D szabálynál azt jelenti, hogy ha az "a" paramétert korábban már használtuk C vagy D szabályban, akkor nem használhatjuk fel újra mert az interpretációban szabadon választható értéket kell biztosítani számára. 

Lehet a D szabályt liberalizálni a következők miatt. Egy paraméter bevezetése D szabállyal a későbbi D szabály alkalmazásokban problémát okozhat, hiszen nincs biztosíték arra, hogy ugyanaz az indivíduumelem mindkét elvárásnak eleget tud tenni. Azonban ha az "a" paramétert C szabállyal már korábban bevezettük a tabló aktuális ágán, akkor később egy D szabállyal újra felhasználhatjuk, mivel a C szabállyal bevezetett paraméter értéke tetszőleges, tehát megfelel a D szabállyal bevezetett érték a számára. Ezzel a liberalizálással a tabló sok esetben rövidíthető (11. ábra).
Példa: megmutatunk két tabló bizonyítást a yxP(x)P(y) formulára (jelölt formula technikával).
Nem liberalizált paramétertechnikával
(1) Fy[xP(x)P(y)]
(2) FxP(x)P(a)	(1)
(3) TxP(x)		(2)
(4) FP(a)		(2)
(5) TP(b)		(3)
(6) FxP(x)P(b)	(1)
(7) FP(b)		(6)
	   X

Liberalizált paramétertechnikával

(1) Fy[xP(x)P(y)]
(2) FxP(x)P(a)	(1)
(3) TxP(x)		(2)
(4) FP(a)		(2)
(5) TP(a)		(3)
	   X

11. ábra

Az elsőrendű tabló helyességének bizonyításához be kell látni, hogy a tabló közvetlen kiterjesztésével a C és a D szabályok esetén is kielégíthetőek maradnak a kielégíthető ágak. Legyen  a T tabló egy kielégíthető ága. Más szóval legyen T igaz tabló. Ha C szabállyal történt a közvetlen kiterjesztés, akkor a megfelelő  formula igaz volt az ágat kielégítő interpretációban, de emiatt a (a) is igaz lesz bármely paraméterre ebben az interpretációban. Ha D szabállyal történt a közvetlen kiterjesztés, akkor a megfelelő  formula igaz volt az ágat kielégítő interpretációban, de amiatt, hogy a (a)-ban az “a” paraméter új,megválaszható úgy, hogy a (a) is igaz legyen.

Abból, hogy egy igaz tabló minden közvetlen kiterjesztése igaz következik, hogy ha a gyökérben lévő G formula igaz egy 0 interpretációban, akkor a G formula T tablója is igaz a 0 interpretációban. Ha egy T tabló zárt, akkor T nem lehet igaz egyetlen interpretációban sem és így a gyökérben lévő formula kielégíthetetlen.

Tétel. Ha az elsőrendű G formula tablója zárt, akkor G kielégíthetetlen. (tabló módszer helyessége) 

Bizonyítás: Ha egy T tabló zárt, akkor egyetlen ága sem igaz. Amiből a fentiek szerint következik, hogy a T gyökerében lévő formula kielégíthetetlen.

Az elsőrendű tabló teljessége.

Definíció: Egy U univerzum feletti elsőrendű Hintikka halmaznak nevezik azt a S formulahalmazt, amelyre fennállnak az alábbi tulajdonságok.

H0 - komplemens pár nem fordul elő benne. (U feletti atom és a negáltja)
H1 - S  1 S és 2 S
H2 -. S  1S vagy 2 S.
H3 -. S  (k)S, minden kU-ra.
H4 -. S  (k)S, legalább egy kU-ra.

Lemma (Hintikka lemma az elsőrendű logikában): minden az U feletti S Hintikka halmaz elsőrendben kielégíthető (az U felett).

Bizonyítás: Tekintsük azt az atomi kiértékelést, ami a P(1, 2, …, n)-hez igazat rendel, ha T P(1, 2, …, n) S és hamisat, ha F P(1, 2, …, n)S. Tegyül fel, hogy d(G)=n-ig a tétel fennáll.  és  típusú formulákra már láttuk a kielégíthetőséget az ítéletlogikában. Tekintsünk egy  formulát, ahol d()=n+1. Ekkor H3 miatt minden kU-ra (k)S amelyek az indukciós feltétel miatt igazak. Ennélfogva  igaz. Tekintsünk egy  formulát, ahol d()=n+1. Ekkor H4 miatt (k)S, legalább egy kU-ra. Az indukciós feltétel miatt (k) igaz. Ennélfogva  igaz. 

Ezután olyan szisztematikus tablóépítést vezetünk be, amely biztosítja, hogy minden teljes nyitott ágon Hintikka halmaz álljon elő.

1. Az A, B, D szabályok végrehajtása amíg lehet.
2. A C szabály végrehajtása, ahol a (a),  formulák kerülnek be a nyitott ágak végére.

Befejezett szisztematikus tablónak nevezzük azt a szisztematikus tablót, amely vagy végtelen vagy véges, de további kiterjesztése már nem lehetséges: 
(a) minden nem atomi formula már fel van dolgozva. 
(b) az ágon már előállt egy Hintikka halmaz.

Tétel: Bármely befejezett szisztematikus tabló nyitott ágain Hintikka halmaz áll elő.

Tétel: Bármely befejezett szisztematikus tabló nyitott ágai elsőrendben kielégíthetők.

Tétel (teljesség): Ha X érvényes, akkor létezik FX-re zárt befejezett tabló.
Bizonyítás: Legyen X érvényes. Legyen T az FX befejezett szisztematikus tablója. Ha T-nek lenne egy  nyitott ága, akkor  (és így FX is) kielégíthető lenne ellentétben az X érvényes feltétellel.

Tétel(Löwenheim): Ha X kielégíthető egyáltalán, akkor kielégíthető legfeljebb megszámlálható univerzumon.
Bizonyítás: Legyen T az X befejezett szisztematikus tablója. Mivel X kielégíthető a T-nek van nyitott ága. Egy nyitott ágon megszámlálhatóan végtelen sok paraméter fordulhat elő. Interpretációjukhoz megszámlálhatóan végtelen számosságú univerzum szükséges.
Atomi lezárás, mint nulladrendben.
Véges univerzum feletti kielégíthetőség. Tegyük fel hogy egy tabló nem zárt és van legalább egy nyitott ága  amelyen Hintikka halmaz állt elő az ágon előforduló paraméterek véges halmazára nézve. Ekkor értelmetlen folytatni az eljárást, mivel a Hintikka lemma szerint  (és így a gyökérben lévő formula is) kielégíthető véges univerzumon (12. ábra).

A [xP(x) xQ(x)] x(P(x)Q(x)) formula érvényes (logikailag igaz). a x(P(x)Q(x))xP(x) xQ(x) formula viszont nem érvényes. Más szóval a Fx(P(x)Q(x))xP(x) xQ(x) jelölt formula kielégíthető. Ahol ez kielégíthető ott lesz hamis az eredeti formula. (Probléma: Nem lehetne-e a Tx(P(x)Q(x))xP(x) xQ(x) jelölt formula tablójából is levonni ugyanezt a következtetést?)

Tekintsük a Fx(P(x)Q(x))xP(x) xQ(x) jelölt formula tablóját.

(1)	                  Fx(P(x)Q(x))xP(x) xQ(x)
(2)                   Tx(P(x)Q(x))		(1)
(3)                   FxP(x) xQ(x)		(1)
(4)                   FxP(x)		       	            (3)
(5)                   FxQ(x)			(3)
(6)                    FP(a)			            (4)
(7)                   FQ(b)			            (5)
(8)	          TP(a) Q(a)			(2)
(9) TP(a)	  (8)	|	(10) TQ(a)		(8)
 X 			|	(11) TP(b) Q(b)       (2)		
  (12) TP(b)  (11)    |   (13) TQ(b)  (11) 
								X
12. ábra

n-paraméteres Hintikka halmaznak nevezzük azt a formulahalmazt, amelyre a H0, H1, H2, H4 követelmények teljesülnek. A H3 pedig a következőkép teljesül: S  (a)S, minden az ágon a D szabállyal bevezetett “a” paraméterre.
A  ágon Hintikka halmaz állt elő két paraméterrel {a, b}. A gyökérben lévő formula kielégíthető a  
P(a) – h		
P(b) – i
Q(a) – i		
Q(b) – h
Interpretációban (ami az alábbi szemantikus fa megjelölt ágán is látható), ami azt jelenti, hogy az eredeti formula ebben az interpretációban hamis.

					
			P(a)					 P(a)

	     P(b) 		P(b) 			P(b) 			P(b)

Q(a) 	Q(a) 	      Q(a) 	Q(a) 	      Q(a)         Q(a) 	       Q(a) 	   Q(a) 

Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) Q(b) 

Szemantikus fa a P(a), P(b), Q(a), Q(b) bázis esetén

Probléma: Legyen a G formula a
xyR(x,y),
xR(x,x),
xyz[(R(x,y)R(y,z))R(x,z)]
formulák konjunkciója. 

Könnyű belátni, hogy ez a formula igaz a természetes számok halmazán, ha R a "kisebb" reláció. Ami azt jelenti, hogy megszámlálható univerzumon kielégíthető. Lássa be tabló módszerrel, hogy egyetlen véges univerzumon sem kielégíthető.

Elsőrendű tabló klasszikus L nyelv esetén. A kvantoros szabályok – közvetlen tablók

		C szabály 		C szabály	
		xA		xA	
		A(x/t)		A(x/t)	

		D szabály 		D szabály	
		xA		xA	
		A(x/y)		A(x/y)	
			megkötéssel		
13. ábra

Amennyiben a nyelvben csak az univerzális kvantor szerepel, akkor a
-szabály   		- szabály szerinti közvetlen tabókiterjesztés:
		…			…
xA				xA
…			…
A(x/t)			A(x/y)

A - szabályban t bármely L-term lehet. Amennyiben nem megengedett a t helyettesítése, akkor a formula változónév cseréjével el kell érni, hogy az legyen. A - szabályban az y lehet bármely olyan indivíduum változó, amely nem szabad a kiterjesztett ág egyetlen formulájában sem. y-t kritikus változónak is hívják. 

Ha L egyenlőségjeles nyelv, akkor az “egyenlőség szabályokat is hozzá kell venni a tabló szabályokhoz

		SI szabály 	
			
		t=t	

		SF szabály 	
			
		t1=tn+1 t2=tn+2… tn=t2n f(t1, t2, … tn)=f(tn+1 tn+2, … t2n)	

		SP szabály 	
			
		t1=tn+1 t2=tn+2… tn=t2n P(t1, t2, … tn)P(tn+1 tn+2, … t2n)	

14. ábra

Vizsgáljuk meg, hogy a (x)x() zárt formula logikailag igaz-e

		(1)	((x)x()
		(2)	x	(1)
		(3)	x()	(1)
	(4)	x	(2)		(5)		(2)
	(6)	(x/x) (4)		(7) () (x/x)   (3)
	(8)()( x/x)  (3)		(9)		  (7)
	(10)		(8)			(11)		  (7)
	(12)		(8)				X
		X

Itt a (4)-re a  szabályt alkalmaztuk de x mint kritikus változó szerepelhet (6)-ban, mivel x nem szabad -ban. (3)-ra a  szabályt alkalmaztuk, ahol bármely termet választhatjuk – x-et is.

Atomi lezárás is lehetséges.

A helyesség és teljesség bizonyítása nem változik. A szisztematikus tabló generálás itt is végrehajtható. 

Mutassuk meg tablóval, hogy az alábbi formulák logikai törvények.
(a) x(AB)xAxB,
(b) AxA, ahol x nem szabad változója A-nak,
(c) xAA(x/t),
(d) A(x/t)A, 
Ahol t bármely term lehet.

Feladatok
Legyenek s és t termek, amelyekben az y változó nem fordul elő. Mutassuk meg, hogy logikailag ekvivalensek:
s=t, 
y(s=yt=y) 
y(s=yt=y)

Probléma. Valamely kétváltozós R-nek az A struktúrában való RA interpretációja esetén az RA tranzitzív lezárása az összes olyan (a, b) párok halmaza, amelyekre létezik véges RA út a-ból b-be. Definiáljuk a n(x,y)-t rekurzív módon: 
1(x,y) R(x,y)- 
n+1(x,y) z(R(x,z) n(z,y))
Tegyük fel, hogy létezik egy TC(x,y) formula, hogy bármely A struktúrára és (a,b)A-ra ATC(a,b)  (a,b) az RA tranzitív lezárása. Ha ez lehetséges lenne, akkor az összes (a,b)-re kapott { TC(a,b)}{ n(a,b)} végtelen formulahalmaz kielégíthetőségének problémájával találkozunk.