Monadisk predikatkalkyl

Inom logik är den monadiska predikatkalkylen (även kallad monadisk första ordningens logik ) fragmentet av första ordningens logik där alla relationssymboler ] i signaturen är monadiska (det vill säga de tar bara ett argument), det finns inga funktionssymboler. Alla atomformler är alltså av formen $P(x)$ , där $P$ är en relationssymbol och $x$ är en variabel .

Monadisk predikatkalkyl kan jämföras med polyadisk predikatkalkyl, som tillåter relationssymboler som tar två eller flera argument.

Uttrycksförmåga

Frånvaron av polyadiska relationssymboler begränsar allvarligt vad som kan uttryckas i den monadiska predikatkalkylen. Den är så svag att den, till skillnad från den fullständiga predikatkalkylen, är avgörbar - det finns en beslutsprocedur som avgör om en given formel för monadisk predikatkalkyl är logiskt giltig (sant för alla icke-tomma domäner ). Att lägga till en enda binär relationssymbol till monadisk logik resulterar dock i en logik som inte kan avgöras.

Förhållande till termlogik

Behovet av att gå bortom monadisk logik uppskattades inte förrän arbetet med relationernas logik, av Augustus De Morgan och Charles Sanders Peirce på artonhundratalet, och av Frege i hans 1879 Begriffsschrifft . Före arbetet med dessa tre män termlogik (syllogistisk logik) allmänt vara tillräcklig för formella deduktiva resonemang.

Inferenser i termlogik kan alla representeras i den monadiska predikatkalkylen. Till exempel argumentet

Alla hundar är däggdjur.

Inget däggdjur är en fågel.

Ingen hund är alltså en fågel.

kan noteras på det monadiska predikatkalkylens språk som

$[( \forall x\,D(x)\Högerpil M(x))\land \neg (\finns y\,M(y)\land B(y))]\Högerpil \neg (\exists z\,D( z)\land B(z))$

där $D$ , $M$ och $B$ betecknar predikaten för att vara en hund, ett däggdjur respektive en fågel.

Omvänt är monadisk predikatkalkyl inte signifikant mer uttrycksfull än termlogik. Varje formel i den monadiska predikatkalkylen är ekvivalent med en formel där kvantifierare endast förekommer i slutna underformler av formen

$\forall x\,P_{1}(x)\lor \cdots \lor P_{n}(x)\lor \neg P'_{1}(x)\lor \cdots \lor \neg P'_{m}(x)$

eller

$\exists x\,\neg P_{1}(x )\land \cdots \land \neg P_{n}(x)\land P'_{1}(x)\land \cdots \land P'_{m}(x),$

Dessa formler generaliserar något de grundläggande bedömningarna som betraktas i termlogik. Till exempel tillåter detta formulär uttalanden som " Varje däggdjur är antingen en växtätare eller en köttätare (eller båda) ", $(\forall) x\,\neg M(x)\lor H(x)\lor C(x))$ . Resonemang kring sådana påståenden kan dock fortfarande hanteras inom ramen för termlogik, dock inte enbart med de 19 klassiska aristoteliska syllogismerna .

Om man tar propositionell logik som given, uttrycker varje formel i den monadiska predikatkalkylen något som likaså kan formuleras i termlogik. Å andra sidan drar en modern syn på problemet med multipel generalitet i traditionell logik slutsatsen att kvantifierare inte kan bygga ihop sig på ett användbart sätt om det inte finns några polyadiska predikat för att relatera de bundna variablerna.

Varianter

Det formella systemet som beskrivs ovan kallas ibland för den rena monadiska predikatkalkylen, där "ren" betyder frånvaron av funktionsbokstäver. Att tillåta monadiska funktionsbokstäver ändrar logiken endast ytligt , medan tillåtelse av även en enda binär funktionsbokstav resulterar i en logik som inte kan avgöras.

Monadisk andra ordningens logik tillåter predikat av högre aritet i formler, men begränsar andra ordningens kvantifiering till unära predikat, dvs. de enda andra ordningens variabler som är tillåtna är delmängdsvariabler.