On Fri, Apr 3, 2015 at 1:46 PM, Keean Schupke <[email protected]> wrote: > On 3 April 2015 at 18:42, Matt Oliveri <[email protected]> wrote: >> On Fri, Apr 3, 2015 at 1:39 PM, Matt Oliveri <[email protected]> wrote: >> > 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: >> >>> 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. >> >> Define two predicates on natural numbers, even and odd: >> even : nat->type >> even_z : even z >> even_ss : even N->even (s (s N)) >> >> odd : nat->type >> odd_sz : odd (s z) >> odd_ss : odd N->odd (s (s N)) >> >> (I'm not sure those are valid Twelf, but you know what I mean.) >> >> Prove that any natural number that isn't even is odd. >> >> For starters how would you _express_ that proposition, seeing that LF >> doesn't have negation or falsehood? >> >> No, proving that every number is either even or odd is not good >> enough. The point is you're missing negation. > > Indeed, but we an add negation, using negation elimination: > > http://www.cs.cmu.edu/afs/cs/user/mobile/thesis/bella/thesis.ps.gz
OK. I'll give you the benefit of the doubt that with additions like this, a logic programming language can be made strong enough for formalizing math. (It still doesn't seem like a very convenient way to go to me.) But it seems we agree that regular Prolog or Twelf aren't strong/expressive enough, which was what I was arguing. One of the things I wasn't clear on before was whether you were talking about using Twelf as a logical framework. It seems the answer is "no". You were talking about Twelf as a logic programming language with inductive types, basically. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
