logik (Prædikatslogik)

Der er mange logiske slutningsformer, hvis gyldighed ikke kan påvises, hvis de formuleres i sætningslogikkens sprog. Betragt fx følgende slutning:
1) For alle mennesker gælder: hvis de spiser gift, så dør de; 2) Søren spiser gift; 3) Altså: Søren dør.
Udtrykkene "for alle..." og "der findes..." er andre vigtige logiske konnektiver. De kaldes hhv. alkvantor og eksistenskvantor og betegnes ∀ og ∃. Udvides sætningslogikkens sprog med disse nye konnektiver, fremkommer prædikatslogikken, der er langt mere udtryksfuld end sætningslogikken. Disse to logiske systemer udgør grundlaget for den moderne logik.

Prædikatslogikken er også semantisk fuldstændig i betydningen "A1,...,An ⊧ K hvis og kun hvis, A1,...,An ⊦ K", hvilket igen betyder, at alle gyldige prædikatslogiske slutninger kan bevises ud fra en lille mængde simple slutningsskemaer. Dette blev vist af Kurt Gödel i 1930.

Selvom det i prædikatslogikken er muligt at bevise alle logisk sande sætninger, er prædikatslogikken ikke afgørlig. Der findes nemlig ingen effektiv procedure, som til en given sætning afgør, om den er sand eller ej. Prædikatslogikkens principielle uafgørlighed blev bevist af Alonzo Church i 1936.