Elsőrendű logika

Az oldal jelenlegi verzióját még nem ellenőrizték tapasztalt közreműködők, és jelentősen eltérhet a 2021. június 30-án felülvizsgált verziótól ; az ellenőrzések 2 szerkesztést igényelnek .

Az elsőrendű logika egy formális számítás , amely lehetővé teszi a változókra , rögzített függvényekre és predikátumokra vonatkozó kijelentéseket . Kibővíti a propozíciós logikát .

Az elsőrendű logikán kívül léteznek magasabb rendű logikák is , amelyekben a kvantorok nemcsak változókra, hanem predikátumokra is alkalmazhatók. A predikátum logika és az állítmányszámítás kifejezések jelenthetnek elsőrendű logikát és elsőrendű és magasabb rendű logikát együtt; az első esetben néha tiszta predikátumlogikáról vagy tiszta predikátumszámításról beszélünk .

Alapdefiníciók

Az elsőrendű logika nyelve egy függvényszimbólum-készletből és predikátumszimbólum- készletből álló aláírás alapján épül fel. Minden függvényhez és predikátumszimbólumhoz tartozik egy aritás , azaz a lehetséges argumentumok száma. A 0 arity funkcionális és predikátumszimbóluma egyaránt megengedett. Az előbbieket néha külön konstanskészletre különítik el . Ezenkívül a következő kiegészítő karakterek használatosak: ${\mathcal {F}}$ ${\mathcal {P}}$

változó szimbólumok (általában , , , , , , , , stb.); $x$ $y$ $z$ $x_{1}$ $y_1$ $z_{1}$ $x_{2}$ $y_2$ $z_{2}$
logikai műveletek:

Szimbólum	Jelentése
$\neg$	Negatív (nem)
$\föld$	Kötőszó ("és")
$\lor$	Disjunkció ("vagy")
$\nak nek$	Implikáció ("ha ..., akkor...")

kvantorok :

Szimbólum	Jelentése
$\mindenkinek$	Univerzális kvantor
$\létezik$	Létezési kvantor

szervizkarakterek: zárójelek és vessző .

A felsorolt szimbólumok a és a szimbólumokkal együtt alkotják az elsőrendű logika ábécéjét . A bonyolultabb konstrukciókat induktív módon határozzuk meg . ${\mathcal {P}}$ ${\mathcal {F}}$

A kifejezés egy változó szimbóluma, vagy alakja , ahol az arity funkcionális szimbóluma , és kifejezések. $f(t_{1},\lpontok,t_{n})$ $f$ $n$ $t_{1},\ldots ,t_{n}$
Az atom (atomképlet) alakja , ahol az állítmányi aritás szimbólum , és kifejezések. $p(t_{1},\lpontok,t_{n})$ $p$ $n$ $t_{1},\ldots ,t_{n}$
- Például ez egy atomi képlet, amely bármely valós számra igaz . A képlet egy 2 tagú predikátumból áll , melynek argumentumai tagok és 0. Ugyanakkor a tag az 1 konstansból (ami 0-s függvénynek tekinthető), egy változóból és a bináris (2 ) szimbólumokból áll. -ary) függvények + és ×. $(x+1)\times (x+1)\geqslant 0$ $x$ $\geqslant$ ${\megjelenítési stílus (x+1)\times (x+1)}$ ${\megjelenítési stílus (x+1)\times (x+1)}$ $x$
A képlet egy atom vagy a következő konstrukciók egyike: , , , , , , ahol a függvények és egy változó. $\neg F$ $F_{1}\vagy F_{2}$ $F_{1}\land F_{2}$ $F_{1}\–F_{2}$ $\forall xF$ $\exists xF$ ${\displaystyle F,F_{1},F_{2))$ $x$

Egy változót akkor nevezünk kötöttnek a képletben , ha alakja vagy , vagy a , , alakok egyikében reprezentálható , és már kötött a , és . Ha nincs bekötve , akkor szabadnak nevezzük . A szabad változók nélküli képletet zárt képletnek vagy mondatnak nevezzük . Az elsőrendű elmélet az állítások bármely halmaza. $x$ $F$ $F$ $\forall xG$ $\létezik xG$ $\neg H$ $F_{1}\vagy F_{2}$ $F_{1}\land F_{2}$ $F_{1}\–F_{2}$ $x$ $H$ $F_{1}$ $F_{2}$ $x$ $F$ $F$

