11
$\begingroup$

Glivenko's theorem says that $\lnot\lnot P$ is a theorem of intuitionistic logic whenever $P$ is a theorem of classical logic. Is it closely related to the so-called Gödel–Gentzen negative translation which embeds classical logic into intuitionistic logic.

Since $P\vee\lnot P$ is a well-known theorem of classical logic, I expect that by Glivenko's theorem, $\lnot\lnot(P\vee\lnot P)$ is provable in intuitionistic logic. But I cannot find a proof! I must be overlooking something obvious.

If $\lnot\lnot(P\vee\lnot P)$ is indeed provable in IL, I would like to see a natural deduction or sequent calculus proof of it, or especially a construction of a typed $\lambda$-calculus term with the type $((P\vee(P\to \bot))\to\bot)\to\bot$.

If it is not provable in IL, what have I misunderstood?

Addendum: I cross-checked the proposition with the usual model, letting $P$ be a subset of $\mathbb R$, and interpreting $\vee$ as set union and $\lnot x$ as the interior of the complement of $x$, and the proposition $\lnot\lnot(P\vee\lnot P)$ did seem to come out as all of $\mathbb R$ for any choice of $P$, so if I have made a mistake here too I would like to know what subset of $\mathbb R$ is the counterexample.

  • 0
    Thanks. This is essentially the construction Wadler gives (originally due to Selinger) in [Call-by-Value is Dual to Call-by-Name](http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf), in his story about the Devil offering a man either a billion dollars, or the chance to exchange a billion dollars for an unlimited wish.2014-02-21

6 Answers 6

17

Per the BHK interpetation, a proof of $(P \lor (P \to \bot)) \to \bot$ is pair of procedures, one for each disjunct in the hypothesis.

  • The first, $s_1$, is a procedure which takes a proof of $P$ as input and produces a proof of $\bot$. In other words, the first is a proof of $P \to \bot$.

  • The second, $s_2$, takes any proof of $P \to \bot$ as input and produces a proof of $\bot$. In other words, it is a proof of $(P \to \bot) \to \bot$.

By composing these to form $s_2(s_1)$, we obtain a procedure which takes no input and produces a proof of $\bot$.

The procedure just described (composition) takes any proof of $(P \lor (P \to \bot)) \to \bot$ and produces a proof of $\bot$. This means that $((P \lor (P \to \bot))\to \bot) \to \bot$ is provable.

This description shows how to write a $\lambda$ expression of the appropriate type. All that it does is to break the input into its two components and run the second one with the first as input. In particular, if we view $(P \lor \lnot P) \to \bot$ as a type $p(n,s)$ such that $\lambda s.p(1,s)$ is of type $P \to \bot$ and $\lambda\,s.p(2,s)$ is of type $\lnot P \to \bot$ then $\lambda\, p(n,s) . p(2,\lambda\, s.p(1,s))$ is of type $((P \lor \lnot P) \to \bot) \to \bot$

  • 1
    Thanks very much; this is exactly what I was looking for. I now understand several things better than I did before.2012-05-03
9

Here's a natural deduction proof:

  1. $\lnot (P \lor \lnot P)$ [Assumption]
  2. $\lnot P \land \lnot \lnot P$ [De Morgan]
  3. $\lnot P$ [$\land$ elimination]
  4. $\lnot \lnot P$ [$\land$ elimination]
  5. $\bot$ [$\bot$ introduction from 3., 4.]
  6. $\lnot \lnot (P \lor \lnot P)$ [$\lnot$ introduction]
  • 0
    Sure thing MJD, no problem.2015-10-14
6

Although I've already accepted Carl Mummert's answer, which was just what I wanted, I'm going to append the following variations for future reference.

First, a proof:

1: Assume $((a\vee(a\to\bot))\to\bot$
2a: Assume $a$
2b: $a\vee(a\to\bot)$ [2a, right $\vee$]
2c: $\bot$ [1, 2b, mp]
3: $a\to\bot$ [2a–2c]
4: $a\vee(a\to\bot)$ [3, left $\vee$]
5: $\bot$ [1, 4, mp]
6: $(((a\vee(a\to\bot))\to\bot)\to\bot$ [1–5]

And a program with the requisite type:

λf.   let g = λa. f (Left a)   let h = λn. f (Right n) in   h g 

a has type $a$,
n and g have type $a\to\bot$,
f has type $(((a\vee(a\to\bot))\to\bot)$, and
h has type $((a\to\bot)\to\bot)$.

Finally, the Haskell term

\f -> let            g = \a -> f (Left a)         h = \n -> f (Right n)         in h g 

is accepted by GHC and has type (Either a (a -> t) -> t) -> t.
We can β-reduce this term to

\f -> f (Right ( \a -> f (Left a) )) 

which has the same type.

3

Here is the intuitive argument: To prove $\lnot \lnot (P \lor \lnot P)$, assume $\lnot (P \lor \lnot P)$ and derive a contradiction. Now assume $P$. So $P \lor \lnot P$ by rule $\lor$-intro, a contradiction. Therefore $\lnot P$. Now $P \lor \lnot P$ by $\lor$-intro, again a contradiction. Therefore $\lnot \lnot (P \lor \lnot P)$.

The fascinating thing is that the analogue for predicate logic fails:

$ \lnot \lnot (\forall x)(A(x) \lor \lnot A(x)) $ is underivable in intuitionistic logic!

  • 2
    Yikes! Thanks for adding this, otherwise I would have been in the (probably common) pitfall of thinking that for any classical theorem $p$, we can always just prove $\lnot \lnot p$ in intuitionist logic. If I understand it right, we can indeed prove an "associated formula" in intuitionist logic ([the associated formula is defined recursively here](https://en.wikipedia.org/wiki/Double-negation_translation#First-order_logic)) but it won't always be $\lnot \lnot p$. In this example the associated formula would be $\forall x (\lnot \lnot Ax \lor \lnot \lnot \lnot Ax)$.2015-10-09
2

The prover online http://tassi.web.cs.unibo.it/logic/ should help you to understand the intuitionistic proof in sequent calculus (G3ip) for $\neg \neg (\neg P \lor P)$. In fact this formula is provable in minimal logic i.e. a subsystem of intuitionistic logic. Note that the proof below (produced by the prover for G3ip that I just mentioned) does not really uses the intuitionistic absurdity rule $L\bot$ in spite of the use of this label by the prover: it is clear that the axiom $P , \bot \Rightarrow \bot$ is the identity axiom and not the expression of the famous Ex Falso Quodlibet in sequent calculus. Here is the png image of the proof:

Proof in G3ip
(source: philfree.org)

Now the following proof in G4ip (i.e. Dyckhoff's LJT) is shorter:

Proof in G4ip
(source: philfree.org)

Here are now the proofs in natural deduction.

In Fitch style:

Proof in Fitch style
(source: philfree.org)

and in Gentzen style:

Proof in Gentzen style
(source: philfree.org)

We see on this example that the repetition of assumption (1) is unavoidable. (That is why it is not clear in my opinion why Gentzen style in natural deduction should always be preferred by proof theorists.)

Best wishes,

Jo.

-1

How about: Define g:((A+(A->0)->0)->0 by g(f) = finr(finl)

The type of functions A->0 is the negation of A and A+(A->0) is the type of A or not(A). The construction of g is the proof we want. inl:A -> A+(A->0) is the left inclusion. inr is the right inclusion. I hope it is clear now. The notation comes (to me) from the HoTT book.

  • 2
    I don't understand this. I does not appear to be at all related to the notation used in the Question.2015-08-18