On Mon, Nov 26, 2012 at 3:21 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></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) -> 0) -> 0<br>
A => B = (A -> 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->2). Then I can't use your theorem with that sequence.<br>
</blockquote>
<br></div>
Why not?<br>
<br>
(1) That it cannot be defined doesn't mean that it isn't there.<br>
<br>
(For example, the vast majority of the computable sequences N->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 -> 2 in ZF is merely the set of ZF-definable boolean sequences. Everything you can prove about N -> 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 -> 2 are true _only_ of the ZF-definable sequences, and not of the set of 'all' boolean sequences.</div><div><br></div><div>
-- Dan</div></div></div>