System formalny
Z Wikipedii
W logice i matematyce, system formalny to ję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 jakichś rzeczywistych zjawisk.
W matematyce, formalne dowody twierdzeń są tworzone w systemach formalnych posiadających aksjomaty oraz reguły dedukcji - wyprowadzania. Twierdzenia są wtedy 'ostatnimi liniami' takich dowodów. Zbiór aksjomatów i wszystkich możliwych twierdzeń jest też nazywany domknięciem zbioru aksjomatów ze względu na wyprowadzanie. Takie podejście do matematyki nazywane jest formalizmem matematycznym. David Hilbert zdefiniował metamatematykę jako naukę badającą systemy formalne.
System formalny w matematyce zawiera następujące elementy:
- Skończony zbiór symboli z którego konstruowane są formuły.
- Gramatykę opisującą jakie formuły są poprawnie skonstruowane i pozwalającą zweryfikować poprawność dowolnej formuły.
- Zbiór aksjomatów, będących poprawnie skonstruowanymi formułami.
- Zbiór reguł wyprowadzania
- 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, nie oznacza to, że istnieje procedura decyzyjna określająca czy formuła ta jest twierdzeniem.
