On Mon, Nov 26, 2012 at 3:21 PM, Martin Escardo <span dir="ltr">&lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>&gt;</span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br>
<br>
On 26/11/12 15:44, Peter Divianszky wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I would like to do classical math with<br></blockquote></div><div class="im"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<br>
A \/ B = ((A + B) -&gt; 0) -&gt; 0<br>
A =&gt; B = (A -&gt; 0) \/ B<br>
etc.<br>
<br>
or use R instead of 0.<br>
<br>
Suppose that I have a classical sequence which cannot be defined in<br>
(N-&gt;2). Then I can&#39;t use your theorem with that sequence.<br>
</blockquote>
<br></div>
Why not?<br>
<br>
(1) That it cannot be defined doesn&#39;t mean that it isn&#39;t there.<br>
<br>
(For example, the vast majority of the computable sequences N-&gt;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).<br>
</blockquote><div><br></div><div>For another example of this, consider classical formalisms like ZF.</div><div><br></div><div>Because of downward Loewenheim-Skolem, we could make a similar argument that N -&gt; 2 in ZF is merely the set of ZF-definable boolean sequences. Everything you can prove about N -&gt; 2 in ZF must hold true of the ZF-definable sequences; a countable set (externally, anyhow).</div>
<div><br></div><div>But no one seems to think that the properties provable in ZF about N -&gt; 2 are true _only_ of the ZF-definable sequences, and not of the set of &#39;all&#39; boolean sequences.</div><div><br></div><div>
-- Dan</div></div></div>