Re: João!

[Jeremy Weissmann]

A response from João:

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?)

   Why would a student think to eliminate the conjunct  odd.(d.a)  from the range of a quantification?  (Especially when to do so involves several steps of predicate calculus, facts about  'even' ,  '1' ,  and properties of summation?)

   Both of our proofs are explorations -- they both involve bottom-up reasoning, as well as top-down.  Of course, bottom-up reasoning is much more unrestricted than top-down reasoning; it is very much an  'art' ,  and we are often guided less by what seems simplest than by what seems sweetly reasonable.

   Because degrees are themselves summations, it is not a huge leap to start exploring summations of degrees.  For example, we might consider:

     deg.e  =  (+n : n in e : deg.n)     ,

which is I believe a useful concept, especially when we generalize to hypergraphs, where edges can connect any number of vertices.

   You ask,  "Why would a student consider the sum of degrees?" .   But why would they consider degrees in the first place?!  Your question is a good one, but it only reveals that there is never a true  "bottom"  to any theory.  Given a theorem from a theory, even a basic one, there is no knowing how much scaffolding needs to be in place to prove it (well).

   Apurva once asked how we could derive a proof of Andrew's Challenge  (see EWD1247, 1249, various writings of Gries and Backhouse, etc — it is a theorem of predicate calculus)  from first principles.  The problem here is that one needs to be pretty fluent in the predicate calculus to tackle this problem.  In fact, I'd venture to say that to approach this problem from a position of total ignorance would require you to reinvent the predicate calculus!

   So, some knowledge is necessary.  And sweetly reasonable bottom-up exploration (theory building) is necessary.  And it is not the case that every statement of every theorem provides enough contextual information for its own proof.

+j

[Jeremy Weissmann]

Here is my recreation of your design, as I understand it.

   Suppose someone has plopped on our desk the following demonstrandum:

(0)     even.(+v : ¬even.(deg.v) : 1)     .

What can do with it?  Since  even  distributes over  + ,  we can start with the following simple massage:

     even.(+v : ¬even.(deg.v) : 1)

==     {  even  over  +  }

     (==v : ¬even.(deg.v) : even.1)

==     {  ¬even.1  }

     (==v : ¬even.(deg.v) : false)     .

   Now we are stuck — there is no obvious way to proceed.  If we expand  deg.v  and distribute  even  over it, we could obtain the expression:

     (==v : ¬ (==e : v in e : false) : false)     .

I wonder if there is a way to manipulate this further, but unfortunately I am not familiar with rules for quantified  == .

   If we wish to proceed in a different way, we have to rewrite  false  in the last line of our calculation.  Naturally, there are many ways to rewrite  false  —  which should we choose?  I propose we use the most local contextual information, that is, the range of the quantification, and proceed as follows:

     (==v : ¬even.(deg.v) : false)

==     { rewriting the term in the context of the range }

     (==v : ¬even.(deg.v) : even.(deg.v))

==     {  even  over  ==  }

     even.(+v : ¬even.(deg.v) : deg.v)     .

Now that sums of degrees are in the picture, we can proceed as in my exposition.

* * *

   I hope I have really extracted the essence of your approach, João:  to let the calculational style aid in the suggestion of routes for exploration.  I am not sure if I find the rewriting of  false  in this way altogether compelling... but it is a way!

+j

[João Ferreira]

Hi Jeremy,

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

[Jeremy Weissmann]

I am really glad you've recreated the design, because it made me
realize that we are missing the trading rule!

   Oh shame on me!  (And us all, I suppose.)

   When I saw the expression:

 

     (==v : ¬even.(deg.v) : false)

my mind screamed  "Trading!" .   But I had no idea if this was true, and I was not in the mood to explore properties of the quantified equivalence.  Now you have given me a good way to remember this.

By the way, why do you use == in your calculation steps? Doesn't it
make == dependent on the context?

   I've been asked this question before... possibly by you, possibly by Eric Macaulay, possibly by Diethard Michaelis.

   My first answer is:  Who cares?

   My second answer is:  Proof is about communication.  Communication is always imprecise, and hence the art of communication lies in the choices we make.  You use  =  in calculations so that the symbol  ==  is exclusively used associatively.  The burden this places on the reader is that you make them look at different symbols, depending on whether they are inside or outside a calculation.

   I on the other hand practically never use  = , ≤ , < , et al  conjunctively in calculational mathematics, so this isn't a concern for me.  I also think that Wim Feijen's proof format is very distinctive, and I never worry that a reader is not sure whether to read what I write conjunctively or associatively.  I much prefer to have the symbols in my calculations communicate as much as possible without being a burden, and I like that one can look at the left-hand column of a calculation and know immediately that booleans (or reals, or whatever) are being manipulated.

   In short:  Context-independence is not the only concern.  (In fact, when was the last time you thought about it?)

   If you like, though, you can consider:

     == { }   ,   => { }   ,   etc

as conjunctive operators in their own right.

+j