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

[Abhishek Anand]

Here is an alternate argument which shows that the halting problem can be
reduced to `question`.
Given a TM (turing machine) and an input to it, construct P and Q as
follows:
P n iff the TM halts within n steps
Q n iff the TM does not halt within n steps.

Note that P and Q can be defined by primitive (structural) recursion on n.

If `question` was inhabited, you could use it to get      (¬ isFinite P) ⊎
(¬ isFinite Q),
Now note that  (¬ isFinite P)  implies the TM halts and (¬ isFinite Q)
 implies the TM does not halt
Qed.


-- Abhishek
http://www.cs.cornell.edu/~aa755/

On Sat, Oct 25, 2014 at 12:51 PM, Paolo Capriotti <paolo at capriotti.io>
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.
>
> Paolo
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141025/2f877325/attachment.html