Seznam systémů Hilbert - List of Hilbert systems

Tento článek obsahuje seznam ukázkových deduktivních systémů Hilbertova stylu pro výrokovou logiku .

Klasické výrokové systémy

Klasický výrokový kalkul je standardní výroková logika. Jeho zamýšlená sémantika je bivalentní a jeho hlavní vlastností je, že je silně úplná , jinak se říká, že kdykoli vzorec sémanticky vyplývá ze sady prostor sémanticky, vyplývá také z této sady syntakticky. Bylo formulováno mnoho různých ekvivalentních úplných systémů axiomu. Liší se výběrem použitých základních spojek , které musí být ve všech případech funkčně úplné (tj. Schopné vyjádřit složením všechny n -ary pravdivostní tabulky ), a přesným úplným výběrem axiomů nad zvoleným základem spojek.

Důsledky a negace

Formulace zde používají implikaci a negaci jako funkčně kompletní sadu základních spojek. Každý logický systém vyžaduje alespoň jedno pravidlo nullary odvození . Klasický výrokový kalkul obvykle používá pravidlo modus ponens : ${\ displaystyle \ {\ to, \ neg \}}$

${\ displaystyle A, A \ až B \ vdash B.}$

Předpokládáme, že toto pravidlo je zahrnuto ve všech níže uvedených systémech, pokud není uvedeno jinak.

Fregeův axiomový systém:

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až (B \ až C)) \ až ((A \ až B) \ až (A \ až C))}$

${\ displaystyle (A \ až B) \ až (\ neg B \ až \ neg A)}$

${\ displaystyle \ neg \ neg A \ až A}$

${\ displaystyle A \ až \ neg \ neg A}$

Hilbertův axiomový systém:

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až (B \ až C)) \ až (B \ až (A \ až C))}$

${\ Displaystyle (B \ až C) \ až ((A \ až B) \ až (A \ až C))}$

${\ displaystyle A \ to (\ neg A \ až B)}$

${\ displaystyle (A \ až B) \ až ((\ neg A \ až B) \ až B)}$

Łukasiewiczovy axiomové systémy:

• První:

  ${\ displaystyle (A \ až B) \ až ((B \ až C) \ až (A \ až C))}$

  ${\ displaystyle (\ neg A \ na A) \ na A}$

  ${\ displaystyle A \ to (\ neg A \ až B)}$

• Druhý:

  ${\ displaystyle ((A \ až B) \ až C) \ až (\ neg A \ až C)}$

  ${\ displaystyle ((A \ až B) \ až C) \ až (B \ až C)}$

  ${\ displaystyle (\ neg A \ až C) \ až ((B \ až C) \ až ((A \ až B) \ až C))}$

• Třetí:

  ${\ displaystyle A \ do (B \ do A)}$

  ${\ displaystyle (A \ až (B \ až C)) \ až ((A \ až B) \ až (A \ až C))}$

  ${\ displaystyle (\ neg A \ až \ neg B) \ až (B \ až A)}$

• Čtvrtý:

  ${\ displaystyle (A \ až B) \ až ((B \ až C) \ až (A \ až C))}$

  ${\ displaystyle A \ to (\ neg A \ až B)}$

  ${\ displaystyle (\ neg A \ až B) \ až ((B \ až A) \ až A)}$

Łukasiewicz a Tarskiho axiomový systém:

${\ Displaystyle [(A \ až (B \ až A)) \ \ ([(\ neg C \ až (D \ až \ neg E)) \ až [(C \ až (D \ až F)) \ ((E \ to D) \ to (E \ to F))]] \ to G)] \ to (H \ to G)}$

Meriomův axiomový systém:

${\ Displaystyle (((((A \ až B) \ až (\ neg C \ až \ neg D)) \ až C) \ až E) \ až ((E \ až A) \ až (D \ až A) )}$

Mendelsonův axiomový systém:

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až (B \ až C)) \ až ((A \ až B) \ až (A \ až C))}$

${\ displaystyle (\ neg A \ až \ neg B) \ až ((\ neg A \ až B) \ až A)}$

Russellův axiomový systém:

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až B) \ až ((B \ až C) \ až (A \ až C))}$

${\ displaystyle (A \ až (B \ až C)) \ až (B \ až (A \ až C))}$

${\ displaystyle \ neg \ neg A \ až A}$

${\ displaystyle (A \ to \ neg A) \ to \ neg A}$

${\ displaystyle (A \ to \ neg B) \ to (B \ to \ neg A)}$

