Sekvencinis skaičiavimas

Sekvencinis skaičiavimas – matematinės logikos formulių įrodymo būdas. Šis būdas pasižymi tuo, kad įrodymo metu yra konstruojama formulių seka, dar kitaip vadinama sekvencija, kurioje kiekviena formulė yra gaunama iš prieš tai buvusių formulių pagal skaičiavimo taisykles arba aksiomas^[1].

Sekvencinis skaičiavimas yra formulių įrodymo sritis, kuri susideda iš šių skaičiavimų:

Hilberto tipo teiginių skaičiavimo,
Gentzeno tipo teiginių skaičiavimo, kuris susideda iš:
- Natūraliosios dedukcijos,
- Sekvencinio skaičiavimo (kartais dar vadinamo skaičiavimu $G$ ).

Kontekstas redaguoti

XX a. pradėjus atsirasti informatikos užuomazgoms, matematikai stengėsi formalizuoti matematines žinias, jog šios galėtų būti panaudotos algoritmų kūrime, tad vienas iš formalizavimo rezultatų - sekvencinis skaičiavimas. Hilberto tipo teiginių skaičiavimas buvo aprašytas vokiečių mokslininko Deivido Hilberto kaip tiesioginis tapačiai teisingų formulių formalus įrodymo būdas. Gentzeno tipo sekvencinis skaičiavimas (natūralioji dedukcija ir sekvencinis skaičiavimas) - 1934 m. vokiečių matematiko Gerardo Gentzeno aprašytas formalizavimo būdas, kuris nustato tapačiai teisingas formules. Sekvencinį skaičiavimą taip pat tyrinėjo mokslininkai Dagas Pravitsas, Džordžas Kreisleris ir kiti.^[2] ^[3]

Hilberto tipo teiginių skaičiavimas redaguoti

Hilberto tipo teiginių skaičiavimas - tai skaičiavimas su aksiomų schemomis 1.1-4.3 ir Modus Ponens taisykle. Formulė $F$ įrodoma Hilberto tipo teiginių skaičiavime, jei yra tokia formulių seka, kurioje kiekviena formulė yra aksioma arba gauta pagal Modus Ponens taisyklę iš prieš tai parašytų ir kuri (seka) baigiasi formule $F$ ^[4] ^[5].

Formulė $F$ įrodoma Hilberto tipo teiginių skaičiavime tada ir tik tada, kai ji yra tapačiai teisinga. Iš to išplaukia, jog galime įrodyti ir faktą, jog formulė $F$ yra tapačiai klaidinga įrodydami, kad $\lnot F$ yra tapačiai teisinga. Jeigu formulės tapataus teisingumo arba klaidingumo įrodyti nepavyksta, šis skaičiavimas nieko nepasako apie formulės teisingumą ar klaidingumą.

Aksiomų schemos

$1.1.$ $A\rightarrow (B\rightarrow A)$

$1.2.$ $(A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C))$

$2.1.$ $(A\land B)\rightarrow A$

$2.2.$ $(A\land B)\rightarrow B$

$2.3.$ $(A\rightarrow B)\rightarrow ((A\rightarrow C)\rightarrow (A\rightarrow (B\land C)))$

$3.1.$ $A\rightarrow (A\lor B)$

$3.2.$ $B\rightarrow (A\lor B)$

$3.3.$ $(A\rightarrow C)\rightarrow ((B\rightarrow C)\rightarrow ((A\lor B)\rightarrow C))$

$4.1.$ $(A\rightarrow B)\rightarrow (\lnot B\rightarrow \lnot A)$

$4.2.$ $A\rightarrow \lnot \lnot A$

$4.3.$ $\lnot \lnot A\rightarrow A$

Taisyklė Modus ponens:

$P\to Q,\;P\;\;\vdash \;\;Q$

Gentzeno tipo sekvencinis skaičiavimas redaguoti

Gentzeno tipo sekvenciniuose skaičiavimuose yra formuojamas išvedimo medis tikrinamai formulei $F$ . Jis konstruojamas pagal tam skaičiavimui priklausančias taisykles bandant gauti visose šakose aksiomas. Sekvencinio skaičiavimo taisyklė yra apverčiama, jei taisyklės išvada išvedama tada ir tik tada, kai išvedamos visos taisyklės prielaidos. Ne visos natūraliosios dedukcijos taisyklės yra apverčiamos, sekvenciniame skaičiavime apverčiamos taisyklės yra visos^[6].

