FOL(4) - syntax(2)

 

we'll introduce some theorems later used. i won't give full proof for below theorems but some basic ideas. readers are welcomed to prove for his own.

 

theorem A : $\Gamma \vdash \varphi$ iff $\Gamma \cup \Lambda$ tautologically implies $\varphi$.

 

proof

for $(\rightarrow)$, use induction for all $i<k$ at deduction sequence $<a_1,\ldots, a_n>$ where $a_n=\varphi$ theorem of $\Gamma$. for $a_k$, use induction principle(2 cases. $\varphi \in \Gamma \cup \Lambda$ and $\varphi$ is obtained by modus ponens).

for $(\leftarrow)$, use compactness theorem for sentential logic(second version). then you can get tautology and by using modus ponens finitely, you can get deduction of $\varphi$ from $\Gamma$

 

 

Generalization theorem : let $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$. then $\Gamma \vdash \forall x \varphi$.

 

proof

define $S=\{\varphi | \Gamma \vdash \forall x \varphi\}$ where $\varphi$ is any theorem of $\Gamma$. use induction principle introduced at FOL(3). then you can get the result that every theorem $\varphi$ of $\Gamma$ belongs to $S$.

 

 

Rule T : if $\Gamma \vdash \alpha_1$, $\ldots$, $\Gamma \vdash \alpha_n$ and $\{\alpha_1, \ldots, \alpha_n \} \models \beta$, $\Gamma \vdash \beta$.

 

proof : $\alpha_1 \rightarrow \alpha_2 \rightarrow \ldots \rightarrow \alpha_n \rightarrow \beta$ is tautology. now use modus ponens at deduction from $\Gamma$ where $a_n$ for all $n \in \mathbb{N}$ is enumerated.

 

 

Deduction theorem : if $\Gamma ;\gamma \vdash \varphi$, then $\Gamma \vdash (\gamma \rightarrow \varphi)$.

 

