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