Is there an intuitionistic proof of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$, what would Herbrand's Theorem say? I am currently studying Herbrand's Theorem and wonder in which form it would hold for intuitionistic logic. I guess in intuitionistic logic we will have only one witness.
To be practical I am experimenting with the following derivation, which is classically valid:
$$\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$$
But I don't find an intuitionistic derivation. Isn't there any? Could eventually an intuitionistic version of Herbrands theorem be used to establish that there isn't a derivation.
Best Regards  
 A: I assume $a$ and $b$ are constants of the language, and you want to prove
$$ \vdash \exists x (\lnot p(a) \rightarrow p(b)) \rightarrow p(x) $$
which is provable in classical logic by doing a contraction on the right, then instantiating $x$ and $x$ with $a$ and $b$.
If you have a cut-free intuitionistic proof of that statement, then it must start with giving a witness term $t$ for $x$, and then proving $\vdash (\lnot p(a) \rightarrow p(b)) \rightarrow p(t)$. But there is no term $t$ for which this is provable. It is not long to look for all possible cut-free proofs in this case.
The cut-elimination theorem here is really doing all the work for you because proofs that are cut-free are much easier to look for (especially since there is no contraction on the right in intuitionistic logic).
A: Herbrand's theorem also holds for intuitionistic first order logic, actually you can argue directly but simply saying if something is provable in intuitionistic logic, then it is also provable in classical logic.
In general you can not expect to have only one witness to get a stronger version of the Herbrand's theorem because classical logic is an extension of intuitionistic logic and therefore you can prove theorems in a classical theory and if you have a stronger version it would apply to the classical logic. On the other hand, for certain theories like $\mathbf{HA}$ it is possible to prove stronger versions like the existential property which essentially means that if you prove that a number satisfying a formula exists, then there is a natural number that witnesses it provably.
To prove that the formula you are discussing is not provable you can either use cut-elimination theorem or just come up with a model (e.g. Kripke model) which will make the statement false. It is not difficult to come up with such a model.
A: 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
