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.
Definíció Az
,
és
szimbólumok.
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
Definíció A fomulafa és magasságának induktív definíciója:
Minden
formula
magasságú formulafa, melyben
alsó formula, és nincs nála feljebb levő formula.
Ha
és
magasságú olyan formulafák, melyben az alsó formulák
és
alakúak, akkor az
alakzat is formulafa. A nyert formulafábanaz alsó formula, melynél
és
minden formulája feljebb van. A formulafa magassága pedig
.
Ha
magasságú olyan formulafa, amelyben az alsó formula
, akkor az
alakzat is formulafa.alsó formula, melynél
minden formulája feljebb van, és a formulafa magassága
.
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
.
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
.
Az indukciós feltevésünk szerint legyen igaz az állítás minden
-nél nem magasabb levezetésfa esetén.
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ó).