Frege-kalkulus

A Frege-kalkulus egy matematikai logikai kalkulus (levezetőrendszer), azaz egy alapjelekből, axiómákból, levezetési szabályokból álló formális nyelv vagy elmélet, melyet Gottlob Frege jénai matematikus alkotott meg 1879-ben megjelent, Fogalomírás (Begriffsschrift) c. könyvében.

A levezetési szabályok

Két levezetési szabályt használ: a modus ponenst és a generalizációs törvényt. Ezen kívül említ még egy konvenciót, amit, lévén máshová még kevésbé sorolható, itt említünk.

• A modus ponens a következő: amennyiben érvényes $\vdash A$ és $\vdash A\rightarrow B$ is, akkor $\vdash B$ is (tehát „ha A igaz és a-ból következik, hogy B, akkor B is igaz”).
• A behelyettesítési szabály: ha X összetett ítélet, melyben Y egy függvény argumentumának, függvénynek vagy határozatlan ítéletnek a jele (változója), akkor az Y betű minden X-beli előfordulása helyébe egy megfelelő típusú másik betűt vagy összetett kifejezést – függvény argumentumát, függvényjelet vagy ítéletjelet – helyettesítve az így kapott Z ítélet érvényes, ha X is az volt.
• A generalizációs szabály konvenciója: egy $\vdash \Phi (x)$ alakú kifejezésen a következőt kell érteni: $\vdash \forall x:\ \Phi (x)$ . Tehát megengedhető ítéletben betű szabad előfordulása, de ez mindig univerzális kvantorral kötött előfordulást jelent (ez a konvenció egyszerűsíti az ítéletek formáját, könnyebb kiolvasást téve lehetővé).

Az axiómák

A kilenc axióma

Frege kilenc axiómára alapozza a Fogalomírás rendszerét (axiómák azok az ítéletek, melyeket szemantikailag és nem szintaktikailag igazol).

Ezek a Fogalomírás számozása szerinti (1), (2), (8), (28), (31), (41), (52), (54), (58) tételek (a változókon és egyéb betűkön kívül az első háromban csak a feltételesség, a második háromban a tagadás jele is szerepel, az utánuk következő kettőben az egyenlőségjel is, végül az utolsó, kilencedik axiómában pedig az univerzális kvantifikáció). Az axiómák modern logikai átiratban:

1. $\vdash \ \ A\rightarrow \left(B\rightarrow A\right)$
2. $\vdash \ \ \left[\ A\rightarrow \left(B\rightarrow C\right)\ \right]\ \rightarrow \ \left[\ \left(A\rightarrow B\right)\rightarrow \left(A\rightarrow C\right)\ \right]$
3. $\vdash \ \ \left[\ D\rightarrow \left(B\rightarrow A\right)\ \right]\ \rightarrow \ \left[\ B\rightarrow \left(D\rightarrow A\right)\ \right]$
4. $\vdash \ \ \left(B\rightarrow A\right)\ \rightarrow \ \left(\lnot A\rightarrow \lnot B\right)$
5. $\vdash \ \ \lnot \lnot A\rightarrow A$
6. $\vdash \ \ A\rightarrow \lnot \lnot A$
7. $\vdash \ \ \left(a=b\right)\rightarrow \left(f(a)=f(b)\right)$
8. $\vdash \ \ a=b$
9. $\vdash \ \ \left(\ \forall a:f(a)\ \right)\ \rightarrow \ f(b)$

Az axiómák értelmezése régen és ma

Ezeken az axiómákon Frege a generalizációs konvenció alapján másodrendű ítéleteket ért. Például

⊢ A→(B→A)

azt jelenti, úgy kell érteni,

⊢ ∀A∀B: [A→(B→A)].

A modern logikatankönyvek általában nem követik ezt a felfogásmódot (tekintve, hogy a másodrendű logika még csak nem is egyetemi tananyag, ez nem is igen lenne lehetséges). A legelterjedtebb modern felfogás szerint az axiómák sémák, azaz maguk nem ítéletek, csak ítéletváltozókból és logikai operátorokból álló jelsorok; melyekben a betűk helyébe megfelelő módon ítélet(nev)eket helyettesítve, igaz ítéletet kell kapnunk bármely helyettesítéssel (azaz tautologikus sémák).