proof : use theorem A. the converse part can be got from modus ponens(for this, you've to check if $\Gamma_1 \vdash \varphi$, then $\Gamma_2 \vdash \varphi$ where $\Gamma_1 \subseteq \Gamma_2$, which is trivial from definition of 'deduction'. rigorously, use induction for deduction sequence)

 

 

Contraposition theorem : if $\Gamma ; \varphi \vdash \neg \psi$, then $\Gamma ; \psi \vdash \neg\varphi$.

 

proof : use rule T and deduction theorem.

 

 

reduction to absurdity(reductio ad absurdum, RAA) : if $\Gamma ; \varphi$ is inconsistent, then $\Gamma \vdash \neg\varphi$.

(*$\Gamma$ is inconsistent iff $\Gamma \vdash \beta$ and $\Gamma \vdash \neg\beta$ for some $\beta$)

 

proof : use definition of inconsistent, deduction theorem, and rule T. actually, antecedent and consequent of RAA is equivalent if you konw 'if $\Gamma_1 \vdash \varphi$, then $\Gamma_2 \vdash \varphi$ where $\Gamma_1 \subseteq \Gamma_2$'.

 

 

Generalization on constants : Assume that $\Gamma \vdash \varphi$ and that $c$ is a constant symbol that does not occur in $\Gamma$. Then there is a variable $y$ (which does not occur in $\varphi$) such that $\Gamma \vdash \forall y \varphi_{y}^{c}$. Furthermore, there is a deduction of  $\forall y \varphi_{y}^{c}$ from $\Gamma$ in which $c$ does not occur.

(*$\varphi_{y}^{c}$ is a result of replacing $c$ to $y$)

 

proof

part 1 : consider deduction sequence of $\varphi$ from $\Gamma$. $<a_1,\ldots, a_n>$ where $a_n=\varphi$. verify $<{a_1}_{y}^{c},\ldots,{a_n}_{y}^{c}>$ is a deduction from $\Gamma$ using defintion of deduction(use strong induction for all $i<k$)(you can find $y$ for any variable that does not occur in deduction sequence). then we get $\Gamma \vdash \varphi_{y}^{c}$.

 

part 2 : consider $\Phi \subseteq \Gamma$ finite set which is used for deducing $\varphi_{y}^{c}$. then trivially $\Phi \vdash \varphi_{y}^{c}$. then $y$ does not occur in $\Phi$(consider the case $a_k \in \Gamma$. then you can understand $y$ does not occur in $a_k$ by assumption. and since c does not occur in $a_k$, $(a_k)_{y}^{c}=a_k$). then by generalization theorem, $\Phi \vdash \forall y \varphi_{y}^{c}$. thus $\Gamma \vdash \forall y \varphi_{y}^{c}$.

 

 

Theorem B : Assume that $\Gamma \vdash \varphi_{c}^{x}$ , where the constant symbol $c$ does not either occur in $\Gamma$ or in $\varphi$. Then $\Gamma \vdash \forall x \varphi$, and there is a deduction of $\forall x \varphi$ from $\Gamma$ in which $c$ does not occur.

 

proof : use generalization theorem and axiom group 2 and re-replacement lemma.

 

(* re-replacement lemma : if $y$ does not occur in $\varphi$, then $x$ is substitutable for $y$ in $\varphi_{x}^{y}$ and $(\varphi_{y}^{x})_{x}^{y}=\varphi$)(for this, use induction for formulas)

 

 

Rule EI : let $c$ does not occur in $\varphi,\psi, \Gamma$ and $\Gamma ; \varphi_{c}^{x} \vdash \psi$. then $\Gamma ; \exists \varphi \vdash \psi$.

 

proof : use contraposition theorem and rule T(or use tautology that $(\alpha \rightarrow \beta) \rightarrow (\neg\beta \rightarrow \neg\alpha)$. also use theorem B.

 

 

alphabetic variants theorem : let $\varphi$ be any formula, $t$ a term, $x$ a variable. then there exists $\varphi'$ such that $\varphi \vdash \varphi'$ and $\varphi' \vdash \varphi$, and $t$ is substitutable for $x$ in $\varphi'$.

 

proof : use induction for formulas. for atomic, $\varphi'=\varphi$. and each case, take $(\neg\varphi)'=\neg\varphi'$, $(\varphi \rightarrow \psi)'=\varphi' \rightarrow \psi'$. but situation differs about $\forall y \varphi$. in this case, take $(\forall y \varphi)'=\forall z(\varphi')_{z}^{y}$. and divide cases into $x$ does not occur free, and $x$ does occur free in $\varphi'$ where $t$ is substitutable for $x$ in $\varphi'$ by inductive hypothesis. the intuitive idea for quantifier is like this;

 

suppose we want to have '$y$ is substitutable for $x$' in $\forall y Pxy$ for getting axiom group2 formula $\vdash \forall x \forall y Pxy \rightarrow \forall y Pyy$. but this always fails. to get this, we can change some variables in $\forall x \forall y Pxy$ like $\forall x \forall z Pxz$ where they are deducible from each other. then clearly $y$ is substitutable for $x$ in $\forall x \forall z Pxz$ we've taken and thus $\vdash \forall x \forall z Pxz \rightarrow \forall y Pyy$. thus if you can calculate $\vdash \forall x \forall y Pxy \rightarrow \forall x \forall z Pxz$, original formula can be proved.

 

 

Equality theorem(equivalence relation of '=')

 

(i) '=' is reflexive : $\vdash x=x$

 

(ii) '=' is symmetric : $\vdash x=y\rightarrow y=x$

proof

$\vdash x=x\rightarrow (x=x \rightarrow x=y)$ by axiom group6

$\vdash x=x\rightarrow x=y$ since $x=x$ is in axiom group5 & using rule T

 

(iii) '=' is transitive : $\vdash x=y\rightarrow y=z\rightarrow x=z$

proof

$\vdash y=x \rightarrow y=z\rightarrow x=z$ by axiom group5

then $x=y\vdash y=x$ thus $x=y\vdash y=z\rightarrow x=z$. hence,

$\vdash x=y\rightarrow y=z\rightarrow x=z$ by deduction theorem.

 

using generaliation theorem on (i), (ii), (iii), we get

$\vdash \forall x x=x$

$\vdash \forall x \forall y x=y\rightarrow y=x$

$\vdash \forall x \forall y \forall z x=y\rightarrow y=z\rightarrow x=z$