Derywacja formuły zdaniowej w oparciu o zbiór formuł zdaniowych
Zasugerowano, aby zintegrować ten artykuł z artykułem [[::rachunek kwantyfikatorów|rachunek kwantyfikatorów]]. Nie opisano powodu propozycji integracji. |
Zasugerowano, aby zintegrować ten artykuł z artykułem [[::system formalny|system formalny]]. Nie opisano powodu propozycji integracji. |
Ten artykuł należy dopracować zgodnie z zaleceniami edycyjnymi: wyjaśnić nazwy użytych formuł wnioskowania. Po wyeliminowaniu niedoskonałości prosimy usunąć szablon {{Dopracować}} z kodu tego artykułu. |
Derywacją (dowodem) formuły zdaniowej A w oparciu o zbiór formuł zdaniowych X 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:
- należy do zbioru X lub jest aksjomatem rachunku kwantyfikatorów 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.
Jeżeli zbiór X jest zbiorem pustym, to formułę A nazywamy tautologią klasycznego rachunku kwantyfikatorów (predykatów).
Dowodem formuły zdaniowej w oparciu o zbiór aksjomatów klasycznego rachunku predykatów nazywamy derywację w oparciu o zbiór aksjomatów KRP.