Logika prvního řádu

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 30. června 2021; kontroly vyžadují 2 úpravy .

Logika prvního řádu je formální počet , který umožňuje prohlášení o proměnných , pevných funkcích a predikátech . Rozšiřuje výrokovou logiku .

Kromě logiky prvního řádu existují také logiky vyššího řádu , ve kterých lze kvantifikátory aplikovat nejen na proměnné, ale také na predikáty. Termíny predikátová logika a predikátový počet mohou znamenat jak logiku prvního řádu, tak logiku prvního řádu a logiku vyššího řádu dohromady; v prvním případě se někdy mluví o čisté predikátové logice nebo čistém predikátovém kalkulu .

Základní definice

Jazyk logiky prvního řádu je postaven na základě podpisu sestávajícího ze sady funkčních symbolůa sady predikátových symbolů. Každá funkce a predikátový symbol má přidruženou aritu , tedy počet možných argumentů. Jsou povoleny funkční i predikátové symboly arity 0. První z nich jsou někdy odděleny do samostatné sady konstant . Kromě toho se používají následující další znaky: ${\mathcal {F}}$ ${\mathcal {P}}$

variabilní symboly (obvykle , , , , , , , atd .); $X$ $y$ $z$ $x_{1}$ $y_1$ $z_{1}$ $x_{2}$ $y_2$ $z_{2}$
logické operace:

Symbol	Význam
$\neg$	negativní (ne)
$\přistát$	Konjunkce ("a")
$\lor$	Disjunkce ("nebo")
$\na$	Implikace ("jestliže..., pak...")

kvantifikátory :

Symbol	Význam
$\pro všechny$	Univerzální kvantifikátor
$\existuje$	Kvantifikátor existence

servisní znaky: závorky a čárka .

Symboly uvedené spolu se symboly z a tvoří abecedu logiky prvního řádu . Složitější konstrukce jsou definovány induktivně . ${\mathcal {P}}$ ${\mathcal {F}}$

Termín je symbolem proměnné nebo má tvar , kde je funkční symbol arity , a jsou termíny. $f(t_{1},\ldots ,t_{n})$ $F$ $n$ $t_{1},\ldots ,t_{n}$
Atom (atomový vzorec) má tvar , kde je symbol arity predikátu a jsou pojmy. $p(t_{1},\ldots ,t_{n})$ $p$ $n$ $t_{1},\ldots ,t_{n}$
- Toto je například atomový vzorec, který platí pro jakékoli reálné číslo . Vzorec se skládá z 2-árního predikátu , jehož argumenty jsou členy a 0. Zároveň se člen skládá z konstanty 1 (kterou lze považovat za 0-ární funkci), proměnné a symbolů binárních (2 -ary) funkce + a ×. $(x+1)\times (x+1)\geqslant 0$ $X$ $\geqslant$ $(x+1)\times (x+1)$ $(x+1)\times (x+1)$ $X$
Vzorec je buď atom nebo jedna z následujících konstrukcí: , , , , , , kde jsou funkce a je proměnná. $\neg F$ $F_{1}\lor F_{2}$ $F_{1}\land F_{2}$ $F_{1}\to F_{2}$ $\forall xF$ $\existuje xF$ ${\displaystyle F,F_{1},F_{2))$ $X$

Proměnná se ve vzorci nazývá vázaná , pokud má tvar buď , nebo je reprezentovatelná v jedné z forem , , , , a je již vázána v , a . Pokud není vázán v , nazývá se volný v . Vzorec bez volných proměnných se nazývá uzavřený vzorec nebo věta . Teorie prvního řádu je jakákoliv sada návrhů. $X$ $F$ $F$ $\forall xG$ $\existuje xG$ $\neg H$ $F_{1}\lor F_{2}$ $F_{1}\land F_{2}$ $F_{1}\to F_{2}$ $X$ $H$ $F_{1}$ $F_{2}$ $X$ $F$ $F$

Axiomatika a důkaz formulí

