Oblig3 - tips

Oppgave

1. Se "Sunnhet av f?rsteordens sekventkalkyle" forelesning 8
2. Gj?r oppgave 4 og 5 i ukesoppgavesett 10
   Analyser allkvantorerene f?rst, ikke g? direkte p? eksistenskvantoren.
   Ide: AxEy Pxy - "for enhver x eksisterer en y slik at Pxy holder". Ax Pxf(x); La f tolkes i en modell slik at f for enhver x, dvs. f(x), gir nettopp det elementet (den eksisterende y'en) for den gitte x. Husk ogs? for senere oppgaver i settet at phi ikke n?dvendivis er en kvantorfri formel, og legg ogs? merke til hvilke variabler som velges som argumenter til skolemfunksjonen.
3. => Beskriv en metode/pseudoalgoritme for ? finne den ekvivalente formlen p? SNF.
   <= Denne retningen er triviell fordi ...
4. Gj?r om til PNF f?rst og husk at matrisen av formelen, dvs. den kvantorfrie delen, skal v?re p? NNF.
6. Her burde det i oppgavesettet st?tt forklart at den f?rste regelen er et aksiom. Hva m? vises for aksiomene i kalkylen for ? etablere sunnhet? For den andre regelen m? det vises at reglen bevarer en spesiell egenskap ved anvendelse. Forklar hvorfor dette er nok for ? vise sunnhet.
7. Forst? de nye reglene definert i forrige oppgave skikkelig.
8. I oppgave 4 ukesoppgavesett 8, finnes et eksempel p? en mengde formler som aksiomatiserer en ekvivalensrelasjon.