Första beställningslogik

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 30 juni 2021; kontroller kräver 2 redigeringar .

Första ordningens logik är en formell kalkyl som tillåter uttalanden om variabler , fasta funktioner och predikat . Utökar propositionell logik .

Förutom logik av första ordningen finns det också logik av högre ordning , där kvantifierare kan tillämpas inte bara på variabler utan också på predikat. Termerna predikatlogik och predikatkalkyl kan betyda både första ordningens logik och första ordningens och högre ordningens logik tillsammans; i det första fallet talar man ibland om ren predikatslogik eller ren predikatkalkyl .

Grundläggande definitioner

Språket för första ordningens logik är byggt på basis av en signatur som består av en uppsättning funktionssymboleroch en uppsättning predikatsymboler. Varje funktion och predikatsymbol har en tillhörande aritet , det vill säga antalet möjliga argument. Både funktionella symboler och predikatsymboler för aritet 0 är tillåtna. De förra separeras ibland i en separat uppsättning konstanter . Dessutom används följande extra tecken: ${\mathcal {F}}$ ${\mathcal {P}}$

variabla symboler (vanligtvis , , , , , , , , etc.); $x$ $y$ $z$ $x_{1}$ $y_1$ $z_{1}$ $x_{2}$ $y_2$ $z_{2}$
logiska operationer:

Symbol	Menande
$\neg$	Negativ (inte)
$\landa$	Konjunktion ("och")
$\lor$	Disjunktion ("eller")
$\till$	Implikation ("om ..., då ...")

kvantifierare :

Symbol	Menande
$\för alla$	Universell kvantifierare
$\existerar$	Existens kvantifierare

servicetecken: parenteser och kommatecken .

Symbolerna listade tillsammans med symbolerna från och bildar alfabetet av första ordningens logik . Mer komplexa konstruktioner definieras induktivt . ${\mathcal {P}}$ ${\mathcal {F}}$

En term är en symbol för en variabel, eller den har formen , där är en funktionell symbol för arity , och är termer. $f(t_{1},\ldots ,t_{n})$ $f$ $n$ $t_{1},\ldots ,t_{n}$
En atom (atomformel) har formen , där är predikatet arity-symbol , och är termer. $p(t_{1},\ldots ,t_{n})$ $sid$ $n$ $t_{1},\ldots ,t_{n}$
- Till exempel är detta en atomformel som är sann för alla reella tal . Formeln består av ett 2-ärt predikat , vars argument är termer och 0. Samtidigt består termen av konstanten 1 (som kan betraktas som en 0-är funktion), en variabel och symboler för binär (2 ) -ary) funktioner + och ×. $(x+1)\times (x+1)\geqslant 0$ $x$ $\geqslant$ $(x+1)\ gånger (x+1)$ $(x+1)\ gånger (x+1)$ $x$
En formel är antingen en atom eller en av följande konstruktioner: , , , , , , där är funktioner och är en variabel. $\neg F$ $F_{1}\eller F_{2}$ $F_{1}\land F_{2}$ $F_{1}\till F_{2}$ $\förallt xF$ $\finns xF$ ${\displaystyle F,F_{1},F_{2))$ $x$

En variabel kallas bunden i en formel om den har formen antingen , eller är representerad i någon av formerna , , , , och redan är bunden i , och . Om den inte är bunden i kallas den gratis i . En formel utan fria variabler kallas en sluten formel , eller en mening . En första ordningens teori är vilken uppsättning påståenden som helst. $x$ $F$ $F$ $\förallt xG$ $\finns xG$ $\neg H$ $F_{1}\eller F_{2}$ $F_{1}\land F_{2}$ $F_{1}\till F_{2}$ $x$ $H$ $F_{1}$ $F_{2}$ $x$ $F$ $F$

Axiomatik och bevis för formler

Systemet av logiska axiom av första ordningens logik består av axiomen i propositionskalkylen kompletterade med två nya axiom:

$\förallt xA\till A[t/x]$ ,
$A[t/x]\till \existerar xA$ ,

där är formeln som erhålls genom att ersätta termen för varje fri variabel som förekommer i formeln . $A[t/x]$ $t$ $x$ $A$

Första ordningens logik använder två slutledningsregler:

Modus ponens (denna regel används också i propositionell logik): ${\frac {A,A\to B}{B}}$
Generaliseringsregel : ${\frac {A}{\forall xA}}$

Tolkning

I det klassiska fallet ges tolkningen av första ordningens logiska formler på första ordningens modell , som bestäms av följande data:

Bärset , $\mathcal{D}$
Visning av semantisk funktion $\sigma$
- varje -är funktionssymbol från till -är funktion , $n$ $f$ ${\mathcal {F}}$ $n$ $\sigma (f)\colon \,{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}$
- varje -är predikatsymbol från till -är relation . $n$ $sid$ ${\mathcal {P}}$ $n$ $\sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\mathcal {D}}$

Det är vanligtvis accepterat att identifiera bäraruppsättningen och själva modellen, vilket innebär en implicit semantisk funktion, om detta inte leder till oklarhet. $\mathcal{D}$

Antag, är en funktion som mappar varje variabel till något element från , som vi kallar en substitution . Tolkningen av termen på med avseende på substitution ges induktivt : $s$ $\mathcal{D}$ $[\![t]\!]_{s}$ $t$ $\mathcal{D}$ $s$

$[\![x]\!]_{s}=s(x)$ , om är en variabel, $x$
$[\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)([\!\![\,x_1]\!]_s,\ldots,[\![x_n]\ !]_s)$

I samma anda är förhållandet mellan formlers sanning relativt definierat : $\models_{s}$ $\mathcal{D}$ $s$

${\mathcal {D}}\models _{s}p(t_{1},\ldots ,t_{n})$ , om och bara om , $\sigma(p)([\!\![\,t_1]\!]_s,\ldots,[\![t_n]\!]_s)$
${\mathcal {D}}\modeller _{s}\neg \fi$ , om och bara om - är falskt, ${\mathcal {D}}\models _{s}\phi$
${\mathcal {D}}\models _{s}\phi \land \psi$ , om och bara om och är sanna, ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\models _{s}\phi \lor \psi$ , om och bara om eller är sant, ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\models _{s}\phi \to \psi$ , om och bara om , ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\modeller _{s}\exists x\,\phi$ , om och endast om, för någon substitution , som skiljer sig från endast värdet på variabeln , ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $x$
${\mathcal {D}}\models _{s}\forall x\,\phi$ , om och endast om för alla substitutioner , vilket skiljer sig från endast värdet på variabeln . ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $x$

Formeln är sann på (som betecknas som ) om för alla permutationer . En formel kallas giltig (som betecknas som ) om för alla modeller . En formel kallas satisfiable om för minst en . $\phi$ $\mathcal{D}$ ${\mathcal {D}}\models \phi$ ${\mathcal {D}}\models _{s}\phi$ $s$ $\phi$ $\modeller\phi$ ${\mathcal {D}}\models \phi$ $\mathcal{D}$ $\phi$ ${\mathcal {D}}\models \phi$ $\mathcal{D}$

Egenskaper och huvudresultat

Första ordningens logik har ett antal användbara egenskaper som gör den mycket attraktiv som ett grundläggande verktyg för formalisering av matematik . De viktigaste är:

fullständighet (detta betyder att för varje sluten formel är antingen den själv eller dess negation härledbar);
konsistens (ingen formel kan härledas samtidigt med dess negation).

Dessutom, om konsistens är mer eller mindre uppenbar, så är fullständighet ett icke-trivialt resultat erhållet av Gödel 1930 ( Gödels fullständighetsteorem ). I huvudsak etablerar Gödels teorem en grundläggande likvärdighet mellan begreppen bevisbarhet och giltighet .

