<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"><<a href="mailto:paolo@capriotti.io" target="_blank">paolo@capriotti.io</a>></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 <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br>
> And I have an impression that the statement<br>
><br>
> question : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) →<br>
> (¬ isFinite P) ⊎ (¬ isFinite Q)<br>
><br>
> has not a constructive proof.<br>
><br>
> Has it?<br>
<br>
</span>You're right, it'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>