Here is a derivation in paraconsistent logic of the above. It uses the consequentia mirabilis (*) first and then minimal implication and quantifier rules:
------------ (Id) p(a) |- p(a) --------------------- (Right Ex) ------ (Id) p(a) |- exists x p(x) f |- f --------------------------------------- (Left ->) ------------ (Id) ~exists x p(x), p(a) |- f p(b) |- p(b) ------------------------- (Right ->) ------------------------ (Right Ex) ~exists x p(x) |- ~p(a) p(b) |- exists x p(x) ----------------------------------------------------------- (Left ->) ~p(a) -> p(b), ~exists x p(x) |- exists x p(x) ---------------------------------------------- (Consequantia Mirabilis) ~p(a) -> p(b) |- exists x p(x)
The consequentia mirabilis acts as a kind of contraction rule in the above and allows contracting the two exists x p(x) into a single exists x p(x). Which invalidates the existential property.
What models are possible in paraconsistent logic, which are not possible in intuitionistic logic? How do models of intuitionistic logic with quantifiers look at all?
In the usual kripke semantics the existential quantifier does not change the current possible world. But the implication might do. Here is a counter model:
w1 = p(a) = 1, p(b) = 0 / w0 = p(a) = 0, p(b) = 0
The p(a)=1 in w1 makes the ~p(a) false, and therefore the ~p(a)->p(b) true. But exists x p(x) is nevertheless false on w0. The above counter model is very similar to the counter model of the consequentia mirabilis ~A -> A |- A:
w1 = A = 1 / w0 = A = 0
The A=1 in w1 makes ~A false, therefore the ~A -> A true. But A is nevertheless false on w0. A further obvious reason that the existential property fails, is the case when there is an existential formula in the premisses. But this is not in the scope of the Herbrand theorem.
But intuitionistic logic is not completely free of contraction, and can produce a form consequentia mirabilis in itself. Namely the double negation leads to a form of consequentia mirabilis:
------ (Id) G, ~A |- A f |- f ------------------ (Left ->) G, ~A |- f ---------- (Right ->) G |- ~~A
The reason is that in the (Left ->) rule the implication formula might still occur both in the left branch and in the result sequent. It need not be erased from the left branch. So there are many intuitionistic formula that fail the existential property, but I guess they need not to be proper double negation translations of classical formulas, especially in the presence of quantifiers.
P.S.: But on the other hand the above might be viewed as an alternative explanation why the double negation translation works. It introduces the consequentia mirabilis in intuitionstic logic.
(*) http://en.wikipedia.org/wiki/Consequentia_mirabilis