Teh­tä­vä:
Ak­sioo­mis­ta päät­te­ly

Ly­hyt Math­Check-oh­je (uu­teen vä­li­leh­teen)

Täs­sä teh­tä­väs­sä tu­tus­tu­taan ak­sio­maat­tis­ten teo­rioi­den aja­tuk­seen. Teh­tä­vän asiat aut­ta­vat hah­mot­ta­maan eri lu­ku­jär­jes­tel­mien ja sa­man­kal­tais­ten jär­jes­tel­mien ku­ten mat­rii­sit sa­man­lai­suuk­sia ja ero­ja, ja hie­man ym­mär­tä­mään, min­kä­lai­sia asioi­ta sym­bo­li­seen las­ken­taan ja sii­hen pe­rus­tu­vaan te­ko­älyyn liit­tyy.

Seu­raa­vas­sa on esi­mer­kin vuok­si reaa­li­lu­ku­jen kaik­ki ak­sioo­mat. Nii­den ole­te­taan pä­te­vän kai­kil­la reaa­li­lu­vuil­la x, y ja z. Tar­koi­tus ei ole, et­tä opet­te­let ne ul­koa.

(1)	x + 0 = x	nol­la
(2)	x + −x = 0	vas­ta­lu­ku
(3)	(x + y) + z = x + ( y + z)	yh­teen­las­kun lii­tän­näi­syys
(4)	x + y = y + x	yh­teen­las­kun vaih­dan­nai­suus
(5)	x ⋅ 1 = x	yk­kö­nen
(6)	x ≠ 0 → x ⋅ x−1 = 1	kään­teis­ar­vo
(7)	(x ⋅ y) ⋅ z = x ⋅ ( y ⋅ z)	ker­to­las­kun lii­tän­näi­syys
(8)	x ⋅ y = y ⋅ x	ker­to­las­kun vaih­dan­nai­suus
(9)	x ⋅ ( y + z) = x ⋅ y + x ⋅ z	osit­te­lu­la­ki
(10)	¬(0 = 1)	nol­la ei ole yk­kö­nen
(11)	x ≤ y ∧ y ≤ z → x ≤ z	jär­jes­tyk­sen tran­si­tii­vi­suus
(12)	x ≤ y ∧ y ≤ x → x = y	jär­jes­tyk­sen an­ti­sym­met­ri­syys
(13)	x ≤ y ∨ y ≤ x	jär­jes­tys on täy­si
(14)	x ≤ y → x + z ≤ y + z	jär­jes­tys ja yh­teen­las­ku
(15)	0 ≤ x ∧ 0 ≤ y → 0 ≤ x ⋅ y	jär­jes­tys ja ker­to­las­ku
(16)	(ei käy­te­tä täs­sä teh­tä­väs­sä)	täy­del­li­syys­ak­sioo­ma

Täs­tä lin­kis­tä saat ak­sioo­mat uu­teen ik­ku­naan. Va­roi­tus: täy­del­li­syys­ak­sioo­ma saat­taa ai­heut­taa jär­ky­tyk­sen.

Ak­sioo­mien (1), …, (9) si­säl­tä­miä yh­tä­suu­ruuk­sia saa so­vel­taa kum­paan suun­taan ta­han­sa ja myös osa­lau­sek­kei­siin eli isom­man lau­sek­keen si­säl­lä. Esi­mer­kik­si ak­sioo­mal­la (1) voi­daan joh­taa y + x = y + (x + 0). Ak­sioo­mia saa so­vel­taa myös si­ten, et­tä ak­sioo­man muut­tu­jan pai­kal­la on lau­se­ke, mut­ta tu­los pä­tee vain sil­loin kun lau­se­ke on mää­ri­tel­ty. Esi­mer­kik­si ak­sioo­mal­la (2) voi­daan joh­taa x ⋅ 1 + −(x ⋅ 1) = 0, mut­ta ei voi­da joh­taa 0⁻¹ + −0⁻¹ = 0.

