Viis lehte: mida teoreem ütleb, kuidas valem kokku pannakse, tõestuspuu, mille ehitad ise, võrdlus koolimatemaatikaga ning sama tõestus resolutsiooni meetodiga. Lehtede vahel saad menüüs vabalt liikuda.
Koolis: täisnurkse kolmnurga hüpotenuusi ruut võrdub kaatetite ruutude summaga.
Siin nimetame kolmnurga tipud väikeste tähtedega a, b, c — loogikas on see tavaks. Täisnurk on tipus b. Külgede pikkused kirjutame kaugusfunktsiooniga: d(a,b) on punktide a ja b kaugus.
Lohista lillat punkti b (või vali see Tab-klahviga ja liiguta nooltega). Katkendjoonega ring näitab kohti, kus nurk b juures on täpselt 90°.
Proovi leida asend, kus φ(Täisnurk(a,b,c)) = 1, aga φ(d(a,c)² = d(a,b)² + d(b,c)²) = 0. Sa ei leia — just seda teoreem lubabki. Kui nurk pole täisnurk, on eeldus väär ja implikatsioon on ikka tõene (tõeväärtustabelis 0 → 0 = 1).
Miks katsetamisest ei piisa? Kolmnurki on lõpmata palju. Ükskõik kui palju neid järele proovime, jääb alati proovimata rohkem. Tõestus on argument, mis töötab korraga kõigi kolmnurkade jaoks. Järgmistes sammudes õpime sellise argumendi ehitamist.
Predikaatloogikas on kahte sorti tükke — täpselt nagu tavakeeles on nimisõnad ja laused.
| Mis see on? | Näited | |
|---|---|---|
| Term | Nimetab mingi asja: punkti või arvu. Ei väida midagi. | a, d(a,b), d(a,b)² |
| Valem | Väide, millel on tõeväärtus 0 või 1. | Täisnurk(a,b,c), d(a,b) = d(b,a) |
Küsimus „kas d(a,b) on tõene?" on sama mõttetu kui „kas laud on tõene?". Aga „d(a,b) = 5" on väide — see võib olla tõene või väär.
| Sümbol | Loe nii | Mis ta teeb |
|---|---|---|
| d(x,y) | x ja y kaugus | kahest punktist → arv (term) |
| Kollineaarne(x,y,z) | x, y, z on ühel sirgel | kolmest punktist → väide |
| B(x,y,z) | y on x ja z vahel (B nagu ingl. between) | kolmest punktist → väide |
| Täisnurk(x,y,z) | nurk tipus y on 90° | kolmest punktist → väide |
| Kolmnurk(x,y,z) | x, y, z on kolmnurga tipud | lühend: x≠y ∧ y≠z ∧ x≠z ∧ ¬Kollineaarne(x,y,z) |
| ¬ ∧ ∨ → | ei · ja · või · kui…, siis… | väidetest → uus väide |
| ∀x ∃x | iga x korral · leidub x | väitest → uus väide |
Vali iga rea juures, kas see on term (asi), valem (väide) või hoopis vigaselt kirjutatud.
Teoreem. Kui punktid a, b, c moodustavad kolmnurga ja nurk tipus b on täisnurk, siis hüpotenuusi ruut võrdub kaatetite ruutude summaga. See kehtib iga kolme punkti a, b, c korral.
∀a ∀b ∀c (Kolmnurk(a,b,c) ∧ Täisnurk(a,b,c) → d(a,c)² = d(a,b)² + d(b,c)²)
Mida teoreem ütleb. Teoreemil on kolm osa: „iga a, b, c korral" (∀a ∀b ∀c), „kui a, b, c on kolmnurk ja nurk tipus b on täisnurk" (eeldus) ja „siis d(a,c)² = d(a,b)² + d(b,c)²" (väide).
Kuidas sellist teoreemi tõestatakse.
Sammud 4 ja 5 on tõestuspuu kaks kõige alumist sõlme.
Kuidas tõestuspuud lugeda. Ülal on read, mida me juba teame: eeldus (1), lemmad L1–L3 ja eeldus h. Igast sõlmest läheb joon allapoole: alumine sõlm tuletatakse temaga ühendatud ülemistest sõlmedest ühe reegliga. Kõige all on teoreem ise.
Kuidas liikuda. Klõpsa sõlmel, kus on ? (sõlme saab täita siis, kui kõik tema kohal olevad sõlmed on täidetud). Paremal: (1) vali reegel, (2) vali tulemus, (3) vajuta Kontrolli. Kui ei tea, mida teha, vajuta Vihje.
Eeldus h. Lemma L1 ütleb, et leidub punkt h (kõrguse aluspunkt). Et temaga töötada, ütleme: „olgu h see punkt". See on teine ajutine eeldus. Lõpus, kui tulemuses h-d enam pole, suletakse see reegliga ∃E.
Mida tähendab B(a,h,c)? „Punkt h on punktide a ja c vahel" (B nagu inglise between).
Kolm geomeetria fakti, mida tõestuses kasutame. Igaühe juures on kirjas, mida ta ütleb, miks see kehtib ja milleks seda tõestuses vaja on.
Siin on Pütagorase teoreemi tõestus nii, nagu seda tehakse koolimatemaatikas — joonise, sarnaste kolmnurkade ja tavalise arvutamisega. Iga sammu juures on kast Tõestuspuus: see näitab, millised tõestuspuu sõlmed teevad sama asja loogika keeles.
Miks on tõestuspuus rohkem samme? Koolis jäetakse „iseenesestmõistetavad" sammud kirja panemata. Näiteks lause „kõrgus on olemas" kasutab tegelikult üldist reeglit (kõigi kolmnurkade kohta) meie konkreetse kolmnurga jaoks — tõestuspuus on see reegel ∀E. Loogikas peab iga mõttesamm olema eraldi kirjas, et selle õigsust saaks mehaaniliselt kontrollida.
Tähised. Kaatetid p = |ab| ja q = |bc|, hüpotenuus r = |ac|. Kõrguse aluspunkt on h ning hüpotenuusi osad on x = |ah| ja y = |hc|. Tõestuspuus kirjutatakse sama pikkus kujul d(a,b) jne. (Lülita tõestuspuus sisse „Lühendid p, q, r, x, y", siis näed seal samu tähti.)
Resolutsioon on teine viis sama teoreemi tõestada. Me ei liigu eeldustest teoreemini, vaid teeme vastuväiteliselt: oletame, et teoreem ei kehti, ja näitame, et sellest tuleb vastuolu — tühi klausel □.
Töötame predikaatloogika tasemel: klauslites on muutujad, ∃-kvantorid kõrvaldatakse Skolemi konstantide ja funktsioonidega ning klauslid kirjutame kohe meie kolmnurga a, b, c ja kõrguse aluspunkti h jaoks.
| K(x,y,z) | Kolmnurk(x,y,z) | x, y, z on kolmnurk |
| T(x,y,z) | Täisnurk(x,y,z) | nurk tipus y on täisnurk |
| B(x,y,z) | B(x,y,z) | y on x ja z vahel |
| E₁(x,y,z,h) | d(x,y)² = d(x,h)·d(x,z) | esimene sarnasuse võrdus |
| E₂(x,y,z,h) | d(y,z)² = d(h,z)·d(x,z) | teine sarnasuse võrdus |
| S(x,y,z) | d(x,y) + d(y,z) = d(x,z) | lõigud liituvad |
| P(x,y,z) | d(x,z)² = d(x,y)² + d(y,z)² | Pütagorase võrdus |
Teoreem on siis: ∀x∀y∀z (K(x,y,z) ∧ T(x,y,z) → P(x,y,z)).
¬∀x∀y∀z (K(x,y,z) ∧ T(x,y,z) → P(x,y,z))
1.–2. ∃x∃y∃z (K(x,y,z) ∧ T(x,y,z) ∧ ¬P(x,y,z)) (¬∀ ≡ ∃¬, De Morgan, ¬¬A ≡ A)
4. ∃-kvantorite ees ei ole ühtegi ∀, seega asendame x, y, z Skolemi konstantidega a, b, c — „olgu a, b, c see kolmnurk, mille korral teoreem ei kehti":
(1) K(a,b,c) (2) T(a,b,c) (3) ¬P(a,b,c)
∀x∀y∀z (K(x,y,z) ∧ T(x,y,z) → ∃h (B(x,h,z) ∧ T(x,h,y) ∧ T(y,h,z)))
1.–3. ∀x∀y∀z ∃h (¬K(x,y,z) ∨ ¬T(x,y,z) ∨ (B(x,h,z) ∧ T(x,h,y) ∧ T(y,h,z)))
4. ∃h on ∀x∀y∀z sees, seega punkt h sõltub kolmnurgast. Asendame h Skolemi funktsiooniga h(x,y,z) — kõrguse aluspunkt kolmnurgas xyz:
∀x∀y∀z (¬K(x,y,z) ∨ ¬T(x,y,z) ∨ (B(x,h(x,y,z),z) ∧ T(x,h(x,y,z),y) ∧ T(y,h(x,y,z),z)))
Miks funktsioon, mitte konstant? Igal kolmnurgal on oma kõrguse aluspunkt. Konstant väidaks, et üks ja sama punkt sobib kõigile kolmnurkadele — see oleks vale.
5. Meie kolmnurgas: x = a, y = b, z = c. Kõrguse aluspunkt on h(a,b,c); kirjutame lühidalt h.
6. Distributiivsus A ∨ (X ∧ Y ∧ Z) ≡ (A ∨ X) ∧ (A ∨ Y) ∧ (A ∨ Z) annab kolm klauslit:
(4) ¬K(a,b,c) ∨ ¬T(a,b,c) ∨ B(a,h,c)
(5) ¬K(a,b,c) ∨ ¬T(a,b,c) ∨ T(a,h,b)
(6) ¬K(a,b,c) ∨ ¬T(a,b,c) ∨ T(b,h,c)
∀x∀y∀z∀h (T(x,y,z) ∧ B(x,h,z) ∧ T(x,h,y) ∧ T(y,h,z) → E₁(x,y,z,h) ∧ E₂(x,y,z,h))
∃-kvantorit pole, Skolemi sümboleid pole vaja. Meie punktide jaoks: x = a, y = b, z = c ja h = h(a,b,c). Kaks „siis"-osa annavad kaks klauslit:
(7) ¬T(a,b,c) ∨ ¬B(a,h,c) ∨ ¬T(a,h,b) ∨ ¬T(b,h,c) ∨ E₁(a,b,c,h)
(8) ¬T(a,b,c) ∨ ¬B(a,h,c) ∨ ¬T(a,h,b) ∨ ¬T(b,h,c) ∨ E₂(a,b,c,h)
∀x∀y∀z (B(x,y,z) → S(x,y,z))
Meie lõigu jaoks: x = a, y = h, z = c.
(9) ¬B(a,h,c) ∨ S(a,h,c)
∀x∀y∀z∀h (E₁(x,y,z,h) ∧ E₂(x,y,z,h) ∧ S(x,h,z) → P(x,y,z))
Kui kehtivad mõlemad sarnasuse võrdused ja lõigud liituvad, siis kehtib Pütagorase võrdus — see on kooli arvutus: liida võrdused, too d(x,z) sulgude ette, asenda summa. Meie punktide jaoks: x = a, y = b, z = c, h = h(a,b,c).
(10) ¬E₁(a,b,c,h) ∨ ¬E₂(a,b,c,h) ∨ ¬S(a,h,c) ∨ P(a,b,c)
Suurem osa puust on valmis. Täida tühjad kohad: lohista paremalt sobiv klausel tühja kasti (või klõpsa klauslil ja siis kastil). Iga paigutus kontrollitakse kohe.
Resolveerimine: võtame kaks klauslit, kus ühes on literaal ja teises selle eitus (nt ¬P(a,b,c) ja P(a,b,c)), kustutame selle paari ja ühendame ülejäänud literaalid. Korduv literaal kirjutatakse ühe korra. Valmis sõlmede all on näha, milline paar kustutati.
Kuidas seda lugeda. Alustame eitusest ¬P(a,b,c) ja liigume tagasi. Sammudes 6–8 kasutame Skolemi funktsioonist tulnud punkti h = h(a,b,c): klauslid (4)–(6) ütlevad, et kõrguse aluspunkt on olemas ja tal on vajalikud omadused.