6.2. A szekventkalkulus

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:

  1. (üres) szekvent a

    formulát, azaz logikai ellentmondást ír le.

  2. szekvent a

    , azaz a

    formulát jelöli.

  3. Az

    szekvent jelentése az

    , azaz a

    formula.

  4. jelentése

    .

  5. jelentése pedig

    .

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ő:

  1. A kalkulus minden alapszekventje egy (egyetlen szekventből álló) levezetésfa, ez a szekvent lesz a levezetésfa gyökere. A levezetésfa magassága 1.

  2. Ha

    magasságú olyan levezetésfa, amelynek gyökere a szekventkalkulusbeli levezetési szabályban épp vonal feletti szekvent, akkor a levezetési szabállyal a vonal alatti

    szekventet előállítva

    Equation 6.. 


    is levezetésfa, ahol az

    szekvent a kapott levezetésfa gyökere, és a levezetésfa magassága

    .

  3. Ha

    és

    rendre

    és

    magasságú olyan szekventkalkulusbeli levezetésfák, melyek gyökerei valamely levezetési szabályban épp vonal feletti szekventek, akkor előállítva a levezetési szabállyal a vonal alatti

    szekventet,

    Equation 6.. 


    is levezetésfa a kalkulusban, amelyben az

    szekvent lesz a levezetésfa gyökere, és a levezetésfa magassága

    .

  4. Minden levezetésfa az 1–3. szabályok véges sokszori alkalmazásával áll elő.

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

.

  1. esetén

    a predikátumkalkulus alapformulája, ekkor

    .

  2. Az indukciós feltevésünk szerint legyen igaz az állítás minden

    -nél nem magasabb levezetésfa esetén.

  3. Legyen most

    . Ha a

    szekvenciát megalapozó levezetésfát

    • a modus ponens levezetési szabállyal nyertük

      és

      szekvenciákat megalapozó, legfeljebb

      magasságú levezetésfákból, az indukciós feltevés miatt

      és

      bizonyíthatók a szekventkalkulusban. De a modus ponens elérhető a szekventkalkulusból.

    • az általánosítás szabályával nyertük a

      szekvenciát megalapozó

      magasságú levezetésfából, az indukciós feltevés miatt

      bizonyítható. De az általánosítás szabálya elérhető a szekventkalkulusból.

Ezzel a tételt bebizonyítottuk.