„Elsőrendű nyelv” változatai közötti eltérés

* A szabályok ''([[#Szintaxis|szintaxis]])'' megadják, hogy a szimbólumokból hogyan képezzünk olyan sorozatokat, melyeket értelmesnek, azaz a nyelv részeinek tartunk. Ezen szabályokat többféle módszerrel is megfogalmazhatjuk (mi a logikában általánosan használt és legkézenfekvőbbnek tekintett ''szintaktikus rekurzió''t alkalmazzuk, de lehetséges [[halmazelmélet]]i fogalmakra; és/vagy [[generatív nyelvtan]]okra, [[Markov-algoritmus]]okra vagy egyebekre is építeni).

* Maga a nyelv, mint kifejezéseinek halmaza, a betűkből a szabályok segítségével építhető fel. A betűket és szabályokat együtt a nyelv '''''[[#A nyelvbázis|bázis]]'''''ának nevezzük.

 

Néha az „elsőrendű” kifejezésen pedig az előző tulajdonsággal szoros kapcsolatban álló, de vele mégsem teljesen ekvivalens, szintén szintaktikai jellegű tulajdonságot értenek, ti. hogy a nyelv tartalmaz kvantorokat (tehát több mint nulladrendű), de csak az individuumváltozók a valódi, logikai értelemben vett változók. Azaz csak ezek azok, melyek a nyelv [[#Interpretáció|interpretációi]] által sem egyértelműen meghatározott jelentésűek, vagy ami ezzel szoros kapcsolatban van, csak ezek a kvantifikálható változók; tehát a nyelv még nem másodrendű – mert másodrendű nyelvekben a függvény- és predikátumszimbólumok sem egyértelműen meghatározottak az interpretáció által, hanem kvantifikálhatóak). Az utóbbi két dolog, „interpretációfüggetlenség”/„logikaiság” és kvantifikiálhatóság valóban majdnem ugyanaz, hisz nem-logikai változók kvantifikálása a logikában valóban teljesen értelmetlen/lehetetlen, hiszen ezek egy adott interpretációban konkrét és rögzített jelentést kapnak [[#Példa x.|(lásd az x. példát)]].

 

A szintaktikai szabályokat precíz köznyelvi formában írjuk le; különféle fogalmak alkalmazásával tiszta, formális matematikai alakra is hozhatóak. A fogalmak pontos definíciója [[szerkezeti rekurzió]]n ''(szintaktikus rekurzió''n, ''formularekurzió''n) alapul (ld. lentebb):

# Ha <math> t_{1}, t_{2}, ... , t_{n} </math> termek, rendre az <math> s_{1}, s_{2}, ... , s_{n} </math> fajtából, és <math> f </math> formálisan n-változós és <math> \sigma(f) = \left( s_{1} , s_{2} , ..., s_{n} , s \right) </math> fajtájú műveleti jel, akkor <math> f \left( t_{1}, t_{2}, ... , t_{n} \right) </math> term, mégpedig <math> s </math> fajtájú.

# Valami pontosan akkor term, ha az [[#Az ábécé|ábécé]] <math> C, F, V </math>-beli betűiből az 1)., 2). és 3). szabályok véges sokszori alkalmazásával állítható elő. Tehát '''''termek lényegében a függvényszimbólumokból, változókból és konstansokból képezett összetett kifejezések'''''.

 

== Az elsőrendű nyelv ==

=== Definíció ===

 

E definíció lényegében az 5). szintaktikai szabály precízebb, matematikai formába öntése.

* Ezután az atomi formulákból képezett elsőosztályú kvantifikációs formulákat is előállítjuk. Definiáljuk így a <math> K_{1} </math> formulahalmazt: <br> <math> K_{1} := \left\{ \ Qx(R) \ \ \mathcal{j} \ \ Q \in \left\{ \exist , \forall \right\} \ \wedge \ R \in F_{0} \ \right\} </math> <math> = </math> <math> \left\{ \exist , \forall \right\} \times V \times \left\{ \, ( \, \right\} \times F_{0} \times \left\{ \, ) \, \right\} \ </math> (megjegyzés: ha tartjuk azt a megállapodást, hogy atomi kvantált formula esetén a magot nem kell zárójelbe tenni, akkor egy kis módosításra szorul a definíció, a Z-vel egyenlő tényezők elhagyhatóak).

<math> O_{1} := \left\{ P \oplus Q \in \bar{\Lambda} \ \mathcal{j} \ P,Q \in F_{0} \cup K_{1} \ \wedge \ \oplus \in L \right\} </math>

*Az összes elsőosztályú formula halmaza <math> F_{1} := K_{1} \cup O_{1} \cup F_{0} </math>.

 

== Szemantika ==

=== Struktúra, -típus és modell ===

 

* [[Nyelvbázis]]

 

=== Könyvek ===

 

 

=== Külső hivatkozások ===

* [http://www.cs.elte.hu/~kope/oktatas/ma2.pdf Jegyzet tanárszakos hallgatóknak (PDF)]

* [http://www.pte.hu/~uhi/kurzus/prolog/ Nagyon vázlatos, de nem hiányos összefoglalás az elsőrendű logikáról]