Formální systém

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 31. srpna 2021; kontroly vyžadují 3 úpravy .

Formální systém ( formální teorie , axiomatická teorie , axiomatika , deduktivní systém ) je výsledkem přísné formalizace teorie , která předpokládá úplnou abstrakci od významu slov použitého jazyka a všech podmínek upravujících použití tato slova v teorii jsou výslovně uvedena prostřednictvím axiomů a pravidel, která umožňují odvodit jednu frázi od jiných [1] .

Formální systém je soubor abstraktních objektů, které nesouvisejí s vnějším světem, ve kterém jsou pravidla pro práci se souborem symbolů prezentována v přísně syntaktické interpretaci bez zohlednění sémantického obsahu, tedy sémantiky. Přísně popsané formální systémy se objevily poté, co byl položen Hilbertův problém . První FS se objevil po vydání knih Russella a Whiteheada „Formální systémy“[ specifikovat ] . Tyto FS byly předloženy s určitými požadavky.

Základy

Formální teorie je považována za definovanou, pokud [2] :

  1. Je dána konečná nebo spočetná množina libovolných symbolů. Konečné posloupnosti symbolů se nazývají teoretické výrazy .
  2. Existuje podmnožina výrazů nazývaných vzorce .
  3. Byla vybrána podmnožina vzorců, nazývaná axiomy .
  4. Mezi vzorci existuje konečná množina vztahů, nazývaná inferenční pravidla .

Obvykle existuje účinný postup, který umožňuje danému výrazu určit, zda se jedná o vzorec. Často je soubor vzorců dán induktivní definicí . Tato množina je zpravidla nekonečná. Soubor symbolů a soubor vzorců společně definují jazyk nebo podpis formální teorie.

Nejčastěji lze efektivně zjistit, zda je daný vzorec axiom; v takovém případě se říká, že teorie je účinně axiomatizovaná nebo axiomatická . Množina axiomů může být konečná nebo nekonečná. Pokud je počet axiomů konečný, pak se říká, že teorie je konečně axiomatizovatelná . Pokud je množina axiomů nekonečná, pak se zpravidla specifikuje pomocí konečného počtu axiomových schémat a pravidel pro generování konkrétních axiomů ze schématu axiomů. Obvykle se axiomy dělí na dva typy: logické axiomy (společné pro celou třídu formálních teorií) a nelogické nebo vlastní axiomy (určující specifika a obsah konkrétní teorie).

Pro každé inferenční pravidlo R a pro každý vzorec A je efektivně vyřešena otázka, zda je zvolená množina vzorců ve vztahu k R se vzorcem A , a pokud ano, pak se A nazývá přímým důsledkem těchto vzorců podle pravítko.

Odvození je jakákoliv posloupnost vzorců taková, že jakýkoli vzorec posloupnosti je buď axiomem nebo přímým důsledkem některých předchozích vzorců podle jednoho z odvozovacích pravidel.

Vzorec se nazývá teorém , pokud existuje derivace, ve které je tento vzorec poslední.

Teorie, pro kterou existuje účinný algoritmus, který vám umožňuje z daného vzorce zjistit, zda existuje jeho derivace, se nazývá rozhodnutelná ; jinak je teorie prý nerozhodnutelná .

Teorie, ve které ne všechny formule jsou teorémy, je prý absolutně konzistentní .

Definice a odrůdy

Deduktivní teorie je považována za danou, pokud:

  1. Je uvedena abeceda ( množina ) a pravidla pro tvoření výrazů ( slov ) v této abecedě.
  2. Jsou uvedena pravidla pro tvorbu vzorců (dobře utvořené, správné výrazy).
  3. Z množiny vzorců se nějakým způsobem vybere podmnožina T vět ( ​​dokazatelné vzorce ).

Odrůdy deduktivních teorií

V závislosti na metodě konstrukce množiny vět:

Specifikace axiomů a odvozených pravidel

