Okay, I'm going to try and close off some of these sub-conversations to keep things manageable.
On 3 April 2015 at 18:34, Matt Oliveri <[email protected]> wrote: > When you say "theory" you probably should be saying "theorem". > I'll try and use theorem as I suspect you are right. > Yes. And since you have hypothesized the natural numbers, you have not > constructed them. I hypothesise natural numbers, a normal prolog search proves at least one natural number exists, or I can just start with 'z'. I can the do case analysis and induction to prove all (infinite) natural numbers exist. Twelf will do this for you. > 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. > Well maybe I am using the wrong terminology. Intuitionistic logic is a Heyting algebra Intuitionistic Type Theory is the proof-relevant version of intuitionistic logic. Is that better? > 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? > Is the proof of the Rymann hypothesis trivial? I understand where you are going with this. A hypothesis is any set of axioms I want to propose, it needs to be proved complete and consistent. We can prove things true for one element (there exists at least one natural number, thats what a prolog search on the hypothesis does, or we might want to prove the existance of all natural numbers, which is a bit harder, but can be done with case-analysis and the assumption that transfinite induction is sound). > > 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. > I attempt to explain why its desirable below. > > > 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. > Okay, i'm going to move to the application domain here: Lets consider the value true or false comes from user input at runtime. At compile time we don't yet know what the value will be, and any dependence on such a value will lead to being unable to progress proofs further. As such the type system should consider all objects opaque, it cannot know anything about the actual values. Given this we need a way of representing true and false that are not values, but types. > > 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. > No this is something slightly different. There are type-level booleans, and then there are Heytings (A biary value that behaves according to Heyting algebra not Boolean algibra). Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
