Elsőrendű logika

Logika szintaktikus tárgyalása

Az ítéletlogika szintaktikai alapokon való felépítése az ítéletkalkulus

Elsőrendű logika szintaktikai alapokon való felépítése a predikátumkalkulus vagy függvénykalkulus

Axiómasémák

Itéletlogika mint matematikai struktúra ({i, h}, $\neg , \supset$)
Az axiómasémák megadják a műveletek tulajdonságait
Az itéletlogika nyelvében csak a $\neg \supset$ párt használjuk (funkcionálisan teljes művelethalmaz)

\[ \neg X\lor Y\equiv X\supset Y\\ X\land Y\equiv\neg(\neg X\lor\neg Y)\\ X\land Y\equiv\neg(X\supset\neg Y) \]

Axiómák kapcsolata a szemantikával

Axiómák tautológiai/logikai törvények.

Legyen egy $G$ formula, $G(X|S)$ az a formula, amit $G$-ből $X$ változójának egy $S$ formulával való behelyettesítésével kapjuk. Ha $G$ tautológia, akkor $G(X|S)$ is az.

Következmény: Az axiómákból behelyettesítéssel kapott formulák is logikai törvények - axiómának tekinthetők

Modus ponens

$A \supset B,A \models_{0} B$
Szemantikai és szintaktikai értelem kapcsolatát adja meg.

Bizonyításelméleti levezetés

$G$-nek $\mathcal{F}$-ből való levezetése egy olyan $\varphi_{1},\varphi_{2},\dots,\varphi_{k},\dots,\varphi_{n}$ formulasorozat, amelynek utolsó formulája a $G$, ahol

$\varphi_k \in \mathcal{F}$ , vagy
$\varphi_k$-t axiomasémákból kaptuk, vagy
$\varphi_k$-t a levezetési szabállyal kaptuk $\varphi_s, \varphi_t$-ből $(s,t < k)$, azaz $\varphi_{k} = mp(\varphi_{S},\varphi_{t})$

Levezetés szabály a modus ponens: leválasztási szabály.

Egy $G$ formla az $\mathcal{F} = \{F_1,F_2, \dots, F_n\}$ formulahalmazból levezethető ($\mathcal{F} = \{F_1,F_2, \dots, F_n\} \vdash_0 G$), ha van $G$-nek $\mathcal{F}$-ből való levezetése. Ez a szintaktikus következményfogalom. Egy $A$ formulának az üres feltételhalmazból (csak axiómákból) való levezetése az $A$ bizonyítása ($\vdash_0A$)

Predikátumkalkulus

Elsődrendü logika bizonyításelméleti felépítése

(B1) $A \supset (B \supset A)$
(B2) $(A \supset (B \supset C)) \supset ((A \supset B) \supset (A \supset C))$
(B3) $(¬A \supset B) \supset ((¬A \supset ¬B) \supset A)$
(B4) $\forall x A \supset [A(x k t)]$
(B5) $\forall x (A \supset B) \supset (\forall x A \supset \forall x B)$
(B6) $A \supset \forall x A, ahol x 6∈ Par(A)$
(B7) a $(B1)–(B6)$ axiómák általánosításai

Bizonyítás elmélet helyessége, teljessége

Helyesség tétel

A bizonyításelméleti kalkulus helyes, ha $F_{1},F_{2},\dots,F_{n} \vdash_{0} G$ m akkor $F_{1},F_{2},\dots,F_{n} \vDash_{0} G$

Teljesség tétel

A bizonyításelméleti kalkulus teljes, azaz ha $\{F_1, F_2,\dots,F_n\}\models_0$ akkor $F_{1},F_{2},\dots,F_{n} \vdash_{0} G$.

Tulajdonságok

levezetés
bizonyítható
ellentmondásos (inkonzisztens) $\neq$ nem ellentmondásos(konzisztens)

Ha $\mathcal{F}$-ből levezethető G, akkor az $\mathcal{F}\cup\{G\}$ ellentmondásos.

Ha $F_{1},F_{2},\dots,F_{n}$ ellentmondásos, akkor kielégíthetetlen Legyen A egy formula, és $\mathcal{F}$ egy konzisztens formulahalmaz, akkor

$\mathcal{F}, \neg A$ ellentmondásos, akkor és csak akkor, ha $\vdash_{0} A$

$\mathcal{F}, A$ ellentmondásos, akkor és csak akkor, ha $\vdash_{0} \neg A$

Tételek folytatás

Kalmár lászló lemmája

Egy $k$ változós $G$ formula igazságtáblájának minden sorában $X'_1,X'_2,\dots,X'_k \vdash G'$

Tétel 2

Ha $X'_1,X'_2,\dots,X'_k \vdash_0 G'$ és $\neg X'_1, X'_2, \dots X'_k \vdash G'$ akkor $X'_2,\dots,X'_k \vdash_0 G'$

Tétel 3

Ha $G$ tautológia, akkor $G$ bizonyítható

Gyenge teljesség

Legyen $\{F_1,F_2,\dots,F_n\}$ véges formulahalmaz.
Ha $\{F_1,F_2,\dots,F_n\}\models_0 G$, akkor $\{F_1,F_2,\dots,F_n\}\vdash_0 G$

Göbel féle teljesség bizonyítás

Ha $\{F_1,F_2,\dots,F_n\}\models_0 G$, akkor $\{F_1,F_2,\dots,F_n\}\vdash_0 G$

Levezetés