V množině vzorců je vyčleněna podmnožina axiomů a specifikován konečný počet odvozovacích pravidel - taková pravidla, s jejichž pomocí (a pouze s jejich pomocí) lze z axiomů a dříve odvozených vět tvořit nové věty. teorémy. Všechny axiomy jsou také zahrnuty v počtu vět. Někdy (například v Peanově axiomatice ) teorie obsahuje nekonečné množství axiomů, které jsou specifikovány pomocí jednoho nebo více schémat axiomů . Axiomům se někdy říká „skryté definice“. Tímto způsobem je specifikována formální teorie ( formální axiomatická teorie , formální (logický) kalkul ).

Ptát se pouze na axiomy

Jsou uvedeny pouze axiomy, pravidla odvození se považují za dobře známá.

S takovou specifikací teorémů se říká, že je dána poloformální axiomatická teorie . Příklady

Geometrie

Určení pouze odvozovacích pravidel

Neexistují žádné axiomy (množina axiomů je prázdná), jsou dána pouze pravidla pro odvozování.

Takto definovaná teorie je ve skutečnosti zvláštním případem té formální, ale má své vlastní jméno: teorie přirozené inference .

Vlastnosti deduktivních teorií

Konzistence

Teorie, ve které množina teorémů pokrývá celou množinu formulí (všechny formule jsou teorémy, „pravdivá tvrzení“), se nazývá nekonzistentní . Jinak se říká, že teorie je konzistentní . Objasnění nekonzistentnosti teorie je jedním z nejdůležitějších a někdy i nejobtížnějších úkolů formální logiky.

Úplnost

Teorie se nazývá úplná , pokud je v ní pro libovolnou větu (uzavřenou formuli) odvoditelná buď sama, nebo její negace . Jinak teorie obsahuje nedokazatelná tvrzení (tvrzení, která nelze samotnou teorií dokázat ani vyvrátit), a nazývá se neúplná .

Nezávislost axiomů

Jednotlivý axiom teorie je řekl, aby byl nezávislý , jestliže tento axiom nelze odvodit ze zbytku axiomů. Závislý axiom je v podstatě nadbytečný a jeho odstranění ze systému axiomů teorii nijak neovlivní. Celý systém axiomů teorie se nazývá nezávislý , pokud je každý axiom v něm nezávislý.

Řešitelnost

Teorie se nazývá rozhodnutelná , pokud je v ní koncept teorému efektivní , to znamená, že existuje efektivní proces (algoritmus), který umožňuje libovolnému vzorci určit v konečném počtu kroků, zda se jedná o teorém nebo ne.

Klíčové výsledky

  • Ve 30. letech. Ve 20. století Kurt Gödel ukázal, že existuje celá třída teorií prvního řádu, které jsou neúplné. Navíc, vzorec konstatující konzistenci teorie je také neodvoditelný pomocí samotné teorie (viz Gödelovy věty o neúplnosti ). Tento závěr byl pro matematiku velmi důležitý, protože formální aritmetika (a jakákoli teorie obsahující ji jako podteorii) je právě takovou teorií prvního řádu, a proto neúplná.
  • Navzdory tomu je teorie reálných uzavřených polí se sčítáním, násobením a relací uspořádání kompletní ( Tarského-Seidenbergova věta ).
  • Alonzo Church dokázal, že problém určení platnosti libovolné formule predikátové logiky je algoritmicky neřešitelný .
  • Výrokový počet je konzistentní, úplná, rozhodnoutelná teorie.

Viz také

Příklady formálních systémů

Poznámky

  1. ↑ Kleene S.K. Úvod do metamatematiky . - M. : IL, 1957. - S. 59-60. Archivováno 1. května 2013 na Wayback Machine
  2. ↑ Mendelssohn E. Úvod do matematické logiky . - M. : "Nauka", 1971. - S. 36. Archivní kopie ze dne 1. května 2013 na Wayback Machine

Literatura

  Přejděte na položku Wikidata  Slovníky a encyklopedie
 Logika
Filosofie • Sémantika • Syntaxe • Historie
Logické skupiny
klasická logika
matematická logika
Neklasická logika
Filosofická logika
Komponenty
Seznam booleovských symbolů