<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><div><span>What I mean by thing is a thing in the model. Judgements, at least, aren't taken to be things in the model, but are, as far as I know, apart from it. They're merely ways of talking about things. So why not treat levels similarly? I'm partly inspired by Boolos's reworking of second order logic to be "merely" syntactic -- he replaced sets and set membership with a variable assignment relation (on top of the assignment function) in the model theory, so that "set" membership is just being related to a variable. There are no sets in Boolos's pseudo-MSO logic, but it looks a lot like there are because of a syntactic trick. So why not do something similar with levels?</span></div><div></div><div> </div><div>- darryl<br></div><div style="font-size: 10pt; "><div><div dir="ltr"><hr size="1"><font size="2"
face="Arial"><b>From:</b> Peter Hancock <hancock@spamcop.net><br><b>To:</b> Darryl McAdams <psygnisfive@yahoo.com> <br><b>Cc:</b> "agda@lists.chalmers.se" <agda@lists.chalmers.se> <br><b>Sent:</b> Monday, July 1, 2013 3:33 PM<br><b>Subject:</b> Re: [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")<br></font></div><div class="yiv8261775159y_msg_container"><br>On 01/07/2013 19:58, Darryl McAdams wrote:<br>> Do levels really have to be things at all?<br><br>Well, I'm not sure what a thing is, but I think I agree with you,<br>if things are elements of sets.<br><br>> If we think of levels as<br>> merely/purely syntactic elements of the type theory, then it seems<br>> like the relational judgment "type_n" that Martin mentions would<br>> sidestep the issue entirely.<br><br>Aren't natural numbers things? There's a set of them.
Natural<br>numbers aren't syntactical.<br><br>>Levels would no more exist in the model<br>> then ":" and "valid-context" do. - darryl<br><br>My favourite natural number (after zero) is 1. It is impervious to arguments<br>about strick finitism, or general vertigo about the transfinite.<br><br>Why don't we just have one universe of Sets, memebership of which we express<br>by a judgement, that is not a Set-inhabitation judgement, perhaps<br>"A is a Set"? Then among the sets, we can have universes like<br>Gothendieck's, and index them by whatever mathematical things we like?<br><br>Hank</div></div></div></div> </div></body></html>