“A hypothesis is a type, a proof is a program.” A program is a set of instructions to be given to a computer. It is a real thing.
A proof is a mathematical concept, it has nothing to do with reality, though it is sometimes useful when it coincides. A type is an abstraction meant to convey meaning to a program for a certain combinations of bits. A hypothesis is a completely random thought that may or may not have anything to do with reality. PKE PS: I’m thinking that someone here has landed far too far into abstraction Lalaland. After all, this is supposed to be a systems language, not Haskell. From: bitc-dev [mailto:[email protected]] On Behalf Of Keean Schupke Sent: Friday, April 03, 2015 2:41 AM To: Discussions about the BitC language Subject: Re: [bitc-dev] Not everything is a type On 3 Apr 2015 09:41, "Matt Oliveri" <[email protected]<mailto:[email protected]>> wrote: > > On Fri, Apr 3, 2015 at 3:11 AM, Keean Schupke > <[email protected]<mailto:[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. 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. 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. > 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. > > > 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. > > 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. 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') > > > 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. > > (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. 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. I think this is what they mean by not replacing set theory. 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). Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