Tiek natūralioji dedukcija, tiek ir sekvencinis skaičiavimas vienodai įrodo formulės tapatų teisingumą, todėl yra įrodyta, jog šie skaičiavimai rezultatų prasme yra izomorfiški^[7]^[8]. Taip pat yra įrodyta, jog Gentzeno tipo sekvencinis skaičiavimas rezultato prasme yra ekvivalentus Hilberto tipo teiginių skaičiavimui^[9].

Natūralioji dedukcija redaguoti

Natūralioji dedukcija yra sekvencinis skaičiavimas su aksioma $A\vdash A$ ir taisyklėmis. Įrodymo metodas įrodymu yra laikomas tada ir tik tada, kai jam pakanka taisyklių, kad būtų gaunama aksioma. Nagrinėjamas skaičiavimas apibendrina natūraliųjų skaičiavimų variantus ir skiriasi nuo pradinių tokio tipo skaičiavimų. Kaip ir sekvenciniame skaičiavime, sekvencija $\vdash F$ išvedama tada ir tiktai tada, kai $F$ tapačiai teisinga ^[6]^[10].

Natūraliojo skaičiavimo įrodymas paremtas implikacijos taisykle: jei $B$ gali būti gaunama iš $A$ pagal išvedimo taisyklę, tai $A\rightarrow B$ įrodyta. Implikacijos ( $\rightarrow$ ) operacijos simbolis taisyklėse žyminas $\vdash$ simboliu. Svarbu, kad sekvencijų dešinėje pusėje nuo paskutinės implikacijos taisyklės yra ne daugiau kaip viena formulė ^[11].

Natūraliosios dedukcijos taisyklės

Loginės įvedimo taisyklės:	Loginės eliminavimo taisyklės:
${\cfrac {\Gamma ,A\vdash B}{\Gamma \vdash A\rightarrow B}}\quad ({\rightarrow }$ įv.* $)$	${\cfrac {\Gamma \vdash A\qquad \Delta \vdash A\rightarrow B}{\Gamma ,\Delta \vdash B}}\quad ({\rightarrow }$ el. $)$
${\cfrac {\Gamma \vdash A\qquad \Delta \vdash B}{\Gamma ,\Delta \vdash A\land B}}\quad ({\land }$ įv. $)$	${\cfrac {\Gamma \vdash A\land B}{\Gamma \vdash A}}\quad ({\land }_{1}$ el. $)$ , $\quad {\cfrac {\Gamma \vdash A\land B}{\Gamma \vdash B}}\quad ({\land }_{2}$ el. $)$
${\cfrac {\Gamma \vdash A}{\Gamma \vdash A\lor B}}\quad ({\lor }_{1}$ įv. $)$ , $\quad {\cfrac {\Gamma \vdash B}{\Gamma \vdash A\lor B}}\quad ({\lor }_{2}$ įv. $)$	${\cfrac {\Gamma \vdash A\lor B\qquad \Delta ,A\vdash C\qquad \Delta ',B\vdash C}{\Gamma ,\Delta ,\Delta '\vdash C}}\quad ({\lor }$ el. $)$
${\cfrac {\Gamma ,A\vdash }{\Gamma \vdash \lnot A}}\quad ({\lnot }$ įv.* $)$	${\cfrac {\Gamma \vdash A\qquad \Delta \vdash \lnot A}{\Gamma ,\Delta \vdash }}\quad ({\lnot }_{1}$ el. $)$ , $\quad {\cfrac {\Gamma ,\lnot A\vdash }{\Gamma \vdash A}}\quad ({\lnot }_{2}$ el.* $)$
Struktūrinės taisyklės:
${\cfrac {\Gamma \vdash }{\Gamma \vdash A}}\quad ($ silpninimas $)$	${\cfrac {\Gamma \vdash A}{\Gamma ,B\vdash A}}\quad ($ silpninimas $)$
${\cfrac {\Gamma ,A,B,\Delta \vdash C}{\Gamma ,B,A,\Delta \vdash C}}\quad ($ perstatymas* $)$	${\cfrac {\Gamma ,A,A,\Delta \vdash C}{\Gamma ,A,\Delta \vdash C}}\quad ($ kartojimas* $)$

Čia $\Gamma ,\Delta ,\Delta '$ yra baigtinės formulių sekos (gali būti ir tuščios). $A,B,C$ — formulės. Taisyklių prielaidose esančių formulių tvarka yra nesvarbi. Žvaigždute pažymėtos taisyklės yra apverčiamos^[12].