A nulladrendű logika vagy ítéletkalkulus szintaktikus (más néven axiomatikus) felépítésének legismertebb módszere, a Hilbert-kalkulus, gyakorlatilag ma is a Frege által használt axiómarendszerre ^lentebb épül, noha hangsúlyozzuk, Frege axiómái nem nulladrendű, hanem (legalább) másodrendű logikai axiómák.

Az axiómarendszer bizonyításelméleti értékelése

Ha Frege logikai rendszerét elsőrendűnek tekintjük (ez megfelelő szintaktikai korlátozásokkal elérhető), akkor eme korlátozott rendszert komplettnek, teljesnek nevezhetjük. Az erre vonatkozó tételt Kurt Gödel bizonyította 1930-ban ^{(ld. az irodalomjegyzéket)} ) . Eszerint ha az $\vdash A$ jól képzett (értelmes) ítéletséma nem vezethető le az elsőrendű logikában, akkor szerkeszthető hozzá „cáfoló interpretáció” (azaz olyan matematikai struktúra, melyben nem érvényes).

A Frege-axiómarendszer viszont nem független. A nulladrendű logika felépítéséhez három axióma is elegendő (az első, második és negyedik), de már Frege is javasol egyszerűsítéseket és összevonásokat műve Előszavában a formálisan elsőrendű (egyenlőségjelet vagy kvantort tartalmazó) axiómákra is.

Sorozatelmélet

A Fogalomírás III. fejezetében Frege felépít egy nagyon alapszintű sorozatelméletet (definiálja a „megelőzés”, „rákövetkezés”, „egyértelmű reláció”) fogalmakat. Frege elmélete erősen másodrendű, rengeteg, függvényekre vonatkozó kvantifikációt foglal magában (a lentebbiekben Ruzsa Imre szóhasználatát és jelöléseit alkalmazzuk, melyek eltérnek Fregéétől).

A legalapvetőbb Frege definiált reláció (a 69-es számú tétel) az öröklődés. Egy predikátumot (egyargumentumú függvényt) öröklődőnek vagy hereditáriusnak nevezünk egy relációra (kétargumentumú függvényre) nézve, ha abból a két tényből, hogy (i) előbbi egy individuumra fennáll, és (ii) utóbbi fennáll az előbbi individuum és egy másik individuum közt, következik, hogy a predikátum fennáll ama másik individuumra is. Jelekben:

$Her\left(\ P(.)\ ,\ r(.,.)\ \right)\ :=\ \forall x:\ \left(\ P(x)\rightarrow \forall y:\left[\ r(x,y)\rightarrow P(y)\ \right]\ \right)$

.

Frege ezután definiálja a megelőzés relációját (76) egy r relációra nézve; ezzel pedig lehetőség nyílik, hogy ha adott egy r reláció, akkor annak segítségével különfle „sorozatokat” képezzünk (pontosabban, egy r meghatároz egy „sorozatot”).

$a<_{r}b\ :=\ \forall P:\left(\ \ Her(P,r)\rightarrow \left(\ \forall x:\ \left[r(a,x)\rightarrow P(x)\right]\rightarrow P(b)\ \right)\ \right)$

Tehát a és b egymás rákövetkezői az r relációra nézve, ha minden e relációra nézve öröklődő predikátum igaz b-re, mely igaz az a-val r relációban lévő dolgokra is.

Ezután rengeteg tételt bizonyít, melyek főképp <_r tranzitivitásának (98) belátásához kellenek:

$\vdash \ \left[\ x<_{r}y\ \rightarrow \ \left(\ y<_{r}z\ \rightarrow \ x<_{r}z\ \right)\ \right]$

.

Végül definiálja az egyértelmű (univalens) reláció fogalmát (115), és bizonyít még 11 ezzel kapcsolatos tételt:

$\vdash \ Un(r(.,.)):=\forall x\forall y:\ f(x,y)\rightarrow \left(\forall z:\ \left[f(x,z)\rightarrow (y=z)\right]\right)$

.

A Fogalomírásban rendszerének műveleti szintaktikája és szemantikája

Frege az 1. f. 7. §.-ban kimutatja, hogy a tradicionális logikában használt logikai műveletek (melyeket az „és”, „vagy”, „sem-sem” .. stb. ) kötőszavak reprezentálnak a köznyelvben, kifejezhetőek fogalomírása segítségével. Ez pusztán a tagadás és a feltételesség jelének kombinációit felírva megtehető.

Az áttekinthetőség kedvéért foglaljuk össze, hogy az 1. f. 7. §.-ban Frege mely példákat veszi sorra (nyomdatechnikai okok miatt modern jelölésben közöljük):

