Szerkesztő:Bbr98/Hilbert rendszere

A matematikai fizikában a Hilbert-rendszer ritkán használt kifejezés a fizikai rendszerre, amelyet egy C * -algebra ír le.

A logikában, különösen a matematikai logikában, a Hilbert-rendszer, amelyet néha Hilbert-számításnak, Hilbert-stílusú deduktív rendszernek vagy Hilbert – Ackermann-rendszernek neveznek, a formális dedukció rendszerének egy típusa, amelyet Gottlob Frege-nek és David Hilbert-nek tulajdonítanak . Ezeket a deduktív rendszereket leggyakrabban az elsőrendű logika szempontjából tanulmányozzák, de érdekesek más logikák szempontjából is.

A Hilbert-rendszerek legtöbb változata jellegzetes tapadást mutat abban, hogy kiegyensúlyozzák a logikai axiómák és a következtetési szabályok közötti kompromisszumot . A Hilbert-rendszereket a logikai axiómák nagyszámú sémájának megválasztásával és a következtetési szabályok kis csoportjával lehet jellemezni. A természetes dedukció rendszerei ellentétes irányúak, sok levonási szabályt tartalmaznak, de nagyon kevés, vagy egyáltalán nem tartalmaz axiómás sémát. A leggyakrabban vizsgált Hilbert-rendszereknek vagy csak egy következtetési szabályuk van – modus ponens, a propozíciós logikához – vagy kettő – általánosítás, a predikátum logikák kezelésére – és számos végtelen axióma séma. A propozicionális modális logika Hilbert-rendszereit általában két további szabállyal, a szükségességi és az egységes helyettesítési szabályokkal axiomatizálják.

A Hilbert-rendszerek sok változatának jellemző vonása, hogy a kontextus egyik következtetési szabályukban sem változik, míg a természetes dedukció és a szekvenciális számítás is tartalmaz néhány kontextust változtató szabályt. Tehát, ha az embert csak a tautológiák levezethetősége érdekli, nincsenek hipotetikus ítéletek, akkor a Hilbert-rendszert oly módon formalizálhatja, hogy következtetési szabályai csak meglehetősen egyszerű formájú ítéleteket tartalmaznak. Ugyanez nem tehető meg a másik két levonási rendszerrel:  mivel a következtetések egyes szabályai megváltoztatják a kontextust, ezért azokat nem lehet formalizálni, hogy elkerülhetők legyenek a hipotetikus ítéletek – akkor sem, ha csak a tautológiák levezethetőségének bizonyítására akarjuk felhasználni őket.

Formális dedukció

A dedukciós rendszer grafikus ábrázolása

A Hilbert-stílusú dedukciós rendszerben a formális dedukció egy olyan véges képletsorozat, amelyben minden képlet axióma, vagy következtetési szabály alapján az előző képletekből származik. Ezeknek a formális dedukcióknak a természetes nyelvű igazolásokat kell tükrözniük, bár sokkal részletesebbek.

Tegyük fel $\Gamma$ egy képletkészlet, amelyet hipotézisnek tekintenek. Például, $\Gamma$ lehet axiómák halmaza a csoportelmélethez vagy halmazelmélethez . A jelölés $\Gamma \vdash \phi$ azt jelenti, hogy van egy levonás, amelynek vége $\phi$ axiómákként csak logikai axiómákat és elemeket használ $\Gamma$ . Így informálisan, $\Gamma \vdash \phi$ azt jelenti, hogy $\phi$ az összes képletet feltételezve bizonyítható $\Gamma$ .

A Hilbert-stílusú dedukciós rendszereket a logikai axiómák számos sémájának alkalmazása jellemzi. Az axióma séma az axiómák végtelen halmaza, amelyet úgy kapunk, hogy valamilyen forma összes képletét egy meghatározott mintába helyettesítjük. A logikai axiómák halmaza nemcsak az ebből a mintából előállított axiómákat foglalja magában, hanem ezen axiómák egyikének általánosítását is. Egy képlet általánosítását úgy kapjuk meg, hogy nulla vagy több univerzális kvantort adunk meg a képleten; például $\forall y(\forall xPxy\to Pty)$ általánosítása $\forall xPxy\to Pty$ .