Näis­tä ak­sioo­mis­ta seu­raa­vat kaik­ki ne reaa­li­lu­ku­jen omi­nai­suu­det, jot­ka ovat lau­sut­ta­vis­sa niis­sä käy­tet­ty­jen mer­kin­tö­jen ja pre­di­kaat­ti­lo­gii­kan avul­la. Tu­tun omi­nai­suu­den to­dis­ta­mi­nen suo­raan näis­tä ak­sioo­mis­ta kä­sin saat­taa kui­ten­kin vaa­tia pit­kän tyl­sän päät­te­ly­ket­jun. Tä­män ha­vain­nol­lis­ta­mi­sek­si to­dis­tam­me, et­tä x ⋅ 0 = 0. Täy­den­nä laa­ti­koi­hin sen ak­sioo­man nu­me­ro, mi­tä so­vel­let­tiin edel­li­sel­tä ri­vil­tä ny­kyi­sel­le ri­vil­le tul­taes­sa.

		x ⋅ 0
only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 1 = 1	=	x ⋅ 0 + 0
end_of_answer arithmetic hide_expr f_nodes 1 2 =	=	x ⋅ 0 + (x + −x)
end_of_answer arithmetic hide_expr f_nodes 1 3 =	=	(x ⋅ 0 + x) + −x
end_of_answer arithmetic hide_expr f_nodes 1 5 =	=	(x ⋅ 0 + x ⋅ 1) + −x
end_of_answer arithmetic hide_expr f_nodes 1 9 =	=	x ⋅ (0 + 1) + −x
end_of_answer arithmetic hide_expr f_nodes 1 4 =	=	x ⋅ (1 + 0) + −x
end_of_answer arithmetic hide_expr f_nodes 1 1 =	=	x ⋅ 1 + −x
end_of_answer arithmetic hide_expr f_nodes 1 5 =	=	x + −x
end_of_answer arithmetic hide_expr f_nodes 1 2 =	=	0

tai

Jot­ta sai­sim­me päät­te­ly­ket­juis­ta ly­hyem­piä, an­nam­me mo­nil­le joh­ta­mil­lem­me to­si­asioil­le nu­me­rot. Jat­kos­sa nii­tä saa käyt­tää sa­maan ta­paan kuin ak­sioo­mien nu­me­roi­ta 1, …, 16.

(17)

x ⋅ 0 = 0

Ote­taan­pa sa­man tien jat­kon hel­pot­ta­mi­sek­si käyt­töön muu­ta­ma kah­del­la as­ke­leel­la joh­det­ta­vis­sa ole­va la­ki. Kir­joi­ta laa­ti­koi­hin nii­den joh­ta­mi­ses­sa käy­tet­ty­jen ak­sioo­mien nu­me­rot.

(18)	0 + x = x	only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 4 = end_of_answer arithmetic hide_expr f_nodes 1 1 = tai
(19)	−x + x = 0	only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 4 = end_of_answer arithmetic hide_expr f_nodes 1 2 = tai
(20)	1 ⋅ x = x	only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 8 = end_of_answer arithmetic hide_expr f_nodes 1 5 = tai
(21)	0 ⋅ x = 0	only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 8 = end_of_answer arithmetic hide_expr f_nodes 1 17 = tai

Seu­raa­vak­si to­dis­tam­me, et­tä on vain yk­si nol­la. Teem­me sen olet­ta­mal­la, et­tä x + o = x pä­tee jo­kai­sel­la x, ja to­dis­tam­me, et­tä o = 0. Näin tu­lee to­dis­tet­tua, et­tä jo­kai­nen lu­ku, jo­ka to­teut­taa nol­lan pe­rus­omi­nai­suu­den, on yh­tä­suu­ri sen ni­men­omai­sen lu­vun kans­sa, jo­ka alun pe­rin nol­lak­si ni­met­tiin. Täl­lä ker­taa mi­nä an­nan la­kien nu­me­rot ja si­nun pi­tää kir­joit­taa lau­sek­keet.

		o
(1)	=	ok_text Oi­kein! tree_compare o+0;
(4)	=	end_of_answer tree_compare 0+o;
ole­tus	=	end_of_answer tree_compare 0;

