Definíció Legyenek

elsőrendű formulák. Ekkor a

Equation 6.. 

formulát szekventnek nevezzük. Jelölése

Equation 6.. 

vagy rövidebben

, ahol

az

és

a

formulák multihalmazai.

A

szekvent tehát egy speciális alakú formula: implikáció, melyben az implikáció bal oldalán a

formuláinak konjunkciós, a jobb oldalán a

formuláinak diszjunkciós láncformulája áll. Ha a szekventben

üres, az implikáció bal oldalán a

törvényt, ha

üres, az implikáció jobb oldalán a

kielégíthetetlen formulát kell elképzelni. Ha

és

formulák, akkor az

jelölés az

szekventet hivatkozza.

Példa Határozzuk meg, hogy az alábbi szekventek mint formulák hogyan adhatók meg:

Világos, hogy ha egy

formulát szekventté szeretnénk alakítani, azaz elő akarjuk állítani azt a szekventet, ami épp az

formulát írja le, csak egy

jelet kell elé írni:

.

Definíció

,

,

,

,

és

szimbólumok.

Ha az

és

szimbólumokat egy ítéletlogikai nyelv formuláival, a

és

szimbólumokat pedig formulák multihalmazaival helyettesítjük, az alapsémából alapszekventeket kapunk, a levezetési szabály segítségével pedig egy vagy két (vonal feletti) szekventből levezetünk egy (vonal alatti) harmadikat.

a nyelv változója és

term.

Tétel

A tétel bizonyítása gyakorló feladat.

Definíció A szekventkalkulusbeli levezetésfa és a levezetésfa magassága a következő:

Példa A szekventkalkulusban az alábbi fa 3 magasságú levezetésfa, melynek gyökere a

szekvent:

A szekventek mellett zárójelek között megadtuk azt a levezetési szabályt, melyet alkalmazva a szekvent előállt.

Definíció Azt mondjuk, hogy az

szekvent a szekventkalkulusban bizonyítható , ha van olyan szekventkalkulusbeli levezetésfa, melynek

a gyökere. Jelölése:

.

Az alábbi tétel bizonyítását az olvasóra bízzzuk.

Tétel [A szekventkalkulus helyessége.] Ha az

szekvent bizonyítható a szekventkalkulusban, akkor a

formula logikai törvény.

Példa A

szekvent a szekventkalkulusban a következő – 6 magasságú – levezetésfával bizonyítható:

Példa A

Equation 6.. 

szekvent (ahol

) a szekventkalkulusban a következő levezetésfával bizonyítható:

A gyakorlatban a szekventkalkulus levezetési szabályait is ,,alulról felfelé'' szoktuk alkalmazni: amikor bizonyítani szeretnénk egy

szekventet, megpróbáljuk a bizonyító levezetésfát a gyökeréből (

-ből) kiindulva ,,alulról felfelé'' haladva felépíteni. Ehhez keresni kell az épülő levezetésfa minden nem alapszekvent leveléhez olyan levezetési szabályt a kalkulusban, mely segítségével a levél előállhat, és a levezetési szabálynak megfelelő vonal feletti szekvent(ek)et be kell írni a készülő levezetésfába ezen levél szülőjeként (szüleiként). A szekventkalkulus levezetési szabályainak megfordíthatósága miatt lényegtelen, hogy az alkalmazható levezetési szabályok közül melyiket választjuk.

Most foglalkozzunk azzal a kérdéssel, hogy vajon a szekventkalkulus ekvivalens-e a predikátumkalkulussal, azaz igaz-e, hogy egy

szekvent pontosan akkor bizonyítható a szekventkalkulusban, amikor

hipotézismentesen levezethető a predikátumkalkulusban. Ha ugyanis a két kalkulus ekvivalens, akkor a szekventkalkulus teljes kalkulus is.

Lemma Ha

a predikátumkalkulus alapformulája, akkor

bizonyítható a szekventkalkulusban.

Bizonyítás A bizonyítást konstruktív módon végezzük el, a predikátumkalkulus alapsémáiból előállított formulák esetén rendre megkonstruáljuk a megfelelő szekvent levezetését.

A többi alapformula esetén a levezetés megadását az olvasóra hagyjuk, a lemmát így bizonyítottnak tekinthetjük.

Lemma A predikátumkalkulus levezetési szabályai elérhetők a szekventkalkulusból.

Bizonyítás Azaz ha

és

bizonyíthatóak a szekventkalkulusban, akkor

is az, továbbá ha

bizonyítható, akkor

is,

Ezzel az állítást beláttuk.

Tétel Ha

hipotézismentesen levezethető a predikátumkalkulusban, akkor

bizonyítható a szekventkalkulusban, azaz ha

, akkor

. Bizonyítás A

szekvenciát megalapozó levezetésfa magassága szerinti indukcióval bizonyítunk. Legyen a levezetésfa magassága

.

Ezzel a tételt bebizonyítottuk.