Enkonduko en la logikon/Arbokalkulo por aserta logiko

En la arbokalkulo oni kreas arbon da formuloj surbaze de iu komenca listo de formuloj. La suba ekzemplo montras arbon, kiun oni povas krei surbaze de la kvar formuloj A, B, (C→¬B) kaj ¬(A∧¬C).

    A
    B
   C→¬B ✓
 ¬(A∧¬C) ✓
   / \
  /   \
 ¬A    C
 ――   / \
     /   \
    ¬C   ¬B 
    ――   ――

Ekzistas certaj reguloj, laŭ kiuj oni povas pluformi la arbon. Certaj reguloj permesas aldoni novan branĉon, aliaj nur aldonas formulon al iu branĉo. Ekzistas reguloj por fermi branĉon (fermita branĉo estas signita per horizontala linio sub ĝi). Se eblas fermi ĉiujn branĉojn, tio signifas, ke la origina listo de formuloj estas memkontraŭdira. La supra arbo estas fermita (do havas nur fermitajn branĉojn), do la origina listo de formuloj estas memkontraŭdira (kiel vi mem povas kontroli per simpla rezonado).

Vi eble miras, ke la arbokalkulo estas uzata por trovi memkontraŭdirojn, dum mi antaŭe diris, ke la logikaj kalkuloj estas uzataj por pruvi la validecon de argumentoj. Por pruvi validecon de argumento per la arbokalkulo, ni devas montri, ke la aro de formuloj, kiu konsistas el la antaŭkondiĉoj kaj la neo de la konkludo, estas memkontraŭdira. Do, se ni volas pruvi ke φ, χ, ψ, ...╞ ω, ni devas pruvi ke estas memkontraŭdiro en φ, χ, ψ, ... , ¬ω. Sed kial tiu memkontraŭdiro pruvas la validecon de la argumento?

Se φ, χ, ψ, ... , ¬ω estas memkontraŭdiraj, tio signifas ke logike ne eblas, ke ĉiuj samtempe estas veraj. Do se la antaŭkondiĉoj φ, χ, ψ, ... ĉiuj estas veraj, ¬ω devas esti malvera, alivorte ω devas esti vera. Do el la vero de la antaŭkondiĉoj sekvas la vero de la konkludo, tiel ke la argumento estas valida.

Reguloj de la arbokalkulo

Ekzistas sep reguloj por aldoni ion al la arbo. Por uzi iun regulon, oni konsideras unu ankoraŭ neuzatan formulon en la arbo. Por ĉiu formulo ekzistas maksimume unu regulo, kiun eblas apliki al ĝi. Ĉe ĉiuj el la sube listigitaj reguloj, la supra formulo montras, kiun formon devas havi iu formulo por ke oni povu apliki tiun regulon al ĝi. Tio, kio aperas sub tiu formulo, devas esti aldonata al ĉiu nefermita branĉo, kiu estas sub la uzata formulo. Post apliko de regulo, oni markas la uzitan formulon per ✓.

    1           2        3         4
   φ∨χ       ¬(φ∨χ)     φ∧χ     ¬(φ∧χ)
   / \         ¬φ        φ        / \
  /   \        ¬χ        χ       /   \
 φ     χ                        ¬φ   ¬χ

    5           6        7
   φ→χ       ¬(φ→χ)     ¬¬φ
   / \          φ        φ
  /   \        ¬χ
 ¬φ    χ 

Do kiun signifon havas tiuj reguloj? Plej facile eblas tion klarigi ĉe la reguloj 1 kaj 3. Ĉe regulo 1, oni uzis formulon de la formo φ∨χ, do formulon kiu asertis ke φ veras aŭ χ veras. Ĉiu el la du eblecoj estas reprezentata per unu branĉo: Unu branĉo ricevas la formulon φ, la alia la formulon χ.

Ĉe regulo 3 aliflanke, oni uzis formulon de la formo φ∧χ, kiu do asertas la veron de φ kaj de χ. Do ne estas du malsamaj eblecoj, sed nur unu ebleco, en kiu ambaŭ formuloj veras. Do ni ne disbranĉigas la arbon, sed simple aldonas φ kaj χ al ĉiu nefermita branĉo, kiu estas sub φ∧χ.