tai

Jat­kos­sa ole­tam­me, et­tä yh­teen- ja ker­to­las­ku ovat va­sem­mal­le lii­tän­näi­siä. Siis x + y + z tar­koit­taa sa­maa kuin (x + y) + z, ja x ⋅ y ⋅ z tar­koit­taa sa­maa kuin (x ⋅ y) ⋅ z. Sen, et­tä ker­to­las­ku si­too voi­mak­kaam­min kuin yh­teen­las­ku, ole­tim­me jo ak­sioo­man nu­me­ro only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 9 = () muo­toi­lus­sa. Muis­ta myös, et­tä −1 ⋅ x = −(1 ⋅ x) ei­kä (−1) ⋅ x.
tai

To­dis­taak­sem­me, et­tä myös vas­ta­lu­ku on yk­si­kä­sit­tei­nen, ole­tam­me, et­tä x + X = 0 pä­tee, ja to­dis­tam­me, et­tä X = −x. Al­la tu­lee ti­lan­tei­ta, jois­sa la­kia voi so­vel­taa useam­mal­la kuin yh­del­lä ta­val­la, mut­ta to­den­nä­köi­ses­ti kek­sit vii­meis­tään toi­sel­la yrit­tä­mäl­lä, mi­tä ta­paa tar­koi­tet­tiin. Voit myös hok­sa­ta, et­tä alim­paan laa­tik­koon tu­lee …−x, ja pää­tel­lä si­tä edel­tä­vien laa­ti­koi­den si­säl­tö­jä.

		X
(1)	=	ok_text Oi­kein! tree_compare X+0;
(2)	=	end_of_answer tree_compare X+(x+−x);
(3)	=	end_of_answer tree_compare (X+x)+−x;
(4)	=	end_of_answer tree_compare (x+X)+−x;
ole­tus	=	end_of_answer tree_compare 0+−x;
(18)	=	end_of_answer tree_compare −x;

tai

Tä­män voi teh­dä myös yh­tä­lön rat­kai­se­mi­se­na. Li­sää­mäl­lä ole­tuk­sen x + X = 0 mo­lem­mil­le puo­lil­le va­sem­mal­le −x saa­daan −x + (x + X) = −x + 0, jos­ta (3), (19) ja (18) muut­ta­vat va­sem­man puo­len muo­toon X ja (1) muut­taa oi­kean puo­len muo­toon −x. Niin­pä X = −x. Pal­jon työ­tä jou­dut­tiin te­ke­mään näin­kin, kos­ka sie­ven­nyk­set jot­ka kou­lus­sa ope­tet­tiin te­ke­mään yh­del­lä as­ke­leel­la, vaa­ti­vat ak­sioo­ma tai jo joh­det­tu la­ki ker­ral­laan edet­täes­sä usei­ta vä­li­vai­hei­ta.

Kun ak­sioo­maa (2) käy­te­tään oi­keal­ta va­sem­mal­le, on vaih­to­eh­to­ja ää­ret­tö­mäs­ti. Nol­la saa­daan muu­tet­tua muo­don x + −x li­säk­si muo­toon y + −y tai vaik­ka muo­toon (a + b) ⋅ (c + 1) + −((a + b) ⋅ (c + 1)). To­dis­tus­ta kir­joit­ta­val­la ih­mi­sel­lä on usein suun­ni­tel­ma, mi­ten to­dis­tus vie­dään lä­pi. Suun­ni­tel­ma ker­too, mi­hin muo­toon nol­la muu­te­taan ak­sioo­mal­la (2) ja jo­pa sen­kin, et­tä nyt käy­te­tään ak­sioo­maa (2) ei­kä esi­mer­kik­si ak­sioo­maa (5). Mi­ten tie­to­ko­ne saa­tai­siin kek­si­mään täl­lai­nen suun­ni­tel­ma on te­ko­älyn iso­ja, osit­tain mut­ta ei ko­ko­naan rat­kais­tu­ja ky­sy­myk­siä.

