System formalny – 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 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.

Systemem formalnym (w zbiorze ${\displaystyle E}$) nazywamy trójkę ${\displaystyle \langle E,R,A\rangle ,}$ gdzie ${\displaystyle E}$ jest dowolnym zbiorem, ${\displaystyle A\subseteq E,}$ a ${\displaystyle R}$ jest zbiorem reguł wnioskowania w ${\displaystyle E.}$ Elementy zbioru ${\displaystyle E}$ nazywa się wyrażeniami tego systemu, elementy zbioru ${\displaystyle A}$ nazywa – aksjomatami, a elementy zbioru ${\displaystyle R}$ – jego regułami.

System formalny jest finitarny, jeśli jego reguły są finitarne.

Niech ${\displaystyle {\mathfrak {S}}=\langle E,R,A\rangle }$ będzie systemem formalnym, ${\displaystyle X\subseteq E}$ oraz ${\displaystyle e\in E.}$

Dowodem elementu ${\displaystyle e}$ ze zbiorem założeń ${\displaystyle X}$ w systemie ${\displaystyle {\mathfrak {S}}}$ jest ciąg ${\displaystyle \langle e_{1},\dots ,e_{n}\rangle }$ elementów zbioru ${\displaystyle E,}$ dla którego:

• ${\displaystyle e=e_{n},}$
• dla każdego ${\displaystyle k=1,\dots ,n}$ zachodzi przynajmniej jeden z warunków:
  • ${\displaystyle e_{k}\in X\cup A,}$
  • ${\displaystyle \exists _{r\in R}\;\exists _{\Pi \subseteq \{1,\dots ,k-1\}}\;\left(\langle \{e_{i}:i\in \Pi \},e_{k}\rangle \in r\right).}$

Zbiór elementów mających w ${\displaystyle {\mathfrak {S}}}$ dowód ze zbiorem założeń ${\displaystyle X}$ oznacza się symbolem ${\displaystyle \mathbf {Prv} _{\mathfrak {S}}(X).}$

Przykłady dowodów w systemach formalnych wybranych rachunków zdaniowych można znaleźć tutaj i tutaj.

• ${\displaystyle X\subseteq \mathbf {Prv} _{\mathfrak {S}}(X).}$
• ${\displaystyle X\subseteq Y\Rightarrow \mathbf {Prv} _{\mathfrak {S}}(X)\subseteq \mathbf {Prv} _{\mathfrak {S}}(Y).}$
• ${\displaystyle \mathbf {Prv} _{\mathfrak {S}}{\big (}\mathbf {Prv} _{\mathfrak {S}}(X){\big )}=\mathbf {Prv} _{\mathfrak {S}}(X).}$

Z własności tych wynika, że ${\displaystyle \mathbf {Prv} }$ jest operatorem domknięcia, co więcej, jest on finitarny:

${\displaystyle e\in \mathbf {Prv} _{\mathfrak {S}}(X)\Leftrightarrow \exists _{X_{0}{\mbox{ – skończony}}}\;\left(X_{0}\subseteq X,\;e\in \mathbf {Prv} _{\mathfrak {S}}(X_{0})\right).}$

Mając dany zbiór „założeń” ${\displaystyle X}$ chciałoby się znać wszystkie „fakty” ${\displaystyle e}$ ze zbioru ${\displaystyle E,}$ które można wywnioskować ze zbioru ${\displaystyle X.}$ Niestety okazuje się, że zbiory ${\displaystyle \mathbf {Prv} _{\mathfrak {S}}(X)}$ nie zawsze zawierają wszystkie „wnioski”.

Otóż, niech

${\displaystyle E=\{0,1,2,\dots \}}$ i ${\displaystyle R=\{r,r_{\omega }\},}$

gdzie ${\displaystyle r=\left\{\langle \{n\},n+1\rangle \colon n\in \omega \right\}}$ i ${\displaystyle r_{\omega }=\left\{\langle \{1,2,\dots \},0\rangle \colon n\in \omega \right\}.}$ Wówczas

${\displaystyle \mathbf {Prv} _{\mathfrak {S}}(\{1\})=\{1,2,3,\dots \},}$

