I'm replying to this with a different subject, since we're not talking about arity anymore.
On Thu, Apr 2, 2015 at 2:28 PM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 18:31, Matt Oliveri <[email protected]> wrote: >> On Thu, Apr 2, 2015 at 12:44 PM, Keean Schupke <[email protected]> >> wrote: >>> When constructing mathematics from type-theory >>> you start with just types, there are no numbers, no booleans, >>> they all have to be made out of types. >> >> This is not an accurate statement about math in Martin-Lof type >> theory, since MLTT comes with natural numbers and booleans, all >> "magicked up" for you. Newer derivatives of MLTT have general >> inductive types magicked up for you. In either case, you don't build >> these objects out of types. How would that even work? > > The Twelf logical-framework is the neatest example of this, quoting the > Twelf manual: OK, now I'm closer to understanding what you're getting at. But note that Twelf's type system is LF, which is not an example of MLTT. Not all dependent type systems are MLTT. >> nat: type. >> z: nat. >> s: nat -> nat. >> The first line declares that nat is a type. The second line declares z >> (zero) to be an object of type nat, and the third line declars s (successor) >> to be a type constructor that takes an object N of type nat and produces >> another object (s N) of type nat. Note the use of the term "declare". This is an _axiomatization_ of the natural numbers, not a construction of them. Axiomatization is pretty much the only thing you do in LF, by design. It's predicative and has no base types, so there's nothing to construct things out of. The problem with axiomatizing everything is that axioms need to be trusted, since there's no mechanism to prevent the addition of inconsistent axioms. Twelf was not designed to be used for formalizing math. The axioms describe an object logic to study, and then the logic programming system is used to prove metatheorems about it. This approach is convenient, but not logically strong enough for math in general. >> plus: nat -> nat -> nat -> type. >> p-z: plus z N N. >> p-s: plus (s N1) N2 (s N3) >> <- plus N1 N2 N3. >> The first line defines the judgment, declaring plus to be a type family >> indexed by three terms of type nat. >> The second line declares that for any natural number N, p-z is an object >> of type plus z N N, which corresponds to the axiom p-z above. The N is an >> implicit parameter - it is treated as a bound variable by Twelf, which you >> can see by looking at Twelf's output after checking the above code. >> The third line says that p-s is a type constructor that, given an object D >> of type plus N1 N2 N3 (where N1, N2, and N3 are all implicit parameters that >> can be treated as metavariables), produces an object, p-s D, with type plus >> (s N1) N2 (s N3). This corresponds to the rule p-s > > Now I realise that is says z is an object, but there is no reason we have to > be operating at the bottom. z can just as easily be one level higher, and be > an empty universe at the U0 level, and 'nat' is now at the U1 level. Now we > don't need values at all, we can build everything from empty universes, like > everything is set theory is built from empty sets. It sounds like you're trying to turn type theory into set theory. Maybe you should be talking to Geoffrey. Many type theorists consider set theory's trick of encoding everything as a set to be a misfeature. The particular encoding of mathematical objects as sets is arbitrary, and allows for stupid questions, like "Is the zeta function an element of pi?". You'd like to consider that question nonsensical, but you can't because the zeta function and pi have been constructed from sets in one way or another, and so you're asking a perfectly valid question about those arbitrarily-chosen sets. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
