[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

On 26/11/2012 21:21, Martin Escardo wrote:
> On 26/11/12 15:44, Peter Divianszky wrote:
>> I have two concerns:
>>
>> A)
>>
>> I would like to use Agda with --safe.
>
> Coquand and Spivak have shown that MLTT remains strongly normalizing if
> you add recursion schemes such as the one used to give a proof term for
> the double-negation shift.
>
> That should be safe enough. If it isn't for you, then, well, you won't
> have classical choice (having it is equivalent to having the
> double-negation shift).

{-# OPTIONS --no-termination-check #-} is fine for me too if there is 
enough evidence that it is safe in the particular case.

>> I would like to do classical math with
>>
>> A \/ B = ((A + B) -> 0) -> 0
>> A => B = (A -> 0) \/ B
>> etc.
>>
>> or use R instead of 0.
>>
>> Suppose that I have a classical sequence which cannot be defined in
>> (N->2). Then I can't use your theorem with that sequence.
>
> Why not?
>
> (1) That it cannot be defined doesn't mean that it isn't there.
>
> (For example, the vast majority of the computable sequences N->2 is
> *not* definable in Agda or MLTT. What is more, what *is* definable
> depends on whether you have universes, how many of them you have, and
> whether or not you have W-types, etc. Moreover, for any extension of
> MLTT that remains strongly normalizing, there will necessarily remain
> plenty of non-definable computable sequences (by diagonalization).
>
> (2) You cannot define in Agda, or for that matter in any system for
> constructive mathematics, a boolean sequence a:N -> 2 such that a(n) ==
> 0 if and only the nth Turing machine halts when given input n, for example.
>
> But you can show that such a sequence not-not-exists, and more generally
> that it K-exists. I.e. that classically it exists.
>
> This kind of thing is precisely what is going on in the classical proof
> of the pigeonhole principle. That every boolean sequence has a constant
> subsequence cannot be proved. But you can show that such a sequence
> K-exists.
>
>
>> I wish that your theorem was stated more general such that it could be
>> used with both (N->2) and classical sequences.
>
> There is no such a thing as a classical sequence. There are just
> sequences. The existence of some sequences can be proved constructively.
> The existence of other sequences can be proved classically only. And, to
> repeat, not every computable sequence can be defined in Agda, and yet
> you don't complain that your theorem cannot be used for all computable
> sequences because you can't define all them.

I have a question.
In module InfinitePigeon you have defintions

------------------------------------------
Pigeonhole : {R : Ω} → ₂ℕ → Ω
Pigeonhole {R} α =
    ∃ \(b : ₂) → ∃ \(g : ℕ → ℕ) →
    ∀(i : ℕ) → g i < g(i + 1) ∧ K {R} (α(g i) ≡ b)


pigeonhole : {R : Ω} →
----------
     ∀(α : ₂ℕ) → K(Pigeonhole α)
pigeonhole R α = ...
------------------------------------------

Could we replace 'Pigeonhole' and 'pigeonhole' with these:

------------------------------------------
Pigeonhole : {R : Ω} → K {R} ₂ℕ → Ω
Pigeonhole {R} α = ...

pigeonhole : {R : Ω} →
----------
     ∀(α : K {R} ₂ℕ) → K(Pigeonhole α)
pigeonhole R α = ...
------------------------------------------


>> B)

I still have to think about your reply to B)


Thanks,
Peter