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.