Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question

3 Answers 3

up vote 3 down vote accepted

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).

share|improve this answer
@jan : I put it in this form in order to make Herbrand's theorem applicable. Looking at its wikipedia article, Herbrand's theorem doesn't seem to say anything about proofs of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$ in classical logic. Showing that $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$ also has no proof in intuitionistic logic, you again need to use the cut-elimination thereom and show that there can be no cut-free proof. –  mercio Mar 14 '11 at 13:18

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.

share|improve this answer
A Kripke model with two nodes would suffice for showing the unprovability of your sequent. –  Kaveh Mar 14 '11 at 13:11
@Kaveh:I see how to do it with three nodes, but not with two. –  Carl Mummert Mar 14 '11 at 13:14
@Carl, here is what I had in mind: two nodes, top node has $p(a)$ and that's all. Then the lhs is forced in the model (because $\lnot p(a)$ is not forced anywhere) but rhs is not forced because there is no witness for it in the bottom node. (Philosophically, we don't know if $p(a)$ is true or not at the current state of knowledge, so we don't have any witness at the current state of knowledge for $p(\cdot)$.) –  Kaveh Mar 14 '11 at 13:17
@Kaveh: thanks for explaining. I was putting in another extension of the bottom node where $p(b)$ holds, but now I see even that isn't needed. –  Carl Mummert Mar 14 '11 at 14:17
@Jan, no, it does not hold for arbitrary theories in intuitionistic logic. It holds only for some theories like HA or the empty theory. –  Kaveh Mar 18 '11 at 13:36

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

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.