Enkonduko en la logikon/Aksioma kalkulo kaj sekvaĵokalkulo

Aksioma kalkulo

Aksioma kalkula baziĝas je aksiomoj, do je bazaj logikaj nepraĵoj, de kiuj oni povas dedukti ĉiujn aliajn logikajn nepraĵojn. Ekzistas deduktoreguloj, kiuj precize difinas, kio estas permesata dedukto kaj kio ne.

La aksioma kalkulo por aserta logiko bezonas nur tri aksiom-skemojn kaj unu deduktan regulon:

Aksiom-skemoj:

$\phi \to \left(\psi \to \phi \right)$
$\left(\phi \to (\psi \rightarrow \chi \right))\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \chi \right)\right)$
$\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$

Ĉiu linio reprezentas ne unu solan aksiomon, sed tutan aksiom-skemon: La literoj φ, χ kaj ψ povas esti anstataŭigitaj per ĉiu ajn formulo. Nur necesas, ke du aperoj de unu greka litero estas anstataŭigitaj per la sama formulo. Ekzemple, pro la unua aksiom-skemo, (A∧B)→(C→(A∧B)) estas aksiomo. Ambaŭ aperoj de φ estis anstataŭigita per (A∧B), kaj la ψ estis anstataŭigita per C.

La dedukta regulo permesas, ke el (φ→ψ) kaj φ oni rajtas dedukti ψ. Tiu regulo nomiĝas elimplikaciigo (multaj lingvoj uzas la latinan nomon modus ponens).

Jen ekzemplo de pruvo de A, (¬B→¬A) ╞ B:

1.              A→((¬B→¬A)→A)              aksiom-skemo 1 kun φ=A kaj ψ=(¬B→¬A)
2.                    A                    antaŭkondiĉo
3.                (¬B→¬A)→A                elimplikaciigo el asertoj 1 kaj 2
4.              (¬B→¬A)→(A→B)              aksiom-skemo 3 kun φ=B kaj ψ=A
5.((¬B→¬A)→(A→B))→(((¬B→¬A)→A)→(¬B→¬A)→B)) aksiom-skemo 2 kun φ=(¬B→¬A), ψ=A, χ=B
6.          ((¬B→¬A)→A)→(¬B→¬A)→B)         elimplikaciigo el asertoj5 kaj 4
7.                (¬B→¬A)→B                elimplikaciigo el asertoj 6 kaj 3
8.                 (¬B→¬A)                 antaŭkondiĉo
9.                    B                    elimplikaciigo el asertoj 7 kaj 8

Same kiel ĉe la arbokalkulo, eblas pruvi, ke la aksioma kalkulo estas senerara kaj kompleta (do ke per la arbokalkulo ĉiam eblas ĝuste decidi, ĉu iu argumento estas valida aŭ ne). Sed la pruvoj per la aksioma kalkulo povas esti tre longaj kaj tedaj, pro kio oni praktike malmulte uzas (kaj malmulte uzu) la aksioman kalkulon. Tamen, la aksioma kalkulo havas belajn teoriajn ecojn: Ĝian senerarecon kaj kompletecon oni povas pli facile pruvi ol la senerarecon kaj kompletecon de aliaj logikaj kalkuloj.

Ekzerco 5-1

Pruvu per la aksioma kalkulo ke A→B sekvas el ¬A.
Pruvu per la aksioma kalkulo, ke A→A estas logika nepraĵo.

Rezultoj

Sekvaĵokalkulo

La sekvaĵokalkulo estas pli praktike uzebla ol la aksioma kalkulo, ĉar en ĝi la normalaj manieroj de argumentado pli bone respeguliĝas.

En la sekvaĵokalkulo oni uzas la esprimon "sekvaĵo" por iu ajn sinsekvo φ₁, φ₂..., φ_n, φ_n+1 de formuloj. La intencita signifo de tia sekvaĵo estas, ke la lasta formulo en ĝi (do ĉi-kaze φ_n+1) logike sekvas el la antaŭaj.

