„Elsőrendű logika” változatai közötti eltérés
| [ellenőrzött változat] | [ellenőrzött változat] |
Tartalom törölve Tartalom hozzáadva
FoBe (vitalap | szerkesztései) |
Nincs szerkesztési összefoglaló |
||
27. sor:
* logikai jelek (kvantorok és [[logikai művelet]]ek jelei).
Egy véges sok [[szimbólum]]ot tartalmazó, adott jelkészlet vagy ábécé feletti logikai nyelvben
* A '''segédjel'''ek „értelmetlennek”, szakszerűbben „jelentés nélkülinek” <sup> [[#MIniesszé erről lentebb]] </sup> nevezhetőek, csak a formulák elválasztását és szintaktikai-pragmatikai támogatását végzik: az elsőrendű nyelvekben két segédjel van, a nyitó- és csukó zárójel ( ( és ) ); mellesleg megoldható lenne az is (az ún. [[lengyel jelölés]]sel vagy a [[Fogalomírás]]ban, de akár jelölési konvenciók/axiómák bevezetése által is), hogy ne is kelljen szerepelniük az elsőrendű logikában.
* Az '''állandók''' vagy '''konstansok''' értelme az adott nyelvben mindig ugyanaz. Kétféle állandót különböztethetünk meg a logikai nyelvekben:
39. sor:
<!-- A nulladrendű nyelvek koncepciója olyasmire épül, hogy az ilyen nyelvek „nem különböztetik meg az individuumokat”. Emiatt nincsenek bennük sem (nem-logikai) konstansszimbólumok (hisz ezek határozottan individuumokat jelölnek)), sem pedig (logikai) változók (hisz ezek is individuumokat jelölnek, csak „határozatlanul”).
Viszont emiatt nincsenek bennük „nem-logikai változók”, azaz függvényszimbólumok sem, hisz a függvények individuumokon hatnak, és ha egy nyelv nem képes az individuumok jelölésére, akkor olyan függvények jelölésére sem, melyek ezeken hatnak (pontosabban: ettől még nullváltozós függvényszimbólumok, azaz konstansjelek lehetnének bennük, de az előbb mondtuk, hogy ezek sincsenek). Nincsenek továbbá egy- vagy ennél többváltozós predikátumszimbólumok sem, hisz ezek is az individuumokon hatnak, argumentumaik individuum- és függvényjelek, és ha utóbbiak
-->
<!--
89. sor:
# Left and right parenthesis.
Some symbols may be omitted as primitive and taken as abbreviations instead; e.g. (P ↔ Q) is an abbreviation for (P → Q) <math>\wedge</math> (Q → P). The minimum number of operators and quantifiers needed is three; for example, ¬,
== Formation rules ==
95. sor:
# '''Simple and complex predicates''' If P is an ''n''-adic (''n'' ≥ 0) predicate, then <math>Pa_1,…,Pa_n</math> is well-formed. If ''n'' ≤ 1, P is atomic.
# '''Inductive Clause I:''' If φ is a ''wff'', then ¬ φ is a ''wff''.
# '''Inductive Clause II:''' If φ and ψ are ''wff''s, then <math>(\phi \wedge \psi)</math>,
# '''Inductive Clause III:''' If φ is a ''wff'' containing a free instance of variable ''x'', then <math> \forall x \, \varphi </math>
# '''Closure Clause:''' Nothing else is a ''wff''.
103. sor:
== Calculus ==
The predicate calculus is an extension of the [[propositional calculus]].
=== Axiomatic extension ===
114. sor:
=== Inference rule ===
The inference rule called [[Generalization (logic)|Universal Generalization]] is characteristic of the predicate calculus.
: <math>\mathit{if} \vdash Z(x), \mathit{then} \vdash \forall x Z(x)</math>
where ''Z(x)'' is supposed to stand for an already-proven theorem of predicate calculus and ∀xZ(x) is its closure with respect to the variable x. The predicate letter Z can be replaced by any other predicate letter.
Notice that Generalization is analogous to the Necessitation Rule of [[modal logic]], which is
:<math>\mathit{if} \vdash P, \mathit{then} \vdash
== Metalogical theorems of first-order logic ==
135. sor:
* [http://www.ltn.lv/~podnieks/ Introduction to mathematical logic] by Karl Podnieks.
* [http://us.metamath.org/index.html Metamath]: a project to construct mathematics using an axiomatic system based on [[propositional calculus]], predicate calculus, and [[set theory]]
-->
144 ⟶ 143 sor:
== Hivatkozások ==
* {{cite book |last=Bach |first=Iván |title=Formális nyelvek: Egyetemi tankönyv |publisher=Typotex |location=Budapest |year=2002 |isbn=963 9132 92 6 |url=http://mek.oszk.hu/05000/05099}}
* Csirmaz
{{csonk-dátum|csonk-mat|2005 júniusából}}
| |||