[Agda] Parametricity is inconsistent with classical logic

[Martin Escardo]

On 09/05/12 11:13, Martin Escardo wrote:
> On 09/05/12 10:59, Danko Ilik wrote:
>> On Wed, May 09, 2012 at 11:27:58AM +0200, Nils Anders Danielsson wrote:
>>>>> postulate choice : {k l : Level} → {X : Set k} → {F : X → Set l} →
>>>>> ((x : X) → ¬ ¬ F x) → ¬ ¬ ((x : X) → F x)
>>>
>>> This corresponds to Spector's Double Negation Shift principle.
>>
>> Not for arbitrary types X, right? See the following message:
>>
>> [...]
>
>> Martin Escardo's argument is that you will not be able to use
>> bar recursion to justify DNS for X≠ℕ, but it does not mean that
>> you could never possible justify it. It seems that with control
>> operators in logic you can do something
>> (ex. http://hal.inria.fr/hal-00647389)
>
> Sounds interesting. Will have a look.

Interesting indeed. Although I don't understand the technical
details (I lack enough background on delimited continuations), the
claims you make in the paper do seem plausible, and I trust you.

What puzzles me is that one can prove, from the DNS for the type
X=(N->2), the principle ¬¬LPO, where LPO is the claim that every
infinite binary sequence is either constantly zero or has a
one. LPO solves the Halting Problem, and ¬LPO is consistent with
type theory. So ¬¬LPO says that it is ridiculous to assume one
cannot solve the Halting Problem, but stops short of providing a
solution.

It seems strange that you can make a constructive system branch
into two constructive systems, one with the extension ¬LPO and the
other with its negation ¬¬LPO, but I suppose I have to accept
that. It is well known that ¬LPO is equivalent to a continuity
axiom: all functions are continuous in a certain sense. Hence
¬¬LPO says that not all functions are continuous (but doesn't give
a counter example, whereas LPO does, although LPO is a taboo).

On the other hand, your proofs in the above paper are for a system
which is not quite the same as type theory, as you said, and so it
would be interesting to know whether your ideas work for type
theory too, and in particular Agda, as you hint in the concluding
section. Anyway, I enjoyed reading your paper.

Cheers,
Martin