Sit­ten to­dis­tam­me, et­tä −−x = x.

		−−x
(1)	=	ok_text Oi­kein! tree_compare (--x)+0;
(19)	=	end_of_answer tree_compare (--x)+((-x)+x);
(3)	=	end_of_answer tree_compare ((--x)+(-x))+x;
(19)	=	end_of_answer tree_compare 0+x;
(18)	=	end_of_answer tree_compare x;

tai

(22)

−−x = x

Vuo­ros­sa on (x + y) ⋅ z = x ⋅ z + y ⋅ z. Nyt si­nun pi­tää kir­joit­taa se­kä la­kien nu­me­rot et­tä lau­sek­keet. Reit­ti, jo­ta päät­te­ly ete­nee, on niin il­mei­nen, et­tä var­maan se on­nis­tuu. Vii­mei­ses­sä vai­hees­sa sa­maa la­kia so­vel­le­taan kaa­vaan kah­des­ti.

		(x + y) ⋅ z
only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 8 =	=	end_of_answer only_no_yes_off tree_compare z*(x+y);
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 9 =	=	end_of_answer only_no_yes_off tree_compare z*x+z*y;
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 8 =	=	end_of_answer only_no_yes_off tree_compare x*z+y*z;

tai

(23)	(x + y) ⋅ z = x ⋅ z + y ⋅ z

Yk­si vie­lä, en­nen kuin alam­me tut­kia mui­ta il­miöi­tä: −(x ⋅ y) = (−x) ⋅ y. Teh­tä­vän hel­pot­ta­mi­sek­si kes­kim­mäi­nen muo­to on an­net­tu val­mii­na.

		−(x ⋅ y)
only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 1 =	=	end_of_answer only_no_yes_off tree_compare −x*y+0;
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 21 =	=	end_of_answer only_no_yes_off tree_compare −x*y+0*y;
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 2 =	=	end_of_answer only_no_yes_off tree_compare −x*y+(x+−x)*y;
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 23 =	=	−(x ⋅ y) + (x ⋅ y + (−x) ⋅ y)
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 3 =	=	end_of_answer only_no_yes_off tree_compare (−x*y+x*y)+(−x)*y;
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 19 =	=	end_of_answer only_no_yes_off tree_compare 0+(−x)*y;
end_of_answer arithmetic only_no_yes_on hide_expr f_nodes 1 18 =	=	(−x) ⋅ y

tai

(24)	−(x ⋅ y) = (−x) ⋅ y

Tä­hän men­nes­sä olem­me käyt­tä­neet vain ak­sioo­mia, joi­den nu­me­ro on al­le 10, em­me­kä ole käyt­tä­neet nu­me­roa (6). Sii­tä seu­raa, et­tä joh­ta­mam­me to­si­asiat pä­te­vät mo­nes­sa muus­sa­kin jär­jes­tel­mäs­sä kuin reaa­li­lu­vuil­la. Esi­mer­kik­si arit­me­tiik­ka mo­du­lo M, mis­sä M ∈ ℤ⁺, nou­dat­taa ak­sioo­mia (1), …, (5) ja (7), …, (9), jo­ten kaik­ki tä­hän men­nes­sä joh­ta­mam­me pä­tee sii­nä­kin. Nu­me­ro (6) rik­kou­tuu, kos­ka lu­vul­la 2 ei ole kään­teis­ar­voa kun M = 4, ja (10) rik­kou­tuu kun M = 1. Jos M on al­ku­lu­ku, mo­du­laa­ri­nen arit­me­tiik­ka nou­dat­taa ak­sioo­mia (1), …, (10). Ru­bi­kin kuu­tion pyö­räy­tyk­set nou­dat­ta­vat ak­sioo­mia (1), …, (3).

Tä­hän men­nes­sä joh­ta­mam­me to­si­asiat ovat niin vaa­ti­mat­to­mia, et­tä eh­kä ei tun­nu kum­mal­li­sel­ta, et­tä ne pä­te­vät mo­nis­sa jär­jes­tel­mis­sä. Ken­ties kum­mal­li­sem­paa on, et­tä on ole­mas­sa hyö­dyl­li­siä jär­jes­tel­miä, jois­sa osa niis­tä ei pä­de. Esi­mer­kik­si mat­rii­si­las­ken­ta ei nou­da­ta ak­sioo­maa (8).