Ha $\{F_1,F_2,\dots\}\models_0 G$, akkor $\{F_1,F_2,\dots\}\cup {\neg G}$ kielégíthetetlen
$\{F_1,F_2,\dots\}\cup {\neg G}$ ellentmondásos (inkonzisztens), akkor $\{F_1,F_2,\dots\}\vdash_0G$

természetes technika strukturális szabályai

Azonosság törvénye

az azonosság törvénye

\[ \Gamma, A \vdash_0 A \]

bővítés szabálya

\[ \frac{\Gamma \vdash_0 A}{\Gamma , B \vdash_0 A} \]

Szűkítés szabálya

\[ \frac{\Gamma, B, B, \Delta \vdash_0 A}{\Gamma, B, \Delta\vdash_0 A} \]

felcserélés szabálya

\[ \frac{\Gamma, B, C, \Delta, \vdash_0 A}{\Gamma, C, B, \Delta, \vdash_0 A} \]

vágás szabálya

\[ \frac{\Gamma \vdash_0 A \qquad \Delta, A \vdash_0 B}{\Gamma, \Delta, \vdash_0 B} \]

	bevezető szabályok		alkalmazó szabályok
($\supset b$)	$ \frac{\Gamma, A \vdash_0 B}{\Gamma \vdash_0 A \supset B} $	($\supset a$)	$\frac{\Gamma \vdash_0 A \quad \Gamma \vdash_0 A\,\supset\,B}{\Gamma \vdash_0 B}$
($\land b$)	$\frac{\Gamma \vdash_0 A \quad \Gamma\,\vdash_0\,B}{\Gamma \vdash_0 A \land B}$	($\land a$)	$\frac{\Gamma,\,A,\,B\,\vdash_0 C}{\Gamma, A \land B \vdash_0 C}$
($\lor b$)	$\frac{\Gamma \vdash_0 A}{\Gamma\,\vdash_0\,A\,\lor\,B} \quad \frac{\Gamma \vdash_0 B}{\Gamma \vdash_0 A \lor B}$	($\lor a$)	$\frac{\Gamma,A \vdash_0 C \quad \Gamma, B\vdash_0 C}{\Gamma,\,A\,\lor\ B \vdash_0 C}$
($\neg b$)	$\frac{\Gamma , A \vdash_0 B \quad \Gamma , A \vdash_0 \neg B}{\Gamma \vdash_0 \neg A}$	($\neg a$)	$\frac{\Gamma\, \vdash_0 \,\neg \neg A}{\Gamma \vdash_0 A}$

További szabályok elsőrendű logikában

	bevezető szabályok		alkalmazó szabályok
($\forall b$)	$\frac{\Gamma\,\vdash\,A}{\Gamma\,\vdash\,\forall x A}$	($\forall a$)	$\frac{\Gamma\,\vdash\,\forall x A}{\Gamma\,\vdash\,[A\left(x \, \\|\\| \, t \right)]}$
($\exist b$)	$\frac{\Gamma \, \vdash \, [\,A\, (x \\|\\| t)\,]}{\Gamma \, \vdash \, \exist xA}$	($\exist a$)	$\frac{\Gamma , A \vdash B}{\Gamma, \exist xA \vdash B}$ $\left(x \notin \text{Par}(\Gamma, B)\right)$

	bevezető szabályok		alkalmazó szabályok
(\(\supset b\))	$ \frac{\Gamma, A \vdash_0 B}{\Gamma \vdash_0 A \supset B} $	(\(\supset a\))	\(\frac{\Gamma \vdash_0 A \quad \Gamma \vdash_0 A\,\supset\,B}{\Gamma \vdash_0 B}\)
(\(\land b\))	\(\frac{\Gamma \vdash_0 A \quad \Gamma\,\vdash_0\,B}{\Gamma \vdash_0 A \land B}\)	(\(\land a\))	\(\frac{\Gamma,\,A,\,B\,\vdash_0 C}{\Gamma, A \land B \vdash_0 C}\)
(\(\lor b\))	\(\frac{\Gamma \vdash_0 A}{\Gamma\,\vdash_0\,A\,\lor\,B} \quad \frac{\Gamma \vdash_0 B}{\Gamma \vdash_0 A \lor B}\)	(\(\lor a\))	\(\frac{\Gamma,A \vdash_0 C \quad \Gamma, B\vdash_0 C}{\Gamma,\,A\,\lor\ B \vdash_0 C}\)
(\(\neg b\))	\(\frac{\Gamma , A \vdash_0 B \quad \Gamma , A \vdash_0 \neg B}{\Gamma \vdash_0 \neg A}\)	(\(\neg a\))	\(\frac{\Gamma\, \vdash_0 \,\neg \neg A}{\Gamma \vdash_0 A}\)

	bevezető szabályok		alkalmazó szabályok
(\(\forall b\))	\(\frac{\Gamma\,\vdash\,A}{\Gamma\,\vdash\,\forall x A}\)	(\(\forall a\))	\(\frac{\Gamma\,\vdash\,\forall x A}{\Gamma\,\vdash\,[A\left(x \, \\|\\| \, t \right)]}\)
(\(\exist b\))	\(\frac{\Gamma \, \vdash \, [\,A\, (x \\|\\| t)\,]}{\Gamma \, \vdash \, \exist xA}\)	(\(\exist a\))	\(\frac{\Gamma , A \vdash B}{\Gamma, \exist xA \vdash B}\) \(\left(x \notin \text{Par}(\Gamma, B)\right)\)