[Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...

[Sergei Meshveliani]

On Sat, 2014-10-25 at 17:51 +0100, Paolo Capriotti wrote:
> On Sat, Oct 25, 2014 at 4:18 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > And I have an impression that the statement
> >
> >     question : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) →
> >                (¬ isFinite P) ⊎ (¬ isFinite Q)
> >
> > has not a constructive proof.
> >
> > Has it?
> 
> You're right, it's unprovable.  In fact, from `question` above you can distill a
> function:
> 
>     h : (ℕ → 2) → 2
> 
> such that
> 
>     ∀ f : ℕ → 2, ¬ isFinite (f⁻¹ (h f))
> 
> Now, `h` cannot be continuous.  In fact, let `m` be the modulus of continuity of
> `h` at `λ _ → 0`, and let `f : ℕ → 2` be defined by:
> 
>     f n = 0 if n ≤ m
>     f n = 1 otherwise
> 
> then
> 
>     0 = h (λ _ → 0) = h f = 1.
> 
> Discontinuous functions are taboo, hence `question` cannot be proved.


Thanks to people for explanations.

I understand the Abhishek's idea about the Turing machine halt
resolution.

As to your explanation with the continuity matters, I fear of that I am
not aware of notions.
Is "2" a set of two elements?
What topology or metric on  ℕ → 2  and  2  is used in a notion of
continuity for a map in  (ℕ → 2) → 2  ?

What does it mean that  m  is a modulus of continuity for  h  at  
g : ℕ → 2   ?

If it is    \forall g ( |h(g') - h(g)| <= m * |g' - g| ),

then what does it mean  |g' - g| ?  
Also  g, g'  map only into a two-value domain ...

Regards,

------
Sergei