1x2 is 2

Wat volgt is een vrij formeel bewijs voor de propositie 1x2=2. Het is echter niet strict formeel, dat zou tien keer zoveel werk zijn.

Inhoud

1 Axiomatisch systeem 1.1 Ongedefinieerde termen 1.2 Syntactische regels 1.3 Afleidingsregels 1.4 Definitie 1.5 Domein 1.6 Axiomas 2 Een model 3 Theorema 4 Bewijs 5 Opmerkingen

Axiomatisch systeem

Ongedefinieerde termen

@ ' + *

Syntactische regels

Correcte uitdrukkingen zijn gedefinieerd door:

1. @ is een correcte uitdrukking;
2. Als x een correcte uitdrukking is, dan is x' ook een correcte uitdrukking;
3. Als x en y correcte uitdrukkingen zijn, dan zijn (x+y) en (x*y) ook correcte uitdrukkingen.

Correcte zinnen hebben de volgende vorm:

x=y

, waar x en y correcte uitdrukkingen zijn.

Afleidingsregels

De gewoonlijke afleidings- en vervangingsregels.

Definitie

x≠y (x en y correcte uitdrukkingen) betekent ¬(x=y).

Domein

De verzameling van alle correcte uitdrukkingen.

Axiomas

• A1 ∀x∀y [(x'=y') → (x=y) ]
• A2 ∀x (@≠x')
• A3 ∀x [(x≠@) → [∃y(x=y')]]
• A4 ∀x [(x+@)=x]
• A5 ∀x∀y [(x+y')=(x+y)']
• A6 ∀x [(x*@)=@]
• A7 ∀x∀y [(x*y)' = ((x*y)+x)]

Een model

Een interpretatie van dit axiomatisch systeem:

• @ als het geheel getal 0
• ' als het eerstvolgende grootste geheel getal (@' als 1, @'' als 2)
• + als het optellen van gehele getallen
• * als het vermenigvuldigen van gehele getallen

Je kunt laten zien dat, met deze interpretatie, de natuurlijke getallen ({1,2,3,...}) met de operaties optellen en vermenigvuldigen een model is van dit axiomatisch systeem.

Opmerking: Een belangrijk axioma - het inductieaxioma - is hier weggelaten. Zie handout voor details.

XXX Welke handout?

Theorema

Theorema: (@'*@'') = @''

Een paar definities om het leven makkelijk te maken:

1 =_δf @'

2 =_δf 1' =_δf @''

Dus, het theorema wordt: (1*2)=2

Bewijs

Het bewijs is een heel klein beetje informeel wat notatie-haakjes betreft. In het bewijs wordt gebruik gemaakt van de substitutieregel, die niet behandeld is: premissen a=b, b=c geven conclusie a=c.

1.	∀x ((x+@) = x)	(Axioma)
2.	∀x∀y [(x+y') = (x+y)']	(Axioma)
3.	∀x ((x*@) = @)	(Axioma)
4.	∀x∀y [(x*y') = ((x*y)+x)]	(Axioma)
5.	∀y [(1*y') = ((1*y)+1]	(4; UC)
6.	(1*1') = ((1*1)+1)	(5; UC)
7.	(1*2) = ((1*1)+1)	(6; definitie 2)
8.	∀y [((1*1)+y') = ((1*1)+y)']	(2; UC)
9.	((1*1)+@') = ((1*1)+@)'	(8; UC)
10.	((1*1)+@) = (1*1)	(1; UC)
11.	((1*1)+@') = (1*1)'	(9,10; substitutie)
12.	((1*1)+1) = (1*1)'	(11; definitie 1)
13.	(1*2) = (1*1)	(7,12; substitutie)
14.	(1*@') = ((1*@)*1)	(5; UC)
15.	∀y [((1*@)+y') = ((1*@)+y)']	(2; UC)
16.	((1*@)+@') = ((1*@)+@)'	(15;UC)
17.	((1*@)+1) = ((1*@)+@)'	(16; definitie 1)
18.	((1*@)+@) = (1*@)	(1; UC)
19.	((1*@)+1) = (1*@)'	(17,18; substitutie)
20.	(1*@') = (1*@)'	(14,19; substitutie)
21.	(1*@) = @	(3; UC)
22.	(1*@') = @'	(20,21; substitutie)
23.	(1*1) = 1	(22; definitie 1)
24.	(1*2) = 1'	(13,23; substitutie)
25.	(1*2) = 2	(24; definitie 2)

Opmerkingen

1. Erg lang en ingewikkeld
2. Indrukwekkend/verbazingwekkend dat de eigenschappen van de natuurlijke getallen afgeleid kunnen worden van slechts een handvol axioma's door middel van een redelijk hard en gemakkelijk formeel bewijs.