Uvolní výrokový počet - Freges propositional calculus - Wikipedia

Tento článek má několik problémů. Prosím pomozte vylepši to nebo diskutovat o těchto otázkách na internetu diskusní stránka. (Zjistěte, jak a kdy tyto zprávy ze šablony odebrat) Tento článek obsahuje a seznam doporučení, související čtení nebo externí odkazy, ale její zdroje zůstávají nejasné, protože jí chybí vložené citace. Prosím pomozte zlepšit tento článek představuji přesnější citace. (Říjen 2019) (Zjistěte, jak a kdy odstranit tuto zprávu šablony) tento článek případně obsahuje původní výzkum. Prosím vylepši to podle ověřování vznesené nároky a přidání vložené citace. Výroky sestávající pouze z původního výzkumu by měly být odstraněny. (Říjen 2019) (Zjistěte, jak a kdy odstranit tuto zprávu šablony) (Zjistěte, jak a kdy odstranit tuto zprávu šablony)

v matematická logika, Fregeův výrokový počet byl první axiomatizace z výrokový kalkul. To bylo vynalezeno Gottlob Frege, který také vynalezl predikátový počet, v roce 1879 jako součást jeho predikátový počet druhého řádu (Ačkoli Charles Peirce jako první použil výraz „druhého řádu“ a nezávisle na Frege vyvinul vlastní verzi predikátového počtu.

Využívá pouze dva logické operátory: implikaci a negaci a je tvořen šesti axiomy a jeden pravidlo odvození: modus ponens.

Fregeův výrokový počet je ekvivalentní jakémukoli jinému klasickému výrokovému počtu, jako je „standardní PC“ s 11 axiomy. Fregeovo PC a standardní PC sdílejí dva společné axiomy: THEN-1 a THEN-2. Všimněte si, že axiomy THEN-1 až THEN-3 využívají (a definují) pouze implikační operátor, zatímco axiomy FRG-1 až FRG-3 definují operátor negace.

Následující věty se zaměří na nalezení zbývajících devíti axiomů standardního PC v „prostoru věty“ Fregeova PC, což ukazuje, že teorie standardního PC je obsažena v teorii Fregeova PC.

(Teorie, zde také nazývaná pro obrazové účely „prostor vět“, je množina vět, které jsou podmnožinou univerzální množiny dobře formulované vzorce. Věty jsou vzájemně propojeny přímým způsobem pomocí odvozovací pravidla, tvořící jakousi dendritickou síť. V kořenech prostoru věty se nacházejí axiomy, které „generují“ prostor věty podobně jako generující sada generuje skupinu.)

Pravidla

Věty

Poznámka: ¬ (A → ¬B) → A (TH4), ¬ (A → ¬B) → B (TH6) a A → (B → ¬ (A → ¬B)) (TH10), takže ¬ (A → ¬B) se chová stejně jako A∧B (ve srovnání s axiomy AND-1, AND-2 a AND-3).

TH11 je axiom NOT-1 standardního PC, nazývaný „reductio ad absurdum ".

Věta TH15 je konverzovat axiomu PAK-2.

Porovnejte TH17 s větou TH5.

Poznámka: A → ((A → B) → B) (TH8), B → ((A → B) → B) (TH9) a (A → C) → ((B → C) → (((A → B) → B) → C)) (TH19), takže ((A → B) → B) se chová stejně jako A∨B. (Porovnejte s axiomy OR-1, OR-2 a OR-3.)

TH20 odpovídá axiomu NOT-3 standardního PC, tzv.tertium non datur ".

TH21 odpovídá axiomu NOT-2 standardního PC s názvem "ex contradictione quodlibet ".

Všechny axiomy standardního PC byly odvozeny z Fregeova PC poté, co byly ponechány

A∧B: = ¬ (A → ¬B) a A∨B: = (A → B) → B. Tyto výrazy nejsou jedinečné, např. A∨B mohl být také definován jako (B → A) → A, ¬A → B nebo ¬B → A. Všimněte si však, že definice A∨B: = (A → B) → B neobsahuje žádná negace. Na druhou stranu A∧B nelze definovat pouze z hlediska implikace bez použití negace.

V jistém smyslu lze výrazy A∧B a A∨B považovat za „černé skříňky“. Uvnitř tyto černé skříňky obsahují vzorce složené pouze z implikace a negace. Černé skříňky mohou obsahovat cokoli, pokud však při zapojení do axiomů AND-1 až AND-3 a OR-1 až OR-3 standardního PC zůstanou axiomy pravdivé. Tyto axiomy poskytují úplné syntaktické definice spojení a disjunkce operátory.

Další sada vět bude mít za cíl najít zbývající čtyři axiomy Fregeova PC v „prostoru věty“ standardního PC, což ukazuje, že teorie Fregeova PC je obsažena v teorii standardního PC.

ST2 je axiom FRG-3 počítače Frege.

ST4 je axiom FRG-2 počítače Frege.

Prokázat ST5: (A → (B → C)) → (B → (A → C))

ST5 je axiom THEN-3 počítače Frege.

ST6 je axiom FRG-1 počítače Frege.

Každý z Fregeových axiomů lze odvodit ze standardních axiomů a každý ze standardních axiomů lze odvodit z Fregeových axiomů. To znamená, že dvě sady axiomů jsou vzájemně závislé a v jedné sadě není žádný axiom, který je nezávislý na druhé sadě. Proto dvě sady axiomů generují stejnou teorii: Fregeovo PC je ekvivalentní standardnímu PC.

(Pokud by se teorie měly lišit, pak by jedna z nich měla obsahovat věty, které nejsou obsaženy v jiné teorii. Tyto věty lze odvodit z axiomové množiny jejich vlastní teorie: ale jak bylo ukázáno, celá tato množina axiomů může být odvozena od druhé. množina teorie axiomů, což znamená, že dané věty lze ve skutečnosti odvodit pouze z množiny axiomů jiné teorie, takže dané věty patří také do jiné teorie. Rozpor: tedy dvě množiny axiomů pokrývají stejný prostor věty. : Jakoukoli větu odvozenou ze standardních axiomů lze odvodit z Fregeových axiomů a naopak tak, že nejprve jako věty prokážeme axiomy jiné teorie, jak je uvedeno výše, a poté použijeme tyto věty jako lemma k odvození požadované věty.

Viz také

• Begriffsschrift
• Hugh MacColl je Počet ekvivalentních výroků

Reference

• Buss, Samuel (1998). „Úvod do teorie důkazů“ (PDF). Příručka teorie důkazů. Elsevier. s. 1–78. ISBN  0-444-89840-9.
• Detlovs, Vilnis; Podnieks, Karlis (24. května 2017). "Axiomy logiky: minimální systém, konstruktivní systém a klasický systém". Úvod do matematické logiky (PDF). Lotyšská univerzita. str. 29–30.