Skaičiavimai vadinami natūraliosiomis sistemomis, nes perėjimai nuo prielaidų prie išvadų modeliuoja tiek šnekamosios kalbos, tiek mokslininkų įrodymuose vartojamus samprotavimus^[13].

Sekvencinis skaičiavimas redaguoti

Sekvencinis skaičiavimas (Gentzeno tipo sekvencinis skaičiavimas arba sekvencinis skaičiavimas $G$ ) - tai skaičiavimas su aksioma $\Gamma ,A,\vdash A,\Delta$ ir taisyklėmis $(\rightarrow \vdash )$ , $(\vdash \rightarrow )$ , $(\land \vdash )$ , $(\vdash \land )$ , $(\lor \vdash )$ , $(\vdash \lor )$ , $(\lnot \vdash )$ , $(\vdash \lnot )$ ^[6].

Sekvencija $S$ išvedama sekvenciniame skaičiavime, jeigu yra toks medis, kuriam teisinga ^[3]:

kiekvienoje medžio viršūnėje yra sekvencija,
medžio šaknyje yra sekvencija $S$ ,
jei viršūnė $V'$ turi vaikus $V_{1}$ (ir $V_{2}$ ) ir viršūnėse $V'$ , $V_{1}$ (, $V_{2}$ ) yra atitinkamai sekvencijos $S'$ , $S_{1}$ (, $S_{2}$ ), tai sekvencija $S'$ yra gauta pagal kurią nors sekvencinio skaičiavimo taisyklę iš sekvencijų $S_{1}$ (ir $S_{2}$ ),
visuose medžio lapuose yra sekvencijos, kurios yra aksiomos.

Logikos formulė $F$ yra tapačiai teisinga tada ir tik tada, kai sekvencija $\vdash F$ yra išvedama sekvenciniame skaičiavime. Iš to išplaukia, jog formulė $F$ yra tapačiai klaidinga tada ir tik tada, kai yra išvedama skaičiavime sekvencija $F\vdash$ .

Aksioma: $\Gamma ,A\vdash A,\Delta$ , kur $A$ yra formulė, o $\Gamma$ ir $\Delta$ yra formulių sekos (gali būti ir tuščios).

Taisyklės:

$(\rightarrow \vdash ){\cfrac {\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\rightarrow B\vdash \Delta }}$	$(\vdash \rightarrow )\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}$
$(\land \vdash )\quad {\cfrac {\Gamma ,A,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}$	$(\vdash \land ){\cfrac {\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}{\Gamma \vdash \Delta ,A\land B}}$
$(\lor \vdash ){\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}$	$(\vdash \lor )\quad {\cfrac {\Gamma \vdash \Delta ,A,B}{\Gamma \vdash \Delta ,A\lor B}}$
$(\lnot \vdash )\quad {\cfrac {\Gamma \vdash \Delta ,A}{\Gamma ,\lnot A\vdash \Delta }}$	$(\vdash \lnot )\quad {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \Delta ,\lnot A}}$

Čia $A$ , $B$ yra formulės, $\Gamma$ , $\Delta$ - formulių sekos (gali būti ir tuščios). Formulių išsidėstymo tvarka nėra svarbi.

Išnašos redaguoti

