Chapter 6. Gentzen kalkulusai

A predikátumkalkulusban egy levezetés megkonstruálása gyakran nagyon kényelmetlen. Egyszerű formulák levezetése is lehet hosszadalmas, ráadásul a levezetések nem nagyon hasonlítanak a szokásos érvelésekre. 1934-ben Gerhart Gentzen (1909-1945) német logikus olyan levezetési rendszert dolgozott ki, mely szabályai a Frege stílusú kalkulusokénál jóval közelebb állnak a gyakorlatban használt érvelés lépéseihez. Gentzen saját rendszerét a Frege stílusú rendszerekkel szembeállítva a természetes levezetés kalkulusának nevezte.

Tágabb értelemben természetes levezetési rendszereknek szokták nevezni a Gentzen eredeti kalkulusához közel álló, de azzal nem tökéletesen megegyező levezetési rendszereket is. Ezek közös jellemzője, hogy bár használhatnak alapformulákat is, alapvetően mégis levezetési szabályokra épülnek.

Most megadjuk a klasszikus elsőrendű logika egy olyan természetes levezetési rendszerét, mely nagyon közel áll Gentzen eredeti kalkulusához. A predikátumkalkulushoz hasonlóan ez a rendszer is helyes és teljes, tehát bizonyos értelemben sem nem több, sem nem kevesebb annál. Az alapvető különbség a hipotézisektől a levezetendő formuláig való eljutás módjában áll.

Hogy megkönnyítsük a levezethetőségi reláció fennállásának igazolását, levezetési sémákra vonatkozó segédszabályok egy egész rendszerére támaszkodunk. A segédszabályok állításokat jelölnek: ha adva van(nak) a vonal feletti szekvenciá(ka)t megalapozó predikátumkalkulusbeli levezetésfa(ák), akkor megkonstruálható a vonal alatti szekvenciát megalapozó levezetésfa is. Segítségükkel a predikátumkalkulusbeli levezethetőség igazolható a levezetés tényleges megkonstruálása nélkül. Továbbá a természetes levezetés technikájának szabályai szoros analógiát mutatnak a matematikai érvelés gyakorlatával, ami megkönnyíti a szekvenciák igazolását.

A természetes levezetés technikája mellett Gentzen kidolgozott egy másik - ún. szekventekkel dolgozó kalkulust is. A szekventkalkulus is igen kényelmesen használható, mivel a levezetési szabályok egyszerűen és a levezetendő szekventben szereplő formulák szerkezete által meghatározott sorrendben alkalmazhatók.

6.1. A természetes levezetés

Definíció Az

,

és

szimbólumok.

  • Az azonosság törvénye

    Equation 6.. 


  • Strukturális szabályok

    Equation 6.. 


  • Logikai szabályok

    Equation 6.. 


    Equation 6.. 


Ha az

és a

szimbólumokat elsőrendű formulákkal, a

és

szimbólumokat formulák multihalmazaival helyettesítjük,

a nyelv változója és

term, akkor predikátumkalkulusbeli levezethetőségre vonatkozó állításokat nyerünk.

Az azonosság törvénye – egyedül itt nincs vonal – például azt állítja, hogy bármely

formulahalmazból és az

formulából mint hipotézisekből levezethető a predikátumkalkulusban

. Az állítás bizonyítása egyszerű: egyetlen formulából, az

-ból álló levezetésfa bizonyítja. A strukturális szabályok igazolása is nagyon egyszerű. A bővítés és a szűkítés szabálya esetén a vonal feletti szekvenciát megalapozó levezetés egyúttal a vonal alatti szekvenciát megalapozó levezetés is. A vágás szabályát a dedukció-tétel részletes bizonyítása után vizsgáljuk meg.

Tétel [Dedukció-tétel.] 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

    • vagy alapformula

      , vagy

      , ekkor

      így

    • vagy

      . De 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 ponenssel nyertük

      és

      szekvenciákat megalapozó, legfeljebb

      magasságú levezetésfákból. Az indukciós feltevés miatt ekkor igaz az állítás, tehát

      és

      .

      Tehát

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

      tehát

      alakú. Az

      magasságú levezetésfa, amiből nyertük, a

      szekvenciát alapozza meg, ahol

      . Az indukciós feltevés miatt ekkor igaz az állítás, tehát

      .

      Tehát

Ezzel a tételt bebizonyítottuk.

A vágás szabályára visszatérve: a dedukciós tétel szerint ha

, akkor

. Ekkor viszont a

-t és a

-t igazoló levezetések konkatenációja megalapozza

-t.