Systém logických axiomů logiky prvního řádu se skládá z axiomů výrokového počtu doplněných o dva nové axiomy:

$\forall xA\to A[t/x]$ ,
$A[t/x]\to \existuje xA$ ,

kde je vzorec získaný nahrazením termínu pro každou volnou proměnnou vyskytující se ve vzorci . $A[t/x]$ $t$ $X$ $A$

Logika prvního řádu používá dvě odvozená pravidla:

Modus ponens (toto pravidlo se také používá ve výrokové logice): ${\frac {A,A\to B}{B}}$
Pravidlo zobecnění : ${\frac {A}{\forall xA}}$

Výklad

V klasickém případě je interpretace logických vzorců prvního řádu dána na modelu prvního řádu , který je určen následujícími údaji:

Sada na přenášení , $\mathcal{D}$
Zobrazení sémantické funkce $\sigma$
- každý symbol -ary funkce od do -ary funkce , $n$ $F$ ${\mathcal {F}}$ $n$ $\sigma (f)\colon \,{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}$
- každý -ary predikátový symbol od do -ary vztah . $n$ $p$ ${\mathcal {P}}$ $n$ $\sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\mathcal {D}}$

Obvykle se akceptuje identifikace sady nosičů a modelu samotného, což implikuje implicitní sémantickou funkci, pokud to nevede k nejednoznačnosti. $\mathcal{D}$

Předpokládejme, že je funkce, která mapuje každou proměnnou na nějaký prvek z , kterému budeme říkat substituce . Výklad termínu on s ohledem na substituci je podán induktivně : $s$ $\mathcal{D}$ $[\![t]\!]_{s}$ $t$ $\mathcal{D}$ $s$

$[\![x]\!]_{s}=s(x)$ , pokud je proměnná, $X$
$[\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)([\!\![\,x_1]\!]_s,\ldots,[\![x_n]\ !]_s)$

Ve stejném duchu je definován vztah pravdivosti formulí na relativní : $\models_{s}$ $\mathcal{D}$ $s$

${\mathcal {D}}\models _{s}p(t_{1},\ldots ,t_{n})$ tehdy a jen tehdy , $\sigma(p)([\!\![\,t_1]\!]_s,\ldots,[\![t_n]\!]_s)$
${\mathcal {D}}\modely _{s}\neg \phi$ , právě tehdy, když - je nepravdivé, ${\mathcal {D}}\models _{s}\phi$
${\mathcal {D}}\models _{s}\phi \land \psi$ , pokud a pouze tehdy a jsou pravdivé, ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\models _{s}\phi \lor \psi$ , pokud a pouze tehdy nebo je pravdivé, ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\modely _{s}\phi \to \psi$ tehdy a jen tehdy , ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\modely _{s}\existuje x\,\phi$ , právě tehdy, když pro nějakou substituci , která se liší pouze od hodnoty na proměnné , ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $X$
${\mathcal {D}}\modely _{s}\forall x\,\phi$ , tehdy a jen tehdy pro všechny substituce , které se liší pouze od hodnoty na proměnné . ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $X$

Vzorec je pravdivý na (což je označeno jako ) if pro všechny permutace . Vzorec se nazývá platný (což je označeno jako ) if pro všechny modely . Vzorec se nazývá splnitelný , pokud alespoň pro jeden . $\phi$ $\mathcal{D}$ ${\mathcal {D}} \models \phi$ ${\mathcal {D}}\models _{s}\phi$ $s$ $\phi$ $\models\phi$ ${\mathcal {D}} \models \phi$ $\mathcal{D}$ $\phi$ ${\mathcal {D}} \models \phi$ $\mathcal{D}$

Vlastnosti a hlavní výsledky

Logika prvního řádu má řadu užitečných vlastností, které ji činí velmi atraktivní jako základní nástroj pro formalizaci matematiky . Hlavní jsou:

úplnost (to znamená, že pro jakýkoli uzavřený vzorec je odvoditelný buď on sám, nebo jeho negace);
konzistence (žádný vzorec nelze odvodit současně s jeho negací).

