Movatterモバイル変換

[0]ホーム
URL:

Przejdź do zawartości
Wikipediawolna encyklopedia
Szukaj

System formalny

Z Wikipedii, wolnej encyklopedii

System formalny –język formuł (logiki) wraz zezbioremreguł wyprowadzania (wywodu) i zwykle zbioremaksjomató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ącychaksjomaty 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 jestformalizmem matematycznym.David Hilbert nazwałmetamatematyką naukę badającą systemy formalne.

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

  1. Skończony zbiórsymboli, 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 istniejeprocedura decyzyjna określająca, czy jest ona twierdzeniem.

Definicja

[edytuj |edytuj kod]

Systemem formalnym (w zbiorzeE{\displaystyle E}) nazywamy trójkę⟨E,R,A⟩,{\displaystyle \langle E,R,A\rangle ,} gdzieE{\displaystyle E} jest dowolnym zbiorem,A⊆E,{\displaystyle A\subseteq E,} aR{\displaystyle R} jest zbioremreguł wnioskowania wE.{\displaystyle E.} Elementy zbioruE{\displaystyle E} nazywa sięwyrażeniami tego systemu, elementy zbioruA{\displaystyle A} nazywa –aksjomatami, a elementy zbioruR{\displaystyle R} – jegoregułami.

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

Dowody

[edytuj |edytuj kod]

NiechS=⟨E,R,A⟩{\displaystyle {\mathfrak {S}}=\langle E,R,A\rangle } będzie systemem formalnym,X⊆E{\displaystyle X\subseteq E} oraze∈E.{\displaystyle e\in E.}

Dowodem elementue{\displaystyle e} zezbiorem założeńX{\displaystyle X} w systemieS{\displaystyle {\mathfrak {S}}} jest ciąg⟨e1,…,en⟩{\displaystyle \langle e_{1},\dots ,e_{n}\rangle } elementów zbioruE,{\displaystyle E,} dla którego:

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

Przykłady dowodów w systemach formalnych wybranychrachunków zdaniowych można znaleźćtutaj itutaj.

Własności

[edytuj |edytuj kod]

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

e∈PrvS(X)⇔∃X0 – skończony(X0⊆X,e∈PrvS(X0)).{\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).}

Zakres wnioskowania

[edytuj |edytuj kod]

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

Otóż, niech

E={0,1,2,…}{\displaystyle E=\{0,1,2,\dots \}} iR={r,rω},{\displaystyle R=\{r,r_{\omega }\},}

gdzier={⟨{n},n+1⟩:n∈ω}{\displaystyle r=\left\{\langle \{n\},n+1\rangle \colon n\in \omega \right\}} irω={⟨{1,2,…},0⟩:n∈ω}.{\displaystyle r_{\omega }=\left\{\langle \{1,2,\dots \},0\rangle \colon n\in \omega \right\}.} Wówczas

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

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

Konsekwencje i sprzeczność

[edytuj |edytuj kod]
 Osobny artykuł:operator konsekwencji.

ZbiórY{\displaystyle Y} jestdomknięty wS,{\displaystyle {\mathfrak {S}},} jeśli

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

Konsekwencją zbioruX{\displaystyle X} w systemie formalnymS{\displaystyle {\mathfrak {S}}} nazywa się najmniejszy (w sensiezawierania) zbiór domknięty zawierającyX.{\displaystyle X.} Zbiór ten oznacza się jest symbolemCnS(X).{\displaystyle \mathbf {Cn} _{\mathfrak {S}}(X).}

W ten sposób w systemie formalnymS{\displaystyle {\mathfrak {S}}} można rozważać operatorCnS{\displaystyle \mathbf {Cn} _{\mathfrak {S}}} nazywanyoperatorem konsekwencji lubdomknięcia, który jak pokazuje powyższy przykład, nie zawsze jest finitarny.

Zachodzi następujący związek między operatoramiCnS{\displaystyle \mathbf {Cn} _{\mathfrak {S}}} iPrvS:{\displaystyle \mathbf {Prv} _{\mathfrak {S}}{:}}

PrvS(X)⊆CnS(X),{\displaystyle \mathbf {Prv} _{\mathfrak {S}}(X)\subseteq \mathbf {Cn} _{\mathfrak {S}}(X),}

jeżeli system formalny jestfinitarny, to

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

dla każdego zbioruX.{\displaystyle X.}

ZbiórX{\displaystyle X} jestsprzeczny w systemie formalnymS,{\displaystyle {\mathfrak {S}},} jeżeliCnS(X)=E.{\displaystyle \mathrm {Cn} _{\mathfrak {S}}(X)=E.} System formalny jestzwarty, jeśli każdy zbiór sprzeczny w tym systemie zawiera skończony podzbiór sprzeczny.

Porównywanie

[edytuj |edytuj kod]

NiechS=⟨E,R,A⟩{\displaystyle {\mathfrak {S}}=\langle E,R,A\rangle } będzie systemem formalnym i niechr{\displaystyle r} będzie regułą w zbiorzeE.{\displaystyle E.}

Regułar{\displaystyle r} jestdopuszczalna wS,{\displaystyle {\mathfrak {S}},} jeśli

Π⊆CnS(∅)⇒e∈CnS(∅),{\displaystyle \Pi \subseteq \mathbf {Cn} _{\mathfrak {S}}(\varnothing )\Rightarrow e\in \mathbf {Cn} _{\mathfrak {S}}(\varnothing ),} gdzie⟨Π,e⟩∈r.{\displaystyle \langle \Pi ,e\rangle \in r.}

Regułar{\displaystyle r} jestwyprowadzalna wS,{\displaystyle {\mathfrak {S}},} jeżeli

e∈CnS(Π),{\displaystyle e\in \mathbf {Cn} _{\mathfrak {S}}(\Pi ),} gdzie⟨Π,e⟩∈r.{\displaystyle \langle \Pi ,e\rangle \in r.}

System formalnyS1=⟨E,R1,A1⟩{\displaystyle {\mathfrak {S}}_{1}=\langle E,R_{1},A_{1}\rangle } jestniesłabszy niżS,{\displaystyle {\mathfrak {S}},} co oznacza sięS⪯S1,{\displaystyle {\mathfrak {S}}\preceq {\mathfrak {S}}_{1},} gdy

Systemy sąrównoważne, jeśliS⪯S1{\displaystyle {\mathfrak {S}}\preceq {\mathfrak {S}}_{1}} orazS1⪯S,{\displaystyle {\mathfrak {S}}_{1}\preceq {\mathfrak {S}},} co zapisuje sięS≈S1.{\displaystyle {\mathfrak {S}}\approx {\mathfrak {S}}_{1}.}

Zobacz też

[edytuj |edytuj kod]
Encyklopedie internetowe (rodzaj systemu):
Źródło: „https://pl.wikipedia.org/w/index.php?title=System_formalny&oldid=69289941”
Kategorie:
[8]ページ先頭
©2009-2026 Movatter.jp