Hilbertův systém

V logice , že systémy v Hilbert slouží k definování formální srážky na základě modelu navrženého David Hilbert na začátku XX th století , velkého počtu logických axiomů vyjadřujících hlavní logické vlastnosti, které jsou kombinovány s některých pravidel, zejména modus ponens pravidlo , odvodit nové věty. Systémy Hilbertovy dědí ze systému definovaného Frege a představují první deduktivní systémy, před objevením přírodního odpočtu nebo výpočet sequents , někdy zvané opoziční Gentzen systémů .

Definice

Výrokový počet

Uvažujeme množinu vzorců výrokového počtu . Připomeňme, že se jedná o konečné vzorce, které můžeme sestavit indukčně z výrokových proměnných pomocí logických spojek.

Dáme si množinu logických axiomů, což jsou platné vzorce výrokového počtu. Odpočet je řada vzorců tak, že každý vzorec je uveden v této sérii splňuje jednu z následujících podmínek: $NA$

$NA$ je instance axiomu (nebo věty), tj. jednoho z logických axiomů (nebo jedné z již prokázaných vět), ve kterém jsou výrokové proměnné nahrazeny vzorci;
existují dva předchozí vzorce, které jsou ve formě a ; pak říkáme, že je získán modus ponens mezi těmito dvěma vzorci. $NA\,$ $B \ až A$ $B \,$ $NA\,$

Představujeme dedukci tím, že napíšeme vzorce po řádcích a přidáme komentář ke každému řádku, abychom vysvětlili, jak byl získán odpovídající vzorec.

Existuje několik možných možností axiomatických systémů výrokového počtu. Dáme zde jeden, který je relativně rozvláčný, ale docela intuitivní.

Axiomy pro implikaci . Volba těchto dvou poněkud zvláštních axiomů je odůvodněna skutečností, že zjednodušují důkaz věty o dedukci :
- Axiom : ; $K.$ $f \ to (g \ to f)$
- Axiom : . $S$ $(f \ to (g \ to h)) \ to ((f \ to g) \ to (f \ to h))$

Axiomy pro negaci . Jsou uvedeny dvě z hlavních variant těchto axiomů; jako příklad si může čtenář vybrat jeden z nich a pokusit se najít odpočet od druhého:
- Úvaha o rozporu: ; $(\ neg f \ to g) \ to ((\ neg f \ to \ neg g) \ to f)$
- Kontrapozice: . $(\ neg g \ to \ neg f) \ to (f \ to g)$

Axiomy pro spojení :
- $f \ to (g \ to f \ land g)$ ;
- $f \ land g \ to f$ , . $f \ land g \ to g$

Axiomy pro disjunkce :
- $f \ to f \ lor g$ , ; $g \ to f \ lor g$
- Odůvodnění případem . $f \ lor g \ to ((f \ to h) \ to ((g \ to h) \ to h))$

Příklad odpočtu

Zde je odpočet identity : $f \ až f$

Vezmeme-li axiom : a nahrazením za a tím získáme: $S$ $(f \ to (g \ to h)) \ to ((f \ to g) \ to (f \ to h))$ $G$ $(g \ to f)$ $h$ $F$

$(f \ to ((g \ to f) \ to f)) \ to ((f \ to (g \ to f)) \ to (f \ to f))$ (instance axiomu ) $S$ Pak tím, že axiom : a nahradit ji s , dostaneme: $K.$ $f \ to (g \ to f)$ $G$ $(g \ to f)$
$f \ to ((g \ to f) \ to f)$ (instance axiomu ) $K.$
$(f \ to (g \ to f)) \ to (f \ to f)$ ( modus ponens mezi 1 a 2)
$f \ to (g \ to f)$ (instance axiomu ) $K.$
$f \ až f$ ( modus ponens mezi 3 a 4)

Věta o dedukci

Jak vidíme v předchozím příkladu, je docela nepohodlné demonstrovat nejjednodušší vlastnosti. Proto rozšiřujeme systém přidáním možnosti použití hypotéz , tedy neprokázaných vzorců. Takže místo demonstrace bychom se spokojili s demonstrací pomocí hypotézy , která se rovná napsání jednorázového důkazu. $f \ až f$ $f \,$ $f \,$

Další příklad důkazu s hypotézou je dán tranzitivitou implikace: tím, že si dáme hypotézy , a dokážeme, že : $f \ až g$ $g \ až h$ $f \,$ $h \,$

$f \,$ (hypotéza)
$f \ až g$ (hypotéza)
$g \,$ ( modus ponens mezi 2 a 1)
$g \ až h$ (hypotéza)
$h \,$ ( modus ponens mezi 4 a 3)

Poté vyvstává otázka, zda z důkazu s hypotézami můžeme důkaz získat bez; například lze z výše uvedeného důkazu odvodit existenci důkazu ? Odpověď zní ano a toto uvádí věta o dedukci : máme-li důkaz vzorce pomocí hypotézy, pak můžeme sestrojit důkaz, který již tuto hypotézu nepoužívá, tj. Pokud tedy . $(f \ to g) \ to ((g \ to h) \ to (f \ to h))$ $NA$ $B$ $B \ až A$ $B \ vdash A$ $\ vdash B \ do A$

Použití věty o dedukci umožňuje výrazně zjednodušit hledání důkazů v systémech à la Hilbert. Je to nezbytný krok v důkazu věty o úplnosti takového systému. V přírodním odpočtu nebo kalkulu sequents z Gerhard Gentzen teorém dedukce je nějakým způsobem integrován jako primitivní zpravidla ve formě pravého zavedení implikace.