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: >> 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.
No, I'm saying you won't be able to reason about mathematical objects in general. You can express objects just fine, since that's vague and would include writing a signature for it. Without defining your own notion of proposition, you cannot prove most mathematical theorems in Twelf. >> 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). The logical framework is a logic in a technical sense, but it's not designed for proving things. In that sense it's not a logic. It's designed for defining logics. LF is the metalanguage for a logic of your choice. > For example given the definition of > addition above and natural numbers you can prove its a group for example. That's not much of a theorem. It's just pointing out certain structure on the natural numbers. But yes, that's a good example of something mathematical that LF actually can prove. >> 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? No, that's accurate, but you're arguing for my side, because Prolog can't prove very much about math either. I am using LF to refer to a specific type system implemented by Twelf. Perhaps you are just using it as an acronym for logical framework? (Any logical framework?) >> > 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 :-) Well, I'm worried you'll just misunderstand the task, but that would hopefully clarify the misunderstanding, at least. I'll put it in another email. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
