Tehtävä:
Sieventäminen propositiologiikassa

Lyhyt MathCheck-ohje (uuteen välilehteen)

Propositiologiikassa voi sieventää ja päätellä monella eri tavalla. Yksi helppo tehokas tapa, josta voi jopa tehdä MathCheckillä tarkastettavia tehtävä­sarjoja, on valita jokin muuttuja, sijoittaa sen arvoksi `sf(F)` ja sieventää, sijoittaa sen arvoksi `sf(T)` ja sieventää, ja yhdistää tulokset. Todistamme tällä tavalla, että

`not(P harr Q)``hArr``P harr not Q` .

Tarvitsemme seuraavat aputulokset.

Sitten todistamme tavoitteemme vaiheittain.

Seuraavaksi todistamme, että `harr` on liitännäinen eli `(P harr Q) harr R``hArr``P harr (Q harr R)`. Tarvitsemme seu­raa­van aputuloksen.

Sitten todistamme tavoitteemme vaiheittain.

Propositiologiikassa voi päätellä myös kaavoja käyttämällä samaan tapaan kuin aritmetiikassa. Esi­merk­kinä todistamme, että `P rarr Q``hArr``not Q rarr not P`. Ensin sovella implikaation eliminointia, sitten kaksois­negaation eliminointia, ja lopuksi implikaation määritelmää.




tai

Sovella ensin implikaation eliminointia, sitten de Morganin lakia, ja keksi loppu itse!




tai

Toisinaan sieventämisessä voi hyödyntää sitä, että jos disjunktion jokin osa toteutuu, muiden osien totuus­arvoilla ei ole väliä.
Jos `P hArr sf(T)`, niin `P vv not P ^^ Q hArr` , ja
jos `P hArr sf(F)`, niin `P vv not P ^^ Q hArr` .
Siksi `P vv not P ^^ Q hArr`
tai

Sievennä `P ^^ (not P vv Q) hArr`
tai

Sievennä `(P ^^ Q vv not Q ^^ R) ^^ (P vv not R) hArr`

tai

Sievennä seuraavat lausekkeet mahdollisimman yksin­kertaiseen muotoon, jossa ei esiinny `rarr` eikä `harr`. Valitse itse keinot, joita käytät. Yhdessä kohdassa on kaksi kompleksisuusrajaa. Väljemmän rajan saavut­taminen riittää, mutta on hienoa, jos saavutat tiukem­mankin.

`P rarr not P hArr`

tai

`P harr Q harr P hArr`

tai

`(P rarr Q) ^^ not(Q rarr P) hArr`

tai

`P ^^ not Q vv Q ^^ R ^^ not P vv Q ^^ P hArr`

tai

`(P rarr Q) ^^ (Q rarr R) ^^ (R rarr P) hArr`

tai