Należy pamiętać, że nawet jeżeli dana formuła jest poprawną formułą systemu, to nie oznacza to, że istnieje procedura decyzyjna określająca, czy jest ona twierdzeniem.
Definicja Systemem formalnym (w zbiorze ) nazywamy trójkę gdzie jest dowolnym zbiorem, a jest zbiorem reguł wnioskowania w Elementy zbioru nazywa się wyrażeniami tego systemu, elementy zbioru nazywa – aksjomatami, a elementy zbioru – jego regułami.
System formalny jest finitarny, jeśli jego reguły są finitarne.
Dowody Niech będzie systemem formalnym, oraz
Dowodem elementu ze zbiorem założeń w systemie jest ciąg elementów zbioru dla którego:
dla każdego zachodzi przynajmniej jeden z warunków:
Zbiór elementów mających w dowód ze zbiorem założeń oznacza się symbolem
Przykłady dowodów w systemach formalnych wybranych rachunków zdaniowych można znaleźć tutaj i tutaj.
Własności
Z własności tych wynika, że jest operatorem domknięcia, co więcej, jest on finitarny:
Zakres wnioskowania Mając dany zbiór „założeń” chciałoby się znać wszystkie „fakty” ze zbioru które można wywnioskować ze zbioru Niestety okazuje się, że zbiory nie zawsze zawierają wszystkie „wnioski”.
Otóż, niech i
gdzie i Wówczas
choć z można przecież wywnioskować jeszcze element
Konsekwencje i sprzeczność
Zbiór jest domknięty w jeśli oraz