Logikai axiómák

A predikátumlogika többféle axiomatizációja létezik, mivel minden logika számára van szabadság az axiómák és szabályok kiválasztásában. Itt egy olyan Hilbert rendszert írunk le, amely kilenc axiómával és csak a szabály modus ponensel rendelkezik, amelyet egyszabályos axiomatizációnak hívunk, és amely a klasszikus egyenleti logikát írja le. A logika minimális nyelvével foglalkozunk, ahol a képletek csak az összekötőket használják $\lnot$ és $\to$ és csak a kvantor $\forall$ . Később bemutatjuk, hogyan lehet kibővíteni a rendszert további logikai kapcsolatokkal, például $\land$ és $\lor$, a levezethető képletek osztályának bővítése nélkül.

Az első négy logikai axióma séma lehetővé teszi (a modus ponensel együtt) a logikai kapcsolatok manipulálását.

P1. $\phi \to \phi$

P2. $\phi \to \left(\psi \to \phi \right)$

P3. $\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$

P4. $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$

A P1 axióma redundás, amint az a P3, P2 és a modus ponensből következik (lásd a bizonyítást ). Ezek az axiómák a klasszikus propozíciós logikát írják le; P4 axióma nélkül pozitív implikációs logikát kapunk . A minimális logikát vagy a P4m axióma hozzáadásával, vagy definiálásával érjük el $\lnot \phi$ mint $\phi \to \bot$ .

P4m. $\left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)$

Az intuíciós logikát úgy lehet elérni, hogy a pozitív implikációs logikához hozzáadjuk a P4i és a P5i axiómákat, vagy a minimális logikához a P5i axiómát adjuk. A P4i és a P5i egyaránt a klasszikus propozíciós logika tételei.

P4i. $\left(\phi \to \lnot \phi \right)\to \lnot \phi$

P5i. $\lnot \phi \to \left(\phi \to \psi \right)$

Ne feledjük, hogy ezek axiómás sémák, amelyek végtelenül sok specifikus axiómapéldányt képviselnek. Például P1 képviselheti az adott axióma példányt $p\to p$, vagy képviselheti $\left(p\to q\right)\to \left(p\to q\right)$ : a $\phi$ olyan hely, ahol bármilyen képlet elhelyezhető. Az ilyen változót, amely a képletek felett terjed, „sematikus változónak” nevezzük.

Az egységes helyettesítés második szabályával megváltoztathatjuk ezeket az axiómák sémáit egyetlen axiómává, helyettesítve az egyes sematikus változókat valamilyen olyan propozíciós változóval, amelyet egyetlen axióma sem említ, hogy megkapjuk az úgynevezett szubsztitúciós axiomatizációt. Mindkét formalizációnak vannak változói, de ahol az egyszabályos axiomatizálásnak olyan sematikus változói vannak, amelyek kívül esnek a logika nyelvén, a szubsztitúciós axiomatizálás olyan propozíciós változókat használ, amelyek ugyanazt a munkát végzik.

Legyen $\phi (p)$ képlet, a propozíciós változó egy vagy több példányával $p$, és $\psi$ legyen egy másik képlet. Aztán $\phi (p)$, következtet $\phi (\psi )$ .^[vitatott]

A következő három logikai axióma séma lehetőséget nyújt az univerzális kvantorok hozzáadására, kezelésére és eltávolítására.

Q5. $\forall x\left(\phi \right)\to \phi [x:=t]$ ahol t helyettesítheti az x- et $\,\!\phi$

Q6. $\forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)$

Q7. $\phi \to \forall x\left(\phi \right)$ ahol x nem szabad $\phi$-ben .

Ez a három további szabály kiterjeszti a javaslattételi rendszert a klasszikus állítmányi logika axiomatizálására. Hasonlóképpen, ez a három szabály kiterjeszti az intuíciós propozíciós logika rendszerét (P1-3, P4i és P5i esetén) az intuíciós predikátum logikára .

