[plt-scheme] mathematical logic (was the perfect teaching language)

On Jun 15, 2009, at 8:11 PM, I wrote:

>
> On Jun 15, 2009, at 2:40 PM, Arthur Nunes-Harwit wrote:
>> While Russell & Whitehead's theory to avoid the paradox involved a  
>> hierarchy, the set theories that were widely embraced (eg Zermelo- 
>> Fraenkel and von_Neumann-Bernays-Goedel) had little or no hierarchy.
>
> Russell & Whitehead's hierarchical approach failed; Goedel showed a  
> way around any such system if you've got enough arithmetic to  
> encode proofs about numbers as numbers.  I don't remember exactly  
> how vNBG or ZF get around this.


Arthur was kind enough to straighten me out on this.  I was foolishly  
conflating two different issues: Russell's paradox and Goedel  
incompleteness.  They sort-of intersect in the Principia Mathematica,  
which introduced a hierarchy of sets in order to avoid Russell's  
paradox, and which also hoped to build a complete and consistent  
proof system.

Russell's paradox demonstrates that if you have a "set of all sets",  
and you also have a reasonable comprehension axiom, these lead to an  
actual semantic contradiction.  There is no model that simultaneously  
satisfies both of these, because it would make a particular statement  
both true and false in that model.  Russell & Whitehead introduced a  
hierarchy of sets that successfully avoided this problem.

Goedel's first incompleteness theorem has a different feeling: if you  
have enough power to encode and decode sequences that you can  
interpret as proofs in a formal system, you can have perfectly good  
models (among which, we'd like to think, is ordinary arithmetic), but  
there's a statement which is both true (in all models) and UNPROVABLE  
in this system.

Russell & Whitehead were well aware of the "liar's paradox", in which  
a statement says "this statement is false."  Any language in which  
such a statement is even expressible has problems.  The related but  
different statement "this statement cannot be proven in such-and-such  
formal system" is less toxic: it doesn't make things unsatisfiable,  
but only demonstrates that formal system to be incomplete.  I don't  
think Russell & Whitehead even worried about the latter, since (they  
thought) a statement can't talk about its own provability.  This last  
assumption is where Goedel proved them wrong.

BTW, there's a fascinating "graphic novel" (i.e. "comic book for  
grown-ups") entitled _Logicomix_, just released or about to be  
released, about mathematical logic in the early 20th century.   
Bertrand Russell is the main protagonist; Cantor, Frege,  
Wittgenstein, Goedel, Whitehead, Hilbert, etc. are other major  
supporting characters.

Stephen Bloch
sbloch at adelphi.edu