Teh­tä­vä:
Sie­ven­tä­mi­nen pro­po­si­tio­lo­gii­kas­sa

Ly­hyt Math­Check-oh­je (uu­teen vä­li­leh­teen)

Pro­po­si­tio­lo­gii­kas­sa voi sie­ven­tää ja pää­tel­lä mo­nel­la eri ta­val­la. Yk­si help­po te­ho­kas ta­pa, jos­ta voi jo­pa teh­dä Math­Checkil­lä tar­kas­tet­ta­via teh­tä­vä­sar­jo­ja, on va­li­ta jo­kin muut­tu­ja, si­joit­taa sen ar­vok­si F ja sie­ven­tää, si­joit­taa sen ar­vok­si T ja sie­ven­tää, ja yh­dis­tää tu­lok­set. To­dis­tam­me täl­lä ta­val­la, et­tä

¬(P ↔ Q) ⇔ P ↔ ¬Q .

Tar­vit­sem­me seu­raa­vat apu­tu­lok­set.

• X ↔ T ⇔ prop_logic ok_text Oi­kein! hide_expr f_nodes 1 X <=> tai
• X ↔ F ⇔ prop_logic ok_text Oi­kein! hide_expr f_nodes 2 !X <=> tai

Sit­ten to­dis­tam­me ta­voit­teem­me vai­heit­tain.

• Täy­den­nä va­sem­man puo­len sie­ven­nys, kun Q:n pai­kal­le on si­joi­tet­tu F. prop_logic ok_text Oi­kein! f_nodes 1 !(P <-> FF) <=> !(
  !(P <-> FF) <=> !( ) <=> ) <=>
  tai
• Täy­den­nä oi­kean puo­len sie­ven­nys, kun Q:n pai­kal­le on si­joi­tet­tu F. prop_logic ok_text Oi­kein! /*Muis­tat­han, et­tä false ja true kir­joi­te­taan FF ja TT, siis ei F ja T.*/ f_nodes 1 hide_expr P <=> P <-> !
  P <-> ! <=> P <-> <=> P <-> <=> <=>
  tai
• Tu­li­ko sa­mat? prop_logic ok_text Oi­kein!
  ei
  kyl­lä
  tai
• Täy­den­nä va­sem­man puo­len sie­ven­nys, kun Q:n pai­kal­le on si­joi­tet­tu T. prop_logic ok_text Oi­kein! f_nodes 2 !P <=> !(P <->
  !(P <-> ) <=> ) <=>
  tai
• Täy­den­nä oi­kean puo­len sie­ven­nys, kun Q:n pai­kal­le on si­joi­tet­tu T. prop_logic ok_text Oi­kein! f_nodes 2 hide_expr !P <=> P <-> !
  P <-> ! <=> P <-> <=> P <-> <=> <=>
  tai