Sobiocińského axiomové systémy:

• První:

  ${\ displaystyle \ neg A \ do (A \ do B)}$

  ${\ displaystyle A \ do (B \ do (C \ do A))}$

  ${\ displaystyle (\ neg A \ až C) \ až ((B \ až C) \ až ((A \ až B) \ až C))}$

• Druhý:

  ${\ displaystyle (A \ až B) \ až (\ neg B \ až (A \ až C))}$

  ${\ displaystyle A \ do (B \ do (C \ do A))}$

  ${\ displaystyle (\ neg A \ až B) \ až ((A \ až B) \ až B)}$

Implikace a falsum

Namísto negace lze klasickou logiku formulovat také pomocí funkčně kompletní sady spojek. ${\ displaystyle \ {\ to, \ bot \}}$

Tarski– Bernays - Wajsbergův axiomový systém:

${\ displaystyle (A \ až B) \ až ((B \ až C) \ až (A \ až C))}$

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle ((A \ k B) \ k A) \ k A}$

${\ displaystyle \ bot \ do A}$

Církevní axiomový systém:

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až (B \ až C)) \ až ((A \ až B) \ až (A \ až C))}$

${\ displaystyle ((A \ to \ bot) \ to \ bot) \ to A}$

Meriomovy axiomové systémy:

• První:

  ${\ Displaystyle (((((A \ až B) \ až (C \ až \ bot)) \ až D) \ až E) \ až ((E \ až A) \ až (C \ až A))}$

• Druhý:

  ${\ displaystyle ((A \ až B) \ až ((\ bot \ až C) \ až D)) \ až ((D \ až A) \ až (E \ až (F \ až A)))}$

Negace a disjunkce

Namísto implikace lze klasickou logiku formulovat také pomocí funkčně kompletní sady spojek. Tyto formulace používají následující pravidlo závěru; ${\ displaystyle \ {\ neg, \ lor \}}$

${\ displaystyle A, \ neg A \ lor B \ vdash B.}$

Systém axiomu Russell – Bernays:

${\ Displaystyle \ neg (\ neg B \ lor C) \ lor (\ neg (A \ lor B) \ lor (A \ lor C))}$

${\ displaystyle \ neg (A \ lor B) \ lor (B \ lor A)}$

${\ displaystyle \ neg A \ lor (B \ lor A)}$

${\ displaystyle \ neg (A \ lor A) \ lor A}$

Meriomovy axiomové systémy:

• První:

  ${\ Displaystyle \ neg (\ neg (\ neg A \ lor B) \ lor (C \ lor (D \ lor E))) \ lor (\ neg (\ neg D \ lor A) \ lor (C \ lor ( E \ lor A)))}$

• Druhý:

  ${\ Displaystyle \ neg (\ neg (\ neg A \ lor B) \ lor (C \ lor (D \ lor E))) \ lor (\ neg (\ neg E \ lor D) \ lor (C \ lor ( A \ lor D)))}$

• Třetí:

  ${\ Displaystyle \ neg (\ neg (\ neg A \ lor B) \ lor (C \ lor (D \ lor E))) \ lor (\ neg (\ neg C \ lor A) \ lor (E \ lor ( D \ lor A)))}$

Dvojí klasickou výrokovou logiku lze definovat pouze pomocí konjunkce a negace.

Shefferova mrtvice

Protože Shefferův tah (známý také jako operátor NAND) je funkčně úplný , lze jej použít k vytvoření celé formulace výrokového počtu. Formulace NAND používají pravidlo odvození zvané Nicod 's modus ponens:

${\ displaystyle A, A \ mid (B \ mid C) \ vdash C.}$

Nicodův axiomový systém:

${\ displaystyle (A \ mid (B \ mid C)) \ mid [(E \ mid (E \ mid E)) \ mid ((D \ mid B) \ mid [(A \ mid D) \ mid (A \ mid D)])]}}$

Łukasiewiczovy axiomové systémy:

• První:

  ${\ displaystyle (A \ mid (B \ mid C)) \ mid [(D \ mid (D \ mid D)) \ mid ((D \ mid B) \ mid [(A \ mid D) \ mid (A \ mid D)])]}}$

• Druhý:

  ${\ displaystyle (A \ mid (B \ mid C)) \ mid [(A \ mid (C \ mid A)) \ mid ((D \ mid B) \ mid [(A \ mid D) \ mid (A \ mid D)])]}}$

Wajsbergův axiomový systém:

${\ displaystyle (A \ mid (B \ mid C)) \ mid [((D \ mid C) \ mid [(A \ mid D) \ mid (A \ mid D)]) \ mid (A \ mid ( A \ mid B))]}$

Axgonové systémy Argonne :

• První:

${\ displaystyle (A \ mid (B \ mid C)) \ mid [(A \ mid (B \ mid C)) \ mid ((D \ mid C) \ mid [(C \ mid D) \ mid (A \ mid D)])]}}$

• Druhý:

${\ displaystyle (A \ mid (B \ mid C)) \ mid [([((B \ mid D) \ mid (A \ mid D)] \ mid (D \ mid B)) \ mid ((C \ mid B) \ střední A)]}$

Počítačová analýza společnosti Argonne odhalila> 60 dalších systémů s jednou axiomy, které lze použít k formulování výrokového počtu NAND.

Implikační výrokový počet

Implicational výrokové je fragment klasické výrokové logiky, která pouze připouští implikace pojivové. Není funkčně úplný (protože mu chybí schopnost vyjádřit faleš a negaci), ale je syntakticky úplný . Níže uvedené implicitní kameny používají modus ponens jako pravidlo odvození.

Bernays – Tarskiho axiomový systém:

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až B) \ až ((B \ až C) \ až (A \ až C))}$

${\ displaystyle ((A \ k B) \ k A) \ k A}$

Łukasiewicz a Tarskiho axiomové systémy:

• První:

  ${\ displaystyle [(A \ až (B \ až A)) \ až [([((C \ až D) \ až E) \ až F] \ až [(D \ až F) \ až (C \ to F)]) \ do G]] \ do G}$

• Druhý:

  ${\ Displaystyle [(A \ až B) \ až ((C \ až D) \ až E)] \ až ([F \ až ((C \ až D) \ až E)] \ až [(A \ až F) \ do (D \ do E)])}$

• Třetí:

  ${\ displaystyle ((A \ až B) \ až (C \ až D)) \ až (E \ až ((D \ až A) \ až (C \ až A)))}$

• Čtvrtý:

  ${\ displaystyle ((A \ až B) \ až (C \ až D)) \ až ((D \ až A) \ až (E \ až (C \ až A)))}$

Łukasiewiczův axiomový systém:

${\ displaystyle ((A \ až B) \ až C) \ až ((C \ až A) \ až (D \ až A))}$

Intuicionistická a střední logika

Intuicionistická logika je subsystém klasické logiky. Obvykle je formulován jako sada (funkčně úplných) základních spojek. Není syntakticky úplný, protože postrádá vyloučený střední A∨¬A nebo Peirceův zákon ((A → B) → A) → A, který lze přidat, aniž by byla logika nekonzistentní. Jako pravidlo odvození má modus ponens a následující axiomy: ${\ displaystyle \ {\ to, \ land, \ lor, \ bot \}}$

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až (B \ až C)) \ až ((A \ až B) \ až (A \ až C))}$

${\ displaystyle (A \ land B) \ do A}$

${\ displaystyle (A \ land B) \ až B}$

${\ displaystyle A \ to (B \ to (A \ land B))}$

${\ displaystyle A \ to (A \ lor B)}$

${\ displaystyle B \ to (A \ lor B)}$

${\ displaystyle (A \ až C) \ až ((B \ až C) \ až ((A \ lor B) \ až C))}$

${\ displaystyle \ bot \ do A}$

Alternativně lze intuicionistickou logiku axiomatizovat pomocí sady základních spojek, přičemž poslední axiom nahradíme ${\ displaystyle \ {\ to, \ land, \ lor, \ neg \}}$

${\ displaystyle (A \ to \ neg A) \ to \ neg A}$

${\ displaystyle \ neg A \ do (A \ do B)}$

Střední logika je mezi intuitivní logikou a klasickou logikou. Zde je několik intermediálních logik:

• Jankovova logika (KC) je rozšířením intuitivní logiky, kterou lze axiomatizovat intuitivním axiomatickým systémem plus axiomem

${\ displaystyle \ neg A \ lor \ neg \ neg A.}$

• Gödel – Dummettovu logiku (LC) lze axiomatizovat nad intuitivní logikou přidáním axiomu

${\ displaystyle (A \ až B) \ lor (B \ až A).}$

Pozitivní implikační počet

Pozitivní implikační kalkul je implikačním fragmentem intuicionistické logiky. Níže uvedené kameny používají modus ponens jako pravidlo odvození.

Łukasiewiczův axiomový systém:

