FOM: Re: Midwest Model Theory Meeting

[Charles Silver]

Vaughan Pratt wrote:

>>The inventor of Boolean logic also invented the finite difference calculus
>>("A Treatise on the Calculus of Finite Differences", first edition 1860,
>>second edition substantially reworked by John Moulton 1872), whose toolkit
>>provides induction-free methods for a much larger class of such problems,
>>including summing n^i for fixed integer i and much more.
>
>
>Charles Silver:
>>Can these methods be formalized?


Vaughan Pratt:
>Boole developed the finite difference calculus just as formally as the
>differential calculus on which he modeled it.  Furthermore the potential
>paradoxes in the latter do not arise with the former, so in that sense
>you could say the former was intrinsically more formal.


    Very nice.  Thanks for the helpful explanation.   When I first mentioned
how easy it was to solve the problem of finding the sum of 1 + 2 + ... + n
using Little Gauss's trick (if this is what Gauss really did, which I
doubt), I wasn't paying attention to the question posed by John Baldwin and
Harvey about formalizing such reasoning.  I'm not sure that having a
"calculus" in your sense or an "algorithm" in Andrej Bauer's sense fills the
bill.  Tell me if I'm wrong.   What is being asked for, I think, is
something like formal number theory, with axioms and such.  That is, the
language needs to be specified, and the axioms and rules need to specified.
For example, what would be the language for your calculus?  And what would
the rules be?  My *guess* is that the problem could be solved by the
Gaussian method in a kind of second-order system  of arithmetic without
induction (the original point was to eliminate induction).  But, this is
pure speculation on my part.  Someone much more technically advanced than I
would be in a better position to comment on this.

Charlie Silver