<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><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>&nbsp;</div><div>- darryl<br></div>  <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times
 new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <hr size="1">  <font size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Peter Hancock &lt;hancock@spamcop.net&gt;<br> <b><span style="font-weight: bold;">To:</span></b> Darryl McAdams &lt;psygnisfive@yahoo.com&gt; <br><b><span style="font-weight: bold;">Cc:</span></b> "agda@lists.chalmers.se" &lt;agda@lists.chalmers.se&gt; <br> <b><span style="font-weight: bold;">Sent:</span></b> Monday, July 1, 2013 3:33 PM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re: [Agda] How does level polymorphism fit into a valid type theory?
 (from "More universe polymorphism")<br> </font> </div> <div class="y_msg_container"><br>On 01/07/2013 19:58, Darryl McAdams wrote:<br>&gt; 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>&gt; If we think of levels as<br>&gt; merely/purely syntactic elements of the type theory, then it seems<br>&gt; like the relational judgment "type_n" that Martin mentions would<br>&gt; sidestep the issue entirely.<br><br>Aren't natural numbers things?&nbsp; There's a set of them.&nbsp; Natural<br>numbers aren't syntactical.<br><br>&gt;Levels would no more exist in the model<br>&gt; then ":" and "valid-context" do. - darryl<br><br>My favourite natural number (after zero) is 1.&nbsp; 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"?&nbsp; Then among the sets, we can have universes like<br>Gothendieck's, and index them by whatever mathematical things we like?<br><br>Hank<br><br><br></div> </div> </div>  </div></body></html>