Hilbertovský kalkulus: Porovnání verzí
Smazaný obsah Přidaný obsah
upraveno, na en jsem nenašel odpovídající článek, takže bez iw |
m →Axiomy pro predikátovou logiku: typo |
||
Řádek 15:
Predikátový hilbertovský kalkulus obsahuje všecny výrokové axiomy, dvě odvozovací pravidla – modus ponens a generalizace (viz dále) a také následující predikátové axiomy. Systém těchto axiomů se podobně jako u výrokové verze nazývá souhrnně ''axiomy predikátové logiky (prvního řádu)''.
Predikátové axiomy hilbertovského kalkulu jsou:
* Axiom substituce: <math>(\forall x)(\varphi (x,y_{1},...,y_{n})) \implies \varphi (x/t,y_{1},...,y_{n})</math>, je-li [[term]] ''t'' substituovatelný za ''x'' do <math>
* Axiom <math>\forall</math>-distribuce: <math>((\forall x )(\varphi \implies \psi)) \implies (\varphi \implies (\forall x) \psi)</math>, není-li [[proměnná]] ''x'' volná ve <math>
V případě predikátové logiky prvního řádu s [[rovnost]]í se k axiomům predikátové logiky prvního řádu přidávají ještě axiomy pro [[rovnost]].
| |||