- Thread starter
- #1

#### Barioth

##### Member

- Jan 17, 2013

- 52

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.