Axiomatika és képletek bizonyítása

Az elsőrendű logika logikai axiómáinak rendszere a tételszámítás axiómáiból áll, kiegészítve két új axiómával:

$\forall xA\to A[t/x]$ ,
$A[t/x]\to \létezik xA$ ,

ahol az a képlet, amelyet a képletben előforduló egyes szabad változók kifejezésének helyettesítésével kapunk . $A[t/x]$ $t$ $x$ $A$

Az elsőrendű logika két következtetési szabályt használ:

Modus ponens (ezt a szabályt a propozíciós logikában is használják): ${\frac {A,A\to B}{B}}$
Általánosítási szabály : ${\frac {A}{\forall xA}}$

Értelmezés

Klasszikus esetben az elsőrendű logikai képletek értelmezését az elsőrendű modellen adjuk meg , amelyet a következő adatok határoznak meg:

hordozókészlet , $\mathcal{D}$
Szemantikus függvény megjelenítése $\sigma$
- minden -ary függvény szimbólum tól -ary függvényre , $n$ $f$ ${\mathcal {F}}$ $n$ $\sigma (f)\colon \,{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}$
- minden -ary predikátum szimbólum -tól -árig reláció . $n$ $p$ ${\mathcal {P}}$ $n$ $\sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\mathcal {D}}$

Általában elfogadott a hordozóhalmaz és magának a modellnek az azonosítása, implicit szemantikai függvényre utalva, ha ez nem vezet kétértelműséghez. $\mathcal{D}$

Tegyük fel, hogy egy olyan függvény, amely minden változót leképez a -ból származó valamely elemre , amelyet helyettesítésnek nevezünk . Az on kifejezés helyettesítésre vonatkozó értelmezését induktív módon adjuk meg : $s$ $\mathcal{D}$ $[\![t]\!]_{s}$ $t$ $\mathcal{D}$ $s$

$[\![x]\!]_{s}=s(x)$ , ha egy változó, $x$
$[\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)([\!\![\,x_1]\!]_s,\ldots,[\![x_n]\ !]_s)$

Ugyanebben a szellemben definiáljuk a képletek relatív igazságának viszonyát : $\models_{s}$ $\mathcal{D}$ $s$

