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:

1) jazyk - syntax, tj. množiny symbolů pro označení logických konstant, atomických formulí, symbolů pro výrokové spojky a pomocné symboly (, ),

2) axiomy - formule představující základní věty tohoto jazyka,

3) odvozovací pravidla - pravidla umožňující na základě syntaxe základních vět odvodit nové věty.

Odvozovací pravidla spolu s axiomy jsou tím základem, v němž se různé formální systémy navzájem liší.

Hilbertovský formální systém

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:

1. A (B A)

2. (A (B C)) ((A B) (A C))

3. (( B) ( A)) (A B)

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á).