1. $B\rightarrow \lnot A$, ma $A||B$ exklúzió, Sheffer-művelet;
2. $\lnot B\rightarrow A$, ma $A\vee B$ alternáció (diszjunkció); emellett beszél a „vagy” kötőszó kizáró (diszjunktív) használatáról, de csak az 5.-6. példa alatt formalizálja;
3. $\lnot C\rightarrow \left(\lnot B\rightarrow A\right)$ , ma $A\vee B\vee C$ (háromváltozós) alternáció;
4. $\lnot \left(B\rightarrow \lnot A\right)$ , ma $A\wedge B$ konjunkció;
5. $\lnot C\rightarrow \left(\lnot B\rightarrow A\right)$ , ma $A\wedge B\wedge C$ (háromváltozós) konjunkció.
6. $\lnot \left(\left(\lnot B\rightarrow A\right)\rightarrow \lnot \left(B\rightarrow \lnot A\right)\right)$ , ma $A\oplus B$ antivalencia (kontravalencia);
7. $\lnot \left(\left(B\rightarrow \lnot A\right)\rightarrow \lnot \left(\lnot B\rightarrow A\right)\right)$ , ami szintén az antivalencia egy lehetséges formalizálása a fogalomírásban;
8. $\lnot \left(A\rightarrow B\right)$ , az $A\wedge \lnot B$ művelet;
9. $\lnot \left(\lnot B\rightarrow \lnot A\right)$ , ugyanaz mint az előbbi;
10. $\lnot \left(\lnot A\rightarrow B\right)$ , ma a Webb-féle $A\nabla B$ „sem-sem” (konnegáció) művelet.

Logikai műveletek formalizálása a fogalomírásban

Sorra véve, hogy két A,B ítélet, a tagadás és a feltételesség jeléből összekombinálva milyen logikai függvények kaphatóak, azt tapasztaljuk, hogy az összes fontos (a modern logika által számontartott) kétváltozós logikai művelet előáll Frege rendszerében.

Az alternáció előállítása

Például egyszerűen látható, hogy a „megengedő vagy”, azaz alternáció (vagy diszjunkció) művelete hogyan fejezhető ki. Mivel

├────┬───── A │ └───── B

„tagadja azt az esetet, amikor B-t állítjuk és A-t tagadjuk”, ezért ennek állítása azt jelenti, hogy B-t nem állítjuk, vagy pedig A-t nem tagadjuk. Azaz hogy B-t tagadjuk és A-t állítjuk. Ezért

├────┬───── A │ └───┬─ B

tagadja, hogy B tagadását állítjuk és A-t tagadjuk, azaz azt, hogy B-t és A-t is tagadjuk, tehát B-t nem tagadjuk vagy A-t nem tagadjuk. Ez tehát azt jelenti, hogy A-t állítjuk, vagy B-t. Ez tehát a „vagy” kötőszóval leírt diszjunkció. Mai jelölésekkel elmondva, $A\vee B\equiv \lnot B\rightarrow A$ .

Implikáció

$\vdash A\rightarrow B$ „ha … akkor …” művelet, kondicionális (vagy implikáció):

├────┬───── B │ └───── A

($A\rightarrow B\equiv \lnot \left(A\wedge \lnot B\right)$ alapján)

Exklúzió

$\vdash A|B$ „A kizárja B-t” művelet, Sheffer-művelet (exklúzió, 7. §. 1. példa):

├────┬───┬─ B │ └───── A

($A|B\equiv \lnot A\vee \lnot B\equiv \lnot \left(A\rightarrow \lnot B\right)\equiv \lnot \left(A\wedge \lnot \lnot B\right)$ $\left(\equiv \lnot \left(A\wedge B\right)\right)\$ alapján)

Alternáció

$\vdash A\vee B$ „vagy” művelet, alternáció (7. §. 2. példa):

├────┬───── B │ └───┬─ A

($A\vee B\equiv \lnot A\rightarrow B\equiv \lnot \left(\lnot A\wedge \lnot B\right)$ alapján)

Szubtrakció

$\vdash A-B$ „ … és nem … ” művelet (kivonás, szubtrakció; mely kétféleképp is kifejezhető: a 7. §. 7. példa illetve a 7. §. 8. példa szerint):

├───┬─┬───── B ├───┬─┬───┬─ B │ │ └───── A └───┬─ A

