On Fri, Apr 3, 2015 at 5:40 AM, Keean Schupke <[email protected]> wrote: > On 3 Apr 2015 09:41, "Matt Oliveri" <[email protected]> wrote: >> 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. > > A hypothesis is a type, a proof is a program.
A hypothesis is a variable, the proposition hypothesized is the type of the variable. Maybe that's what you meant. When you say nat : type in Twelf, you're not defining nat, you're hypothesizing it. The other way to see it is that all LF signatures have semantics as HOAS. In that case, you're defining a fancy type of syntax tree. In this case it happens to get you syntax isomorphic to the natural numbers. However this trick will not continue to work once you're dealing with mathematical objects that aren't just syntax. So for the purpose of developing math internally to an LF-defined logic, the signature should be viewed as the rules and axioms for the logic. > Starting with an LF that is sound in a Herbrand universe, you propose the > theory, and if you can find the proof it is proved. What is "an LF"? LF is a specific type system. If you can find the proof of what? > Your theory can > anything, you can make up whatever axioms you like, as it is your theory. > Whether it is provable or not is another matter. I'm not sure what you're trying to say here. One doesn't ask whether a theory is provable. If you're saying the theory that you define may not be consistent, that's basically what I said in the previous email. >> 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.) > > A LF is a logic, although often sub structural and intuitionistic. Again with "A LF"... The LF I'm talking about is not really a full-fledged logic, in that it doesn't have enough propositional connectives. So you can't really say whether it's intuitionistic or not. And as a matter of fact, LF is _not_ substructural. (There are modified versions that are, I think.) >> > 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. > > It constructed a theory about nats. If you view it as a logic program > (everything in Twelf is both a type signature and a logic program), you can > ask it to search for a nat. > > So executing that program constructs a nat, proving that such a thing > exists. You can go on to use the case analysis and induction to prove > addition over all nats etc. This is due to the HOAS semantics. Again, you cannot expect to go about all of math in this manner. >> > 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. > > I think this was a misunderstanding. I thought you were saying that bool > could both be a type and a kind. Actually there are two books. For > disambiguation let's append a ' for each level above a value. So we have > Bool' a type and Bool'' a kind. Bool' /= Bool''. They contain True/False and > True'/False' respectively. They are not the same but are related by lifting. > We can lift the definition one level, but that does not mean they are the > same. We can say: Bool'' = lift(Bool') So in Tarski-style presentations of MLTT, types are the things judged to be types, not the things judged to be elements of a universe. Bool' and Bool'' are elements of universes, not types. To coerce them to types, you use "El". And El(Bool') = El(Bool''). So in that sense, they are the same type. Since you want types whether you have universes or not, Tarski-style also simply has the type Bool, which = El(Bool') = El(Bool''). In Russel-style/PTS-style presentations of MLTT, types are literally the elements of universes. And there is only one type Bool, and it is an element of all universes. In neither case are there multiple types of bool. You are wrong about there being True/False and True'/False'. Just True and False, as elements of Bool. >> > 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. > > Sorry, I thought you were trying to argue that type theory is not an > alternative foundation for mathematics. Yet here you state MLTT is an > alternative to Set theory? This would seem to agree with my points. Don't lump all your points together. I disagree with most of what you've said. Here's what I think: - MLTT is a viable alternative to set theory. - HoTT is not. - LF is definitely not, nor is it trying to be. >> (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.) > > Human languages always cause this kind of confusion. Actually I don't want to blame English this time. "Foundation" has everyday meaning as the supporting base of a building. It's used metaphorically for supporting bases in other areas, including math, originally. Then the categorists came along and decided math didn't need a single foundation in that sense, and changed the meaning of the word. > Starting with universes, we can clearly define natural numbers and > arithmetic, using nothing but intuitionistic logic. As we can define all of > mathematics using set theory from the natural numbers (ie the correctness of > set theory us proved by mapping to natural numbers), and we can define these > from intuitionistic logic, we have a simple axiomatic system for all > mathematics. You are completely ignoring the issue of consistency. Yes, you can model sets as natural numbers, but using which theory of naturals? Not Peano arithmetic. And certainly not Twelf's logic programming engine. And I still suspect you're all confused about "defining" natural numbers. > I think this is what they mean by not replacing set theory. It's not. To be more specific, Vladimir Voevodsky wants to use ZFC to prove the consistency of HoTT using his Kan simplicial set model. None of the others have called for set theory specifically, but they are depending on it implicitly until they develop a model in some other system. While the models use category theory, and category theorists claim that proper developments in category theory do not depend on set theory, I don't think anyone has actually checked that all the necessary machinery can be developed in any other system. (Realistically, it probably can be, possibly with minor modifications.) More importantly, the intended way to use HoTT is *absolutely not* to just bootstrap up to set theory. If anything, it should be the other way around. > Set theory can be defined within the proof-relevant world of type theory, but > not the other way around (you cannot recover proof relevance from proof > irrelevance). Wrong again. Just interpret proof-relevant propositions as sets of proof objects. Piece of cake. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