A logikai szabályok igazolása sem nehéz. Néhány szabály bizonyításának ötletét vázoljuk.

  1. Az implikáció bevezetésének szabálya épp a dedukciós tétel.

  2. Az implikáció eltávolításának a szabálya: Ha adottak a

    és a

    állításokat megalapozó levezetések, a kettő konkatenációja után alkalmazható a modus ponens, és így épp

    -nek egy, a

    -ból való levezetését állítottuk elő.

  3. A diszjunkció bevezetése: Ha adott

    -ból

    -nak a levezetése, akkor az

    alapformulát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk a

    -ból az

    egy levezetését.

  4. A diszjunkció eltávolítása: Ha adottak a

    és a

    állításokat megalapozó levezetések, akkor a dedukciós tétel miatt elkészíthető a

    és a

    állításokat megalapozó levezetések is. Ezt a két levezetést konkatenáljuk, és írjuk le az

    Equation 6.. 


    alapformulát. Kétszer alkalmazva a modus ponenst megalapoztuk, hogy

    . Írjuk be a levezetésbe a vonal alatti szekvenciából az

    hipotézist, és ha most újból alkalmazzuk a modus ponenst, megkapjuk a

    -t megalapozó levezetést.

  5. Az univerzális kvantor bevezetésének szabálya éppen az általánosítás szabálya.

  6. Az univerzális kvantor eltávolításának szabálya: Ha adott a

    szekvenciát megalapozó levezetés, akkor a

    alapformulát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk

    egy levezetését

    -ból.

  7. Az egzisztenciális kvantort bevezető szabály: Ha adott a

    szekvenciát megalapozó levezetés, akkor írjuk be az

    alapformulát a levezetésbe, és alkalmazzuk a modus ponenst. Így

    -ból levezettük

    -t.

  8. Az egzisztenciális kvantor eltávolításásának szabálya: A

    szekvenciát megalapozó levezetésből a dedukciós tétel miatt elkészíthető a

    szekvenciát megalapozó levezetés is. Ebből az általánosítás szabálya miatt – mivel

    adódik. Ha most a levezetésbe beírjuk a

    alapformulát (lényeges, hogy

    ), alkalmazhatjuk a modus ponenst. Ezzel megkapjuk a

    egy levezetését

    -ból. A dedukciós tétel újbóli alkalmazásával pedig igazoltuk, hogy

    .

A gyakorlatban a természetes technikai szabályokat inkább ,,alulról felfelé'' szoktuk alkalmazni: amikor igazolni kell egy vonal alatti állítást, elegendő bebizonyítani, hogy a vonal feletti állítások igazak. Ekkor világosan látható, hogy a felsorolt szabályok elég jól tükrözik a matematikusok által széles körben használt bizonyítási módszereket.

  • Például a diszjunkció eltávolítása megfelel az esetelemzés módszerének . Ha le kell vezetni

    -ből

    -t, akkor az esetelemzés a következőképpen történik: ha

    igaz, akkor vagy

    , vagy

    igaz, ezért elegendő két esetet megvizsgálni. Külön-külön le kell vezetni

    -ból

    -t és

    -ből

    -t.

  • A negáció bevezetése a matematikai gyakorlatban az indirekt bizonyítás , azaz az ellentmondáshoz való visszavezetés módszere . Hogy bebizonyítsuk

    -t, elegendő – feltéve, hogy

    teljesül – ellentmondáshoz jutni, vagyis egy

    -t kiválasztva

    -ból levezetni

    -t és

    -t is.

Példa Bizonyítsuk be természetes technikával, hogy

Equation 6.. 


Felvetődhet az a kérdés is, hogy ha egy formulahalmazból a predikátumkalkulusban levezethető egy formula, akkor ezt be tudjuk-e mindig bizonyítani csupán a természetes levezetés technikájával.

Tétel Ha

, akkor ez belátható a természetes technikával. 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

    • vagy alapformula, ekkor

      belátható a természetes technikával (ezeket a bizonyításokat az olvasóra bízzuk), így – a bővítés szabálya alapján –

      is bizonyítható természetes technikával.

    • vagy hipotézis, azaz eleme a

      formulahalmaznak, akkor a

      az azonosság törvénye.

  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 ekkor ezek a szekvenciák megalapozhatók természetes technikával. Az implikáció eltávolításának a szabályával pedig a

      -t is bizonyítottuk.

    • 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 ez a szekvencia megalapozható természetes technikával. Ekkor az univerzális kvantor bevezetésének szabályával a

      -t is bizonyítottuk.

Ezzel a tételt bebizonyítottuk. Ezzel beláttuk azt is, hogy a természetes levezetés kalkulusa ekvivalens a predikátumkalkulussal, így bebizonyítottuk adekvátságát a klasszikus elsőrendű szemantikával.

Tétel [A természetes levezetés helyes és teljes.]

pontosan akkor látható be természetes levezetéssel, ha

.

Példa Bizonyítsuk be a természetes levezetés segítségével, hogy a

Equation 6.. 


formula logikai törvény.