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.

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

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.

Hilberto tipo teiginių skaičiavimas

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$ .

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 $\mathrm{\neg }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\to (B\to A)$

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

$2.1.$ $(A\wedge B)\to A$

$2.2.$ $(A\wedge B)\to B$

$2.3.$ $(A\to B)\to ((A\to C)\to (A\to (B\wedge C)))$

$3.1.$ $A\to (A\vee B)$

$3.2.$ $B\to (A\vee B)$

$3.3.$ $(A\to C)\to ((B\to C)\to ((A\vee B)\to C))$

$4.1.$ $(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$

$4.2.$ $A\to \mathrm{\neg }\mathrm{\neg }A$

$4.3.$ $\mathrm{\neg }\mathrm{\neg }A\to A$

Taisyklė Modus ponens:

$P\to Q,P⊢Q$

Gentzeno tipo sekvencinis skaičiavimas

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.

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. Taip pat yra įrodyta, jog Gentzeno tipo sekvencinis skaičiavimas rezultato prasme yra ekvivalentus Hilberto tipo teiginių skaičiavimui.

Natūralioji dedukcija

Natūralioji dedukcija yra sekvencinis skaičiavimas su aksioma $A⊢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 $⊢F$ išvedama tada ir tiktai tada, kai $F$ tapačiai teisinga .

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

Natūraliosios dedukcijos taisyklės

Loginės įvedimo taisyklės:	Loginės eliminavimo taisyklės:
$\frac{\mathrm{\Gamma },A⊢B}{\mathrm{\Gamma }⊢A\to B}(\to$ įv.*$)$	$\frac{\mathrm{\Gamma }⊢A\mathrm{\Delta }⊢A\to B}{\mathrm{\Gamma },\mathrm{\Delta }⊢B}(\to$ el.$)$
$\frac{\mathrm{\Gamma }⊢A\mathrm{\Delta }⊢B}{\mathrm{\Gamma },\mathrm{\Delta }⊢A\wedge B}(\wedge$ įv.$)$	$\frac{\mathrm{\Gamma }⊢A\wedge B}{\mathrm{\Gamma }⊢A}({\wedge }_1$ el.$)$,$\frac{\mathrm{\Gamma }⊢A\wedge B}{\mathrm{\Gamma }⊢B}({\wedge }_2$ el.$)$
$\frac{\mathrm{\Gamma }⊢A}{\mathrm{\Gamma }⊢A\vee B}({\vee }_1$ įv.$)$,$\frac{\mathrm{\Gamma }⊢B}{\mathrm{\Gamma }⊢A\vee B}({\vee }_2$ įv.$)$	$\frac{\mathrm{\Gamma }⊢A\vee B\mathrm{\Delta },A⊢C{\mathrm{\Delta }}^{\prime },B⊢C}{\mathrm{\Gamma },\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C}(\vee$ el.$)$
$\frac{\mathrm{\Gamma },A⊢}{\mathrm{\Gamma }⊢\mathrm{\neg }A}(\mathrm{\neg }$ įv.*$)$	$\frac{\mathrm{\Gamma }⊢A\mathrm{\Delta }⊢\mathrm{\neg }A}{\mathrm{\Gamma },\mathrm{\Delta }⊢}({\mathrm{\neg }}_1$ el.$)$,$\frac{\mathrm{\Gamma },\mathrm{\neg }A⊢}{\mathrm{\Gamma }⊢A}({\mathrm{\neg }}_2$ el.*$)$
Struktūrinės taisyklės:
$\frac{\mathrm{\Gamma }⊢}{\mathrm{\Gamma }⊢A}($silpninimas$)$	$\frac{\mathrm{\Gamma }⊢A}{\mathrm{\Gamma },B⊢A}($silpninimas$)$
$\frac{\mathrm{\Gamma },A,B,\mathrm{\Delta }⊢C}{\mathrm{\Gamma },B,A,\mathrm{\Delta }⊢C}($perstatymas*$)$	$\frac{\mathrm{\Gamma },A,A,\mathrm{\Delta }⊢C}{\mathrm{\Gamma },A,\mathrm{\Delta }⊢C}($kartojimas*$)$

Čia $\mathrm{\Gamma },\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }$ 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.

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

Sekvencinis skaičiavimas

Sekvencinis skaičiavimas (Gentzeno tipo sekvencinis skaičiavimas arba sekvencinis skaičiavimas $G$) - tai skaičiavimas su aksioma $\mathrm{\Gamma },A,⊢A,\mathrm{\Delta }$ ir taisyklėmis $(\to ⊢)$, $(⊢\to )$, $(\wedge ⊢)$, $(⊢\wedge )$, $(\vee ⊢)$, $(⊢\vee )$, $(\mathrm{\neg }⊢)$, $(⊢\mathrm{\neg })$ .

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

• kiekvienoje medžio viršūnėje yra sekvencija,
• medžio šaknyje yra sekvencija $S$,
• jei viršūnė $V^{\prime }$ turi vaikus $V_1$ (ir $V_2$) ir viršūnėse $V^{\prime }$, $V_1$(, $V_2$) yra atitinkamai sekvencijos $S^{\prime }$, $S_1$(, $S_2$), tai sekvencija $S^{\prime }$ 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 $⊢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⊢$.

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

Taisyklės:

$(\to ⊢)\frac{\mathrm{\Gamma }⊢\mathrm{\Delta },A\mathrm{\Gamma },B⊢\mathrm{\Delta }}{\mathrm{\Gamma },A\to B⊢\mathrm{\Delta }}$	$(⊢\to )\frac{\mathrm{\Gamma }⊢\mathrm{\Delta },A\to B}{\mathrm{\Gamma },A⊢\mathrm{\Delta },B}$
$(\wedge ⊢)\frac{\mathrm{\Gamma },A,B⊢\mathrm{\Delta }}{\mathrm{\Gamma },A\wedge B⊢\mathrm{\Delta }}$	$(⊢\wedge )\frac{\mathrm{\Gamma }⊢\mathrm{\Delta },A\mathrm{\Gamma }⊢\mathrm{\Delta },B}{\mathrm{\Gamma }⊢\mathrm{\Delta },A\wedge B}$
$(\vee ⊢)\frac{\mathrm{\Gamma },A⊢\mathrm{\Delta }\mathrm{\Gamma },B⊢\mathrm{\Delta }}{\mathrm{\Gamma },A\vee B⊢\mathrm{\Delta }}$	$(⊢\vee )\frac{\mathrm{\Gamma }⊢\mathrm{\Delta },A,B}{\mathrm{\Gamma }⊢\mathrm{\Delta },A\vee B}$
$(\mathrm{\neg }⊢)\frac{\mathrm{\Gamma }⊢\mathrm{\Delta },A}{\mathrm{\Gamma },\mathrm{\neg }A⊢\mathrm{\Delta }}$	$(⊢\mathrm{\neg })\frac{\mathrm{\Gamma },A⊢\mathrm{\Delta }}{\mathrm{\Gamma }⊢\mathrm{\Delta },\mathrm{\neg }A}$

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