Az univerzális kvantifikációnak gyakran alternatív axiomatizálást adnak egy általánosítás általános szabályának alkalmazásával (lásd a Metatoreoremek című részt), amely esetben a Q6 és Q7 szabályok feleslegesek.^[vitatott]

A végső axióma sémáknak az egyenlőség szimbólumot tartalmazó képletekkel kell dolgozniuk.

I8. $x=x$ minden x változóra.

I9. $\left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)$

Konzervatív kiterjesztések

A Hilbert-stílusú dedukciós rendszerbe általában csak axiómákat vonnak be implikáció és tagadás céljából. Ezeknek az axiómáknak a figyelembevételével lehetséges a dedukciós tétel konzervatív kiterjesztése, amely lehetővé teszi további kapcsolatok használatát. Ezeket a kiterjesztéseket azért hívjuk konzervatívnak, mert ha egy új összekötőket magában foglaló formula képletet logikailag ekvivalens képletként írunk át θ, amely csak negációt, implikációt és univerzális kvantifikációt tartalmaz, akkor a φ a kibővített rendszerben csak akkor levezethető, ha θ levezethető az eredeti rendszerben . Teljesen kibővítve a Hilbert-stílusú rendszer jobban hasonlít a természetes dedukció rendszerére.

Egzisztenciális számszerűsítés

• Bevezetés

$\forall x(\phi \to \exists y(\phi [x:=y]))$

• Megszüntetés

$\forall x(\phi \to \psi )\to \exists x(\phi )\to \psi$ hol $x$ nem szabad változója $\psi$ -nek.

Konjunkció és diszjunkció

• A konjunkció bevezetése és megszüntetése

bevezetés: $\alpha \to \beta \to \alpha \land \beta$

kiesés bal: $\alpha \wedge \beta \to \alpha$

kiküszöbölési jobb: $\alpha \wedge \beta \to \beta$

• A diszjunkció bevezetése és megszüntetése

bevezető bal: $\alpha \to \alpha \vee \beta$

bevezető jobb: $\beta \to \alpha \vee \beta$

megszüntetés: $(\alpha \to \gamma )\to (\beta \to \gamma )\to \alpha \vee \beta \to \gamma$

Metatételek

Mivel a Hilbert-stílusú rendszerek nagyon kevés levonási szabályt tartalmaznak, gyakran bizonyítanak olyan metatételeket, amelyek azt mutatják, hogy a további levonási szabályok nem adnak deduktív erőt abban az értelemben, hogy az új levonási szabályokat használó dedukció csak az eredeti dedukció szabállyal konvertálható dedukcióvá.

Ennek a formának néhány általános metatételei:

• A levonási tétel : $\Gamma ;\phi \vdash \psi$ akkor, és csak akkor ha $\Gamma \vdash \phi \to \psi$ .
• $\Gamma \vdash \phi \leftrightarrow \psi$ akkor, és csak akkor ha $\Gamma \vdash \phi \to \psi$ és $\Gamma \vdash \psi \to \phi$ .
• Ellentét: Ha $\Gamma ;\phi \vdash \psi$ akkor $\Gamma ;\lnot \psi \vdash \lnot \phi$ .
• Általánosítás : Ha $\Gamma \vdash \phi$ és x nem fordul elő szabadon a (z) $\Gamma$ akkor $\Gamma \vdash \forall x\phi$ .

Néhány hasznos tétel és azok igazolása

Az alábbiakban a tételes logika számos tétele szerepel a bizonyításukkal (vagy más cikkekben ezekre a bizonyításokra mutató linkekkel). Megjegyezzük, hogy mivel maga a (P1) bizonyítható a többi axióma felhasználásával, valójában (P2), (P3) és (P4) elegendő mindezek a tételek bizonyításához.

(HS1) $(q\to r)\to ((p\to q)\to (p\to r))$ - Hipotetikus szillogizmus, lásd a bizonyítást .

