<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> </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 <hancock@spamcop.net><br> <b><span style="font-weight: bold;">To:</span></b> Darryl McAdams <psygnisfive@yahoo.com> <br><b><span style="font-weight: bold;">Cc:</span></b> "agda@lists.chalmers.se" <agda@lists.chalmers.se> <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>> 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<br><br><br></div> </div> </div> </div></body></html>