Predikaattilogiikka

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 seuraavistasymboleista:

Merkitys	Merkintä
konnektiivit	${\displaystyle \neg ,\wedge ,\vee ,\to ,\leftrightarrow \,\!}$
sulkeet	${\displaystyle (,)\,\!}$
kvanttorit	${\displaystyle \forall ,\exists \,\!}$
identiteettisymboli	${\displaystyle \equiv \,\!}$
relaatiosymbolit	${\displaystyle R_{0},R_{1},R_{2},\ldots \,\!}$
funktiosymbolit	${\displaystyle f_{0},f_{1},f_{2},\ldots \,\!}$
muuttujat	${\displaystyle v_{0},v_{1},v_{2},\ldots \,\!}$
yksilövakiot	${\displaystyle c_{0},c_{1},c_{2},\ldots \,\!}$

Predikaattilogiikassa merkitään lisäksi kaavamuuttujia symboleilla${\displaystyle \phi ,\psi ,\ldots \,\!}$ , tai symboleilla A, B, ... .

Määritelmä. Predikaattilogiikan termit

1. Yksilövakiot ovat termejä.
2. Muuttujat ovat termejä.
3. Jos ${\displaystyle t_{1},\ldots ,t_{n}\,\!}$ ovat termejä, niin ${\displaystyle ft_{1}\ldots {}t_{n}\,\!}$ on termi.

Määritelmä. Predikaattilogiikan kaavat
Olkoot${\displaystyle t_{1},t_{2},\ldots \,\!}$ termejä.

1. ${\displaystyle t_{1}=t_{2}\,\!}$ on kaava.
2. Jos ${\displaystyle R_{i}\,\!}$ on n-paikkainen predikaattisymboli, niin ${\displaystyle R_{i}{}t_{1}\ldots {}t_{n}\,\!}$ on kaava.
3. Jos ${\displaystyle \phi \,\!}$ on kaava, niin ${\displaystyle \neg \phi \,\!}$ on kaava.
4. Jos ${\displaystyle \phi \,\!}$ ja ${\displaystyle \psi \,\!}$ ovat kaavoja, niin ...
5. ...

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.

${\displaystyle {\frac {A\land \neg A}{\neg B}}\ \neg T\ (*\qquad {\frac {\neg \neg A}{A}}\ \neg E}$

2. Konjunktion tuonti- ja eliminointisäännöt.

${\displaystyle {\frac {\begin{matrix}A&B\end{matrix}}{A\land B}}\ \land T\qquad {\frac {A\land B}{A}}\ \land E}$

3. Kaikilla-kvanttorin tuonti- ja eliminointisäännöt.

${\displaystyle {\frac {A}{\forall xA}}\ \forall T\ (**\qquad {\frac {\forall xA}{A(x/t)}}\ \forall E}$

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 (elijohdettavuuteen tai päättelyyn) toisista lauseista tiettyjen sääntöjenmukaisesti. Totuuden käsite on syntaktisen todistuksen suhteenmerkityksetö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 ontotuuden säilyttävää ja siis tosista lauseista voidaan todistaa vaintosia lauseita, mutta se on eri asia. Syntaktisen todistuksentarkoituksena 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 onjoukko-opillinen struktuuri, joka toimii logiikankaavojen tulkintana Tarskin totuusmääritelmän mukaisesti.

Tarskin totuusmääritelmä. Olkoon ${\displaystyle L}$ aakkosto ja ${\displaystyle \phi \,L}$ -kaava. Olkoon ${\displaystyle {\mathcal {M}}\,L}$ -struktuuri ja ${\displaystyle s}$ sen tulkintajono, ts. ${\displaystyle s\colon \mathbb {N} \rightarrow {\mathcal {M}}}$ . Tällöin kaavan ${\displaystyle \phi }$ totuus mallissa ${\displaystyle {\mathcal {M}}}$ tulkintajonolla ${\displaystyle s}$ , merk. ${\displaystyle {\mathcal {M}},s\models \phi }$ , määritellään seuraavasti:

1. ${\displaystyle \phi =P(t_{0},\ldots ,t_{n}):\,(t_{0}^{{\mathcal {M}},s},\ldots ,t_{n}^{{\mathcal {M}},s})\in P^{\mathcal {M}},}$
2. ${\displaystyle \phi =\neg \psi :\,{\mathcal {M}},s\not \models \psi ,}$
3. ${\displaystyle \phi =\psi \rightarrow \theta :\,{\mathcal {M}},s\not \models \psi }$ tai ${\displaystyle {\mathcal {M}},s\models \theta ,}$
4. ${\displaystyle \phi =\forall v_{i}\psi :\,{\mathcal {M}},s(a/i)\models \psi }$ kaikilla ${\displaystyle a\in {\mathcal {M}}}$ .

Jos ${\displaystyle \Sigma \,\!}$ on joukko ${\displaystyle L}$ -kaavoja ja ${\displaystyle {\mathcal {M}},s\models \phi }$ kaikilla ${\displaystyle \phi \in \Sigma }$ , niin merkitään ${\displaystyle {\mathcal {M}},s\models \Sigma }$ .

Malliteoriassa todistukselle rinnakkainen käsite on looginenseuraaminen.Jos kaikille niille malleille${\displaystyle {\mathcal {M}}\,\!}$ ja tulkintajonoille${\displaystyle s\,\!}$ ,joille pätee${\displaystyle {\mathcal {M}}\models _{s}\Sigma \,\!}$ ,pätee myös${\displaystyle {\mathcal {M}}\models _{s}\phi \,\!}$ ,sanotaan kaavan${\displaystyle \phi \,\!}$ seuraavan loogisesti kaavajoukosta${\displaystyle \Sigma \,\!}$ .Tämä merkitään${\displaystyle \Sigma \models \phi \,\!}$ .

Malliteorian tärkeä nimi: Alfred Tarski.

Logiikassa pyritään eheään ja täydelliseen aksiomaattiseenjärjestelmään. Eheydellä tarkoitetaan sitä, että tosista lauseista tietynpäättelysysteemin nojalla päätellyt lauseet ovat nekin tosia.Täydellisyydellä taas tarkoitetaan sitä, että kaikki ne lauseet, jotkaovat 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 todistiensimmäisenä Kurt Gödel vuonna 1930.

• Toisen kertaluvun predikaattilogiikka
• Yleistetyt kvanttorit
• Äärettömät kielet

Logiikkapohjainen ohjelmointi on ohjelmointiparadigma, jossa predikaattilogiikalla on keskeinen rooli. Logiikkaohjelmoinnin tärkein kieli on Prolog.

• Thompson, Jan & Martinsson, Thomas: Matematiikan käsikirja. Helsinki: Tammi, 1994. ISBN 951-31-0471-0.
• Allwood, Jens & Andersson, Lars-Gunnar & Dahl, Östen (1988): Logiikka ja kieli. 2. painos. Suomentanut Paavo Siro. Helsinki: Yliopistopaino. (1. painos 1980 Gaudeamuksen kustantamana. Alkuteos: Logik för lingvister, 1972. Suomennettu englanninkielisestä laitoksesta Logic in Linguistics, 1979.) ISBN 951-570-020-5