On 3 April 2015 at 13:02, Keean Schupke <[email protected]> wrote: > > > On 3 April 2015 at 12:21, Matt Oliveri <[email protected]> wrote: >> >> A hypothesis is a variable, the proposition hypothesized is the type >> of the variable. Maybe that's what you meant. >> > > I'm not sure I understand what you are saying. A hypothesis is an unproved > theory. We hypothesise something as a type. if the type is inhabited it is > proved, and is therefore a theory. > > When you say >> nat : type >> in Twelf, you're not defining nat, you're hypothesizing it. >> > > Yes the other bit is the hypothesis where z and s are introduced. > > >> 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. >> > > Really? Proof by example. Please provide a mathematical object you cannot > express. > > 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. >> > > The logical framework is a logic, (the core semantics of Twelf map to > lambda-Prolog). > > > 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? >> > > The proof of your proposed theorem. Intuitionistic Type Theory = > Intuitionistic Logic (via curry-howard). You can therefore use the > associated logic-program to search for a proof. > > > 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. >> > > You ask if a hypothesis is provable. For example given the definition of > addition above and natural numbers you can prove its a group for example. > > >> 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.) >> > > An LF is a logic in the sense that Prolog is a logic language. Maybe I am > over-generalising to all logical-frameworks. Maybe I need a different word > for a logical-framework that is also a logic? > > onstructs 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. >> > > Please provide an example. I think you can derive the whole of maths :-) > > 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''). >> > > Does it? I dont see why El(Bool') would be El(Bool'')? Maybe I need to > define something else to get the behaviour I want? If I want to define: > > Bool' = True | False > Bool'' = True' | False' > Bool''' = True'' | False'' > > Where: Bool'' = lift(Bool') > > What do you suggest I call it? > > The property I am after is that you cannot have a type level Boolean > dependent on a value. So a Bool'' is not dependent on value-objects. > > So Bool is a type, and it has objects true/false. The point of talking > about a Bool is that we can prove things about all values. For example we > can say: > > Bool' type > ------------------- > (True | False) true > > The one thing we don't know when discussing a Bool type is whether its > value is True or False. > > However, now we want to talk about the truth or falsehood of statements > involving Bool'. This cannot be the same True/False, as we cannot look > inside a Bool 'to see what the value is, so we need a lift(Bool) to Bool'', > so we can write statements about Bool', which are True' or False' and > therefore have type Bool''. > > >> > 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. >> > > Yes, Peano arithmetic: > > > http://web.mat.bham.ac.uk/R.W.Kaye/publ/papers/finitesettheory/finitesettheory.pdf > > >> 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.) >> > > I don't think this is the right approach. > > 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. >> > > I think we disagree here. > > >> >> > 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 > > > Prof. Bob Harper would disagree here, unless he has changed his mind, and > can probably make the point better than I can. >
Also I would like to reference "Computational Trinitarianism": http://ncatlab.org/nlab/show/computational+trinitarianism Logic = Type Theory = Category Theory So if Category-theory does not depend on set-theory, and category theory = type-theory, then type-theory does not depend on set-theory. In general so far every proof in mathematics exists by proving a mapping to an already accepted theory. At the end of the chain we have natural numbers/arithmetic, which Godel proved consistent using inuitionistic logic and transfinite induction (Godel's T is a kind of intuitionistic logic). So indirecty, every proof maps to natural numbers, and we can define natural numbers in type-theory, and type theory is equivalent to intuitionistic logic. So you can reduce the whole of mathematics to natural numbers (which we cannot prove completeness/consistency of), or you can reduce the whole of mathematics to intuitionistic logic (which we cannot prove the consistency of in itself) + transfinite induction. So my choice is to start from intuitionistic type theory and transfinite-induction, and you can prove the consistency of peano arithmetic in such a system.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
