# Hilbert's style proof (FO logic)

I am stuck with this question to check whether the following formulas are valid and if they are valid, then derive them using Hilbert's axiom schema and Modes Ponens for First Order Logic. \begin{align} \exists x(\alpha \rightarrow \beta) \rightarrow (\exists x \alpha \rightarrow \exists x \beta) , x \notin FV(\beta) \end{align}

\begin{align} (\alpha \rightarrow \beta) \rightarrow (\exists x \alpha \rightarrow \exists x \beta) , x \notin FV(\beta) \end{align} The relevant axioms are:

• $\alpha \rightarrow (\beta \rightarrow \alpha)$
• $(\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta)\rightarrow(\alpha \rightarrow\gamma))$
• $\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$
• $\alpha \rightarrow \forall x \alpha, x \notin FV(\alpha)$
• $\forall x (\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$

I am not really sure if any other axioms will be required or if all the above listed ones will be required. Any hints will be appreciated.

Neither : $(α→β) → (∃xα→∃xβ), x \notin FV(β)$ is valid.

In order to manufacture a counter-example, we can "re-cycle" that of Tetori's answer.

We refer to Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 88 for the definition of :

Logical Implication : Let $\Gamma$ be a set of wffs, $\varphi$ a wff. Then $\Gamma$ logically implies $\varphi$, written $\Gamma \vDash \varphi$, iff for every structure $\mathfrak A$ for the language and every function $s : Var \to |\mathfrak A|$ such that $\mathfrak A$ satisfies every member of $\Gamma$ with $s, \mathfrak A$ also satisfies $\varphi$ with $s$ [in symbols : $\vDash_{ \mathfrak A} \varphi[s]$ ].

We apply the definition to the example above, with $\Gamma = \{ α→β \}$ and $\varphi := (∃xα→∃xβ)$.

Consider the domain of natural numbers $\mathbb N$ and let $\alpha := x = 0$ and $\beta := \exists y (y < 0)$.

$\exists y (y < 0)$ is false in $\mathbb N$; thus, also : $\exists x (x = 0) \rightarrow \exists x \exists y (y < 0)$ is false in it, i.e. : $\nvDash_{ \mathbb N} (\exists x(x = 0) \rightarrow \exists x \exists y (y < 0))$.

Consider now a variable assignment fuction $s$ such that $s(x)=1$.

We have that $(x = 0)[s]$ is false is $\mathbb N$, and thus : $\vDash_{ \mathbb N} ((x = 0) \rightarrow \exists y (y < 0))[s]$.

In conclusion, we have found a structure $\mathfrak A$ and a variable assignment function $s$ such that $\mathfrak A$ satisfies $(x = 0) \rightarrow \exists y (y < 0)$ with $s$, but $\mathfrak A$ does not satisfy $(\exists x(x = 0) \rightarrow \exists x \exists y (y < 0))$ with $s$, i.e. :

$(α→β) \nvDash (∃xα→∃xβ)$.

Thus $(α→β) \rightarrow (∃xα→∃xβ)$ is not valid.

A different approach is that of Dirk van Dalen, Logic and Structure (5th ed - 2013), page 67 :

Definition 3.4.4 : $\mathfrak A \vDash \varphi$ iff $\mathfrak A \vDash Cl(\varphi)$,

where : let $FV(\varphi) = \{ z_1, \ldots,z_k \}$, then $Cl(\varphi) := ∀z_1 \ldots z_k \varphi$ is the universal closure of $\varphi$.

The same counterexample above may be used to show that :

$\forall x[(α→β) → (∃xα→∃xβ)]$

is not valid.

Note

The axioms for quantifiers used in Enederton [see page 112] are the same of your post. But in your post a third propositional axiom is missing : the two that you are listed are not enough for a complete system of axioms for the propositional part.

• The propositional axiom involving negation, right? – user183763 Nov 24 '14 at 11:27
• @jayakrishnan - YES; it msut be $(\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ or $(\lnot A \rightarrow \lnot B) \rightarrow ((\lnot A \rightarrow B) \rightarrow A))$. – Mauro ALLEGRANZA Nov 24 '14 at 12:08

You can't prove it.

Consider the field of rationals. Take $\alpha(x)$ as $x=0$ and take $\beta$ as $\exists y(y\cdot 0=1)$. Then $\exists x (\alpha(x)\to\beta)$ holds (just take $x=1$) and $\exists x\alpha(x)$ also holds, but $\exists x\beta$ is false.

• How about $(\alpha \rightarrow \beta) \rightarrow (\exists x \alpha \rightarrow \exists x \beta), x \notin FV(\beta)$? – user183763 Nov 24 '14 at 2:55
• @jayakrishnan I think it is also unprovable, but I don't know how to prove it. – Hanul Jeon Nov 24 '14 at 3:01