Are you doing the Henkin proof? If so, isn't it true that the sentence
is a first order validity? I suppose you can prove this if you really need to - the natural deduction rules are strong enough to get it.
So my question is, why do you need to prove this? In the Henkin construction, at least, you usually just take these statements as axioms. At least, the book Language, Proof, and Logic does it that way. What book are you using?
EDIT: Forget what I said about biconditional; I was looking at the wrong thing.
Note: I don't have that book, so my remarks may need some adjustment to meet the exact particulars of that book.
I showed you how to start. Do you not see how to go on from there?
And just to be clear: You should understand that the deduction theorem is not a theorem IN the system you're working with but rather is a theorem ABOUT the system you're working it.
The deduction theorem (a META-theorem ABOUT the system we're working in) is:
For all formulas P and Q, if
P |- Q then |- (P -> Q).
(We can write "|- (P -> Q)" as "|- P -> Q".)
And the other direction:
If |- P -> Q then P |- Q
is basically modus ponens.
So we get:
P |- Q if and only if P |- P -> Q
And I showed you how to get started using it for your example.
I noticed that the actual exercise doesn't ask you also to show that "second half". (See the edited version of my previous post.)
But we can do it anyway.
You've ALMOST got the right idea. But we don't show a contradiction between Ax Fx and ~Ax Fx. We ALREADY KNOW that it is a contradiction; it doesn't do us any good. Rather, we find a contradiction between Ax Fx and Ex ~Fx.
But first, finish the rest of the "first half" I started.