I am separating the reply into multiple emails. On Fri, Apr 3, 2015 at 8:02 AM, 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 "theory" you probably should be saying "theorem". The Curry-Howard correspondence is propositions as types, proofs as programs. You said a hypothesis is a type. That is not the right correspondence. I was correcting you: Propositions are types, hypotheses are variables. >> 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. Yes. And since you have hypothesized the natural numbers, you have not constructed them. >> > 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). That's wrong, unless I were to interpret it extremely loosely. Intuitionistic Type Theory is another name for Martin-Lof Type Theory, which already uses both sides of the Curry-Howard correspondence. So it Curry-Howard corresponds to itself, in a sense. Intuitionistic logic is not a specific system. Roughly, it refers to any logic that can express excluded middle (or an equivalent) but can't prove it. > 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. No, you ask if a _proposition_ is provable. If you've already hypothesized it, its "proof" is trivial. Keean, I can't tell for sure whether you have deep misunderstandings about logic, or you merely misuse most of the terminology. Have you actually ever used logic besides logic programming? >> 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'')? You're missing the point. MLTT was designed to have one base type for the booleans. And it does. The fact that in Tarski-style, you get multiple universe elements corresponding to it is a quirk of the formulation. There is nothing interesting about the fact that MLTT successfully granted itself a single base type for booleans. If you must know how the derivation works, just look up the rules of MLTT. > 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? I don't understand your question. You are just showing me a system I don't like because it comes with duplicate Bool types. > 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. You're talking nonsense. > 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''. You seem to be confusing the propositions True and False with the booleans true and false. You are right that they should not be the same, but the the universe of propositions (or truth values, if you prefer) is syntactically quite different from the type of booleans. So it's not just a matter of duplicating the definition of Bool. (Actually, in an impredicative classical logic, you might be able to make propositions and booleans the same.) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
