Dowód formuły zdaniowej w oparciu o zbiór aksjomatów klasycznego rachunku predykatów.html |
| | | ca | | | de | | | en | | | es | | | fr | | | it | | | nl | | | no | | | pl | | | pt | | | ru | | | ro | | | fi | | | sv | | | tr | | | vo | | |
| |  |
Dowodem formuły zdaniowej A w oparciu o zbiór aksjomatów KRP nazywamy skończony ciąg formuł zdaniowych, którego ostatnim wyrazem jest formuła A, taki, że dowolna formuła zdaniowa będąca wyrazem tego ciągu:
- jest aksjomatem KRP, lub
- powstaje z jakiegoś wcześniejszego wyrazu rozważanego ciągu poprzez zastosowanie:
- reguły podstawiania RP, lub
- reguły opuszczania dużego kwantyfikatora O∀, lub
- reguły dołączania dużego kwantyfikatora D∀, lub
- reguły opuszczania małego kwantyfikatora O∃, lub
- reguły dołączania małego kwantyfikatora D∃, lub
- powstaje z jakichś wcześniejszych wyrazów tego ciągu poprzez zastosowania reguły odrywania RO.
Dowodem nazywamy więc derywację w oparciu o zbiór aksjomatów KRP.