FOL(3) - syntax(1)

 

For saying 'syntax', we mean we have some formal rules which indicates how to yields some formulas from inference rules. In this part, basically, we don't inquire any semantical concepts; just do give some finite sequences from selected rules.

 

now define deduction of $\varphi$ from $\Gamma$ as a finite sequence $<a_1,\ldots,a_n>$ of formulas where $a_n = \varphi$, and for every formula $a_k$,

 

(a) $a_k \in \Gamma \cup \Lambda$ or

(b) $a_k$ is obtained by modus ponens from $a_i$ and $a_j=(a_i \rightarrow a_k)$ where for some $i,j<k$.

 

if there is a deduction of $\varphi$ from $\Gamma$, we call $\varphi$ is a theorem of $\Gamma$ or $\varphi$ is deducible from $\Gamma$. In our notation, we define this $\Gamma \vdash \varphi$.

 

$\Lambda$ is a set of axioms. basic axioms we'll use are divided into 6 groups.

 

1. tautologies.

2. $\forall x \alpha \rightarrow \alpha_{t}^{x}$, where $t$ is substitutable for $x$ in $\alpha$

3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$

4. $\alpha \rightarrow \forall x \alpha$ where $x$ does not occur free in $\alpha$

5. $x=x$

6. $(x=y) \rightarrow (\alpha \rightarrow \alpha')$, where $\alpha$ is an atomic formula, and $\alpha'$ is obtained by replacing zero or more times $x$ by $y$.

 

then define $\varphi \in \Lambda$ iff $\varphi$ is a generalization of $\psi$. $\varphi$ is a generalization of $\psi$ iff $\varphi = \forall x_1 \ldots \forall x_n \psi$ where $n \in \mathbb{N} \cup \{0\}$.

 

 

explanation will be needed for some axiom groups.

 

1. tautology is a concept of PL. and we can consider each FOL formulas each sentence symbols in PL. for axmple, $Pt$and $\forall x Px$ are regarded as sentence symbols. for precise definition, we've to introduce some notions.

 

define prime formula $\varphi$ as $\varphi$ is atomic formula or $\varphi = \forall x \psi$. then for every prime formulas, using sentential connectives $\rightarrow, \neg$, we can construct every FOL formulas. and every FOL formula can be regarded as PL formula. using this idea, we'll use tautologies as axioms.

 

for example, $Px \rightarrow Px$ is tautology and so does $(\forall x Py \rightarrow \neg Pc) \rightarrow (Pc \rightarrow \neg\forall x Py)$. remember any generalizations of these are axioms.

 

 

2. now define $\alpha_{t}^{x}$ and '$t$ is substitutable for $x$ in $\alpha$'.

 

a. we define substitution $\alpha_{t}^{x}$ of $\alpha$ recursively;replacing free variable $x$ of $\alpha$ by term $t$.

 

(i) if $\alpha$ is atomic formula, then $\alpha_{t}^{x}$ is replacing every $x$ occurs in $\alpha$ by $t$.

(ii) $(\neg \alpha)_{t}^{x} = (\neg \alpha_{t}^{x})$

(iii) $(\alpha \rightarrow \beta)_{t}^{x} = (\alpha_{t}^{x} \rightarrow \beta_{t}^{x})$

(iv) $(\forall y \alpha)_{t}^{x} = \forall y \alpha \quad\text{if $x=y$},\quad \text{or}\quad \forall y (\alpha_{t}^{x}) \quad\text{if $x \neq y$} $.

 

b. define $t$ is substitutable for $x$ in $\alpha$ recursively.

 

(i) $t$ is always substitutable for $x$ in any atomic formula $\alpha$.

(ii) $t$ is substitutable for $x$ in $\neg \alpha$ iff $t$ is substitutable for $x$ in $\alpha$

(iii) $t$ is substitutable for $x$ in $\alpha \rightarrow \beta$ iff $t$ is substitutable for $x$ in $\alpha$ and $\beta$

(iv) $t$ is substitutable for $x$ in $\forall y \alpha$ iff (1) $x$ does not occur free in $\forall \alpha$ or (2) $y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\alpha$.

 

note for substitution.

 

1. $\varphi_{x}^{x}=\varphi$

2. $x$ is substitutable for $x$ in any formula.

3. if $t$ contains no variables in $\varphi$, then $t$ is substitutable for $x$ in $\varphi$.

(you can check 2-3 using induction for formulas)

 

 

now introduce a induction principle for our syntax.

 

define a set $S$ of formulas is closed under modus ponens if $\alpha \in S$ and $(\alpha\rightarrow\beta) \in S$, then $\beta \in S$.

 

Induction principle : let a set $S$ of formulas such that $\Gamma \cup \Lambda \subseteq S$ and $S$ is closed under modus ponens. then $S$ contains every theorem of $\Gamma$.

 

proof : consider any $\varphi$ theorem of $\Gamma$. then there exists a deduction $<a_1,\ldots, a_n>$ where $a_n=\varphi$. give strong induction for all $i<k$ such that $a_i \in S$. now think about $a_k$.

 

case 1 : $a_k \in \Gamma \cup \Lambda$. then trivially $a_k \in S$.

case 2 : $a_K$ is obtained by modus ponens using earily made formulas $a_i$ and $a_j=(a_i \rightarrow a_k)$ for some $i,j<k$ where $a_i, a_j \in S$ by inductive hypothesis. since $S$ is closed under modus ponens, we get $a_k \in S$ trivially.

 

we'll use this induction principle many times from now on.

 

 

P.S. you may wonder the intuitive idea about 'substitutable'.

 

revisited; 2. $\forall x \alpha \rightarrow \alpha_{t}^{x}$, where $t$ is substitutable for $x$ in $\alpha$

 

it is easy to understand for $\alpha_{t}^{x}$ where we change every free variable $x$ in $\alpha$ to term $t$. if $x$ does not freely occur or does not occur in $\alpha$, then $\alpha_{t}^{x}=\alpha$ trivially. this concept is easy to understand. but 'substitutable' is somewhat complicated concept introduced for some reasons(one reason is for the soundness theorem of FOL, but you do not need to care details yet).

 

consider $\forall x \alpha \rightarrow \alpha_{t}^{x}$. consider $\alpha= \forall x \neg\forall y x=y$. then $\forall x \alpha \rightarrow \alpha_{t}^{x}$ is $\forall x \neg\forall y x=y \rightarrow \neg\forall y y=y$. since latter part of conditional is always false, we cannot say without the condition '$t$ is substitutable for $x$', axiom group 2 could be false. so for this not to happen, we gave that condition.