Första ordningens logik

Från Rilpedia

Texten från svenska Wikipedia

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".

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 Peanoaxiomen (första ordningens). Ett första ordningens språk kan emellertid inte kategoriskt uttrycka uppräknelighet. Det kan uttryckas kategoriskt med andra ordningens logik.