Kvantorilausekkeiden

Kvantorilausekkeiden käsite kattaa loogisten lauseiden rakennetta, joissa kvanttorit sitovat muuttujia. Yleisimmät kvanttorilausekkeet ovat ∀x φ(x) ja ∃x φ(x), joissa φ on lauseke ja x on sidottu muuttuja. Kvantorilausekkeet ovat keskeinen osa predikaattilogiikkaa ja niitä käytetään ilmaisemaan väitteitä siitä, miten lausekkeen φ(x) pätee kaikille tai joillekin muuttujan arvoille.

Syntaksi: Lausekkeet rakennetaan peruslausekkeista sekä kvanttorin ja lausekkeen yhdistelmästä. Muoto ∀x φ tai ∃x φ ilmaisee, että φ pätee kaikille x:tä koskeville arvoille (universaali kvanttori) tai että on olemassa x, jonka φ toteuttaa (eksistenssi). φ voi olla predikaatti tai monimutkaisempi lauseke, jonka sisällä x esiintyy. Lausekkeet voivat olla osia suuremmassa kaavassa.

Semantiikka: Merkitään domain D ja tulkitseminen predikaateille. ∀x φ(x) on tosi, jos φ(x) on tosi jokaisella x ∈ D; ∃x φ(x) on tosi, jos on ainakin yksi x ∈ D, jonka φ(x) on tosi. Sidotut muuttujat eivät ole vapaasti käytettävissä ulkona kvanttorin ulkopuolella. Vapaat muuttujat voivat esiintyä laajemman lauseen kontekstissa.

Sidonta ja muunnokset: Muuttujien nimeäminen (α-konversio) on sallittua, kun se ei muuta lausekkeen totuusarvoa. Kvanttorilausekkeita voidaan esittää prenex-normalimuodossa, jossa kaikki kvanttorit ovat lausekkeen etupuolella ja jäljellä oleva osa on matriisi.

Käyttökohteet: Kvantorilausekkeet ovat keskeisiä matematiikassa, logiikassa, tietojenkäsittelytieteessä ja muodollisessa todistuksessa. Esimerkki: ∀x ∈ N, ∃y ∈ N: x ≤ y, eli jokaiselle luonnolliselle luvulle löytyy suurempi luku.