Se ak­sioo­ma, jo­ka erot­taa reaa­li­lu­vut arit­me­tii­kas­ta mo­du­lo al­ku­lu­ku, on (14). Kaik­ki muut to­teu­tu­vat, kun re­laa­tio­na ≤ käy­te­tään lu­ku­jen 0, …, M − 1 ta­val­lis­ta suu­ruus­jär­jes­tys­tä. (Nu­me­ro (15) on sil­loin san­gen tyl­sä, kos­ka 0 ≤ x pä­tee jo­kai­sel­la x.) Vaik­ka ero ak­sioo­mien ta­sol­la on näin pie­ni, reaa­li­lu­vut ja arit­me­tiik­ka mo­du­lo al­ku­lu­ku ovat hy­vin eri­lai­sia jär­jes­tel­miä! Esi­mer­kik­si arit­me­tii­kas­sa mo­du­lo al­ku­lu­ku on vain ää­rel­li­nen mää­rä eri lu­ku­ja, mut­ta reaa­li­lu­ku­ja on yli­nu­me­roi­tu­vas­ti.

Jos re­laa­tion ≤ ti­lal­la oli­si­kin ≥, kaik­ki muut ak­sioo­mat (1), …, (16) to­teu­tui­si­vat pait­si nu­me­ro only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 15 = (). Niin­pä juu­ri tä­mä ak­sioo­ma on se, jo­ka rat­kai­see, et­tä 0 ≤ 1 ei­kä 1 ≤ 0. Mo­lem­mat ei­vät voi pä­teä yh­tä­ai­kaa ak­sioo­mien end_of_answer arithmetic hide_expr f_nodes 1 10 = () ja end_of_answer arithmetic hide_expr f_nodes 1 12 = () vuok­si (an­na pie­nem­pi nu­me­ro en­sin).
tai

Siis­pä to­dis­tam­me, et­tä 0 ≤ 1! Olet­ta­mal­la 1 ≤ 0, li­sää­mäl­lä mo­lem­mil­le puo­lil­le oi­keal­le −1 ja käyt­tä­mäl­lä (2):sta ja (18):sta saa­daan ok_text Oi­kein! tree_compare 0 <= -1; . Siis edel­lä mai­ni­tun ak­sioo­man →:n va­sen puo­li to­teu­tuu si­joit­ta­mal­la −1 se­kä x:n et­tä y:n pai­kal­le. Sil­loin saa­daan →:n oi­keal­le puo­lel­le end_of_answer tree_compare 0 <= (-1)*(-1); .
tai

Lau­se­ket­ta (−1) ⋅ (−1) voi sie­ven­tää seu­raa­vas­ti:

		(−1) ⋅ (−1)
(24)	=	ok_text Oi­kein! tree_compare -(1*(-1));
(20)	=	end_of_answer tree_compare -(-1);
(22)	=	end_of_answer tree_compare 1;

tai

Siis ole­tuk­ses­ta 1 ≤ 0 joh­dim­me 0 ≤ 1. Kos­ka, ku­ten edel­lä to­te­sim­me, mo­lem­mat ei­vät voi pä­teä yh­tä­ai­kaa, ole­tus 1 ≤ 0 on vää­rä. Sik­si ak­sioo­man only_no_yes_on ok_text Oi­kein! hide_expr f_nodes 1 13 = () no­jal­la 0 ≤ 1.
tai

Kai­ken tä­män vai­van­näön kaut­ta saim­me to­dis­tet­tua 0 ≤ 1! Jot­ta to­dis­tus­jär­jes­tel­mäs­tä oli­si käy­tän­nön hyö­tyä, sen pi­tää pys­tyä to­dis­ta­maan pal­jon sy­väl­li­sem­piä tu­lok­sia. Käy­tän­nös­sä hyö­dyl­li­siä au­to­maat­ti­sia to­dis­tus­jär­jes­tel­miä on ke­hi­tet­ty, mut­ta ai­van help­poa se ei ole ol­lut.