choć z ${\displaystyle \{1,2,\dots \}}$ można przecież wywnioskować jeszcze element ${\displaystyle 0.}$

 Osobny artykuł: operator konsekwencji.

Zbiór ${\displaystyle Y}$ jest domknięty w ${\displaystyle {\mathfrak {S}},}$ jeśli

• ${\displaystyle A\subseteq Y}$ oraz
• ${\displaystyle \forall _{r\in R}\;\forall _{\langle \Pi ,e\rangle \in r}\;(\Pi \subseteq Y\Rightarrow e\in Y)}$

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

Konsekwencją zbioru ${\displaystyle X}$ w systemie formalnym ${\displaystyle {\mathfrak {S}}}$ nazywa się najmniejszy (w sensie zawierania) zbiór domknięty zawierający ${\displaystyle X.}$ Zbiór ten oznacza się jest symbolem ${\displaystyle \mathbf {Cn} _{\mathfrak {S}}(X).}$

W ten sposób w systemie formalnym ${\displaystyle {\mathfrak {S}}}$ można rozważać operator ${\displaystyle \mathbf {Cn} _{\mathfrak {S}}}$ 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 ${\displaystyle \mathbf {Cn} _{\mathfrak {S}}}$ i ${\displaystyle \mathbf {Prv} _{\mathfrak {S}}{:}}$

${\displaystyle \mathbf {Prv} _{\mathfrak {S}}(X)\subseteq \mathbf {Cn} _{\mathfrak {S}}(X),}$

jeżeli system formalny jest finitarny, to

${\displaystyle \mathbf {Prv} _{\mathfrak {S}}(X)=\mathbf {Cn} _{\mathfrak {S}}(X)}$

dla każdego zbioru ${\displaystyle X.}$

Zbiór ${\displaystyle X}$ jest sprzeczny w systemie formalnym ${\displaystyle {\mathfrak {S}},}$ jeżeli ${\displaystyle \mathrm {Cn} _{\mathfrak {S}}(X)=E.}$ System formalny jest zwarty, jeśli każdy zbiór sprzeczny w tym systemie zawiera skończony podzbiór sprzeczny.

Niech ${\displaystyle {\mathfrak {S}}=\langle E,R,A\rangle }$ będzie systemem formalnym i niech ${\displaystyle r}$ będzie regułą w zbiorze ${\displaystyle E.}$

Reguła ${\displaystyle r}$ jest dopuszczalna w ${\displaystyle {\mathfrak {S}},}$ jeśli

${\displaystyle \Pi \subseteq \mathbf {Cn} _{\mathfrak {S}}(\varnothing )\Rightarrow e\in \mathbf {Cn} _{\mathfrak {S}}(\varnothing ),}$ gdzie ${\displaystyle \langle \Pi ,e\rangle \in r.}$

Reguła ${\displaystyle r}$ jest wyprowadzalna w ${\displaystyle {\mathfrak {S}},}$ jeżeli

${\displaystyle e\in \mathbf {Cn} _{\mathfrak {S}}(\Pi ),}$ gdzie ${\displaystyle \langle \Pi ,e\rangle \in r.}$

System formalny ${\displaystyle {\mathfrak {S}}_{1}=\langle E,R_{1},A_{1}\rangle }$ jest niesłabszy niż ${\displaystyle {\mathfrak {S}},}$ co oznacza się ${\displaystyle {\mathfrak {S}}\preceq {\mathfrak {S}}_{1},}$ gdy

• ${\displaystyle A\subseteq \mathbf {Cn} _{{\mathfrak {S}}_{1}}(\varnothing )}$ oraz
• wszystkie reguły w ${\displaystyle R}$ są wyprowadzalne w ${\displaystyle {\mathfrak {S}}_{1}.}$

Systemy są równoważne, jeśli ${\displaystyle {\mathfrak {S}}\preceq {\mathfrak {S}}_{1}}$ oraz ${\displaystyle {\mathfrak {S}}_{1}\preceq {\mathfrak {S}},}$ co zapisuje się ${\displaystyle {\mathfrak {S}}\approx {\mathfrak {S}}_{1}.}$

• twierdzenie Lindenbauma