Atomistinen kaava

Atomistinen sääntö eli atomistinen kaava on matemaattisessa logiikassa käytetty erikoistapaus kaavasta, jolla ei ole syvempiä sisärakenteita. Sitä kutsutaan lyhyesti myös atomiksi. Atomistisessa kaavassa ei siis ole alakaavoja sisällään. Atomit ovat siten yksinkertaisimpia hyvin-määriteltyjä logiikan kaavoja. Yhdistettyjä kaavoja voidaan muodostaa yhdistämällä atomistisia sääntöjä keskenään tyypillisillä logiikan konnektiiveilla.

Atomististen kaavojen tarkka muoto riippuu käsiteltävästä logiikasta. Esimerkiksi propositiologiikassa atomistiset kaavat ovat muuttujia, jotka viittaavat propositioihin. Predikaattilogiikassa atomit ovat predikaattisymboleita, joihin voi liittyä argumenttejakin. Tällöin kukin argumentti on luonteeltaan termi, joka voi edelleen sisältää atomistisia kaavoja. Prolog-ohjelmointikielessä on käytettävissä edellä kuvatut predikaattilogiikan piirteet, mutta niiden lisäksi vielä rekursio, peräytys ja samastus, joiden ansiosta Prologia voidaan pitää tyypillisenä Turing-vahvana ohjelmointikielenä.

Atomistinen kaava on ensimmäisen kertaluvun logiikkaa

Hyvin määritellyille ensimmäisen kertaluvun logiikan termeille ja proposioitioille pätee seuraava syntaksi:

Termit ovat muotoa:

t ::= c | x | f (t₁, …, t_n),

joten termi on määritelty rekursiivisesti joko vakioksi c (nimetty objekti), tai muuttujaksi x, tai funktiksi f, johon liittyy n kappaletta argumentteja. Funktiot sovittavat objektien joukkoja ja viittauksia itse objekteihin.

Propositiot ovat muotoa:

A, B, … ::= P (t₁, …, t_n) | A ∧ B | ⊤ | A ∨ B | ⊥ | A ⊃ B | ∀x. A | ∃x. A ,

joten propositio määritellään rekursiivisesti n-argumenttiseksi predikaatiksi P, jonka argumentteina ovat termit t_k, mutta myös lausekkeeksi, joka koostuu loogisista konnektiiveista (and, or) sekä kvanttoreista (for-all, there-exists), joita käytetään yhdessä muiden propositioiden kanssa.

Atomistinen kaava (atomi) on yksinkertaisesti predikaatti, jota on sovellettu viittaamaan termien muodostamaan monikkoon. Atomistinen kaava on siten muotoa P (t₁, …, t_n) predikaatille P ja termeille t_k.

Muita hyvin määriteltyjä kaavioja saadaan kokoamalla atomeja yhteen kvanttoreiden ja konnektiivien avulla.

Esimerkiksi kaava ∀x, P(x) ∧ ∃y, Q(y,f(x))∨ ∃z. R(z) sisältää atomit

P(x)
Q(y, f(x))
R(z)

Kun kaikki atomin termit ovat maadoitettuja, silloin atomia kutsutaan maadoitetuksi atomiksi tai maadoitetuksi predikaatiksi.