A természetes levezetés módszere és a Gentzen szekventek.
A logika axiomatizálása, a bizonyításelméleti kalkulus kidolgozása (Hilbert - 1928) teremtette meg az alapját a természetes levezetés és a Gentzen szekventek módszerének (Gentzen - 1936). A természetes levezetés a logikai törvények igazolását tűzte ki célul (eldöntésprobléma megoldása). A természetes levezetés legfontosabb eszköze a dedukciós tétel.
,AB, akkor és csak akkor AB.
A tételt levezetési szabályként jelenítve meg, azt kapjuk, hogy ha bármelyik esetre rendelkezünk levezetéssel, akkor ez azt jelenti, hogy a másik eset levezetése meglévőnek tekinthető. A  formulahalmaz üres is lehet.

		,AB	
		AB	

Például
AB BA levezetése a feladat, de csak az AB, B  A levezetést ismerjük. A dedukciós tétel alapján ezzel a levezetéssel már igazoltuk, hogy AB BA. 
A levezetés:
1. BAB	ax.
2. B		feltétel
3. AB	mp(1,2)
4. AB	feltétel
5. (AB)( AB) A	ax.
6. (AB) A		mp(4,5)
7. A				mp(3,6)
Alkalmazva a dedukciós tételt a (AB)(BA) formulára, a problémát az előző probléma megoldására vezethetjük vissza. Mivel már adott a A bizonyításelméleti levezetése 
{AB, B}-ből, ezért a  (AB)(BA) formula logikai törvény.

		AB, B  A	
		AB(BA)	
			
		AB(BA)	
		(AB)(BA)	

Az ilyen bizonyítás azonban feltételezi, hogy valamilyen szinten egy-egy konkrét esetre bizonyításelméleti levezetést kell konstruálni. Ezért a feltételhalmaz és a levezetendő formula alakításához olyan szabályokra lenne szükség, amelyek mind a feltétel formulák mind a levezetendő formula bonyolultságát csökkentik addig, míg a levezetés létezésének feltételei elő nem állnak. Ezek a megalapozott szekvenciák. 
- azonosság törvénye 
,AA és az 
- ellentmondás törvénye 
ha   A, akkor  és csak akkor ,AC és  , ,A C.
Ha a logikai összekötőjelek közül nem csak az -t kívánjuk használni, akkor az implikációra vonatkozó szabályok mellett meg kell adni a többi logikai összekötőjelre vonatkozó szabályokat is. Ezek a dedukciós tételen túl alkalmasak arra, hogy úgy alakítsák a levezetési előírásban a feltétel részt és a következmény részt, hogy azok egyre kevésbé bonyolult formulákból álljanak. Igy kiderül, hogy el lehet-e jutni az összes elvárt esetben az azonosság vagy az ellentmondás törvényéhez.
Példa arra az esetre, amikor a dedukciós szabály elegendő.
CAC szekvencia megalapozását kell belátni, de elegendő belátni, a
CAC szekvencia megalapozását, ehelyett viszont elegendő belátni, a
C, AC szekvencia megalapozását. 
Ez már az azonosság törvénye, tehát  : CAC.

Egyes szerzők az algoritmizálás érdekében grafikai megjelenítéssel próbálják megmutatni a természetes levezetés lépéseinek hierarchiáját. A levezetés egy állapotát egy keretbe (box) foglalják. A dedukciós tétel első alkalmazása a formulára (amiről igazolni kell hogy logikai törvény), eredményezi az első keretet. Ennek első sorában is és utolsó sorában is egy-egy formula áll. Ez azt mutatja, hogy az első sorban lévő formulából az utolsó sorban álló formula levezetését kell megadni ahhoz, hogy az eredeti formula logikai törvény voltát igazoljuk.
Amennyiben az új levezetendő formulára még lehet alkalmazni a dedukciós tételt, akkor ez a lépés egy a levezetendő formula és annak feltételformulája közé egy új keretet eredményez, amelynek első és utolsó sorában egy-egy formula áll. Az első az új feltétel, az utolsó az aktuális levezetendő formula. Az egymásba ágyazott keretek első soraiban lévő formulák a feltételei a legbelső keret utolsó sorában lévő a levezetendő formulának. Ha ez a levezetés sikeres (pl. az azonosság törvénye alkalmazható), akkor a bizonyítás kész (1. ábra).