${\ displaystyle A \ do (B \ do A)}$

${\ displaystyle (A \ až (B \ až C)) \ až ((A \ až B) \ až (A \ až C))}$

Meriomovy axiomové systémy:

• První:

  ${\ Displaystyle E \ to ((A \ až B) \ až (((D \ až A) \ až (B \ až C)) \ až (A \ až C)))}$

• Druhý:

  ${\ displaystyle A \ do (B \ do A)}$

  ${\ displaystyle (A \ až B) \ až ((A \ až (B \ až C)) \ až (A \ až C))}$

• Třetí:

  ${\ displaystyle ((A \ až B) \ až C) \ až (D \ až ((B \ až (C \ až E)) \ až (B \ až E)))}$

Hilbertovy axiomové systémy:

• První:

  ${\ displaystyle (A \ až (A \ až B)) \ až (A \ až B)}$

  ${\ Displaystyle (B \ až C) \ až ((A \ až B) \ až (A \ až C))}$

  ${\ displaystyle (A \ až (B \ až C)) \ až (B \ až (A \ až C))}$

  ${\ displaystyle A \ do (B \ do A)}$

• Druhý:

  ${\ displaystyle (A \ až (A \ až B)) \ až (A \ až B)}$

  ${\ displaystyle (A \ až B) \ až ((B \ až C) \ až (A \ až C))}$

  ${\ displaystyle A \ do (B \ do A)}$

• Třetí:

  ${\ displaystyle A \ až A}$

  ${\ displaystyle (A \ až B) \ až ((B \ až C) \ až (A \ až C))}$

  ${\ Displaystyle (B \ až C) \ až ((A \ až B) \ až (A \ až C))}$

  ${\ displaystyle (A \ až (A \ až B)) \ až (A \ až B)}$

Pozitivní výrokový počet

Pozitivní výrokový kalkul je fragment intuicionistické logiky využívající pouze (nefunkčně úplné) spojky . Může být axiomatizován kterýmkoli z výše uvedených kalkulů pro pozitivní implikační kalkul spolu s axiomy ${\ displaystyle \ {\ to, \ land, \ lor \}}$

${\ displaystyle (A \ land B) \ do A}$

${\ displaystyle (A \ land B) \ až B}$

${\ displaystyle A \ to (B \ to (A \ land B))}$

${\ displaystyle A \ to (A \ lor B)}$

${\ displaystyle B \ to (A \ lor B)}$

${\ displaystyle (A \ až C) \ až ((B \ až C) \ až ((A \ lor B) \ až C))}$

Případně můžeme zahrnout také spojovací a axiomy ${\ displaystyle \ leftrightarrow}$

${\ displaystyle (A \ leftrightarrow B) \ to (A \ to B)}$

${\ displaystyle (A \ leftrightarrow B) \ to (B \ až A)}$

${\ displaystyle (A \ až B) \ do ((B \ do A) \ do (A \ levá šipka B))}$

Johansson je minimální logika může být axiomatized některou z axiomu systémů pro pozitivní výrokové logiky a rozšiřuje svůj jazyk s nullary pojivových , bez dalších axiom schémata. Alternativně jej lze také axiomatizovat v jazyce rozšířením kladného výrokového počtu o axiom ${\ displaystyle \ bot}$${\ displaystyle \ {\ to, \ land, \ lor, \ neg \}}$

${\ displaystyle (A \ to \ neg B) \ to (B \ to \ neg A)}$

nebo dvojice axiomů

${\ displaystyle (A \ až B) \ až (\ neg B \ až \ neg A)}$

${\ displaystyle A \ až \ neg \ neg A}$

Intuicionistickou logiku v jazyce s negací lze axiomatizovat nad kladným počtem dvojicí axiomů

${\ displaystyle (A \ to \ neg B) \ to (B \ to \ neg A)}$

${\ displaystyle \ neg A \ do (A \ do B)}$

nebo dvojice axiomů

${\ displaystyle (A \ to \ neg A) \ to \ neg A}$

${\ displaystyle \ neg A \ do (A \ do B)}$

Klasickou logiku v jazyce lze získat z pozitivního výrokového počtu přidáním axiomu ${\ displaystyle \ {\ to, \ land, \ lor, \ neg \}}$

${\ displaystyle (\ neg A \ až \ neg B) \ až (B \ až A)}$

nebo dvojice axiomů

${\ displaystyle (A \ to \ neg B) \ to (B \ to \ neg A)}$

${\ displaystyle \ neg \ neg A \ až A}$

