předchozí - ÚVOD - následující
Hilbertovský formální systém výrokové logiky
Ještě před zavedením Hilbertovského a Gentzenovského formálního axiomatického systému je nutné zavést pojem formální systém. Formální (axiomatický) systém, v němž se mají odvozování neboli důkazy vět provádět, musí mít definován:
Odvozovací pravidla spolu s axiomy jsou tím základem, v němž se různé formální systémy navzájem liší. Odvozovací pravidlo má hilbertovský formální systém výrokové logiky jediné, a to pravidlo modus ponens |- A |- A ® B
"Z formulí (vět) A a A B odvoď formuli (větu) B." Formule B se nazývá bezprostřední důsledek formulí A a A B.
Dále obsahuje Hilbertovský formální systém 3 axiomy:
Věta o dedukci Jedním z nejužitečnějších pravidel sloužících ke zjednodušení struktury zápisu důkazů je pravidlo dedukce vyjádřené takto:
Korektnost a úplnost Formální systém je sémanticky korektní, je-li každá v něm dokazatelná formule formulí logicky platná (tautologie). Formální systém je sémanticky úplný, existuje-li v něm ke každé formuli, která je logicky platná, její formální důkaz. Postova věta Formule dokazatelná v hilbertovském axiomatickém systému výrokové logiky jsou právě tautologie, tj. pro libovolnou formuli A platí: |- A |= A (formule A je dokazatelná právě když je pravdivá). |
předchozí - ÚVOD - následující