($A-B\equiv A\wedge \lnot B$ $\equiv$ $\lnot \left(A\rightarrow B\right)$, illetve $A-B\equiv A\wedge \lnot B$ $\equiv$ $\lnot \left(A\rightarrow B\right)$ alapján, láthatóan tagadása az implikációnak)

Konjunkció

$\vdash A\wedge B$ „és” művelet, konjunkció (7. §. 4. példa):

├───┬─┬───┬─ B │ └───── A

($A\wedge B\equiv \lnot \left(A\rightarrow \lnot B\right)$ alapján, láthatóan tagadása a Sheffer-műveletnek)

Webb-művelet

$\vdash A\nabla B$ „sem-sem” („Nor” vagy Webb-féle) művelet, konnegáció (7. §. 9. példa):

├───┬─┬───── B │ └───┬─ A

($A\nabla B\equiv \lnot \left(A\vee B\right)\equiv \lnot \lnot \left(\left(\lnot A\right)\wedge \lnot B\right)$ $\equiv$ $\lnot \left(\lnot A\rightarrow B\right)$ alapján, láthatóan tagadása a diszjunkciónak)

„Retrokondicionális”

Végül nézzük meg az utolsó kombinációt, amelyben két tagadás szerepel (és ezzel az összes lehetséges kombinációt megnéztük két argumentum esetében); mármost az $\vdash B\rightarrow A$ ítélet fog adódni (frege nem tárgyalja):

├────┬───┬─ B ├────┬───── A │ │ └───┬─ A └───── B

