Første ordens logik

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 30. juni 2021; checks kræver 2 redigeringer .

Første-ordens logik er en formel beregning , der tillader udsagn om variabler , faste funktioner og prædikater . Udvider propositionel logik .

Ud over førsteordens logik er der også højere ordens logikker , hvor kvantifikatorer ikke kun kan anvendes på variabler, men også på prædikater. Udtrykkene prædikatlogik og prædikatregning kan betyde både førsteordenslogik og førsteordens- og højereordenslogik tilsammen; i det første tilfælde taler man nogle gange om ren prædikatlogik eller ren prædikatregning .

Grundlæggende definitioner

Sproget i første-ordens logik er bygget på basis af en signatur bestående af et sæt funktionssymbolerog et sæt prædikatsymboler. Hvert funktions- og prædikatsymbol har en tilknyttet aritet , det vil sige antallet af mulige argumenter. Både funktionelle symboler og prædikatsymboler for arity 0 er tilladt. De førstnævnte er nogle gange adskilt i et separat sæt konstanter . Derudover bruges følgende ekstra tegn: ${\mathcal {F}}$ ${\mathcal {P}}$

variable symboler (normalt , , , , , , , osv .); $x$ $y$ $z$ $x_{1}$ $y_1$ $z_{1}$ $x_{2}$ $y_2$ $z_{2}$
logiske operationer:

Symbol	Betyder
$\neg$	Negativ (ikke)
$\jord$	Konjunktion ("og")
$\lor$	Disjunktion ("eller")
$\til$	Implikation ("hvis ..., så ...")

kvantificerere :

Symbol	Betyder
$\for alle$	Universal kvantifier
$\eksisterer$	Eksistens kvantifier

servicetegn: parenteser og komma .

Symbolerne opført sammen med symbolerne fra og danner alfabetet af førsteordens logik . Mere komplekse konstruktioner defineres induktivt . ${\mathcal {P}}$ ${\mathcal {F}}$

Et udtryk er et symbol på en variabel, eller det har formen , hvor er et funktionelt symbol på arity , og er udtryk. $f(t_{1},\ldots ,t_{n})$ $f$ $n$ $t_{1},\ldots ,t_{n}$
Et atom (atomformel) har formen , hvor er prædikatet arity symbol , og er udtryk. $p(t_{1},\ldots ,t_{n})$ $s$ $n$ $t_{1},\ldots ,t_{n}$
- For eksempel er dette en atomformel, der er sand for ethvert reelt tal . Formlen består af et 2-ært prædikat , hvis argumenter er led og 0. Samtidig består udtrykket af konstanten 1 (som kan betragtes som en 0-ær funktion), en variabel og symboler for binær (2 ) -ary) funktioner + og ×. $(x+1)\ gange (x+1)\geqslant 0$ $x$ $\geqslant$ $(x+1)\ gange (x+1)$ $(x+1)\ gange (x+1)$ $x$
En formel er enten et atom eller en af følgende konstruktioner: , , , , , , hvor er funktioner og er en variabel. $\neg F$ $F_{1}\eller F_{2}$ $F_{1}\land F_{2}$ $F_{1}\til F_{2}$ $\forall xF$ $\eksisterer xF$ ${\displaystyle F,F_{1},F_{2))$ $x$

En variabel kaldes bundet i en formel , hvis den har formen enten , eller kan repræsenteres i en af formerne , , , , og allerede er bundet i , og . Hvis det ikke er bundet i , kaldes det gratis i . En formel uden frie variable kaldes en lukket formel eller en sætning . En førsteordensteori er ethvert sæt af påstande. $x$ $F$ $F$ $\forall xG$ $\eksisterer xG$ $\neg H$ $F_{1}\eller F_{2}$ $F_{1}\land F_{2}$ $F_{1}\til F_{2}$ $x$ $H$ $F_{1}$ $F_{2}$ $x$ $F$ $F$

Aksiomatik og bevis for formler

Systemet af logiske aksiomer af første ordens logik består af aksiomer af propositionalregningen suppleret med to nye aksiomer:

$\foralt xA\til A[t/x]$ ,
$A[t/x]\til \eksisterer xA$ ,

hvor er formlen opnået ved at erstatte udtrykket for hver fri variabel , der forekommer i formlen . $A[t/x]$ $t$ $x$ $EN$

Førsteordens logik bruger to inferensregler:

Modus ponens (denne regel bruges også i propositionel logik): ${\frac {A,A\to B}{B}}$
Generaliseringsregel : ${\frac {A}{\forall xA}}$

Fortolkning

I det klassiske tilfælde er fortolkningen af førsteordens logiske formler givet på førsteordensmodellen , som bestemmes af følgende data:

Bæresæt , $\mathcal{D}$
Visning af semantisk funktion $\sigma$
- hvert -ær funktionssymbol fra til -ær funktion , $n$ $f$ ${\mathcal {F}}$ $n$ $\sigma (f)\colon \,{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}$
- hvert -ært prædikatsymbol fra til -ær relation . $n$ $s$ ${\mathcal {P}}$ $n$ $\sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\mathcal {D}}$

Det er normalt accepteret at identificere bærersættet og selve modellen, hvilket indebærer en implicit semantisk funktion, hvis dette ikke fører til tvetydighed. $\mathcal{D}$

Antag, er en funktion, der kortlægger hver variabel til et element fra , som vi vil kalde en substitution . Fortolkningen af udtrykket på med hensyn til substitution er givet induktivt : $s$ $\mathcal{D}$ $[\![t]\!]_{s}$ $t$ $\mathcal{D}$ $s$

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

I samme ånd er forholdet mellem formlers sandhed relativt defineret : $\models_{s}$ $\mathcal{D}$ $s$

