On 6/8/13, Marta Bunge <martabunge@hotmail.com> wrote:
The assertion "the theory of programming languages and the field of logic can be seen as essentially identical to category theory " is pure nonsense, even more so as it is given an outrageous name - "computational trinitarianism" even if spoken in jest.
The term "computational trinitarianism" http://ncatlab.org/nlab/show/computational+trinitarianism refers to the theorem relating category theory and type theory http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theor... The further relation between type theory to logic and programming languages is similarly well established. The term "computational trinitarianism" was invented by Bob Harper in an expositional blog post http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ designed to alert an unspecialized public about these nice and useful facts. I guess that's what the author of that article about Spivak's paper picked up. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Vaughan Pratt <pratt@cs.stanford.edu> suggested:
From Rehmeyer's article:
"It?s even proving valuable in developing rigorous models of music theory."
" 'If people adopt the level of rigor of category theory,' [Spivak] says, 'it will provide a precise language for science as a whole, and it will help individual scientists to clarify their thinking.' "
I don't know what "rigor" is, but if we identify it with consistency then there is a limit to the rigor of category theory: Goedel's second incompleteness theorem shows that category theory cannot be rigorous enough to establish its own rigor.
In my estimation, the "rigor" in Rehmeyer's adjective "rigorous" and the "rigor" in Spivak's quote have about as little to do with each other as either has to do with the one in the phrase "rigor mortis" :-) . Cheers, -- Fred [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
Fred E.J. Linton -
Urs Schreiber