C					C		C, AC-t kell megmutatni.
		CAC		A		CAC
		CAC		C		CAC
AC				AC
CAC 				CAC
			1. ábra		

A dedukciós tétel alkalmazásai során kapott formulahalmaz alaki tulajdonságai alapján való kezelésére szolgálnak a stuktúrális szabályok (2.ábra).

1. Azonosság törvénye
			, AA
2. Bővítési szabály
		A	
		, BA	

3. Permutálási szabály 
		, B, C,A	
		, C, B, A	

4. Redukciós szabály 
		, B, B,A	
		, B, A	

5. Vágás szabály (cut rule)
		A;   , AB	
		, B	
2. ábra
Az 1-5 szabályok igazolása: 
Az 1. szabályhoz tartozó levezetés az A formula. A 2-5 szabályok igazolásához meg kell mutatni, hogy a felső sorban jelzett levezetés léte biztosítja az alsó sorban előírt levezetést. A vágás szabály igazolásához a , AB-ból a dedukciós tétel miatt  AB. A AB és A miatt , B.
A logikai műveletekre vonatkozó szabályok közül csak a dedukciós szabályt ismerjük, amely úgy csökkenti a levezetendő formula bonyolultságát (amennyiben az implikációs formula), hogy az előtagot a feltételek közé teszi át. Ha kezelni akarunk más formulafajtákat is, akkor a többi logikai művelethez is meg kell adni ilyen szabályokat. Kétféle szabályt vezetünk be. Az egyik fajtát a bevezető (b) szabálynak nevezik. A másik fajtát alkalmazó (a) ) szabálynak nevezik. Ha egy szabály azt mutatja meg, hogy egy kétváltozós műveletnek megfelelő formula hogyan vezethető le, úgy hogy csak a formula egyik argumentumának kell biztosítani a levezetését a másik argumentummal bővített feltételhalmazból, akkor a szabály a művelet bevezetési szabálya. Ha egy szabály azt mutatja meg, hogy egy kétváltozós műveletnek megfelelő formula levezetése, milyen esetben vezet el valamelyik argumentumformula levezetéséhez, akkor a szabály a művelet alkalmazásának szabálya. Megadjuk a szabályokat , , ,  típusú formulákra is.
bevezetési				alkalmazási szabályok.
Implikáció
		, AB		A; AB	
		AB		B	

Konjunkció
		A;   B		,A,B C; 	
		 AB		,ABC	
 típus
		 1;   2		,1, 1 C; 	
		 		,  C	

Diszjunkció
		BA		, AB		,A C; , BC	
		 AB		 AB		, AB C	
 típus
		, 1 2		1; 	
				2	

Negáció
		, AB; , A B		 A	
		 A		A	

Ekvivalencia
		, AB; , B A		A; AB		B; AB	
		 AB		B		A	

Általános kvantor (yA ill. )				t tetsz. term
		A 	;  (y)	y 		 yA	; 	
		 yA	; 			A(y/t)	; (y/t)	

Egzisztenciális kvantor	t tetsz. Term		y kritikus változó
		A(x/t)	; (x/t)		 xA	; 		
		 xA			 A(y)	; (y)	y , A	

A következmény formulákra vonatkozó szabályok más elnevezés szerint jobboldali szabályok. A feltétel formulákra vonatkozó szabályok  a baloldali szabályok. Itt a feltételformulák bonyolultságának csökkentése a cél. Igy a bevezetési szabályt célszerű megadni a logikai műveletekre. Ezek a szabályok megadják, hogy ha egy levezetendő formula feltétel formulái között valamely műveletnek megfelelő formula szerepel, hogyan adható(k) meg olyan feltételhalmaz(ok), amelyben az illető formulának csak az argumentum formulái jelennek meg és a formula levezetését biztosítják
Baloldali bevezetési szabályok.

Implikáció
		, AC ; , BC			
		, , AB C			

Konjunkció
		, A BC	
		, AB C	
 típus
		, 1, 2C	
		, C	

Diszjunkció
		, AC ; , BC		
		, AB C		
 típus
		, 1 C; , 2 C			
		, C			

Bevezetjük a  (azonosan igaz),  (azonosan hamis) konstansokat. Összefoglajuk a konstans szabályokat és felhasználásukkal az ellentmondás törvényére kidolgozott szabályokat.
Konstans szabályok
					
		X			

