On Fri, Apr 3, 2015 at 3:11 AM, Keean Schupke <[email protected]> wrote: > > A LF can prove things about mathematics, and you have to build up all the > mathematical rules to formalise the proof.
When you use LF to "prove" things about math in that way, what you're actually doing is using the object language you've defined to prove things about math. If you add features and axioms freely to the object language as you go along, your proofs will not be very trustworthy, because new axioms can introduce inconsistency. Just as one shouldn't invent new programming language features freely without implementing them, one shouldn't invent new logic features freely without proving their consistency. A particular logic is sort of an agreement between the proof writer and the skeptical proof reader. Making up new rules for a proof is cheating. This is why it's fundamental to understand the difference between constructions/proofs and signatures/axioms. LF lets you write signatures/axioms. Once you've axiomatized a useful logic, you can get on to some constructions and proofs. But whatever logic you defined will have to be trusted by the proof reader. (Twelf also has the metatheorem system outside the object logic, as I explained before.) > If we can make natural numbers out of types, what do we need the natural > numbers for? It becomes a redundant definition. I guess I wasn't clear enough. What you showed from Twelf does not constitute "making natural numbers out of types". It's a signature for the intro forms of a nat type. (The signature also had derivations for addition as a ternary relation.) Nothing at all was constructed. To translate the code into English: 'Consider some type "nat", a nat "z", and a function symbol "s" that takes a nat to a nat.' That's it. You're just naming some things to be used in a particular way. They may or may not mean anything, as far as Twelf is concerned. It's very ironic that after declaring yourself a constructivist by misinterpreting the meaning of "constructivist" to be about constructing things in type theory, it begins to appear that you don't understand what a construction is. > Surely there is no difference between Nat1 (the type of nats) and Nat2 the > kind of type level nats, they can be the same definition, one is just lifted > a level. Agree. That's more or less what I was arguing about bool yesterday, after you claimed that having only one bool type would be impredicative. It seems you see things my way now. But you've completely changed the subject. Lifting types to higher universes is in MLTT, not LF. > Isn't this what HoTT is talking about with the univalent foundation of > mathematics, and being an alternative to set theory? What I have is a subset > of HoTT as I haven't got to the point of needing type identities, the J > operator, or paths yet. Isn't _what_ what HoTT is talking about with the univalent foundation of matematics? Not lifting the nat type, I hope? You changed the subject again. HoTT isn't the first alternative to set theory, you know. After all, MLTT came earlier. So why do you bring it up? It isn't even a promising alternative, if you ask me, though it's a nice supplement. (In fact when I started a thread on the HoTT list to argue just that, but more tactfully, it turned out that they do not see it as a complete replacement for set theory either! The confusion seems to come from the unconventional use of "foundation" in category theory circles. For them, "foundation" just means "system in which you can formalize a lot of math" basically.) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
