Udvidelse af S-reglerne

Maja Hanne Tønnesen, Rune Christoffer Kildetoft Andresen & Niels Peter Meyn Milthers

30. juni 2006

Indhold

1 Introduktion

Dette skriftlige projekt er lavet i forbindelse med Logik-kurset 2006^{1}. Vores mål i denne opgave var at bruge Logiweb^{2} til at bevise en delmængde af udsagnene^{3} vedrørende læresætningerne^{4} fra S-systemet, som er beskrevet i Mendelson [?] i kapitel 3.1. For lethedens skyld er alle nummereringer de samme som i Mendelson. Mere præcist går opgaven ud på at bevise 3.2(j-o), bevise 3.4, bevise 3.5, tilføje aksiomet x < y ⇔ ∃z : z ≠ 0 ∧ z + x = y, bevise 3.7, tilføje aksiomer, der definere ¬∀_{obj}z: ¬\overline{y} = \overline{x} · z, bevise 3.10 og bevise 3.11. I afsnittene 3 til 7 er beviserne for de påviste lemmaer gennemgået. Alle trivielle hjælpelemmaer er bevist i appendix ??.

2 Konklusion

Vi har ikke løst opgaven til fulde, men har dog formået at bevise 3.2j-o, 3.4, 3.5a-g. På grund af problemer med definitionen af reglen svarende til “existensial rule” side 77 i Mendelson, har vi som beskrevet i afsnit ?? ikke været i stand til at kunne bevise lemmaerne fra 3.5h og frem. Vi har dog som beskrevet i afsnit ?? og ?? gennemgået hvordan beviserne for 3.5h og “existensial rule” ville have set ud, hvis problemet ikke var opstået. Vi har endvidere kort gennemgået de definitioner, som ville være nødvendige for at kunne påvise Lemma 3.7

1Kursus 061004/202 Logik

2http://logiweb.eu

3Eng.: proposition

4Eng.: theorem