Chapter 5. Frege stílusú kalkulus

A modern logika egyik első nagy eredménye Gottlob Frege (1848-1925) német matematikus logikai rendszere. Bár Frege a rendszere felépítése során minden lépést szemantikai okokkal indokolt, nem hozott létre olyan szemantikai felépítést logikájához, mint amit a Bevezetésben megadtunk. Frege logikai rendszere szintaktikai felépítésű rendszer, kalkulus volt. A fejezetben egy a Frege rendszeréhez stílusában hasonló predikátumkalkulust mutatunk be.

5.1. A predikátumkalkulus

Definíció Az

,

és

szimbólumok.

  • A predikátumkalkulus alapsémái :

  • A predikátumkalkulus levezetési szabályai :

    Equation 5.. 


Ha az

és

szimbólumokat egy elsőrendű logikai nyelv formuláival helyettesítjük,

a nyelv változója,

pedig term, akkor az alapsémákból alapformulákat kapunk, a levezetési szabályok segítségével pedig egy vagy két (vonal feletti) formulából levezetünk egy (vonal alatti) harmadikat.

Tétel

  • A predikátumkalkulus alapformulái logikai törvények.

  • .

  • Ha

    és

    akkor

Definíció A fomulafa és magasságának induktív definíciója:

  1. Minden

    formula

    magasságú formulafa, melyben

    alsó formula, és nincs nála feljebb levő formula.

  2. Ha

    és

    magasságú olyan formulafák, melyben az alsó formulák

    és

    alakúak, akkor az

    Equation 5.. 


    alakzat is formulafa. A nyert formulafában

    az alsó formula, melynél

    és

    minden formulája feljebb van. A formulafa magassága pedig

    .

  3. Ha

    magasságú olyan formulafa, amelyben az alsó formula

    , akkor az

    Equation 5.. 


    alakzat is formulafa.

    alsó formula, melynél

    minden formulája feljebb van, és a formulafa magassága

    .

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

A formulafában azok a formulák, melyeknél nincs feljebb levő, vagy alapformulák, vagy ún. hipotézisek .

Definíció A levezetésfa egy formulafa, melyben ha

-ból az általánosítás szabályával akarjuk a

-t nyerni, akkor

nem paraméter egyetlen, a

-nál feljebb levő hipotézisben sem.

Példa Jellemezzük az alábbi formulafát:

magasságú formulafa alsó formula:

alapformula:

hipotézis:

Definíció A

véges formulahalmazból az

formula levezethető , ha van olyan levezetésfa, melyben

alsó formula, és a hipotésisek mind elemei

-nak. (Jelölése

, az alakzat neve szekvencia .) Ha

üres, akkor

hipotézismentesen vezethető le a kalkulusban (jelölése

).

Példa Bizonyítsuk be, hogy

.

Tétel [A predikátumkalkulus helyessége.] 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

      , ekkor

      , így nyilván

      is.

    • vagy

      , azaz hipotézis, ekkor minden olyan interpretációban és értékelés mellett, amikor minden hipotézis igaz, nyilván

      is igaz, tehát

      .

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

      é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

      . De minden olyan interpretációban és értékelés mellett, amikor a

      -beli hipotézisek mind igazak, ezek szerint igazak ezen interpretációkban és értékelések mellett az

      és az

      formula is, így a

      formula is. Tehát

      is.

    • 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

      . De minden olyan interpretációban és értékelés mellett, amikor a

      -beli hipotézisek mind igazak, ezek szerint igaz ezen interpretációkban és értékelések mellett az

      is. Mivel

      , a

      -beli formulákat igazzá tevő értékelésekben

      -et bárhogy lehet értékelni, így az

      is

      bármilyen értékelése esetén igaz, tehát a

      is. Ezért

      .

Ezzel a tételt bebizonyítottuk.

Tétel [A predikátumkalkulus teljessége.] Ha

, akkor

. A tétel legismertebb bizonyítását Leon Henkin (1921-2006) amerikai matematikus adta meg (ez például [Smullyan]-ben is megtalálható).