Et bevis i Peano aritmetik

Frederik Eriksen (eriksen@diku.dk)

29. juni 2005

Indhold Figurer Tabeller

1

1 Indledning

Her er en matematisk sætning: Ligheden

n + m = m + n  (1)

gælder for alle naturlige tal n og m. (Ved et “naturligt tal” forstår jeg et ikkenegativt heltal).

Denne rapport indeholder et formelt bevis for sætning (1). Beviset gennemføres inden for rammerne af et formelt system kaldet “Peano aritmetik”. Rapporten er udarbejdet ved hjælp af Logiweb, som er et system til verifikation og publikation af tekster, der indeholder formel matematik. Logiweb har vericeret, at rapportens bevis for sætning (1) er korrekt — så jeg kan tillade mig at påstå, at rapporten ikke indeholder nogen formelle fejl. Jeg har også brugt Logiweb til at publicere rapporten på internettet; adressen er:

http://www.diku.dk/~grue/logiweb/20050502/home/eriksen/peano-commutativity.

Rapportens bevis for (1) findes allerede i litteraturen — se [?], sætning 3.2(h). Det er altså mere rimeligt at betragte rapporten som en formel øvelse i at bruge Logiweb, end som et selvstændigt stykke matematisk arbejde; men formelle øvelser har jo også deres berettigelse.

Rapporten er struktueret som følger: Afsnit 2 handler om Logiweb. Det er ikke en detaljeret beskrivelse af systemet, men giver forhåbentlig oplysninger nok til, at man kan forstå rapportens formelle indhold uden yderligere viden om Logiweb. Afsnit ?? beskriver syntaksen for Peano aritmetik samt det aksiomsystem, der bliver brugt i rapporten. Afsnit ?? præsenterer de 28 hjælpesætninger, som jeg vil bruge til at bevise ligning (1). For overskuelighedens skyld har jeg inddelt hjælpesætningerne i 3 undergrupper: Lemmaer, afledte lemmaer og makroer. Makroerne bliver bevist i afsnit ??; og de resterende hjælpesætninger bliver bevist i afsnit ??.

2 Lidt om Logiweb

Som nævnt i indledningen er denne rapport skrevet ved hjælp af Logiweb. Dette betyder dels, at rapportens formelle indhold er defineret ud fra nogle andre Logiweb-dokumenter, og dels at rapporten har nogle stilistiske særtræk. Disse to facetter ved Logiweb vil jeg kort forklare i afsnit 2.1 og ??. For en detaljeret beskrivelse af hele Logiweb systemet vil jeg henvise til [?]; her kan man bla. læse om den bevischecker, der har verificeret rapportens beviser.

2.1 Formelle konstruktioner

Det formelle indhold af et Logiweb-dokument er sammensat af en række formelle konstruktioner. En formel konstruktion kan repræsentere alt, hvad der har med formel matematik at gøre: Variable, funktioner, lemmaer, beviser, osv. Der er to kilder til konstruktionerne i et Logiweb-dokument: Dels kan man indføre sine egne konstruktioner, og dels kan man importere konstruktioner fra andre