Första ordningens logik
 |
Den här artikeln behöver källhänvisningar för att kunna verifieras. (2020-04) Åtgärda genom att lägga till pålitliga källor (gärna som fotnoter). Uppgifter utan källhänvisning kan ifrågasättas och tas bort utan att det behöver diskuteras på diskussionssidan. |
Första ordningens logik (FOL) är ett formellt deduktivt system som används i matematik, filosofi, lingvistik och datavetenskap. Det har ett flertal olika namn på engelska: first-order predicate calculus (FOPC), the lower predicate calculus, the language of first-order logic och predicate logic. Till skillnad från naturliga språk, som svenska, använder sig FOL av ett helt otvetydigt formellt språk som tolkas av matematiska strukturer. FOL är ett deduktivt system som går bortom satslogiken genom att tillåta kvantifiering av objekt inom en given domän. Man kan exempelvis med FOL uttrycka satsen "Varje individ har egenskapen P".
| Logik, Formellt system |
|---|
| Logiska system |
|
|
Medan satslogik endast behandlar enkla propositioner så inkluderar första ordningens logik även predikat och kvantifikatorer. Inom satslogiken är de två satserna "Sokrates är en man" och "Platon är en man" helt orelaterade och uttrycks till exempel med p och q. Med FOL uttrycks dock båda dessa satser med samma predikat: Man(x) där Man(x) betyder att x är en man. När x=Sokrates får vi den första satsen, p, och när x=Platon får vi den andra satsen, q. Detta språk blir mycket kraftfullt då man introducerar kvantifikatorer, då man kan uttrycka satser som "för varje x...", som i "för varje x gäller det att, om Man(x), så...". Utan kvantifikatorer är varje giltigt argument i FOL även giltigt i satslogik och vice versa.
En första ordningens teori består av en uppsättning axiom (vanligtvis ändlig eller rekursivt räknebar) och de uttryck som går att deducera från dem givet ett antal regler för giltig deduktion inom systemet. Ett första ordningens språk har tillräcklig uttryckskraft för att formalisera två viktiga matematiska teorier: Zermelo-Fraenkels mängdteori och Peanos axiom (första ordningens). Ett första ordningens språk kan emellertid inte kategoriskt uttrycka uppräknelighet. Det kan uttryckas kategoriskt med andra ordningens logik.