HUMIT1750MN oppgaver uke 38

Gjør deg kjent med teorembeviseren hos Gateway to logic:  Det vil si, tast inn noe du tror er en tautologi og velg Prove the proposition i menyen Task to be performed.  Du kan for eksempel skrive inn formler som blir bevist i dette notatet.  Du vil få ut beviser i et system for naturlig deduksjon som ligner ganske mye på ND1750, men med litt andre regler. (Til dels har de bare andre navn.)   Bevisene skrives i nesten samme format som i notat i lenken over, og som vi har sett på forelesningene; eneste forskjell (utover at de dropper indenteringer) er at kolonnen som viser avhengigheter er flyttet helt til venstre, og kolonnen med linjenumre står helt inntil kolonnen med utsagn, inni parenteser.  Finn ut hvilke regler dette systemet inneholder, og skriv dem, hvis mulig, opp i formatet som er brukt i boka (f.eks. i boksen side 371) og i arket som beskriver ND1750.  Finner du noen regler av samme type som våre CP og IP, det vil si regler som eliminerer avhengigheter?  Jeg har selv funnet 2.  Forsøk å gi generelle beskrivelser av disse reglene også.

Systemet produserer i mange tilfeller unødvendig lange og nokså klønete beviser.  Dette er fordi det bruker en nokså enkel, generell strategi for å finne beviser.  Klarer du å se omtrent hva denne strategien går ut på?

Gjør oppgavene 1, 2, 4, 5ab og 8 side 381−383 i læreboka.  Prøv å klare deg med reglene i ND1750.  Bevis dessuten (også i ND1750) implikasjonene   ¬ (A ∨ B) → (¬ A ∧ ¬ B)   og    (¬ A ∧ ¬ B)  →   ¬ (A ∨ B) .

Bevis til slutt de to utsagnene (A → B) → ((B → C) → (A → C)) og  (¬ C ∨ ¬ D) → ((A → C) → ((B → D) → (¬ A ∨ ¬ B))) i  ND1750 uten bruk av reglene HS og DD.  Forklar hvorfor dette viser at versjonene av ND1750 med og uten HS og DD er like sterke, det vil si at de lar oss bevise nøyaktig de samme utsagnene.