Let me just say this: your argument is definitely more disentangled,
but I am not sufficiently happy with your introduction of the sum of
all degrees. Although I am not happy with my calculation (the problem
is step 2, of course), I like the way in which the sum of all degrees
comes into play. (Put another way: Why would a student think about the
sum of all degrees just because the definition of degree is a sum?)
I am really glad you've recreated the design, because it made me
realize that we are missing the trading rule!
even.(+v : ¬even.(deg.v) : 1)
= { even over + }
(==v : ¬even.(deg.v) : even.1)
= { ¬even.1 }
(==v : ¬even.(deg.v) : false)
= { trading (see below for more details) }
(==v : : even.(deg.v))
= { even over +}
even.(+v : : deg.v) .
For a quantifier Q generalizing an operator * with identity 1, the
trading rule is:
(Qk : P /\ Q : T) = (Qk : P : if Q -> T ◻ ¬Q -> 1 fi) .
Hence, we have the following equality (because true is the unit of ==):
(==k : P /\ Q : T) = (==k : P : if Q -> T ◻ ¬Q -> true fi) .
That is,
(==k : P /\ Q : T) = (==k : P : Q => T) .
***
I should have had this discussion a long time ago, before the
submission of my thesis. :)
By the way, why do you use == in your calculation steps? Doesn't it
make == dependent on the context? (That is, if == occurs in the proof
format, we read it conjunctionally; if it appears anywhere else, we
read it associatively.)
All the best,
Joao
2011/6/24 Jeremy Weissmann <plusj...@gmail.com>:
--
João F. Ferreira
I am really glad you've recreated the design, because it made me
realize that we are missing the trading rule!
By the way, why do you use == in your calculation steps? Doesn't it
make == dependent on the context?