↑ Hughes, Dominic (2010). „A minimal classical sequent calculus free of structural rules“. Annals of Pure and Applied Logic. 161: 1244–1253.
↑ Zucker, J (1974). „The correspondence between cut-elimination and normalization“ (PDF). Annals of mathematical logic. Eindhoven, The Netherlands: North-Holland. 7: 1–112.
↑ ^3,0 ^3,1 Farooque, Mahfuza (2013). „Automated reasoning techniques as proof-search in sequent calculus“: 13–29. {{cite journal}}: Citatai journal privalomas |journal= (pagalba)
↑ Zach, Richard (2007). Jacquette, Dale (red.). „Hilbert's Program Then and Now“. Philosophy of Logic. Handbook of the Philosophy of Science. Amsterdam: North-Holland: 411–447. ISSN 1878-9846.
↑ Sieg, Wilfried (2009). „Hilbert’s Proof Theory“. Logic from Russell to Church. Handbook of the History of Logic. Amsterdam: North-Holland. 5: 321–384. ISSN 1874-5857.
↑ ^6,0 ^6,1 ^6,2 Norgėla, Stanislovas (2007). „Logika ir dirbtinis intelektas“. Vilnius: TEV. ISBN 978-9955-680-55-0. {{cite journal}}: Citatai journal privalomas |journal= (pagalba)
↑ von Plato, Jan (2011). „A sequent calculus isomorphic to Gentzen's natural deduction“. The Review of Symbolic Logic. Cambridge University Press. 4: 43–53.
↑ Statman, Richard (1977). Barwise, Jon (red.). „Herbrand's Theorem and Gentzen's Notion of a Direct Proof“. Handbook of mathematical logic. Studies in Logic and the Foundations of Mathematics. Elsevier. 90: 897–912. ISSN 0049-237X.
↑ Mints, G. E. (1995). Prawitz, Dag; Skyrms, Brian; Westerståhl, Dag (eds.). „Gentzen-type systems and Hilbert's epsilon substitution method. I“. Logic, Methodology and Philosophy of Science IX. Studies in Logic and the Foundations of Mathematics. Elsevier. 134: 91–122. ISSN 0049-237X.
↑ van der Giessen, Iris (2018). „Natural Deduction Derived from Truth Tables“ (PDF). {{cite journal}}: Citatai journal privalomas |journal= (pagalba)^{[neveikianti nuoroda]}
↑ Indrzejczak, Andrzej. „Natural Deduction“. Internet Encyclopedia of Philosophy.
↑ von Plato, Jan. „The Development of Proof Theory“. The Stanford Encyclopedia of Philosophy (Winter 2018 Edition).
↑ Perea, Miranda; Arevalo, Favio; Arevalo, Linares; Llera, Pilar; Llera, Aliseda; Atocha (2015). „How to prove it in Natural Deduction: A Tactical Approach“. {{cite journal}}: Citatai journal privalomas |journal= (pagalba)

[1] Hughes, Dominic (2010). „A minimal classical sequent calculus free of structural rules“. Annals of Pure and Applied Logic. 161: 1244–1253.

[jz-2] Zucker, J (1974). „The correspondence between cut-elimination and normalization“ (PDF). Annals of mathematical logic. Eindhoven, The Netherlands: North-Holland. 7: 1–112.

[mf-3] 3,0 ^3,1 Farooque, Mahfuza (2013). „Automated reasoning techniques as proof-search in sequent calculus“: 13–29. {{cite journal}}: Citatai journal privalomas |journal= (pagalba)

[4] Zach, Richard (2007). Jacquette, Dale (red.). „Hilbert's Program Then and Now“. Philosophy of Logic. Handbook of the Philosophy of Science. Amsterdam: North-Holland: 411–447. ISSN 1878-9846.

[5] Sieg, Wilfried (2009). „Hilbert’s Proof Theory“. Logic from Russell to Church. Handbook of the History of Logic. Amsterdam: North-Holland. 5: 321–384. ISSN 1874-5857.

[sn-6] 6,0 ^6,1 ^6,2 Norgėla, Stanislovas (2007). „Logika ir dirbtinis intelektas“. Vilnius: TEV. ISBN 978-9955-680-55-0. {{cite journal}}: Citatai journal privalomas |journal= (pagalba)

[7] von Plato, Jan (2011). „A sequent calculus isomorphic to Gentzen's natural deduction“. The Review of Symbolic Logic. Cambridge University Press. 4: 43–53.

[8] Statman, Richard (1977). Barwise, Jon (red.). „Herbrand's Theorem and Gentzen's Notion of a Direct Proof“. Handbook of mathematical logic. Studies in Logic and the Foundations of Mathematics. Elsevier. 90: 897–912. ISSN 0049-237X.

[9] Mints, G. E. (1995). Prawitz, Dag; Skyrms, Brian; Westerståhl, Dag (eds.). „Gentzen-type systems and Hilbert's epsilon substitution method. I“. Logic, Methodology and Philosophy of Science IX. Studies in Logic and the Foundations of Mathematics. Elsevier. 134: 91–122. ISSN 0049-237X.

[10] van der Giessen, Iris (2018). „Natural Deduction Derived from Truth Tables“ (PDF). {{cite journal}}: Citatai journal privalomas |journal= (pagalba)^{[neveikianti nuoroda]}

[11] Indrzejczak, Andrzej. „Natural Deduction“. Internet Encyclopedia of Philosophy.

[12] von Plato, Jan. „The Development of Proof Theory“. The Stanford Encyclopedia of Philosophy (Winter 2018 Edition).

[13] Perea, Miranda; Arevalo, Favio; Arevalo, Linares; Llera, Pilar; Llera, Aliseda; Atocha (2015). „How to prove it in Natural Deduction: A Tactical Approach“. {{cite journal}}: Citatai journal privalomas |journal= (pagalba)

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]