Fitchův kalkul bere některý ze systémů axiomu pro kladný výrokový kalkul a přidává axiomy

${\ displaystyle \ neg A \ do (A \ do B)}$

${\ displaystyle A \ leftrightarrow \ neg \ neg A}$

${\ displaystyle \ neg (A \ lor B) \ leftrightarrow (\ neg A \ land \ neg B)}$

${\ displaystyle \ neg (A \ land B) \ leftrightarrow (\ neg A \ lor \ neg B)}$

Všimněte si, že první a třetí axiomy jsou také platné v intuicionistické logice.

Ekvivalenční počet

Ekvivalenční počet je subsystém klasického výrokového počtu, který umožňuje pouze (funkčně neúplné) ekvivalenční pojivo, zde označené jako . Pravidlo odvození použité v těchto systémech je následující: ${\ displaystyle \ equiv}$

${\ displaystyle A, A \ equiv B \ vdash B}$

Isékiho axiomový systém:

${\ displaystyle ((A \ equiv C) \ equiv (B \ equiv A)) \ equiv (C \ equiv B)}$

${\ displaystyle (A \ equiv (B \ equiv C)) \ equiv ((A \ equiv B) \ equiv C)}$

Systém axiomů Iséki – Arai:

${\ displaystyle A \ equiv A}$

${\ displaystyle (A \ equiv B) \ equiv (B \ equiv A)}$

${\ displaystyle (A \ ekviv B) \ ekviv ((B \ ekviv C) \ ekviv (A \ ekviv C))}$

Araiovy axiomové systémy;

• První:

  ${\ displaystyle (A \ equiv (B \ equiv C)) \ equiv ((A \ equiv B) \ equiv C)}$

  ${\ displaystyle ((A \ equiv C) \ equiv (B \ equiv A)) \ equiv (C \ equiv B)}$

• Druhý:

  ${\ displaystyle (A \ equiv B) \ equiv (B \ equiv A)}$

  ${\ displaystyle ((A \ equiv C) \ equiv (B \ equiv A)) \ equiv (C \ equiv B)}$

Łukasiewiczovy axiomové systémy:

• První:

  ${\ displaystyle (A \ ekviv B) \ ekviv ((C \ ekviv B) \ ekviv (A \ ekviv C))}$

• Druhý:

  ${\ displaystyle (A \ ekviv B) \ ekviv ((A \ ekviv C) \ ekviv (C \ ekviv B))}$

• Třetí:

  ${\ displaystyle (A \ equiv B) \ equiv ((C \ equiv A) \ equiv (B \ equiv C))}$

Meriomovy axiomové systémy:

• První:

  ${\ displaystyle ((A \ ekviv B) \ ekviv C) \ ekviv (B \ ekviv (C \ ekv. A))}$

• Druhý:

  ${\ displaystyle A \ equiv ((B \ equiv (A \ equiv C)) \ equiv (C \ equiv B))}$

• Třetí:

  ${\ displaystyle (A \ ekviv (B \ ekviv C)) \ ekviv (C \ ekviv (A \ ekviv B))}$

• Čtvrtý:

  ${\ displaystyle (A \ ekviv B) \ ekviv (C \ ekviv ((B \ ekviv C) \ ekviv A))}$

• Pátý:

  ${\ displaystyle (A \ ekviv B) \ ekviv (C \ ekviv ((C \ ekviv B) \ ekviv A))}$

• Šestý:

  ${\ displaystyle ((A \ equiv (B \ equiv C)) \ equiv C) \ equiv (B \ equiv A)}$

• Sedmý:

  ${\ displaystyle ((A \ equiv (B \ equiv C)) \ equiv B) \ equiv (C \ equiv A)}$

Kalmanův axiomový systém:

${\ displaystyle A \ equiv ((B \ equiv (C \ equiv A)) \ equiv (C \ equiv B))}$

Winkerovy axiomové systémy:

• První:

  ${\ displaystyle A \ equiv ((B \ equiv C) \ equiv ((A \ equiv C) \ equiv B))}$

• Druhý:

  ${\ displaystyle A \ equiv ((B \ equiv C) \ equiv ((C \ equiv A) \ equiv B))}$

XCB axiomový systém:

${\ displaystyle A \ equiv (((A \ equiv B) \ equiv (C \ equiv B)) \ equiv C)}$

Viz také

• Parakonzistentní logika § Zahrnuto - seznam schémat axiomu pro parakonzistentní logiku Hilbertova stylu

Reference