Sekvaĵa kalkulo

En pruva teorio kaj matematika logiko, la sekvaĵa kalkulo estas larĝe sciata konkluda sistemo por logiko de la unua ordo (kaj propona logiko kiel speciala okazo de ĝi). La sistemo estas ankaŭ konata sub la nomo LK, distinganta ĝin de diversaj aliaj sistemoj de simila maniero, kiuj estas kreitaj poste kaj kiuj estas iam ankaŭ nomitaj sekvaĵaj kalkuloj. Alia termino por tiaj sistemoj en ĝeneralo estas gentzen-sistemoj ^[1].

Ĉar sekvaĵaj kalkuloj kaj la ĝeneralaj konceptoj rilatante al ili estas de majora graveco al la tuta kampo de pruva teorio kaj matematika logiko, la sistemo LK estos eksplikita en pli granda detalo pli sube. Iu familiareco kun la bazaj nocioj de predikata logiko (aparte ĝia sintaksa strukturo) estas alprenita.

La sistemo LK

(Formala) pruvo en ĉi tiu kalkulo estas vico de sekvaĵoj, kie ĉiu de la eroj estas derivebla de aro de sekvaĵoj, kiuj troviĝas pli frue en la vico, per uzo de unu el la pli sube reguloj. Intuicia ekspliko de ĉi tiuj reguloj estas donita post tio. Bonvolu ankaŭ konsulti en sekvaĵo kaj regulon de konkludo se vi estas ne familiara kun ĉi tiuj konceptoj.

Historio

La sekvaĵa kalkulo LK estas prezentita far Gerhard Gentzen kiel ilo por studanta natura konkludo (kiu estas ĉirkaŭ antaŭ, kvankam netute tiel formala). Ĝi sinsekve elturniĝis esti multe pli facile trakti kalkulon dum konstruo de logikaj derivaĵoj. La nomo mem estas derivita de la Germana termino Logischer Kalkül, signifa logika kalkulo. Sekvaj kalkuloj estas la maniero de elekto por multaj esploroj pri la subjekto.

La konkludo-reguloj por LK

Jena notacio estos uzata:

$A$ kaj $B$ signifas formulojn de predikato de la unua orda logiko (oni povas ankaŭ limigi ĉi tion al propona logiko),
$\Gamma ,\Delta ,\Sigma$ , kaj $\Pi$ estas finiaj (eble malplenaj) vicoj de formuloj, nomitaj ĉirkaŭtekstoj,
$t$ signifas ajnan termon,
$A[t]$ signifas formulon $A$ , en kiu iuj aperoj de termo $t$ estas de intereso
$A[s/t]$ signifas la formulon kio estas ricevita per anstataŭigo de la termo $s$ por la precizigaj aperoj de $t$ en $A[t]$ ,
$x$ kaj $y$ signifas variablojn,
variablo estas okazanta libera en formulo se ĝiaj nuraj aperoj en la formulo estas ne en la regiono de la kvantizantoj $\forall$ aŭ $\exists$ .
$WL$ kaj $WR$ estas por Malfortigo Maldekstre/Dekstra (en:Weakening Left/Right), $CL$ kaj $CR$ por Kuntiro (en:Contraction), kaj $PL$ kaj $PR$ por Permuto.

Aksiomo	Tranĉo
${\cfrac {\qquad }{A\vdash A}}\quad (I)$	${\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})$
Maldekstraj logikaj reguloj	Dekstraj logikaj reguloj:
${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})$	${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})$
${\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})$	${\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})$
${\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)$
${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)$	${\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)$
${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)$	${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)$
${\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)$	${\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)$
${\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)$	${\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)$
Maldekstraj strukturaj reguloj	Dekstraj strukturaj reguloj
${\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})$	${\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})$
${\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})$	${\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})$
${\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})$	${\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})$

Limigoj: En la reguloj (∀R) kaj (∃L), la variablo y devas ne esti libera en γ, A[x/y], aŭ δ.

Intuicia ekspliko

La pli supraj reguloj povas esti dividitaj en du ĉefajn grupojn: logika kaj struktura aĵoj. Ĉiu el la logikaj reguloj prezentas novan logikan formulon ĉu maldekstre aŭ dekstre de la turita litero "T" $\vdash$ . En kontrasto, la strukturaj reguloj operacias super la strukturo de la sekvaĵoj, ignorante la ĝustan formon de la formuloj. La du esceptoj al ĉi tiu ĝenerala projekto estas la aksiomo de idento (I) kaj la regulo de (Tranĉo).