• Tu­li­ko sa­mat? ok_text Kos­ka va­sen ja oi­kea puo­li sie­ve­ni­vät sa­moik­si kum­mal­la­kin si­joi­tuk­sel­la, ne ovat loo­gi­ses­ti yh­tä­pi­tä­vät, jo­ten ¬(#<i#>P#</i#> ↔ #<i#>Q#</i#>) ⇔ #<i#>P#</i#> ↔ ¬#<i#>Q#</i#> on to­dis­tet­tu. prop_logic
  kyl­lä
  tai

Seu­raa­vak­si to­dis­tam­me, et­tä ↔ on lii­tän­näi­nen eli (P ↔ Q) ↔ R ⇔ P ↔ (Q ↔ R). Tar­vit­sem­me seu­raa­van apu­tu­lok­sen. VihjeTie­to­ko­ne­pe­leis­sä­kin ai­kai­sem­min sa­man pe­lin ai­ka­na koh­da­tuil­la asioil­la saat­taa ol­la käyt­töä myö­hem­min.

• X ↔ ¬Y ⇔ prop_logic ok_text Oi­kein! hide_expr f_top_opr ! f_nodes 4 X <-> !Y <=>
  tai

Sit­ten to­dis­tam­me ta­voit­teem­me vai­heit­tain.

• Si­joi­ta R:n pai­kal­le T ja sie­ven­nä va­sen puo­li. prop_logic ok_text Oi­kein! f_nodes 3
  (P <-> Q) <-> TT
  <=>
  tai
• Si­joi­ta R:n pai­kal­le T ja sie­ven­nä oi­kea puo­li. prop_logic ok_text Oi­kein! f_nodes 3
  P <-> (Q <-> TT)
  <=>
  tai
• Tu­li­han sa­mat?
• Si­joi­ta R:n pai­kal­le F ja sie­ven­nä va­sen puo­li. prop_logic ok_text Oi­kein! f_top_opr ! f_nodes 4
  (P <-> Q) <-> FF
  <=>
  tai
• Si­joi­ta R:n pai­kal­le F ja sie­ven­nä oi­kea puo­li. prop_logic ok_text Oi­kein! f_top_opr <-> f_nodes 4
  P <-> (Q <-> FF)
  <=> end_of_answer prop_logic f_top_opr ! f_nodes 4 hide_expr P <-> !Q
  <=>
  tai
• Jos mo­lem­mis­sa ta­pauk­sis­sa tu­li sa­mat, ↔:n lii­tän­näi­syys on to­dis­tet­tu.

Pro­po­si­tio­lo­gii­kas­sa voi pää­tel­lä myös kaa­vo­ja käyt­tä­mäl­lä sa­maan ta­paan kuin arit­me­tii­kas­sa. Esi­merk­ki­nä to­dis­tam­me, et­tä P → Q ⇔ ¬Q → ¬P. En­sin so­vel­la imp­li­kaa­tion eli­mi­noin­tia, sit­ten kak­sois­ne­gaa­tion eli­mi­noin­tia, ja lo­puk­si imp­li­kaa­tion mää­ri­tel­mää. prop_logic ok_text Oi­kein! f_top_opr \/ f_nodes 6
!Q --> !P
<=> end_of_answer prop_logic f_top_opr \/ f_nodes 4 hide_expr !Q --> !P
<=> end_of_answer prop_logic f_top_opr --> f_nodes 3 hide_expr !Q --> !P
<=>
tai

So­vel­la en­sin imp­li­kaa­tion eli­mi­noin­tia, sit­ten de Mor­ga­nin la­kia, ja kek­si lop­pu it­se! prop_logic ok_text Oi­kein! f_top_opr \/ f_nodes 6
P /\ Q --> P
<=> end_of_answer prop_logic f_nodes 7 hide_expr P /\ Q --> P
<=> end_of_answer prop_logic f_nodes 1 hide_expr P /\ Q --> P
<=>
tai

Toi­si­naan sie­ven­tä­mi­ses­sä voi hyö­dyn­tää si­tä, et­tä jos dis­junk­tion jo­kin osa to­teu­tuu, mui­den osien to­tuus­ar­voil­la ei ole vä­liä.
Jos P ⇔ T, niin P ∨ ¬P ∧ Q ⇔ prop_logic ok_text Oi­kein! f_nodes 1 TT \/ ! TT /\ Q <=> , ja
jos P ⇔ F, niin P ∨ ¬P ∧ Q ⇔ end_of_answer prop_logic f_nodes 1 FF \/ ! FF /\ Q <=> .
Sik­si P ∨ ¬P ∧ Q ⇔ end_of_answer prop_logic f_nodes 3 P \/ ! P /\ Q <=>
tai

Sie­ven­nä P ∧ (¬P ∨ Q) ⇔ prop_logic ok_text Oi­kein! f_nodes 3 P /\ (! P \/ Q) <=>
tai

Sie­ven­nä (P ∧ Q ∨ ¬Q ∧ R) ∧ (P ∨ ¬R) ⇔ prop_logic ok_text Oi­kein! f_nodes 5 (P /\ Q \/ !Q /\ R) /\ (P \/ !R) <=>

tai

Sie­ven­nä seu­raa­vat lau­sek­keet mah­dol­li­sim­man yk­sin­ker­tai­seen muo­toon, jos­sa ei esiin­ny → ei­kä ↔. Va­lit­se it­se kei­not, joi­ta käy­tät. Yh­des­sä koh­das­sa on kak­si komp­lek­si­suus­ra­jaa. Väl­jem­män ra­jan saa­vut­ta­mi­nen riit­tää, mut­ta on hie­noa, jos saa­vu­tat tiu­kem­man­kin.

P → ¬P ⇔ prop_logic ok_text Oi­kein! f_ban --> <->; f_nodes 2 P --> !P <=>

tai

P ↔ Q ↔ P ⇔ prop_logic ok_text Oi­kein! f_ban --> <->; f_nodes 1 P <-> Q <-> P <=>

tai

(P → Q) ∧ ¬(Q → P) ⇔ prop_logic ok_text Oi­kein! f_ban --> <->; f_nodes 4 (P --> Q) /\ !(Q --> P) <=>

tai

P ∧ ¬Q ∨ Q ∧ R ∧ ¬P ∨ Q ∧ P ⇔ prop_logic ok_text Oi­kein! f_ban --> <->; f_nodes 5 P /\ !Q \/ Q /\ R /\ ! P \/ Q /\ P <=>

tai

(P → Q) ∧ (Q → R) ∧ (R → P) ⇔ prop_logic ok_text Oi­kein! f_ban --> <->; f_nodes 14 b_nodes 12 (P --> Q) /\ (Q --> R) /\ (R --> P) <=>

tai

Loo­gi­ses­ti aja­tel­tu!