Derywacja formuły zdaniowej w oparciu o zbiór formuł zdaniowych

Z PrePedia
Skocz do: nawigacja, szukaj
Information icon4.svg W Wikipedii odbyła się dyskusja nad usunięciem tego artykułu, zobacz ją.

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:

  1. należy do zbioru X lub jest aksjomatem rachunku kwantyfikatorów lub
  2. 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
  3. 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.