Por pli ŝpareme skribi, ni uzas la simbolon Γ por sinsekvo da formuloj. Γφ tiam estas la sekvaĵo, kies intencita signifo estas ke φ sekvas el la formuloj en Γ. Γφψ havas la signifon, ke ψ sekvas el la formuloj en Γφ, do el φ kaj la formuloj en Γ.

La ideo de la sekvaĵokalkulo estas ke oni transformas sekvaĵojn en aliajn sekvaĵojn ĝis oni alvenas al la sekvaĵo kiu reprezentas la argumenton, kies validecon oni volis pruvi. La reguloj de la sekvaĵokalkulo difinas, per kia sekvaĵo oni rajtas komenci, kaj kiamaniere oni rajtas transformi unu sekvaĵon en alian.

Jen kiel aspektas la reguloj de la sekvaĵokalkulo:

Malfortiga regulo

${\frac {\Gamma \varphi }{\Gamma '\varphi }}$ se $\Gamma$ estas parto de $\Gamma '$ .

Tiu ĉi regulo esprimas, ke se oni pruvis la sekvaĵon $\Gamma \varphi$ , validas ankaŭ la sekvaĵo $\Gamma '\varphi$ , se $\Gamma$ estas parto de $\Gamma '$ . Alivorte, oni ĉiam rajtas aldoni antaŭkondiĉojn al iu valida pruvo sen perdi la validecon.

Antaŭkondiĉa regulo

${\frac {}{\Gamma \varphi }}$ se la formulo $\varphi$ estas en la sinsekvo $\Gamma$ da formuloj.

Tiu ĉi regulo esprimas, ke ĉiam validas sekvaĵo, kies konkludo jam estas inter ĝiaj antaŭkondiĉoj. (La fakto ke neniu sekvaĵo aperas supre de la horizontala linio signifas, ke oni ne bezonas jam antaŭe pruvi iujn ajn aliajn sekvaĵojn, do ke eblas komenci pruvon per ĉi tiu regulo.)

Okazodistingo

${\frac {\begin{aligned}{\Gamma \psi \varphi }\\{\Gamma \neg \psi \varphi }\end{aligned}}{\Gamma \varphi }}$

Por apliki ĉi tiun regulon, la du sekvaĵoj super la linio jam devas esti pruvitaj, por konkludi la validecon de la sekvaĵo sub la linio. La regulo esprimas, ke se oni povas konkludi φ el ψ kaj ankaŭ povas konkludi φ el ¬ψ, tiam oni povas konkludi φ sen supozi ion ajn pri ψ aŭ ¬ψ. Estas kvazaŭ oni distingas du okazojn: Vero de ψ kaj malvero de ψ. Se en ambaŭ okazoj validas φ, ĝi ĉiam validas.

Kontraŭdiro

${\frac {\begin{aligned}{\Gamma \neg \psi \varphi }\\{\Gamma \neg \psi \neg \varphi }\end{aligned}}{\Gamma \psi }}$

Alivorte, se la supozo ke ¬ψ kondukas al kontraŭdiro (al konkludo de φ, kaj al konkludo de ĝia neo ¬φ), tiam ¬ψ devas esti malvera, kaj do eblas konkludi ψ.

Enkonduko de "aŭ" en la antaŭkondiĉojn

${\frac {\begin{aligned}{\Gamma \varphi \omega }\\{\Gamma \psi \omega }\end{aligned}}{\Gamma (\varphi \vee \psi )\omega }}$

Tiu ĉi regulo esprimas, ke se ω sekvas kaj el φ kaj el ψ, tiam ĝi sekvas ankaŭ el la formulo φ∨ψ.

Enkonduko de "aŭ" en la konkludon

Maldekstra versio:

${\frac {\begin{aligned}{\Gamma \varphi }\end{aligned}}{\Gamma (\varphi \vee \psi )}}$

Dekstra versio:

${\frac {\begin{aligned}{\Gamma \varphi }\end{aligned}}{\Gamma (\psi \vee \varphi )}}$

Laŭ ĉi tiu regulo, oni povas malfortigi konkludon φ al φ∨ψ aŭ al ψ∨φ.

redaktata

Daŭrigu per la 6-a ĉapitro: Predikata logiko.