Jos ra­jaus x ≠ 0 pois­tet­tai­siin ak­sioo­mas­ta (6), 0⁻¹ oli­si ole­mas­sa ja sil­le pä­ti­si 0 ⋅ 0⁻¹ = 1. Li­säk­si (21) lu­pai­si, et­tä 0 = 0 ⋅ 0⁻¹. Saa­tai­siin 0 = 1, mi­kä on ris­ti­rii­das­sa ak­sioo­man (10) kans­sa. Ris­ti­rii­das­ta voi­daan lo­gii­kas­sa joh­taa mi­tä ta­han­sa, jo­ten ris­ti­rii­tai­nen jär­jes­tel­mä on käyt­tö­kel­vo­ton. Sik­si ak­sioo­ma­jär­jes­tel­män pi­tää ol­la ris­ti­rii­da­ton. Va­li­tet­ta­vas­ti usein on erit­täin vai­keaa, ken­ties jo­pa mah­do­ton­ta, var­mis­tua, et­tä ak­sioo­ma­jär­jes­tel­mä on ris­ti­rii­da­ton. Reaa­li­lu­ku­jen ak­sioo­ma­jär­jes­tel­män us­ko­taan ole­van ris­ti­rii­da­ton.

Ak­sioo­ma­jär­jes­tel­mä on täy­del­li­nen, jos ja vain jos jo­kai­nen sen kie­lel­lä muo­dos­tet­ta­vis­sa ole­va väit­tä­mä voi­daan sen avul­la osoit­taa oi­keak­si tai vää­räk­si. Väit­tä­män osoit­ta­mi­nen vää­räk­si tar­koit­taa väit­tä­män ne­gaa­tion osoit­ta­mis­ta oi­keak­si. Esi­mer­kik­si väit­tä­mäs­tä, jo­ta ei voi muo­dos­taa ak­sioo­mien (1), …, (15) kie­lel­lä kel­paa sin² x + cos² x = 1, kos­ka se käyt­tää sym­bo­lei­ta sin ja cos, jois­ta (1), …, (15) ei­vät pu­hu.

Reaa­li­lu­ku­jen li­säk­si myös ra­tio­naa­li­lu­vut to­teut­ta­vat ak­sioo­mat (1), …, (15). Kos­ka ∃ x: x ⋅ x = 1 + 1 pä­tee reaa­li­lu­vuil­le mut­ta ei ra­tio­naa­li­lu­vuil­le (kak­ko­sen ne­liö­juu­ri ei ole ra­tio­naa­li­nen), ak­sioo­mis­ta (1), …, (15) ei voi to­dis­taa ∃ x: x ⋅ x = 1 + 1 ei­kä ¬∃ x: x ⋅ x = 1 + 1 (pait­si jos (1), …, (15) on ris­ti­rii­tai­nen, mi­kä on pe­riaat­tees­sa mah­dol­lis­ta mut­ta erit­täin epä­to­den­nä­köis­tä). Niin­pä (1), …, (15) ei­vät muo­dos­ta täy­del­lis­tä ak­sioo­ma­jär­jes­tel­mää (pait­si jos ma­te­ma­tiik­ka on pa­has­ti rik­ki).

Ak­sioo­man (16) ni­men pe­rus­teel­la voi ar­va­ta, mi­ten ti­lan­ne muut­tuu, jos se ote­taan mu­kaan. Ak­sioo­man (16) ta­ri­na on oman teh­tä­vän­sä ar­voi­nen. Ak­sioo­man loo­gi­nen muo­toi­lu on hir­veän nä­köi­nen, mut­ta sen ei pi­dä an­taa pe­läs­tyt­tää. Kun loo­gi­nen muo­toi­lu se­li­te­tään, sen ta­kaa pal­jas­tuu mie­len­kiin­toi­nen ta­ri­na.