Formální systém (také nazývaný logický kalkul[citace nutná]) se ve formální logice skládá z formálního jazyka a souboru pravidel odvození, používaných k odvození (uzavření) výrazu z jedné nebo více dalších premis, které jsou předpokládány (axiomy) nebo odvozeny (věty). axiomy a pravidla mohou být nazývány deduktivním aparátem. Formální systém může být formulován a studován pro své vnitřní vlastnosti, nebo může být zamýšlen jako popis (tj. model) vnějších jevů.
Každý formální systém má formální jazyk, který je složen z primitivních symbolů. Tyto symboly působí na určitá pravidla formování a jsou vytvořeny odvozením od množiny axiomů. Systém se tedy skládá z libovolného počtu vzorců vytvořených konečnými kombinacemi primitivních symbolů – kombinací, které jsou vytvořeny z axiomů v souladu s uvedenými pravidly.[1]
Formální systémy v matematice se skládají z těchto prvků:
O formálním systému se říká, že je rekurzivní (tj. efektivní), pokud množina axiomů a množina pravidel inference jsou podle kontextu decidable množiny nebo semidecidable množiny.
Někteří teoretikové používají termín formalismus jako hrubé synonymum pro formální systém, ale termín se používá také k odkazu na určitý styl zápisu, například na zápis podprsenky Paula Diraca.
Logický systém nebo ve zkratce logika je formální systém spolu s formou sémantiky, obvykle ve formě modelově-teoretické interpretace, která přiřazuje hodnoty pravdy větám formálního jazyka, tedy vzorcům, které neobsahují žádné volné proměnné. Logika je zdravá, pokud všechny věty, které lze odvodit, jsou při interpretaci pravdivé, a úplná, pokud naopak lze odvodit všechny pravdivé věty.
Formální důkazy jsou posloupnosti wffs. Aby se wff kvalifikoval jako část důkazu, může to být buď axiom, nebo produkt aplikace pravidla odvození na předchozí wffs v posloupnosti důkazu. Poslední wff v posloupnosti je rozpoznán jako věta.
Názor, že generování formálních důkazů je vše, co v matematice je, je často nazýván formalismem. David Hilbert založil metamatematiku jako disciplínu pro diskusi o formálních systémech. Jakýkoli jazyk, který člověk používá k hovoru o formálním systému, se nazývá metalanguage. Metoagege nemusí být nic jiného než obyčejný přirozený jazyk, nebo může být sama částečně formalizována, ale obecně je méně zcela formalizována než formální jazyková složka zkoumaného formálního systému, který je pak nazýván objektovým jazykem, tedy předmětem dotyčné diskuse.
Jakmile je formální systém dán, lze definovat množinu vět, které mohou být dokázány uvnitř formálního systému. Tato množina se skládá ze všech wffs, pro které existuje důkaz. Tudíž všechny axiomy jsou považovány za věty. Na rozdíl od gramatiky pro wffs, neexistuje žádná záruka, že bude existovat rozhodovací postup pro rozhodování, zda daný wff je věta nebo ne. Pojem právě definované věty by neměl být zaměňován s větami o formálním systému, které, aby se předešlo záměně, se obvykle nazývají metavěty.
Formální jazyk je v matematice, logice a informatice jazyk, který je definován přesnými matematickými nebo strojově zpracovatelnými vzorci. Formální jazyky mají podobně jako jazyky v lingvistice obecně dva aspekty:
Existuje zvláštní obor matematiky a informatiky, který se věnuje výhradně teorii syntaxe jazyka: teorii formálního jazyka. Ve formální teorii jazyka není jazyk ničím jiným než svou syntaxí; otázky sémantiky nejsou do této specializace zahrnuty.
Formální gramatika je v informatice a lingvistice přesný popis formálního jazyka: množina řetězců. Dvě hlavní kategorie formální gramatiky jsou generativní gramatiky, což jsou množiny pravidel, jak lze generovat řetězce v jazyce, a analytické gramatiky, což jsou množiny pravidel, jak lze analyzovat řetězec, aby se zjistilo, zda je členem jazyka. Stručně řečeno, analytická gramatika popisuje, jak rozpoznat, kdy jsou řetězce členy v množině, zatímco generativní gramatika popisuje, jak psát pouze ty řetězce v množině.
Najít tuto stránku na Wiktionary:
formalizace