Otsene tõestus predikaatarvutuses

Mis on otsene tõestus?

Otsene tõestus on valemite jada, kus iga rida on premiss, oletus või saadud varasematest ridadest mõne reegli abil. Viimane rida on see, mida tahtsime tõestada.

Predikaatarvutuses kehtivad kõik lausearvutuse reeglid edasi. Juurde tuleb neli kvantorireeglit ja kvantorite eituse seadused. Kogu töö seisneb selles, et kvantorid õigel viisil maha võtta, lausearvutuse sammud teha ja kvantorid tagasi panna.

Keel

x, y, z, u, v, w	muutujad, tähistavad suvalist objekti
a, b, c, s, m, …	konstandid, tähistavad kindlat objekti
P(x), L(x,y)	predikaadid, väidavad objektide kohta midagi
∀x A	iga x korral kehtib A
∃x A	leidub x, mille korral kehtib A

Valemis ∀x L(x,y) on x seotud ja y vaba. Vaba muutuja käib ühe kindla, kuigi nimetamata objekti kohta. Asendus A(t) tähendab, et muutuja x iga vaba esinemine valemis A(x) asendatakse termiga t; see on lubatud ainult siis, kui ükski t muutuja ei satu seejuures mõne kvantori alla.

Kvantor seob nõrgemini kui tehted: ∀x P(x) → Q(x) tähendab (∀x P(x)) → Q(x). Kui kvantor peab haarama tervet valemit, kirjuta sulud: ∀x(P(x) → Q(x)). Kvantorireeglid rakenduvad ainult siis, kui kvantor haarab tervet rida.

Neli kvantorireeglit

Kahel neist on piirang ja just nendes tehakse enamik vigu.

Kvantorite eitus

Need on asendusreeglid: need töötavad mõlemas suunas ja ka alamvalemi sees. Eitust saab niimoodi kvantorist mööda liigutada, nii et kvantor satub rea etteotsa ja UI või EI muutub rakendatavaks.

Lausearvutuse reeglid

Kõik klassikalised reeglid kehtivad ka siin ja neid rakendatakse täpselt samamoodi: tuletusreeglid (MP, MT, HS, DS, KD, Simp, Konj, Add) ainult tervele reale, asendusreeglid (DN, DeM, Komm, Assots, Distr, Kontrap, Impl, Eksp, Taut, Ekviv) mõlemas suunas ja ka alamvalemile.

Predikaatarvutuses rakendad neid kvantoriteta valemitele, mis tekivad pärast UI-d ja EI-d. Nende reeglite skeemid on lahti kirjutatud lausearvutuse materjalis.

Tinglik tõestus

Kui järeldus on implikatsioon A → B, oleta A ja tuleta sellest B. Oletuse all olevad read on tähistatud vasakul vertikaaljoonega ja pärast sulgemist neid enam kasutada ei saa.

Tüüpiline strateegia

Vii eitused kvantoritest mööda. QN teeb reast ¬∀x A rea ∃x ¬A, nii et kvantor satub etteotsa.
Eemalda kvantorid, EI enne UI-d. EI nõuab uut konstanti, UI võib kasutada mis tahes termi, ka sedasama äsja loodud konstanti. Vastupidises järjekorras oleks konstant juba kulutatud.
Tee lausearvutuse sammud kvantoriteta valemitega.
Pane kvantorid tagasi. Konkreetse objekti (konstandi) kohta saadud tulemusest tuleb EG. Suvalise objekti (muutuja, mis ei ole premissides vaba) kohta saadud tulemusest tuleb UG.