Negációs szabályok
		X,X		, A 	
				  A	

Nézzünk néhány feladatot.

(PQ) 
					 formula 1=P, 2= Q
P				(PQ), P  Q
Q

PQ				(PQ)  PQ

(PQ)PQ		 (PQ)PQ

x[P(x)Q(x)]

  xP(x)

    xQ(x)				a levezetendő negáltja
    Q(p)				
     P(p)					
    P(p)Q(p)				
    Q(p)

 xQ(x)
 
xP(x)xQ(x)

x[P(x)Q(x)]xP(x)xQ(x)

A szekvent kalkulus.
Legyenek  és  véges formulahalmazok, A, B, … formulák. Egy szekvent egy (, ) pár. A későbbiekben    alakban írjuk. A  jel szándék szerint implikációt reprezentál. A szekventben  és  véges formulasorozat.
, helyett  -t írunk értelemszerűen.
Azt mondjuk, hogy egy szekvent teljesül, ha valahányszor  a nyíl baloldalán lévő minden formula igaz a nyíl jobboldalán lévő formulák legalább egyike igaz.
Jelöljön v egy Boole kiértékelést vagy egy interpretációt.
Def. V(  )=i, ha v(X)=h valamely X-ra vagy v(Y)=i valamely Y-ra.
A definíció alapján v()=h és v(X)=v(X).
Megjegyzés: Legyen ={A1, A2, …, An} és ={ B1, B2, …, Bk} ekkor a    igaz akkor és csak akkor, ha A1 A2 … An B1 B2 … Bk =i.

Axiómák:  XX,	,		,
Strukturális szabályok:
Szűkítés. Ha 12 és 12, akkor
		11	
		2 2	

Negációs szabályok
		  , X		, X 	
		, X  		  , X	

Konjunkciós szabályok:
		, X, Y  		 , X   , Y	
		, XY  		  , XY	

Diszjunkciós szabályok:
		, X   , Y  		 , X, Y	
		, XY  		  , XY	
Implikációs szabályok:
		 , X  , Y  		, X , Y	
		, XY  		  , XY	

 szabály 
		, (t) 		  , (p)	
		,  		  , 	

szabály 
		  , (t)		, (p) 	
		  , 		,  	

1. példa. Bizonyítsuk be szekvent kalkulussal, hogy  (PQ)PQ.

1. P  P				2. Q  Q
3. Q, P  P				4. Q, P  Q
5. Q, P  (PQ)
6. Q  (PQ), P
7.  (PQ), P, Q
8. (PQ)  P, Q
9. (PQ)  PQ
10.  (PQ)PQ

2. példa. Bizonyítsuk be szekvent kalkulussal, hogy x[P(x)Q(x)]xP(x)xQ(x)

1. P(p)  P(p)			2. Q(p) Q(p)
3. P(p) Q(p), P(p)		4. Q(p), P(p) Q(p)
5. P(p)Q(p), P(p) Q(p)
6. x[P(x)Q(x)], P(p) Q(p)
7. x[P(x)Q(x)], xP(x) Q(p)
8. x[P(x)Q(x)], xP(x) xQ(x)
9. x[P(x)Q(x)] xP(x)xQ(x)
10. x[P(x)Q(x)]xP(x)xQ(x)
Def. Egy szekventet a Gentzen-kalkulusban levezethetőnek nevezünk, ha
-	vagy axióma
-	vagy olyan levezetési szabály, melyben ez a vonal alatti szekvent és a vonal feletti szekvent vagy szekventek levezethetőek.

A Gentzen-kalkulus helyes, mert ha az A1, A2, …, AnB1, B2, …, Bk szekvent levezethető a Gentzen-kalkulusban, akkor a A1 A2 … An B1 B2 … Bk formula logikai törvény. (A levezethetőség miatt a levezethető szekventhez a vonal feletti szekvent vagy szekventek levezethetőek. Ezt folytatva olyan vonal feletti szekventekhez jutunk, amelyek axiómák, tehát a hozzájuk asszociált formulák logikai törvények. Ha a vonal feletti szekvent logikai törvény, akkor a vonal alatti is az.)
 A szekvent kalkulus teljes, mert ha az X formula logikai törvény, akkor a X szekvent levezethető a szekvent kalkulusban.