${\mathcal {D}}\models _{s}p(t_{1},\ldots ,t_{n})$ , hvis og kun hvis , $\sigma(p)([\!\![\,t_1]\!]_s,\ldots,[\![t_n]\!]_s)$
${\mathcal {D}}\models _{s}\neg \phi$ , hvis og kun hvis - er falsk, ${\mathcal {D}}\models _{s}\phi$
${\mathcal {D}}\modeller _{s}\phi \land \psi$ , hvis og kun hvis og er sande, ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\modeller _{s}\phi \lor \psi$ , hvis og kun hvis eller er sandt, ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\models _{s}\phi \to \psi$ , hvis og kun hvis , ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\modeller _{s}\eksisterer x\,\phi$ , hvis og kun hvis, for en eller anden substitution , som afviger fra kun værdien på variablen , ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $x$
${\mathcal {D}}\models _{s}\forall x\,\phi$ , hvis og kun hvis for alle substitutioner , hvilket afviger fra kun værdien på variablen . ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $x$

Formlen er sand på (som er angivet som ) hvis for alle permutationer . En formel kaldes gyldig (som betegnes som ) hvis for alle modeller . En formel kaldes satisfiable if for mindst én . $\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}$

Egenskaber og hovedresultater

Første-ordens logik har en række nyttige egenskaber, der gør den meget attraktiv som et grundlæggende værktøj til formalisering af matematik . De vigtigste er:

fuldstændighed (dette betyder, at for enhver lukket formel kan enten den selv eller dens negation udledes);
konsistens (ingen formel kan udledes samtidig med dens negation).

Desuden, hvis konsistens er mere eller mindre indlysende, så er fuldstændighed et ikke-trivielt resultat opnået af Gödel i 1930 ( Gödels fuldstændighedsteorem ). I det væsentlige etablerer Gödels sætning en grundlæggende ækvivalens mellem begreberne bevisbarhed og gyldighed .

Første-ordens logik har egenskaben kompakthed , bevist af Maltsev : hvis et sæt af formler ikke er gennemførligt, så er nogle af dets endelige delmængder heller ikke gennemførlige.

Ifølge Löwenheim-Skolem-sætningen, hvis et sæt formler har en model, så har det også en model med højst tællelig kardinalitet . Beslægtet med denne sætning er Skolems paradoks , som dog kun er et imaginært paradoks .

Førsteordens logik med lighed

Mange førsteordensteorier involverer symbolet på lighed. Det omtales ofte som symboler for logik og suppleres med de tilsvarende aksiomer, der definerer det. Sådan logik kaldes førsteordens logik med lighed , og de tilsvarende teorier kaldes førsteordensteorier med lighed . Lighedstegnet introduceres som et binært prædikatsymbol . De yderligere aksiomer introduceret for det er som følger: $=$

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

Brug

Førsteordens logik som en formel ræsonnementmodel

Som en formaliseret analog til almindelig logik gør førsteordenslogik det muligt strengt at ræsonnere om sandheden og falskheden af udsagn og deres forhold, især om den logiske konsekvens af et udsagn fra et andet, eller for eksempel om deres ækvivalens . Overvej et klassisk eksempel på formalisering af naturlige sprogudsagn i førsteordenslogik .

Lad os tage ræsonnementet "Alle mennesker er dødelige. Sokrates er en mand. Derfor er Sokrates dødelig ." Lad os betegne "x er en mand" gennem MAN (x) og "x er dødelig" gennem MERTEN (x). Så kan udsagnet "enhver person er dødelig" repræsenteres ved formlen: x( MAN (x) → DØD (x)) udsagnet "Sokrates er en mand" med formlen MENNESKE ( Sokrates ), og "Sokrates er dødelig" ved formlen DØD ( Sokrates ). Redegørelsen som helhed kan nu skrives som $\for alle$

( x( MAN (x) → DØD (x)) MAN ( Sokrates )) → DØD ( Sokrates )

\for alle

\land

Se også

Litteratur

Gilbert D., Akkerman V. Fundamentals of theoretical logic. M., 1947
Kleene S.K. Introduktion til metamatematik. M., 1957
V. I. Markin. Prædikaternes logik // New Philosophical Encyclopedia : i 4 bind / prev. videnskabeligt udg. råd fra V. S. Stepin . — 2. udg., rettet. og yderligere - M . : Tanke , 2010. - 2816 s.
Mendelson E. Introduktion til matematisk logik. M., 1976
Novikov PS Elementer af matematisk logik. M., 1959
Church A. Introduktion til matematisk logik, bind I. M. 1960

Ordbøger og encyklopædier	Stor russer Britannica (online) Universalis

Logikker

Filosofi • Semantik • Syntaks • Historie

Logiske grupper

klassisk logik	Aristotelisk logik propositionel logik Første ordens logik Anden ordens logik højere ordens logik
matematisk logik	mængdeteori Modelteori Beregnelighedsteori Bevisteori og konstruktiv matematik Lineær logik formelt system naturlig konklusion Sekvensberegning Algebra af logik Relevant logik Deontisk logik intuitionistisk logik Lambek regning
Ikke-klassisk logik	intuitionisme sløret logik Substrukturel logik logik Beskrivelseslogik Flerværdilogik Logisk syntese Bindende logik Tidsmæssig logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritisk tænkning uformel logik deduktiv ræsonnement

Komponenter

Bortførelse (logik)
Sandsynlighed
udmelding
Fradrag / Induktion / Traduktion
Virkelighed
Induktiv begrundelse
slutning
boolsk konstant
Rigtigt
logisk følge
Logisk form
Nødvendige og tilstrækkelige betingelser
Beskrivelse
Definition
Substitution
Pakke
Kontrovers ( Antinomy )
Syntetisk dømmekraft / Analytisk dømmekraft
Link

Liste over booleske symboler