Navíc, pokud je konzistence více či méně zřejmá, pak úplnost je netriviální výsledek získaný Gödelem v roce 1930 ( Gödelův teorém úplnosti ). Gödelův teorém v podstatě zakládá základní ekvivalenci mezi pojmy dokazatelnost a platnost .

Logika prvního řádu má vlastnost kompaktnosti , dokázanou Malcevem : jestliže některá množina formulí není proveditelná, pak některé její konečné podmnožiny rovněž nejsou proveditelné.

Podle Löwenheim-Skolemovy věty, pokud má množina formulí model, pak má také model nanejvýš spočetné mohutnosti . S touto větou souvisí Skolemův paradox , který je však pouze pomyslným paradoxem .

Logika prvního řádu s rovností

Mnoho teorií prvního řádu zahrnuje symbol rovnosti. Bývá označována jako symboly logiky a doplněna o odpovídající axiomy, které ji definují. Taková logika se nazývá logika prvního řádu s rovností a odpovídající teorie se nazývají teorie prvního řádu s rovností . Rovnítko je zavedeno jako binární predikátový symbol . Další axiomy zavedené pro něj jsou následující: $=$

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

Použití

Logika prvního řádu jako formální model uvažování

Jako formalizovaná analogie běžné logiky umožňuje logika prvního řádu přísně uvažovat o pravdivosti a nepravdivosti výroků a jejich vztahu, zejména o logickém důsledku jednoho výroku z druhého, nebo například o jejich rovnocennosti. . Zvažte klasický příklad formalizace příkazů přirozeného jazyka v logice prvního řádu .

Vezměme si úvahu „Každý člověk je smrtelný. Sokrates je muž. Proto je Sokrates smrtelný ." Označme "x je člověk" přes ČLOVĚKA (x) a "x je smrtelník" přes MERTEN (x). Pak lze výrok „každý člověk je smrtelný“ reprezentovat vzorcem: x( ČLOVĚK (x) → SMRT (x)) výrok „Sokrates je člověk“ vzorcem ČLOVĚK ( Sokrates ) a „Sokrates je smrtelný“ formulí SMRT ( Sokrates ). Výpis jako celek lze nyní zapsat jako $\pro všechny$

( x( ČLOVĚK (x) → SMRT (x)) ČLOVĚK ( Sokrates )) → SMRT ( Sokrates )

\pro všechny

\land

Viz také

Literatura

Gilbert D., Akkerman V. Základy teoretické logiky. M., 1947
Kleene S.K. Úvod do metamatematiky. M., 1957
V. I. Markin. Logika predikátů // Nová filozofická encyklopedie : ve 4 svazcích / předchozí. vědecky vyd. rada V. S. Stepina . — 2. vyd., opraveno. a doplňkové - M . : Myšlenka , 2010. - 2816 s.
Mendelson E. Úvod do matematické logiky. M., 1976
Novikov PS Základy matematické logiky. M., 1959
Church A. Úvod do matematické logiky, díl I. M. 1960

Slovníky a encyklopedie	Velký Rus Britannica (online) Universalis

Logika

Filosofie • Sémantika • Syntaxe • Historie

Logické skupiny

klasická logika	Aristotelská logika výroková logika Logika prvního řádu Logika druhého řádu logika vyššího řádu
matematická logika	teorie množin Teorie modelu Teorie vyčíslitelnosti Důkazová teorie a konstruktivní matematika Lineární logika formální systém přirozený závěr Sekvenční počet Algebra logiky Relevantní logika Deontická logika intuicionistická logika Lambekův počet
Neklasická logika	intuicionismus fuzzy logika Substrukturální logika logika Popisná logika Vícehodnotová logika Logická syntéza Závazná logika Temporální logika Modální logika ( Hybrid logic ) epistemická logika
Filosofická logika	Kritické myšlení neformální logika deduktivní uvažování

Komponenty

Seznam booleovských symbolů