Otwórz menu główne

System formalnyjęzyk formuł (logiki) wraz ze zbiorem reguł wyprowadzania (wywodu) i zwykle zbiorem aksjomatów. Systemy formalne są tworzone i badane zarówno jako samodzielne abstrakcyjne twory, jak i systemy opisu rzeczywistości.

W matematyce formalnie dowody twierdzeń konstruuje się w systemach formalnych zawierających aksjomaty oraz reguły dedukcji (wyprowadzania). Twierdzenia są wtedy „ostatnimi liniami” takich dowodów. Zbiór aksjomatów i wszystkich możliwych twierdzeń nazywa się domknięciem zbioru aksjomatów ze względu na wyprowadzanie. Takie podejście do matematyki nazywane jest formalizmem matematycznym. David Hilbert nazwał metamatematyką naukę badającą systemy formalne.

System formalny w matematyce zawiera następujące elementy:

  1. Skończony zbiór symboli, z którego konstruowane są formuły.
  2. Gramatykę opisującą jakie formuły są poprawnie skonstruowane i pozwalającą zweryfikować poprawność dowolnej formuły.
  3. Zbiór aksjomatów, będących poprawnie skonstruowanymi formułami.
  4. Zbiór reguł wyprowadzania.
  5. Zbiór twierdzeń zawierający wszystkie aksjomaty oraz wszystkie poprawnie skonstruowane formuły, które da się wyprowadzić z aksjomatów za pomocą reguł wyprowadzania.

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.

Spis treści

DefinicjaEdytuj

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.

DowodyEdytuj

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ściEdytuj

  •  
  •  
  •  

Z własności tych wynika, że   jest operatorem domknięcia, co więcej, jest on finitarny:

 

Zakres wnioskowaniaEdytuj

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śćEdytuj

Osobny artykuł: operator konsekwencji.

Zbiór   jest domknięty w   jeśli

  •   oraz
  •  

Czasami zbiory domknięte w systemie formalnym nazywa się teoriami tego systemu.

Konsekwencją zbioru   w systemie formalnym   nazywa się najmniejszy (w sensie zawierania) zbiór domknięty zawierający   Zbiór ten oznacza się jest symbolem  

W ten sposób w systemie formalnym   można rozważać operator   nazywany operatorem konsekwencji lub domknięcia, który jak pokazuje powyższy przykład, nie zawsze jest finitarny.

Zachodzi następujący związek między operatorami   i  

 

jeżeli system formalny jest finitarny, to

 

dla każdego zbioru  

Zbiór   jest sprzeczny w systemie formalnym   jeżeli   System formalny jest zwarty, jeśli każdy zbiór sprzeczny w tym systemie zawiera skończony podzbiór sprzeczny.

PorównywanieEdytuj

Niech   będzie systemem formalnym i niech   będzie regułą w zbiorze  

Reguła   jest dopuszczalna w   jeśli

  gdzie  

Reguła   jest wyprowadzalna w   jeżeli

  gdzie  

System formalny   jest niesłabszy niż   co oznacza się   gdy

  •   oraz
  • wszystkie reguły w   są wyprowadzalne w  

Systemy są równoważne, jeśli   oraz   co zapisuje się  

Zobacz teżEdytuj