${\mathcal {D}}\models _{s}p(t_{1},\ldots ,t_{n})$ , akkor és csak akkor , $\sigma(p)([\!\![\,t_1]\!]_s,\ldots,[\![t_n]\!]_s)$
${\mathcal {D}}\models _{s}\neg \phi$ , akkor és csak akkor, ha - hamis, ${\mathcal {D}}\models _{s}\phi$
${\mathcal {D}}\models _{s}\phi \land \psi$ , ha és csak akkor igaz , ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\models _{s}\phi \lor \psi$ , akkor és csak akkor, ha vagy igaz, ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\models _{s}\phi \to \psi$ , akkor és csak akkor , ${\mathcal {D}}\models _{s}\phi$ ${\mathcal {D}}\models _{s}\psi$
${\mathcal {D}}\models _{s}\exists x\,\phi$ , akkor és csak akkor, valamilyen helyettesítésre , amely csak a változó értékétől különbözik , ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $x$
${\mathcal {D}}\models _{s}\forall x\,\phi$ , akkor és csak akkor minden helyettesítésre , ami csak a változó értékétől különbözik . ${\mathcal {D}}\models _{{s'}}\phi$ $s'$ $s$ $x$

A képlet igaz -on (amit jelölünk ), ha minden permutációra . Egy képletet érvényesnek nevezünk (amelyet jelölünk ), ha minden modellre . Egy képletet kielégítőnek nevezünk , ha legalább egy . $\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}$

Tulajdonságok és fő eredmények

Az elsőrendű logikának számos hasznos tulajdonsága van, amelyek nagyon vonzóvá teszik a matematika formalizálásának alapvető eszközeként . A főbbek a következők:

teljesség (ez azt jelenti, hogy bármely zárt formulánál vagy maga, vagy tagadása származtatható);
konzisztencia (a tagadásával egyidejűleg képlet sem származtatható).

Sőt, ha a következetesség többé-kevésbé nyilvánvaló, akkor a teljesség egy nem triviális eredmény, amelyet Gödel kapott 1930-ban ( Gödel teljességi tétele ). Lényegében Gödel tétele alapvető ekvivalenciát állít fel a bizonyíthatóság és az érvényesség fogalma között .

Az elsőrendű logika rendelkezik a tömörségi tulajdonsággal , amelyet Maltsev bizonyított : ha a képletek egy halmaza nem megvalósítható, akkor egyes véges részhalmazai sem megvalósíthatók.

A Löwenheim-Skolem tétel szerint, ha egy képlethalmaznak van modellje, akkor legfeljebb megszámlálható számosságú modellje is van . Ehhez a tételhez kapcsolódik a Skolem-féle paradoxon , amely azonban csak egy képzeletbeli paradoxon .

Elsőrendű logika egyenlőséggel

Sok elsőrendű elmélet magában foglalja az egyenlőség szimbólumát. Gyakran a logika szimbólumainak nevezik, és kiegészítik a megfelelő axiómákkal, amelyek meghatározzák. Az ilyen logikát egyenlőséggel rendelkező elsőrendű logikának , a megfelelő elméleteket pedig egyenlőséggel rendelkező elsőrendű elméleteknek nevezzük . Az egyenlőségjel bináris állítmány szimbólumként kerül bevezetésre . Az ehhez bevezetett további axiómák a következők: $=$

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

Használat

Az elsőrendű logika mint formális érvelési modell

A közönséges logika formalizált analógja lévén az elsőrendű logika lehetővé teszi az állítások igazságának és hamisságának, valamint azok kapcsolatának szigorú érvelését, különös tekintettel az egyik kijelentés logikai következményére, vagy például egyenértékűségére. . Tekintsünk egy klasszikus példát a természetes nyelvi állítások formalizálására az elsőrendű logikában .

Vegyük az érvelést: „Minden ember halandó. Szókratész ember. Ezért Szókratész halandó ." Jelöljük, hogy „x egy ember” az MAN -on (x) keresztül, és „x halandó”-t MERTEN -en (x) keresztül. Ekkor a „minden ember halandó” állítás a következő képlettel ábrázolható: x( EMBER (x) → HALÁL (x)) a „Szókratész ember” az EMBER ( Szókratész ) képlettel, és „Szókratész halandó” a HALÁL ( Szókratész ) képlettel . Az állítás egésze most így írható $\mindenkinek$

( x( EMBER (x) → HALÁL (x)) EMBER ( Szókratész )) → HALÁL ( Szókratész )

\mindenkinek

\land

Lásd még

Irodalom

Gilbert D., Akkerman V. Az elméleti logika alapjai. M., 1947
Kleene S.K. Bevezetés a metamatematikába. M., 1957
V. I. Markin. Predikátumok logikája // Új filozófiai enciklopédia : 4 kötetben / előz. tudományos-szerk. V. S. Stepin tanácsa . — 2. kiadás, javítva. és további - M . : Gondolat , 2010. - 2816 p.
Mendelson E. Bevezetés a matematikai logikába. M., 1976
Novikov PS A matematikai logika elemei. M., 1959
Church A. Bevezetés a matematikai logikába, I. M. kötet, 1960

Szótárak és enciklopédiák	Nagy orosz Britannica (online) Universalis

Logikák

Filozófia • Szemantika • Szintaxis • Történelem

Logikai csoportok

klasszikus logika	Arisztotelészi logika propozíciós logika Elsőrendű logika Másodrendű logika magasabb rendű logika
matematikai logika	halmazelmélet Modellelmélet Kiszámíthatóság elmélet Bizonyításelmélet és konstruktív matematika Lineáris logika formális rendszer természetes következtetés Sorozatszámítás Logikai algebra Releváns logika Deontikus logika intuicionista logika Lambek kalkulus
Nem klasszikus logika	intuicionizmus zavaros logika Szubstrukturális logika logika Leírás logika Többértékű logika Logikai szintézis Kötési logika Időbeli logika Modális logika ( Hibrid logika ) episztemikus logika
Filozófiai logika	Kritikus gondolkodás informális logika deduktív érvelés

Alkatrészek

Logikai szimbólumok listája