Predikaattilogiikka
Predikaattilogiikka on symbolisen logiikan osa-alue, jolla tutkitaan tietynlaisia formaalikieliä. Predikaattilogiikka jakautuu ensimmäisen kertaluvun predikaattilogiikkaan ja korkeampien kertalukujen predikaattilogiikoihin. Jälkimmäisten kohdalta mielenkiinto kohdistuu yleensä vain toisen kertaluvun predikaattilogiikkaan.
Ensimmäisen kertaluvun predikaattilogiikka, joskus lyhyemmin pelkästään predikaattilogiikka, tutkii kieliä, jotka mallintavat luonnollisen kielen subjekti-predikaattimuodon lauseita, loogisia operaatioita näillä lauseilla sekä näiden lauseiden yleistyksiä. Mallintaminen voi olla kiinnostavaa esimerkiksi matemaattisista, filosofisista tai kielitieteellisistä syistä. Esimerkkinä muutama predikaattilogiikan lause ja vastine luonnollisessa kielessä.
1. Pii on positiivinen
formula_1
2. Jos pii on ei-positiivinen, niin kuu on juustoa
formula_2
3. Kaikki ihmiset ovat kuolevaisia
formula_3
Tarkempi kuvaus predikaattilogiikan kielestä löytyy alakohdasta syntaksi.
Toisen kertaluvun predikaattilogiikka ja korkeampien kertalukujen predikaattilogiikat eroavat ensimmäisen kertaluvun predikaattilogiikasta siinä, että jälkimmäisissä voidaan puhua olioiden ominaisuuksista (2. kl.), olioiden ominaisuuksien ominaisuuksista (3. kl.) ja niin edelleen.
Syntaksi on se osa predikaattilogiikkaa, jossa kiinnostuksen kohteena ovat vain merkkijonot ja niiden ominaisuudet (ks. myös kalkyyli). Pelkästään syntaktisten piirteiden perusteella voidaan määritellä millaisia lauseet ovat ja millaista on pätevä päättely predikaattilogiikassa.
Määritelmä. Predikaattilogiikan aakkosto koostuu seuraavista
symboleista:
Predikaattilogiikassa merkitään lisäksi kaavamuuttujia symboleilla
formula_4, tai symboleilla "A", "B", ... .
Määritelmä. Predikaattilogiikan termit
Määritelmä. Predikaattilogiikan kaavat
Olkoot
formula_7
termejä.
Nyt voidaan esittää, millaista on pätevä päättely predikaattilogiikassa. Ajatuksena on, että kun tunnemme konnektiivit, tunnemme lauseiden deduktiiviset seuraukset.
Aikojen kuluessa on esitetty useita toisistaan hiukan poikkeavia päättelysysteemejä. Ehkä helpoimmin ymmärrettävissä on nk. luonnollisen päättelyn systeemi predikaattilogiikalle.
Luonnollisen päättelyn systeemissä päättelyn premissit kirjoitetaan viivan päälle, johtopäätös viivan alle. Päättelyjä voi yhdistää toisiinsa kirjoittamalla niitä peräkkäin. Luonnollisen päättelyn päättelysäännöt vastaavat tuonti- ja eliminointisäännöt kaikille konnektiiveille:
1. Negaation tuonti- ja eliminointisäännöt.
formula_15
2. Konjunktion tuonti- ja eliminointisäännöt.
formula_16
3. Kaikilla-kvanttorin tuonti- ja eliminointisäännöt.
formula_17
Huomautuksia: *) Jos "B" on hylkäämätön oletus, se voidaan hylätä. **) Muuttuja "x" ei saa esiintyä vapaana missään kaavan "A" todistuksen hylkäämättömässä oletuksessa.
Todistusteoria keskittyy lauseen syntaktiseen "todistettavuuteen" (eli
johdettavuuteen tai päättelyyn) toisista lauseista tiettyjen sääntöjen
mukaisesti. Totuuden käsite on syntaktisen todistuksen suhteen
merkityksetön. Tulkinta on totuuden välttämätön edellytys eikä
todistettavien lauseiden ei tarvitse olla tulkittuja.
On tietenkin mielekästä, jos todistus on määritelty siten, että se on
totuuden säilyttävää ja siis tosista lauseista voidaan todistaa vain
tosia lauseita, mutta se on eri asia. Syntaktisen todistuksen
tarkoituksena on ainoastaan johtaa jo saaduista lauseista, viime kädessä
aksioomista uusia lauseita.
Todistusteorian tärkeitä nimiä: Gerhard Gentzen, David Hilbert.
Ks. myös Gentzenin luonnollisen päättelyn systeemi.
Malliteoriassa tarkastellaan kieltä semanttisesta näkökulmasta. Malli on
joukko-opillinen struktuuri, joka toimii logiikan
kaavojen tulkintana Tarskin totuusmääritelmän mukaisesti.
Tarskin totuusmääritelmä. Olkoon formula_18 aakkosto ja formula_19-kaava. Olkoon formula_20-struktuuri ja formula_21 sen tulkintajono, ts. formula_22. Tällöin kaavan formula_23 totuus mallissa formula_24 tulkintajonolla formula_21, merk. formula_26, määritellään seuraavasti:Jos 
formula_33
on joukko formula_18-kaavoja ja formula_35 kaikilla formula_36, niin merkitään formula_37.
Malliteoriassa todistukselle rinnakkainen käsite on "looginen
seuraaminen".
Jos kaikille niille malleille
formula_38
ja tulkintajonoille
formula_39,
joille pätee
formula_40,
pätee myös
formula_41,
sanotaan kaavan
formula_11
seuraavan loogisesti kaavajoukosta
formula_33.
Tämä merkitään
formula_44.
Malliteorian tärkeä nimi: Alfred Tarski.
Logiikassa pyritään eheään ja täydelliseen aksiomaattiseen
järjestelmään. Eheydellä tarkoitetaan sitä, että tosista lauseista tietyn
päättelysysteemin nojalla päätellyt lauseet ovat nekin tosia.
Täydellisyydellä taas tarkoitetaan sitä, että kaikki ne lauseet, jotka
ovat aina tosia tiettyjen lauseiden ollessa tosia, ovat jälkimmäisistä
pääteltävissä. Jos tietty logiikan järjestelmä on sekä eheä että
täydellinen, vastaavat todistusteoria ja malliteoria toisiaan tässä
järjestelmässä.
Ensimmäisen kertaluvun predikaattilogiikan täydellisyyslauseen todisti
ensimmäisenä Kurt Gödel vuonna 1930.Logiikkaohjelmointi on ohjelmointiparadigma, jossa predikaattilogiikalla on keskeinen rooli. Logiikkaohjelmoinnin tärkein kieli on Prolog.