MHB Logic, proving theorem in formal system K

[Barioth]

Hi

here is the problem I'm working on,

Let $A(x_1)$ be a well formed formula of a language $L$ in which $x_1$ is free, let $a_1$ an invidual constant of $L$, Show that the formula $A(a_1)\rightarrow(\exists x_1)A(x_1)$ is a theorem of $K_L$

on this link, the first slide as the axiom of $K_L$

http://www.idi.ntnu.no/emner/tdt4135/handouts/slides-9.pdf

I wanted to use the following proof:

$A(a_1)\rightarrow(\exists x_1)A(x_1)$

is equivalent logic to

$(\exists x_1)(A(a_1)\rightarrow A(x_1))$

wich is equivalent logic to

$(\forall x_1)A(a_1)\rightarrow A(x_1)$

then trying to conclude using (K5) from the pdf link,

but I just realized that since $x_1$ is free in A, I cannot move the quantifier like I did.

 

[Evgeny.Makarov]

By "equivalent logic" you may mean "logically equivalent", that is, the formulas logically imply each other. But an appeal to semantics defeats the purpose of proving that a formula is a theorem in a formal system. For this you need a derivation.

Next, system K (Hilbert system) is almost impossible to use for building proofs (though it is easy to prove things about it), at least until a significant number of metatheorems, like the deduction theorem, is proved. You may be stuck if your course or book uses it, but I would recommend some version of natural deduction, which is much more user friendly. The metatheorems I talked about make Hilbert system more like natural deduction anyway.

Also, axioms you gave don't use the existential quantifier. Doe this mean that $\exists x\,A$ is a contraction for $\neg\forall x\,\neg A$? If so, one idea is to prove the contrapositive
\[
\neg\neg\forall x\,\neg A(x)\to\neg A(a)
\]
and then use K3. If you can derive $\forall x\,\neg A(x)$ from $\neg\neg\forall x\,\neg A(x)$, then you can just use K5.