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

Az elsőrendű logika főbb ágai, illetve fontosabb kutatási területei a következők:

* [[Bizonyításelmélet]] – az elsőrendű logikán belül neve [[Predikátumkalkulus]]. A logikai kalkulusok azzal foglalkoznak, hogy hogyan lehet az illető logikai elméletet axiomatikusan felépíteni. Megadunk néhány, általában szemantikai érvek alapján „elfogadott” formulát ('''axiómák''') és néhány szintaktikai '''levezetési szabály'''t, melyek segítségével „elfogadott” formulából „elfogadott” formulák gyárthatóak úgy, hogy ami nem gyártható le, az ne is számítson „elfogadottnak” ('''záradék'''). Ez a három összetevő (lásd: [[Definíció#Matematikai definíciófajták|rekurzív definíció]]) alkot egy kalkulust. A cél, hogy egyrészt minden „elfogadott” formulát le tudjunk vezetni (a kalkulus '''teljes''' legyen), másrészt minden levezethető formula „elfogadott” legyen (a kalkulus '''helyes''' legyen). Röviden szólva, minden igazságot bizonyítani lehessen, de egy hülyeséget sem. Az elsőrendű predikátumkalkulus fejlesztésében szerepet vállaló legfontosabb kutatók: [[Gottlob Frege|G. Frege]], [[Bertrand Russell|B. Russell]], [[David Hilbert|D. Hilbert]], [[Kurt Gödel|K. Gödel]], [[Gerhard Gentzen|G. Gentzen]], [[Leon Henkin|L. Henkin]], [[Alfred Tarski|A. Tarski]], [[John Alan Robinson|J.A. Robinson]], [[Jan Łukasiewicz|J. Łukasiewicz]]. A főbb elméletek, alágak:

** Az elsőrendű [[Frege-kalkulus]]

** [[Gerhard Gentzen|Gentzen]]-stílusú kalkulusok ([[természetes levezetés|természetes levezetőkalkulus]], [[szekventkalkulus]]),

** [[Tablókalkulus]],

** [[Rezolúciós kalkulus]].

* A bizonyításelméletből nőtt ki mára önálló tudományággá a „számításelméleti” vagy „számítógépes logika”, melynek fő területe az automatikus tételbizonyítás kutatása. Legfontosabb elmélete a rezolúciós kalkulus. Ezenkívül foglalkozik a logika számításelméleti vonatkozásaival is (kielégíthetőségi problémák [SAT] és megoldhatóságuk kutatása és jellemzése).

 

== Elsőrendű nyelvek ==

 

Az elsőrendű nyelveket, ahogy a formális nyelveket általában [[formula|logikai formulák]], betűsorozatok [[halmaz]]aként definiáljuk. Ahogy minden formális nyelv esetén, adva van egy [[nyelvbázis]], azaz egy betűkészlet és szabályok egy halmaza, mely megadja, hogy a betűket milyen sorrendben lehet és kell összerakni. Ezeket a szabályokat nevezzük a nyelv [[szintaxis]]ának. A nyelv elemei a következő osztályokban sorolhatók:

* A '''segédjel'''ek „értelmetlennek”, szakszerűbben „jelentés nélkülinek” ^{[[#MIniesszé erről lentebb]]} 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:

** A '''nem-logikai konstansok''', vagy egyszerűen csak konstansok, melyek nem ilyenek, azaz ún. ''individuum''okat jelölnek;

* A '''változók''' jelentése viszont nem feltétlenül állandó, ugyanazon formula egy-egy példányában (ha mondjuk a lap tetején vagy alján fordul elő) mást és mást jelenthet ugyanaz a szimbólum, még ha pontosan ugyanazon a helyen is van. Ezeknek a jeleknek a jelentését meg kell adni, ezt úgy mondjuk, hogy a jeleket '''interpretáljuk'''. Ezen belül a változókat is két csoportra oszthatjuk:

 

----

 

-->

=== Az elsőrendű nyelv és nyelvbázis ===

 

 

==== Jelkészlet ====

 

 

==== Kifejezések (termek) ====

 

 

==== Kijelentések (predikátumok) ====

 

 

==== Interpretáció ====

 

 

==== Az elsőrendűség ====

Nevertheless, first-order logic is strong enough to formalize all of [[set theory]] and thereby virtually all of [[mathematics]]. Its restriction to quantification over individuals makes it difficult to use for the purposes of [[topology]], but it is the classical logical theory underlying mathematics. It is a stronger theory than [[sentential logic]], but a weaker theory than [[second-order logic]].

 

 

* formation rules (i. e. recursive definitions for forming well-formed formulas).

* transformation rules (i. e. [[inference rule]]s for deriving theorems).

When the set of axioms is infinite, it is required that there is an [[algorithm]] which can decide for a given well-formed formula whether it is an axiom or not. Furthermore, there should be an algorithm which can decide whether a given application of an inference rule is correct or not.

 

The "vocabulary" is composed of

# Uppercase letters P, Q, R,… which are predicate variables.

Some symbols may be omitted as primitive and taken as abbreviations instead; e.g. (P &harr; Q) is an abbreviation for (P &rarr; Q) <math>\wedge</math> (Q &rarr; P). The minimum number of operators and quantifiers needed is three; for example, ¬, <math>\wedge</math>, and <math>\forall</math> suffice. A '''term''' is a constant, variable, or function symbol of n&#8805;0 arguments.

 

The set of well-formed formulas (''wff''s) is recursively defined by the following rules:

# '''Simple and complex predicates''' If P is an ''n''-adic (''n'' &ge; 0) predicate, then <math>Pa_1,…,Pa_n</math> is well-formed. If ''n'' &le; 1, P is atomic.

# '''Closure Clause:''' Nothing else is a ''wff''.

 

[[Modus ponens]] suffices as the sole rule of inference. If there are axiom schemata, then a rule of substitution is also required.

 

The predicate calculus is an extension of the [[propositional calculus]]. If the propositional calculus is defined with eleven axioms and one inference rule ([[modus ponens]]), not counting some auxiliary laws for the [[logical equivalence]] operator, then the predicate calculus can be defined by appending four additional axioms and one additional inference rule.

 

The following four logical axioms characterize a predicate calculus:

* PRED-1: <math> \forall x Z(x) \rightarrow Z(y) </math>

These are actually [[axiom schema|axiom schemata]], because the predicate letters ''W'' and ''Z'' in them can be replaced by any other predicate letters, without altering the validity of these formulae.

 

The inference rule called [[Generalization (logic)|Universal Generalization]] is characteristic of the predicate calculus. It can be stated as

: <math>\mathit{if} \vdash Z(x), \mathit{then} \vdash \forall x Z(x)</math>

:<math>\mathit{if} \vdash P, \mathit{then} \vdash \Box P</math>.

 

 

Some important metalogical theorems are listed below in bulleted form.

# Monadic predicate logic (i. e., predicate logic with only predicates of one argument) is decidable.

 

 

* [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]]

* [[Formális nyelv]]

== Hivatkozások ==

* Csirmaz, László: ''Matematikai logika egyetemi jegyzet'', ELTE Bp., 1994 ([http://www.renyi.hu/~csirmaz/ Postscript változat])