Arytmetyka – ujęcie aksjomatyczne (4)

Postanowiłem, że zanim dojdziemy do wykazania interesujących nas własności formuły \beta natrzaskam trochę elementarnych twierdzeń z arytmetyki. Chodzi o to, aby poczuć, jak zasada indukcji pracuje i wyrobić sobie wyczucie. Nie definiuje na razie na sztywno jak będą wyglądały dowody formalne. Na pewno nie będę dowodził ‘maszynowo’. Idea jest taka, aby każdy dowód danej formuły, pokazywał, że ją sie da udowodnić z aksjomatów za pomocą reguł, a nie koniecznie sam to przeprowadzał. Przyświeca mi jednak jeszcze cel dodatkowy. Chcę to pisać w sposób na tyle regularny, aby później w oparciu o to, zdefiniować pewien praktyczny format, na podstawie którego mógłbym napisać parser, który mógłby chociaż sprawdzać poprawność dowodów. Ale to zupełnie odległe rozważania. Zaczynajmy więc:

Dla ułatwienia wypiszę jeszcze raz aksjomaty:

A1. \forall(x) x + 1 \not= 0.
A2. \forall(x,y) x + 1 = y + 1 \to x = y.
A3. \forall(x) x + 0 = x.
A4. \forall(x,y) x + (y + 1) = (x + y) + 1.
A5. \forall(x) x \cdot 0 = 0.
A6. \forall(x,y) x\cdot(y+1) = x \cdot y + x.