Kvankam komencita en formala vojo, la pli supraj reguloj permesas tre intuician legon en terminoj de klasika logiko. Konsideru, ekzemple, la regulon (∧L₁). Ĝi diras, ke se oni povas pruvi, ke δ povas esti konkludita de iu vico de formuloj, kiuj enhavas A, tiam oni povas ankaŭ konkludi δ de la (pli forta) supozo, ke A∧B tenas. Ankaŭ, la regulo (¬R) diras, ke se γ kaj A sufiĉas por konkludi δ, tiam de γ sola oni povas ĉu ankoraŭ konkludi δ aŭ A devas esti malvera, kio estas ¬A validas. Ĉiuj reguloj povas esti interpretitaj tiamaniere.

Por intuicio pri la kvantizaj reguloj, konsideru la regulon (∀R). Kompreneble konkludanta, ke ∀x A[x/y] validas sole de la fakto, ke A[y] estas vera estas ne ĝenerale ebla. Se, tamen, la variablo y estas ne menciita aliloke (tio estas, ĝi povas ankoraŭ elektiĝi libere, sen influi la aliajn formulojn), tiam oni povas alpreni, ke A[y] validas por iun ajn valoron de y. La aliaj reguloj devus tiam esti bele simplaj.

Anstataŭ konsidero de la reguloj kiel priskriboj por veraj derivaĵoj en predikata logiko, oni povas ankaŭ konsideri ilin kiel instrukcioj por la konstruado de pruvo por donita propozicio. En tiu okazo la reguloj povas esti legata fundo-supren. Ekzemple, (∧R) diras, ke, por pruvi, ke A∧B sekvas de la supozoj γ kaj Σ, sufiĉas por pruvi, ke A povas esti konkludita de γ kaj B povas esti konkludita de Σ, respektive. Notu, ke donite iun antaŭaĵon, ne estas klare kiel tio fendiĝu en γ kaj Σ. Tamen, estas nur finie multaj eblecoj kontrolendaj, ĉar la antaŭaĵo por supozo estas finia. Tio ankaŭ ilustras kiel pruva teorio povas esti vidita kiel operacia sur pruvoj en kombina maniero: donite pruvojn por ambaŭ A kaj B, oni povas konstrui pruvon por A∧B.

Kiam oni serĉas pruvon, la plejparto de la reguloj ofertas plimalpli rektajn receptojn de kiel fari tion. La regulo de tranĉo estas malsama: ĝi diras, ke, kiam formulo A povas esti konkludita kaj tiu formulo povas ankaŭ servi kiel premiso por konkludo aliajn propoziciojn, tiam la formulo A povas esti "eltranĉi" kaj la respektivaj derivaĵoj estas aligitaj. Kiam oni konstruas pruvon fundo-supren, tio kreas la problemon de konjektado de A (ĉar ĝi ne troviĝas ajne pli sube). Tiu eligo estas adresita en la teoremo de tranĉi-elimino.

La dua regulo, kiu estas io speciala, estas la aksiomo de idento (I). La intuicia lego de tiu estas evidenta: A pruvas A.

Ekzempla derivaĵo