Laŭ similaj konsideroj eblas klarigi ankaŭ la aliajn regulojn. Ekzemple, ĉe regulo 6 ni uzas ¬(φ→χ). Tiu formulo povas esti vera nur se φ→χ estas malvera. Laŭ la verotabelo de "→" el la antaŭa ĉapitro, φ→χ nur povas esti malvera, se φ estas vera kaj χ estas malvera, do se φ kaj ¬χ estas ambaŭ veraj, do ni aldonas ĉi tiujn du formulojn al ĉiu nefermita branĉo, kiu estas sub ¬(φ→χ).

Kaj kiam oni povas fermi branĉon? Tio eblas, kiam ĝi entenas du formulojn, el kiu unu estas la neo de la alia, do du formulojn de la formo φ kaj ¬φ. Oni povas konsideri ne nur formulojn listigitajn post la disbranĉiĝo, sed ankaŭ formulojn listigitajn antaŭe, supre de la disbranĉiĝo. Do en la ekzemplo de la lasta sekcio, la maldekstra branĉo fermiĝas, ĉar la branĉo entenas ¬A, kaj pli supre (antaŭ la disbranĉiĝo) jam aperas A.

Kiun signifon havas tiu fermado de branĉoj. Kiam estas φ kaj ¬φ en iu branĉo, tio signifas ke estas memkontraŭdiro en ĝi, do ke la "ebleco", kiun tiu branĉo reprezentas, logike ne eblas. Do oni povas ignori ĝin dum la sekva plidaŭrigo de la kalkulo. Se ĉiuj branĉoj fermiĝas, tio signifas, ke ĉiuj manieroj interpreti la originajn formulojn kondukas al memkontraŭdiro, do ke estis jam memkontraŭdiro en la originaj formuloj.

Se oni uzis ĉiujn formulojn, kiuj enhavas "→", "∧" aŭ "∨" aŭ komenciĝas per "¬¬" (ankaŭ tiujn kreitajn dum la kalkulo) kaj daŭre estas iu branĉo, kiun ne eblas fermi, tiam la origina listo de formuloj ne estas memkontraŭdira. Sekve, se tiu listo reprezentis argumenton (do konsistis el la antaŭkondiĉoj kaj la neo de la konkludo de iu argumento), tiam tiu argumento ne estas valida.

Eblas pruvi, ke per la arbokalkulo ĉiam eblas ĝuste decidi, ĉu iu argumento estas valida aŭ ne. Alivorte, la arbokalkulo estas senerara (do ĝi ne pruvas la validecon de malvalidaj argumentoj) kaj kompleta (do ĝi pruvas la validecon de ĉiu valida argumento).

Ekzemploj de pruvoj per arbokalkulo

Unue ni montras ke (A∨B), (A→C), (B→C) ╞ C. Fakte temas pri argumento pri kies valideco ĉiu homo povas sufiĉe facile certiĝi: Se veras aŭ A aŭ B, kaj se el A sekvas C kaj el B sekvas C, tiam certe C devas esti vera. Jen kiel oni pruvas la validecon per la tabelkalkulo: Unue oni neas la konkludon, do konsideras la formulojn (A∨B), (A→C), (B→C) kaj ¬C. Nun oni pruvas ke tiuj estas memkontraŭdiraj per kreo de fermita arbo. Oni komencas kun la unubranĉa arbo kiu entenas tiujn formulojn:

(A∨B)
(A→C)
(B→C)
 ¬C

Nun eblas apliki regulon 1 al la formulo en la unua linio:

   (A∨B) ✓
   (A→C)
   (B→C)
    ¬C
    / \
   /   \
  A     B

Ĉi tie ankoraŭ ne eblas fermi iun branĉon, ĉar neniu branĉo entenas iun formulon kaj ĝian neon. Nun oni aplikas regulon 5 al la dua formulo. Memoru, ke oni devas aldoni la novajn formulojn al ĉiu malferma branĉo (do ĉi-kaze al ambaŭ branĉoj):

     (A∨B) ✓
     (A→C) ✓
     (B→C)
      ¬C
      / \
     /   \
    /     \
   A       B
  / \     / \
 /   \   /   \
¬A   C  ¬A    C
――  ――        ――