(L1) $p\to ((p\to q)\to q)$ - igazolás:

(1) $((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))$   ((P3) példánya)

(2) $(p\to q)\to (p\to q)$   ((P1) példánya)

(3) $((p\to q)\to p)\to ((p\to q)\to q)$   (a (2) és (1) -től modus ponens által )

(4) $(((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))$   (a (HS1) példánya)

(5) $(p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))$   (a (3) és (4) pontról modus ponens által)

(6) $p\to ((p\to q)\to p)$   (a (P2) példánya)

(7) $p\to ((p\to q)\to q)$   (a (6) és (5) -től modus ponens által)

A következő két tétel kettős tagadásként ismert:

(DN1) $\neg \neg p\to p$

(DN2) $p\to \neg \neg p$

Lásd a bizonyításokat .

(L2) $(p\to (q\to r))\to (q\to (p\to r))$ - ehhez a bizonyításhoz a hipotetikus szillogizmus metatoreor módszerét rövidítésként használjuk több bizonyítási lépésnél:

(1) $(p\to (q\to r))\to ((p\to q)\to (p\to r))$   ((P3) példánya)

(2) $((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$   (a (HS1) példánya)

(3) $(p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$   (az (1) és (2) pontokból a hipotetikus szillogizmus metatéma segítségével

(4) $((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))$   ((P3) példánya)

(5) $((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))$   (a (3) és (4) -ből modus ponens használatával)

(6) $q\to (p\to q)$   (a (P2) példánya)

(7) $(q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))$   (a (P2) példánya)

(8) $(p\to (q\to r))\to (q\to (p\to q))$   (a (6) és (7) -ből modus ponens használatával)

(9) $(p\to (q\to r))\to (q\to (p\to r))$   (a (8) és (5) -ből modus ponens használatával)

(HS2) $(p\to q)\to ((q\to r)\to (p\to r))$ - a hipotetikus szillogizmus alternatív formája. bizonyítás:

(1) $(q\to r)\to ((p\to q)\to (p\to r))$   (a (HS1) példánya)

(2) $((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))$   ((L2) példánya)

(3) $(p\to q)\to ((q\to r)\to (p\to r))$ (az (1) és (2) pontról modus ponens)

(TR1) $(p\to q)\to (\neg q\to \neg p)$ - Áthelyezés, lásd a bizonyítást (a másik áthelyezés irány (P4)).

(TR2) $(\neg p\to q)\to (\neg q\to p)$ - az áthelyezés másik formája; bizonyíték:

(1) $(\neg p\to q)\to (\neg q\to \neg \neg p)$   (a (TR1) példánya)

(2) $\neg \neg p\to p$   ((DN1) példánya)

(3) $(\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))$   (a (HS1) példánya)

(4) $(\neg q\to \neg \neg p)\to (\neg q\to p)$   (a (2) és (3) ponttól modus ponens)

(5) $(\neg p\to q)\to (\neg q\to p)$   (az (1) és (4) -ből a hipotetikus szillogizmus metatéma segítségével

(L3) $(\neg p\to p)\to p$ - bizonyítás:

(1) $\neg p\to (\neg \neg (q\to q)\to \neg p)$   (a (P2) példánya)

(2) $(\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))$   (a (P4) példánya)

(3) $\neg p\to (p\to \neg (q\to q))$   (az (1) és (2) pontokból a hipotetikus szillogizmus metatéma segítségével

(4) $(\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))$   ((P3) példánya)

(5) $(\neg p\to p)\to (\neg p\to \neg (q\to q))$   (a (3) és (4) modes ponens használatával)

(6) $(\neg p\to \neg (q\to q))\to ((q\to q)\to p)$   (a (P4) példánya)

(7) $(\neg p\to p)\to ((q\to q)\to p)$   (az (5) és (6) pontokból a hipotetikus szillogizmus metatéma segítségével)

(8) $q\to q$   ((P1) példánya)

(9) $(q\to q)\to (((q\to q)\to p)\to p)$   ((L1) példánya)

(10) $((q\to q)\to p)\to p$   (a (8) és (9) mods ponens használatával)

(11) $(\neg p\to p)\to p$   (a (7) és (10) -ből a hipotetikus szillogizmus metatéma segítségével

Alternatív axiomatizációk

A fenti 3. axióma Łukasiewicz nevéhez fűződik . A Frege eredeti rendszerének P2 és P3 axiómái voltak, de a P4 axióma helyett négy másik axióma volt (lásd Frege propozíciós számítását ). Russell és Whitehead szintén öt felvetési axiómával rendelkező rendszert javasolt.

További csatlakozások

A P1, P2 és P3 axiómák, a modus ponens dedukciós szabállyal (az intuicionista propozíciós logika formalizálása) megfelelnek az I, K és S kombinációs logikai alapkombinátoroknak az alkalmazás operátorral. A Hilbert-rendszer bizonyítékai ezután megfelelnek a kombinatorikus logika kombinátorának. Lásd még Curry – Howard levelezést .

Lásd még

• A Hilbert rendszerek listája
• Természetes dedukció

Hivatkozások

• Curry, Haskell B.. Combinatory Logic Vol. I. Amsterdam: North Holland (1958) 
• Monk, J. Donald. Mathematical Logic, Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag (1976). ISBN 978-0-387-90170-1 978-0-387-90170-1
• Ruzsa, Imre. Bevezetés a modern logikába (hungarian nyelven). Budapest: Osiris Kiadó (1997) 
• Tarski, Alfred. Bizonyítás és igazság (hungarian nyelven). Budapest: Gondolat (1990)  Ez Alfred Tarski válogatott tanulmányainak szemantikai igazságelméleti magyar fordítása.
• David Hilbert (1927) "A matematika alapjai", fordította Stephan Bauer-Menglerberg és Dagfinn Føllesdal (pp. 464 – 479). ban ben:
  • van Heijenoort, Jean. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, 3rd printing 1976, Cambridge MA: Harvard University Press (1967). ISBN 0-674-32449-8 0-674-32449-8
  • Hilbert 1927, alapján egy korábbi 1925 "alapjait" előadás (pp. – bemutatja a 17 axiómák - axiómái hallgatólagosan # 1-4, axiómák & és V # 5-10, axiómák a tagadás # 11- 12, logikai ε-axiómája # 13, egyenlőség axiomai # 14-15 és a # 16-17 szám axiómái - a formalistai "bizonyítási elmélet" többi szükséges elemével együtt - pl. Indukciós axiómák, rekurziós axiómák, stb; lelkes védekezést kínál fel LEJ Brouwer intuíciója ellen is. Lásd még: Hermann Weyl (1927) megjegyzések és az ellenérvek (pp. – Paul Bernay féle (1927) függelékében Hilbert előadás (pp. – valamint Luitzen Egbertus Jan Brouwer (1927) válasz (pp. –
• Kleene, Stephen Cole. Introduction to Metamathematics, 10th impression with 1971 corrections, Amsterdam NY: North Holland Publishing Company (1952). ISBN 0-7204-2103-9 0-7204-2103-9
  • Lásd különösen IV formális rendszer (pp. – ahol Kleene bemutatja alfejezetekben §16 Formai szimbólumok, 17.§ Formation szabályok, 18.§ Szabad és kötött változók (beleértve a szubsztitúció), 19. § transzformációs szabályok (pl Modus ponens) - és ezek közül 21 "posztulátumot" - 18 axiómát és 3 "azonnali következmény" relációt mutat be az alábbiak szerint: Postulátumok az # 1-8 propozíciós számításhoz, További posztulátumok a # 9-12 predikátum kalkulációhoz és További posztulátumok a következőhöz: számelmélet # 13-21.

Külső linkek

• Gaifman: A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness. (pdf)
• Farmer: Propositional logic (pdf) It describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).

[[Kategória:Lapok ellenőrizetlen fordításokkal]]