<div dir="ltr">Here is an alternate argument which shows that the halting problem can be reduced to `question`.<div>Given a TM (turing machine) and an input to it, construct P and Q as follows:</div><div>P n iff the TM halts within n steps</div><div>Q n iff the TM does not halt within n steps.</div><div><br></div><div>Note that P and Q can be defined by primitive (structural) recursion on n.</div><div><br></div><div>If `question` was inhabited, you could use it to get <span style="font-family:arial,sans-serif;font-size:16px">     (¬ isFinite P) ⊎ (¬ isFinite Q),</span></div><div><span style="font-family:arial,sans-serif;font-size:16px">Now note that </span><span style="font-family:arial,sans-serif;font-size:16px"> (¬ isFinite P)</span><span style="font-family:arial,sans-serif;font-size:16px">  implies the TM halts and </span><span style="font-family:arial,sans-serif;font-size:16px">(¬ isFinite Q)  implies the TM does not halt</span></div><div><span style="font-family:arial,sans-serif;font-size:16px">Qed.</span></div><div><span style="font-family:arial,sans-serif;font-size:16px"><br></span></div></div><div class="gmail_extra"><br clear="all"><div><div>-- Abhishek</div><a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a></div>
<br><div class="gmail_quote">On Sat, Oct 25, 2014 at 12:51 PM, Paolo Capriotti <span dir="ltr">&lt;<a href="mailto:paolo@capriotti.io" target="_blank">paolo@capriotti.io</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Sat, Oct 25, 2014 at 4:18 PM, Sergei Meshveliani &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt; wrote:<br>
&gt; And I have an impression that the statement<br>
&gt;<br>
&gt;     question : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) →<br>
&gt;                (¬ isFinite P) ⊎ (¬ isFinite Q)<br>
&gt;<br>
&gt; has not a constructive proof.<br>
&gt;<br>
&gt; Has it?<br>
<br>
</span>You&#39;re right, it&#39;s unprovable.  In fact, from `question` above you can distill a<br>
function:<br>
<br>
    h : (ℕ → 2) → 2<br>
<br>
such that<br>
<br>
    ∀ f : ℕ → 2, ¬ isFinite (f⁻¹ (h f))<br>
<br>
Now, `h` cannot be continuous.  In fact, let `m` be the modulus of continuity of<br>
`h` at `λ _ → 0`, and let `f : ℕ → 2` be defined by:<br>
<br>
    f n = 0 if n ≤ m<br>
    f n = 1 otherwise<br>
<br>
then<br>
<br>
    0 = h (λ _ → 0) = h f = 1.<br>
<br>
Discontinuous functions are taboo, hence `question` cannot be proved.<br>
<span class="HOEnZb"><font color="#888888"><br>
Paolo<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>