AI. Dla każdej formuły \phi(y_1, \dots, y_n, x) następująca formuła jest aksjomatem \forall(\vec{y}) (\phi(\vec{y}, 0) \wedge (\forall(n) \phi(\vec{y}, n) \to \phi(\vec{y}, n + 1)) \to (\forall(x)\phi(\vec{y}, x)), gdzie \vec{y} jest skrótem (meta-symbolem), który oznacza y_1, \dots, y_n

T4.1 (Łączność dodawania)[A3, A4, AI]
\forall(x,y,z) (x + y) + z = x + (y + z)
Dowód.
Niech P(x,y,n)='x + (y + n) = (x + y) + n'.

\forall(x,y)(
A3: P(x,y,0) \wedge
\forall(n)(
I:x + (y + n) = (x + y) + n \to
(x + (y + n)) + 1 = ((x + y) + n) + 1 \to
A4: x + ((y + n) + 1) = (x + y) + (n + 1) \to
A4: x + (y + (n + 1)) = (x + y) + (n + 1)
)\to
AI:\forall(n)P(x,y,n)
).

T4.2[A3, A4, AI]
\forall(x) 0 + x = x
Dowód.
Niech P(n) = '0 + n = n'.
A3: P(0) \wedge
\forall(n)(
I:0 + n = n \to
(0 + n) + 1 = n + 1 \to
A4: 0 + (n + 1) = n + 1
)\to
AI:\forall(n)P(n).

T4.3[A3, A4, AI]
\forall(x) x + 1 = 1 + x
Dowód.
Niech P(n) = '1 + n = n + 1'.
A3, T4.2: P(0) \wedge
\forall(n)(
I:1 + n = n + 1\to
(1 + n) + 1 = (n + 1) + 1\to
A4: 1 + (n + 1) = (n + 1) + 1
)\to
AI:\forall(n)P(n).

T4.4 (Przemienność dodawania)[A3, A4, AI]
\forall(x,y) x + y = y + x

Dowód.
Niech P(x,n)='x + n = n + x'.
\forall(x)(
A3, T4.2: P(x,0) \wedge
\forall(n)(
I: x + n = n + x \to
(x + n) + 1 = (n + x) + 1 \to
A4: x + (n + 1) = n + (x + 1) \to
T4.3: x + (n + 1) = n + (1 + x) \to
T4.1: x + (n + 1) = (n + 1) + x
)\to
AI:\forall(n)P(x,n)
).

T4.5[A3-A6, AI]
\forall(x,y) (y+1)x = yx + x

Dowód.
Niech P(y,n)='(y+1)n = yn + n'.
\forall(y)(
A5, A3: P(y,0) \wedge
\forall(n)(
I: (y + 1)n = yn + n\to
(y + 1)n + (y + 1) = (yn + n) + (y + 1)\to
A6: (y + 1)(n + 1) = (yn + n) + (y + 1)\to
T4.1, T4.4: (y + 1)(n + 1) = (yn + y) + (n + 1)\to
A6: (y + 1)(n + 1) = y(n + 1) + (n + 1)
)\to
AI: \forall(n) P(y,n)
).

Ponieważ pewien trening formalny już nastąpił możemy opuszczać kwantyfikatory, a pokazywać jedynie istotę kroku indukcyjnego. W razie czego będzie wiadomo, jak owy krok indukyjny zapisać bardziej formalnie.

T4.6[A3, A5, A6, AI]
\forall(x) 0\cdot x = 0

Dowód
A5: 0\cdot 0
I: 0\cdot n = 0
0\cdot n + 0 = 0 + 0
A3: 0\cdot n + 0 = 0
A6: 0\cdot (n+1) = 0
AI: 0\cdot x=0.

T4.7 (Przemienność mnożenia)[A3-A6, AI]
\forall(x,y) xy = yx

Dowód
T4.6, A5: x\cdot 0 = 0\cdot x
I: xn = nx
xn + x = nx + x
A5, T4.5: x(n + 1) = (n + 1)x
AI: xy = yx.

T4.8 (Rozdzielność mnożenia względem dodawania)[A3-A6, AI]
\forall(x,y,z) x(y+z)=xy+xz

Dowód
T4.6, A3: 0\cdot (y + z) = 0\cdot y + 0\cdot z
I: n(y+z) = ny + nz
n(y+z) + (y+z) = (ny + nz) + (y + z)
T4.1, T4.4: n(y+z) + (y+z) = (ny + y) + (nz + z)
T4.5: (n+1)(y+z) = (n+1)y + (n+1)z
AI: x(y+z)=xy+xz.

T4.9 (Łączność mnożenia) [A3-A6, AI]
\forall(x,y,z) (xy)z = x(yz)

Dowód
T4.6: (0\cdot y)z = 0\cdot (yz)
I: (ny)z = n(yz)
(ny)z + yz = n(yz) + yz
T4.8, T4.7: (ny + y)z = (n + 1)(yz)
T4.5: ((n+1)y)z = (n+1)(yz)
AI: (xy)z = x(yz).

T4.10[A2-A4, AI]
\forall(x,z) x + z = x \to z = 0

Dowód
T4.2: 0 + z = 0 \to z = 0
I: n + z = n \to z = 0
(
(n+1) + z = n + 1 \to
T4.1, T4.4: (n+z) + 1 = n + 1\to
A2: n+z = n\to
I: z=0
)
AI: Teza.

Przypomnimy teraz definicję relacji mniejszości.

D4.11
x < y będzie meta-skrótem formuły \exists(k) x + k = y

T4.12[A3, A4, AI]
\forall(x,y,z) (x < y) \wedge (y < z)\to x < z

Dowód
\forall(x,y,z)(
(x < y) \wedge (y < z)\to
\exists(k_1,k_2)(
D4.11: x + k_1 = y \wedge y + k_2 = z \to
T4.1: z = y + k_2 = (x + k_1) + k_2 = x + (k_1 + k_2)) \to
D4.11: x < z
)

KOMENTARZE (1)

  1. Michał Stanisław Wójcik2012-12-06 13:10:24

    Tak sobie pomyślałem, że dla początkowych twierdzeń będę wypisywał przy nich wszystkie aksjomaty, które są wymagane do pokazania tego twierdzenia. W przypadku późniejszych twierdzeń, gdy będą one korzystać ze wszystkich aksjomatów, nie będę pisał już nic. Ciekawe jak długo to pociągnę :-) Może uda się jednak dojść tak do funkcji $\beta$.

  2. Podgląd live
    Nie opublikowałeś jeszcze tego komentarza! Aby opublikować naciśnij przycisk Opublikuj Komentarz.

Dodaj komentarz