( itt $\lnot A\rightarrow \lnot B$ $\equiv$ $\lnot (\lnot A\wedge \lnot \lnot B)$ $\equiv$ $\lnot (\lnot A\wedge B)$ $\equiv$ és $B\rightarrow A$ $\equiv$ $\lnot (B\wedge \lnot A)$ $\equiv \lnot (\lnot A\wedge B)$ alapján.

Ekvivalencia művelete

Frege néhány „nem-kétargumentumú” feltételességet is megvizsgál.

$\vdash A\leftrightarrow B$ „pontosan akkor … ha …” művelet, ekvivalencia (ezt Frege nem tárgyalja):

├───┬─┬──┬─┬── A │ └── B └────┬── A └── B

($A\leftrightarrow B\equiv \lnot \left(\left(A\rightarrow \right)\rightarrow \lnot \left(B\rightarrow A\right)\right)$ alapján).

Háromargumentumú alternáció

Ezen kívül szerepel még a háromváltozós $A\vee B\vee C$ alternáció is, tehát háromváltozós műveletek is formalizálhatóak a fogalomírásban (7. §. 3. példa):

├────┬──┬──── C │ └──┬─ B └─────┬─ A

($\lnot A\rightarrow \left(\lnot B\rightarrow \lnot C\right)\equiv A\vee B\vee C$ alapján)

Antivalencia

Szerepel még a manapság $\oplus$-tel vagy $\Delta$ -val jelölt „(kizáró) diszjunkció” avagy antivalencia $\vdash A\oplus B$ művelete is, melynek a köznyelvben leginkább a „vagy … vagy …” kettős kötőszó használata feleltethető meg. Frege kétféleképp is formalizálja (7. §. 5-6. példa):

├───┬─┬──┬─┬──┬─ A ├───┬─┬──┬─┬──── A │ └──── B │ └──┬─ B ├───────── A ├───────┬─ A └───────┬─ B └───────── B

(mindkét példa az $A\oplus B$ $\equiv$ $\left(A\vee B\right)\wedge \left(\lnot A\vee \lnot B\right)$ azonosságon alapul (ez az $A\rightarrow B\ \equiv \ \lnot A\vee B$ felhasználásával látható be), mivel $\lnot \left[\ \left(\lnot B\rightarrow A\right)\rightarrow \lnot \left(B\rightarrow \lnot A\right)\ \right]$ és $\lnot \left[\ \left(B\rightarrow \lnot A\right)\rightarrow \lnot \left(\lnot B\rightarrow A\right)\ \right]$ is ezzel ekvivalens.)

Ma már tudjuk (ahogy azt fentebb említettük), hogy a fregei fogalomírás funkcionálisan teljes, azaz minden n-változós logikai művelet formalizálható benne, nem csak az itt említettek. Ez következik például abból, hogy a konjunkció és a negáció, azaz a $\lnot ,\wedge$ műveletpár funkcionálisan teljes rendszert alkot, és a fogalomírásban mindkettő formalizálható. De már a puszta Sheffer-művelet $|$ is bázisa az összes n-változós logikai műveletnek (mivel $\lnot A\equiv A|A$ alakban a negáció is kifejezhető vele), és ez is formalizálható a fogalomírásban.

A „láncformula”

A feltételesség jeléből és hasonló építőelemekből (a fogalomírás mint nyelv betűiből/szavaiból) már sok mindent lehet építeni. Például

                    ├────┬────── A
                         │
                         └──┬─── B
                            │
                            └─── C

azt az esetet tagadja, amikor

                    ├──────┬──── B
                           │
                           └──── C

-t állítják és A-t tagadják, azaz amikor tagadják azt, hogy egy időben tagadják hogy C-t állítják és B-t tagadják, valamint állítják A-t. Mai jelöléssel ezt $\vdash \ \ (C\rightarrow B)\rightarrow A$ vagy $\vdash \ \ A\vee (\lnot B\wedge C)$ formában írnánk. Megjegyezzük, hogy a Fogalomírás eredeti szövegében, amint erre Ernst Schröder egy, a könyvről írott recenziójában (1880) felhívja a figyelmet, tévedés található ezzel kapcsolatban: „… azt az esetet tagadja, amikor C-t állítják, és B-t és A-t pedig tagadják … ” szerepel. Ez és általában ezek a fajta, „balrekurzív” formulák, melyek előtagja is implikációs formula, csekély fontosságúak, például az axiómák alakjából is látható, hogy Frege előnyben részesíti a jobbrekurziót.

Fontosabbak tehát azok a „jobbrekurzív” implikációs formulák, melyek utótagja is implikáció. A legfontosabb és legegyszerűbb ilyen a következő formula, nevezzük láncformulának (Frege nem ad neki külön nevet), melyet modern jelöléssel egyébként $\vdash \ \ C\rightarrow (B\rightarrow A)$ alakba írhatnánk:

                      ├──┬───┬─── A
                         │   │
                         │   └─── B
                         │
                         └─────── C

Ennek állításával tagadjuk, hogy C állítandó s egyszersmind

                     ├──────┬──── A
                            │
                            └──── B

tagadandó. Mármost ha egy állítás tagad valamit, akkor pontosan abban az esetben hamis, ha igaz, amit tagad. Tehát azt a nehézkes fregei beszédmódot, hogy „az F ítélet tagadja, hogy G” úgy is kifejezhetjük: „az F ítélet pontosan akkor hamis, ha igaz G”. Tehát a láncformula pontosan akkor hamis, ha C igaz, és

                    ├──────┬──── A
                           │
                           └──── B 

mégis hamis, utóbbi pedig „ … tagadja, hogy …”, azaz „ … pontosan akkor hamis, ha …” B igaz és A hamis. Összegezve: a láncformula pontosan akkor hamis, ha C és B igaz és A hamis.

Mellesleg ez Frege implikációra adott definíciója értelmében megfelel az $\vdash \ \ (C\wedge B)\rightarrow A$ formulának (a fogalomírásban nem tudjuk a láncformulánál egyszerűbben felírni, mivel nincs egyszerű, elemi jel a „C és B” formulára, de mai jelölésekkel azt mondanánk, $\vdash \ \ (C\wedge B)\rightarrow A\ \equiv \ C\rightarrow (B\rightarrow A)$). Erre Frege axiómáinak szemantikai levezetésekor is hivatkozik, de a modern levezetéselméletben (Hilbert-kalkulus) még fontosabb, és szintaktikai jelentősége is van. Azt hozzá kell tennünk, Frege szerint az itt leírt ekvicalenciát az implikáció definíciója alapján „könnyű felismerni”, de bizonyítást nemigen ad rá (csak nagyon elnagyoltan, pár szóban). Megjegyezzük még, hogy a láncformula $A\vee \lnot B\vee \lnot C$ alakban is felírható.

A Fogalomírás levezetőrendszere értő használatának egyik kulcsa, hogy tudatában legyünk a formulák jobbrekurzív jellegének. Frege levezetési szabálya, a modus ponens is ilyen alakba formalizálható a modern ítéletkalkulusban: $A\rightarrow \left[\left(A\rightarrow B\right)\rightarrow B\right]$, vagyis itt is egy A→(X→B) alakú vázról van szó. Mindez azzal van kapcsolatban, hogy Frege – tudatosan vagy intuitíven – a logika formalizálásakor erősen épít a manapság Az eldöntésprobléma alaptételének nevezett tétel szintaktikus változatára.