Första ordningens logik har egenskapen compactness , bevisad av Maltsev : om någon uppsättning formler inte är genomförbar, så är några av dess ändliga delmängder inte heller genomförbara.

Enligt Löwenheim-Skolem-satsen, om en uppsättning formler har en modell, så har den också en modell med högst räknebar kardinalitet . Relaterad till denna sats är Skolems paradox , som dock bara är en imaginär paradox .

Första ordningens logik med jämlikhet

Många första ordningens teorier involverar symbolen för jämlikhet. Det hänvisas ofta till som symboler för logik och kompletteras med motsvarande axiom som definierar det. Sådan logik kallas första ordningens logik med jämlikhet , och motsvarande teorier kallas första ordningens teorier med jämlikhet . Likhetstecknet introduceras som en binär predikatsymbol . De ytterligare axiomen som introduceras för det är följande: $=$

$\forall x(x=x)$
$\forall x\forall y(x=y)\to (F(x)\to F(y))$

Användning

Första ordningens logik som en formell resonemangsmodell

Eftersom den är en formaliserad analog till vanlig logik , gör första ordningens logik det möjligt att strikt resonera om sanningen och falskheten i uttalanden och deras relation, i synnerhet om den logiska konsekvensen av ett uttalande från ett annat, eller till exempel om deras likvärdighet . Betrakta ett klassiskt exempel på formalisering av naturliga språkuttalanden i första ordningens logik .

Låt oss ta resonemanget ”Varje människa är dödlig. Sokrates är en man. Därför är Sokrates dödlig .” Låt oss beteckna "x är en man" genom MAN (x) och "x är dödlig" genom MERTEN (x). Sedan kan påståendet "varje människa är dödlig" representeras av formeln: x( MÄNNISKA (x) → DÖD (x)) påståendet "Sokrates är en människa" med formeln MÄNNISKA ( Sokrates ), och "Sokrates är dödlig" med formeln DÖDEN ( Sokrates ). Uttalandet som helhet kan nu skrivas som $\för alla$

( x( MAN (x) → DÖD (x)) MAN ( Sokrates )) → DÖD ( Sokrates )

\för alla

\land

Se även

Litteratur

Gilbert D., Akkerman V. Fundamentals of theoretical logic. M., 1947
Kleene S.K. Introduktion till metamatematik. M., 1957
V. I. Markin. Predikatens logik // New Philosophical Encyclopedia : i 4 volymer / föregående. vetenskaplig-ed. råd av V. S. Stepin . — 2:a uppl., rättad. och ytterligare - M . : Tanke , 2010. - 2816 sid.
Mendelson E. Introduktion till matematisk logik. M., 1976
Novikov PS Element av matematisk logik. M., 1959
Church A. Introduktion till matematisk logik, vol. I. M. 1960

Ordböcker och uppslagsverk	Stor ryss Britannica (online) Universalis

Logik

Filosofi • Semantik • Syntax • Historia

Logiska grupper

klassisk logik	Aristotelisk logik propositionell logik Första beställningslogik Andra ordningens logik högre ordningslogik
matematisk logik	mängdteori Modellteori Beräkningsbarhetsteori Bevisteori och konstruktiv matematik Linjär logik formellt system naturlig slutsats Sekvenskalkyl Algebra av logik Relevant logik Deontisk logik intuitionistisk logik Lambek kalkyl
Icke-klassisk logik	intuitionism rolig logik Substrukturell logik logik Beskrivningslogik Flervärdig logik Logisk syntes Bindande logik Temporal logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritiskt tänkande informell logik deduktiva resonemang

Komponenter

Bortförande (logik)
Sannolikhet
påstående
Avdrag / Induktion / Traduktion
Verklighet
induktivt resonemang
slutledning
boolesk konstant
Sann
logiskt följa
Logisk form
Nödvändiga och tillräckliga förutsättningar
Beskrivning
Definition
Utbyte
Paket
Kontrovers ( Antinomy )
Syntetisk bedömning / Analytisk bedömning
Länk

Lista över booleska symboler