Nun jam eblis fermi tri el la kvar branĉoj: La plej maldekstra branĉo fermiĝi, ĉar en ĝi troviĝis kaj A kaj ¬A. La dua kaj la kvara branĉo fermiĝis ĉar en ili troviĝis kaj C kaj ¬C (memoru ke ¬C troviĝas en ĉiu branĉo, ĉar ĝi troviĝas en la arbo antaŭ ĝia disbranĉiĝo). Do nun ni nur bezonas pluokupiĝi pri la tria branĉo. Ni ankoraŭ povas apliki regulon 5 al la tria formulo:

     (A∨B) ✓
     (A→C) ✓
     (B→C) ✓
      ¬C
      / \
     /   \
    /     \
   A       B
  / \     / \
 /   \   /   \
¬A   C  ¬A    C
――  ――  / \   ――
       /   \
      ¬B    C
      ――    ――

Nun eblis fermi la du restantajn branĉojn: La maldekstran de ili ĉar ĝi enhavis ¬B kaj B, kaj la dekstran ĉar ĝi enhavis ¬C kaj C. Ĉar nun fermiĝis ĉiuj branĉoj, la argumento estis valida.

Nun mi ankoraŭ donas iun ekzemplon, kiu montras kiel oni povas uzi la arbokalkulon por pruvi la nevalidecon de iu argumento. Do ni volas pruvi la nevalidecon de la argumento "(A∧(B∨¬C)), ¬B, ¬(C∧¬D). Tial D.". Alivorte, ni volas pruvi

$A\land (B\lor \lnot C)),\lnot B,\lnot (C\land \lnot D)\not \models D$

Kiel antaŭe, ni komencas per unubranĉa arbo kiu entenas la antaŭkondiĉojn kaj la neon de la konkludo:

(A∧(B∨¬C))
   ¬B
 ¬(C∧¬D)
   ¬D

Ni nun aplikas regulon 3 al la unua formulo:

(A∧(B∨¬C)) ✓
   ¬B
 ¬(C∧¬D)
   ¬D
    A
 (B∨¬C)

Sekve ni aplikas regulon 4 al la tria formulo:

 (A∧(B∨¬C)) ✓
    ¬B
  ¬(C∧¬D) ✓
    ¬D
     A
  (B∨¬C)
    / \
   /   \
  ¬C   ¬¬D
       ―――

Nun fermiĝis la dekstra branĉo, ĉar ĝi entenis ¬D kaj ĝian neon ¬¬D. Sekve ni aplikas regulon 1 al la sesa formulo:

  (A∧(B∨¬C)) ✓
     ¬B
   ¬(C∧¬D) ✓
     ¬D
      A
   (B∨¬C) ✓
     / \
    /   \
   ¬C   ¬¬D
   / \  ―――
  /   \
 B    ¬C
――

La plej maldekstra branĉo fermiĝis, ĉar ĝi entenas ¬B kaj B. Aliflanke, la mezan branĉon ne eblas fermi, ĉar ĝi entenas neniun memkontraŭdiron. Ankaŭ, ne plu eblas apliki iun ajn regulon, ĉar ĉiuj ankoraŭ neuzataj formuloj estas aŭ simplaj literoj, aŭ literoj kun antaŭa "¬". Tial, la arbo ne estas fermebla, do ni pruvis ke la argumento estas nevalida. Aldone, la nefermita branĉo de la arbo reprezentas eblecon, kiu estas la kaŭzo de tiu nevalideco: En tiu branĉo troviĝas ¬B, ¬D, A kaj ¬C, do oni povas diri ke laŭ tiu branĉo B, D kaj C estas malveraj kaj A vera. En tiu kazo la tri antaŭkondiĉoj (A∧(B∨¬C)), ¬B kaj ¬(C∧¬D) estas veraj, sed la konkludo D estas malvera, do la argumento devas esti nevalida.

Ekzerco 4-1

Uzu la arbokalkulon por pruvi la validecon aŭ nevalidecon de jenaj argumentoj:

1. A, B, C. Tial (A∧B).
2. A, B, (C∨D). Tial (D∧A).
3. (B→C). (C→A). Tial (B→A).
4. ¬¬A. ¬B. (C→B). Tial (C∨¬A)

• Rezulto

Daŭrigu per la 5-a ĉapitro: Aksioma kalkulo kaj sekvaĵokalkulo.