# Logic, proving theorem in formal system K

#### Barioth

##### Member
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

##### Well-known member
MHB Math Scholar
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.