Kiel por ekzemplo, ĉi tiu estas la (sekvenca vica derivaĵo de $\vdash$ (A $\lor$ ¬A), sciata kiel la leĝo de ekskludita mezo (tertium ne datur en latina).

Ĉi tiu derivaĵo ankaŭ emfazas la severe formalan strukturon de sintaksa kalkulo. Ekzemple, la dekstraj logikaj reguloj kiel difinitaj pli supre ĉiam operacias sur la unua formulo de la dekstra sekvaĵo, tia, ke la apliko de (Pr) estas formale postulita. Ĉi tiu tre rigida rezonado povas komence esti malfacila por kompreni, sed ĝi formas la centran kernon de la diferenco inter sintakso kaj semantiko en formalaj logikoj. Kvankam oni scias, ke oni celas la samon per la formuloj A $\lor$ ¬A kaj ¬A $\lor$ A, derivaĵo de la lasta devus ne esti ekvivalento al la unua kiu estas donita pli supre. Tamen, oni povas fari sintaksan rezonadon pli oportunan per prezentado de lemoj, kiuj estas aprioraj projektoj por efektivigi certajn normajn derivaĵojn. Kiel ekzemplo oni povus montri, ke jeno estas vera transformo:

${\cfrac {\Gamma \vdash A\lor B,\Delta }{\Gamma \vdash B\lor A,\Delta }}$

Tuj kiam ĝenerala vico de reguloj estas sciata por konstrui ĉi tiu derivaĵon, oni povas uzi ĝin kiel mallongigon en pruvoj. Tamen, kvankam pruvoj iĝas pli legeblajn per uzo de bonaj lemoj, ili povas ankaŭ fari la procezon de derivaĵo pli komplikan, ĉar estas pli multaj eblaj elektoj konsiderindaj. Ĉi tiu estas aparte grava kiam oni uzas pruvan teorion (kiel ofte deziratas) por aŭtomata konkludo.

Strukturaj reguloj

La strukturaj reguloj meritas iun aldonan diskuton. La nomoj de la reguloj estas Malfortigo (W), Kuntiro (C), kaj Permuto (P). Kuntiro kaj Permuto certigas, ke nek la ordo (P) nek la obleco de aperoj (C) de eroj de la vicoj gravas. Tial, oni povas anstataŭ vicoj ankaŭ konsideri arojn.

La superflua peno uzi vicojn, tamen, estas pravigita ĉar parto aŭ ĉiuj el la strukturaj reguloj povas esti nefaritaj. Farante tiel, uoni ricevas la tiel nomatan substrukturaj logikoj.

Propraĵoj de la sistemo LK

Ĉi tiu sistemo de reguloj povas esti montrita esti kaj soneca kaj plena kun respekto al logiko de la unua ordo, kio estas propozicio A sekvas semantike de aro de premisoj γ ( $\Gamma \vDash A$ ) se kaj nur se la sekvaĵo $\Gamma \vdash A$ povas esti derivita per la pli supraj reguloj.

En sekvaĵa kalkulo, la regulo de tranĉo estas konsentebla. Ĉi tiu rezulto estas ankaŭ nomita Hauptsatz de Gentzen ("Ĉefa Teoremo").

Ŝanĝoj de la sistemo

La pli supraj reguloj povas esti aliigita diversmaniere sen ŝanĝi la esencon de la sistemo LK. Ĉiuj el ĉi tiuj ŝanĝoj povas ankoraŭ nomiĝi kiel LK.

Unue, kiel menciitas pli supre, la sekvaĵoj povas esti viditaj kiel konsistantaj el aroj aŭ multaroj. En ĉi tiu okazo, la reguloj por permuti kaj (kiam uzante arojn) kontrakti formulojn estas arkaike.

La regulo de malfortigo iĝos konsentebla, kiam la aksiomo (I) estas ŝanĝita, tiel, ke iu ajn sekvaĵo de la formo γ, A |- A, δ povas esti konkludita. Tio signifas, ke A pruvas A en iu ajn ĉirkaŭteksto. Iu ajn malfortigo, kiu troviĝas en derivaĵo povas tiam esti plenumita tuj je la komenco. Ĉi tio povas esti oportuna ŝanĝo dum konstruado de pruvoj fundo-supren.

Sendepende de ĉi tiuj oni povas ankaŭ ŝanĝi la manieron en kiuj ĉirkaŭtekstoj estas fenditaj en la reguloj: En la okazoj (∧R), (∨L), kaj (→L) la maldekstra ĉirkaŭteksto estas iel fendita en γ kaj Σ kiam iras supren. Ĉar kuntiro permesas por la duobligon de ĉi tiuj, oni povas alpreni, ke la plena ĉirkaŭteksto estas uzata en ambaŭ branĉoj de la derivaĵo. Per fari ĉi tion, oni certigas, ke ne gravaj premisoj estas perditaj en la erara branĉo. Per uzo de malfortigo, la netaŭgaj partoj de la ĉirkaŭteksto povas esti eliminitaj poste.

Ĉiuj el ĉi tiuj ŝanĝoj liveras ekvivalentajn sistemojn en la senco, ke ĉiu derivaĵo en LK povas efike esti konvertita en derivaĵon uzante la alternativajn regulojn, kaj inverse.

La sistemo LJ

Surprize, iu malgrandaj ŝanĝoj en la reguloj de LK sufiĉias por turni ĝin en pruvan sistemon por instituteca logiko. Tiucele, oni devas limigi al institutecaj sekvaĵoj (kio estas la dekstraj ĉirkaŭtekstoj estas eliminitaj) kaj modifi la regulon (∨L) kiel sekvas:

${\cfrac {\Gamma ,A\vdash C\qquad \Sigma ,B\vdash C}{\Gamma ,\Sigma ,A\lor B\vdash C}}\quad \lor _{L_{i}}$

kie C estas ajna formulo.

La rezultanta sistemo estas nomita kiel LJ. Ĝi estas valida kaj kompleta kun respekto al instituteca logiko kaj konsentas similan tranĉo-eliminan pruvon.

Referencoj

↑ Andrzej-Indrzejczak, An Introduction to the Theory and Applications of Propositional Sequent Calculi (2021, chapter "Gentzen's Sequent Calculus LK"). Accessed 3 August 2022.

Bibliotekoj

PeEnEo: 105346

[1] Andrzej-Indrzejczak, An Introduction to the Theory and Applications of Propositional Sequent Calculi (2021, chapter "Gentzen's Sequent Calculus LK"). Accessed 3 August 2022.

[1]