Derywacja formuły zdaniowej w oparciu o zbiór formuł zdaniowych
Z Wikipedii, wolnej encyklopedii
 |
Zasugerowano, aby zintegrować ten artykuł z artykułem rachunek kwantyfikatorów. (dyskusja) |
|
|
Zasugerowano, aby zintegrować ten artykuł z artykułem system formalny. (dyskusja) |
 |
Ten artykuł należy dopracować zgodnie z zaleceniami edycyjnymi: wyjaśnić nazwy użytych formuł wnioskowania. Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się na stronie dyskusji tego artykułu. 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.
