Formala sistemo

Formala sistemo, aŭ formala teorio, aŭ dedukta sistemo estas formala lingvo de formuloj (bonformaj asertoj), inferencaj reguloj, eventuale kun aro da aksiomoj ^{[noto 1]}. Formalajn sistemojn oni konstruas kaj esploras kiel abstraktajn teoriojn aŭ kiel priskribon de io reala. Ili estas uzataj en diversaj sciencaj fakoj, precipe en logiko, matematiko, komputado kaj lingvoscienco.

En matematiko formala pruvo de teoremo kadre de formala sistemo estas ĉeno da laŭregulaj inferencoj, kiu komenciĝas per aksiomo(j) kaj finiĝas per la pruvata aserto (la teoremo). La regulojn eblas apliki sen scio pri la signifo de la formuloj, t.e. pure formale, sintakse (oni konkludas laŭ la formo de aserto = laŭ ilia sintakso).

Sinonime oni ankaŭ uzas la terminon kalkulo^[1] (de kiam Lejbnico rimarkis ke matematika pruvo estas speco de kalkulo-komputo); kaj la terminon formalismo (la vorto havas ankaŭ aliajn signifojn, interalie en la filozofio de matemamtiko).

La aksiomajn deduktajn sistemojn la matematikistoj uzadis ekde la klasika antikvo, tamen rigora difino de tiu nocio (formala sistemo) unue aperis en en:«Principia Mathematica» de Bertrand Russell kaj Alfred North Whitehead; speciale pri tiu temo oni ekokupiĝis de 1921, kiam David Hilbert proponis uzi la formalajn sistemojn kiel la fundamenton de matematiko.^[2] Tamen, en 1931 Kurt Gödel pruvis ke ĉiu kohera formala sistemo sufiĉe potenca por esprimi la bazan aritmetikon estas nekompleta (enhavas aserton nek pruveblan nek refuteblan). Tio signifas ke la programo de Hilbert estas nerealigebla.

Kvankam la ambicia Hilberta programo malsukcesis, la formalaj sistemoj plu estas studataj en logiko kaj aplikataj en difersaj fakoj.

Difino de formala sistemo

Formala sistemo estas kvaropo $F=\langle \Sigma ,B,A,R\rangle$ , kie

$\Sigma \quad$ estas signaro (ankaŭ nomata alfabeto aŭ simbolaro), tio estas, numerebla aro da signoj. Ili estas la bazaj signoj, el kiuj konsistas la signoĉenoj de la formala sistemo estas kunmetitaj. Ekz‑e
$\Sigma \supset {}$ {0,1,2,3,4,x,y,+,=,(,),&}.
$B\quad$ estas formala lingvo super $\Sigma ,\ B\subset \Sigma ^{*}$ . Ĝiajn vortojn (la elementoj de $B$ ) oni nomas bonformaj formuloj de $F$ , aŭ simple formuloj. La formuloj estas esprimoj sintakse ĝustaj, ne nepre veraj. Ekz‑e en la tradicia aritmertiko 2+2=5 ${}\in B$ , x+0=x ${}\in B$ ; sed 2+2)=(4 ${}\notin B$ . Kutime oni postulas, ke $B$ estu decidebla aro (alivorte, «decidebla lingvo»). Kutime ĝi estas nefinia.
$A$ estas aro da bonformaj formuloj, $A\subset B$ , nomataj aksiomoj. Ekz‑e $x+y=y+x$ .
$R\quad$ estas aro da inferencaj reguloj. Inferenca regulo estas $n$ -opo $(n\geq 2)$ da formuloj, el kiuj la lasta estas la konkludo, kaj la ceteraj la premisoj.

Derivo aŭ pruvo estas sinsekvo da formuloj tia, ke ĉiu ĝia formulo estas aŭ aksiomo el $A$ , aŭ konkludo de iu(j) el la antaŭa(j) formulo(j) laŭ unu el la inferencaj reguloj de $R$ .

Formulo $\theta$ estas teoremo, se ekzistas derivo en kiu $\theta$ estas la lasta formulo — tiam oni ankaŭ diras, ke $\theta$ estas derivebla (pruvebla) en la teorio $F$ .

La aroj $A$ kaj $R$ (la aksiomoj kaj la reguloj) estas numereblaj, finiaj aŭ nefiniaj. En la lasta okazo iliajn elemerntojn oni difinas per skemoj, uzante metavariablojn, kies valoroj estas la formuloj de $B$ . Ekz‑e en la pruvoj per matematika indukto en aritmetiko de la naturaj nombroj por ĉiu ajn formulo de la formo $\varphi (x,{\vec {\xi }})$ , kie ${\vec {\xi }}=(\xi _{1},\xi _{2},\dots )$ , oni povas uzi la skemon

{\bigl [}\varphi (0,{\vec {\xi }})\ \&\ \forall n(\varphi (n,{\vec {\xi }})\rightarrow \varphi (n+1,{\vec {\xi }})){\bigr ]}\rightarrow \forall n\,\varphi (n,{\vec {\xi }})

Ĉi tie $\varphi ,\xi _{i}$ ktp estas laŭbezone anstataŭigendaj per formuloj el $B$ , kiel konvenas por koncerna pruvo.

Teorio por kiu ekzistas algoritmo ebliganta determini por ajna donita formulo, ĉu ĝi estas derivebla, nomiĝas decidebla; alie, la teorio nomiĝas nedecidebla.

Notoj

↑ Principe eblas prezenti aksiomojn per inferencaj reguloj.

Referencoj

↑ Ekz‑e en Komputada Leksikono, artikolo «kalkulo (2)».
↑ Zach, Richard. (31 July 2003) “Hilbert's Program”, Hilbert's Program, Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.

Literaturo

David Hilbert, W. Ackermann: Grundzüge der theoretischen Logik (Fundamentoj de teoria logiko)0. 6ª eldono , Springer 1972, ISBN 3-540-05843-5.

Formala sistemo en ReVo

Vidu ankaŭ

Formalaj sciencoj

[1] Principe eblas prezenti aksiomojn per inferencaj reguloj.

[2] Ekz‑e en Komputada Leksikono, artikolo «kalkulo (2)».

[:0-3] Zach, Richard. (31 July 2003) “Hilbert's Program”, Hilbert's Program, Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.

[noto 1]

[1]

[2]