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.
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
