* Theorem or Paradox @ 2017-01-08 12:39 Patrik Eklund 2017-01-08 16:46 ` Robert Seely ` (3 more replies) 0 siblings, 4 replies; 10+ messages in thread From: Patrik Eklund @ 2017-01-08 12:39 UTC (permalink / raw) To: Categories Since the Incompleteness Theorem uses the Liar Paradox, why is it called the Incompleteness Theorem and not the Incompleteness Paradox? A Theorem closes a development or debate, and calls for admiration (because the inventor did something supposedly good), whereas a Paradox opens up development and debate (since the detector has pointed at something being wrong), and delays the call for admiration of the disruptively innovative solution until it is really deserved. Best, Patrik -- Prof. Patrik Eklund Ume?? University Department of Computing Science SE-90187 Ume?? Sweden ------------------------- mobile +46 70 586 4414 website www8.cs.umu.se/~peklund [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-08 12:39 Theorem or Paradox Patrik Eklund @ 2017-01-08 16:46 ` Robert Seely 2017-01-08 18:18 ` John Baez ` (2 subsequent siblings) 3 siblings, 0 replies; 10+ messages in thread From: Robert Seely @ 2017-01-08 16:46 UTC (permalink / raw) To: Patrik Eklund; +Cc: Categories It would take a book-length response to adequately reply to your question - more about that later. But in short here's an answer: a theorem is the conclusion of a valid argument (i.e. a "proof") based on certain assumptions ("hypotheses" or "axioms"). And Godel's result is such a theorem. I won't attempt to define a paradox, but certainly it seems his theorem might also be regarded (and has been) as a paradox as well. But a better answer might be found in the book "Godel's Theorem: an incomplete guide to its use and abuse", by Torkel Franz\'en - I hugely recommend it, if you haven't already done so. -= rags =- PS: Godel's theorem isn't based on the liar paradox - that's Tarski's theorem - but rather on a closely related paradox about provability - which isn't really a paradox after all ... PPS - you don't really think theorems "close development or debate", now, do you?! Experience suggests otherwise I think. On Sun, 8 Jan 2017, Patrik Eklund wrote: > Since the Incompleteness Theorem uses the Liar Paradox, why is it called > the Incompleteness Theorem and not the Incompleteness Paradox? > > A Theorem closes a development or debate, and calls for admiration > (because the inventor did something supposedly good), whereas a Paradox > opens up development and debate (since the detector has pointed at > something being wrong), and delays the call for admiration of the > disruptively innovative solution until it is really deserved. > > Best, > > Patrik > > > > -- <rags@math.mcgill.ca> <www.math.mcgill.ca/rags> [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-08 12:39 Theorem or Paradox Patrik Eklund 2017-01-08 16:46 ` Robert Seely @ 2017-01-08 18:18 ` John Baez 2017-01-08 23:30 ` Vaughan Pratt 2017-01-09 1:09 ` Noson Yanofsky 3 siblings, 0 replies; 10+ messages in thread From: John Baez @ 2017-01-08 18:18 UTC (permalink / raw) To: categories Patrik Eklund wrote: > Since the Incompleteness Theorem uses the Liar Paradox, why is it called > the Incompleteness Theorem and not the Incompleteness Paradox? Because it's a theorem, not a paradox. Indeed it's one of the basic results that sets the stage for modern developments in classical logic and set theory. Best, jb [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-08 12:39 Theorem or Paradox Patrik Eklund 2017-01-08 16:46 ` Robert Seely 2017-01-08 18:18 ` John Baez @ 2017-01-08 23:30 ` Vaughan Pratt 2017-01-09 8:19 ` Patrik Eklund 2017-01-09 11:50 ` Graham White 2017-01-09 1:09 ` Noson Yanofsky 3 siblings, 2 replies; 10+ messages in thread From: Vaughan Pratt @ 2017-01-08 23:30 UTC (permalink / raw) To: Categories What's in a name? A theorem is only paradoxical when it proves the inconsistency of an otherwise plausible axiom system, for example one that assumes there is a set of all sets with a well-defined cardinality, or Hilbert's conviction that all formally definable problems are solvable, or the "self-evident fact" that a dense linear order has no room to interpolate another number, or that an open cover of the rationals must cover the whole real line (as Pure Maths honours students in 1965 Henry Irgang and I visited Max Kelly in his office after class to express our incredulity), etc. etc. Any of these could have been officially called the such-and-such paradox. Furthermore only some of them involve the Liar Paradox. (I taught a freshman seminar titled "Paradox: Bug or Feature?" many years ago loosely based on Mark Sainsbury's book "Paradoxes". A basic example of "Feature" is recursion, associated with the non-existence of a largest integer. True to form I digressed with topics like surreal numbers and other topics the class expressed interest in. The hardest paradox we encountered was the Surprise Exam paradox where the teacher says there will be an exam next week and it will be a surprise---to the pupils' surprise it was given on Tuesday, contrary to a reasonable-looking argument. None of us succeeded in analyzing it as satisfactorily as the other paradoxes we treated. Sol Feferman taught a similar seminar a couple of years later.) Vaughan Pratt On 01/08/17 4:39 AM, Patrik Eklund wrote: > Since the Incompleteness Theorem uses the Liar Paradox, why is it called > the Incompleteness Theorem and not the Incompleteness Paradox? [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-08 23:30 ` Vaughan Pratt @ 2017-01-09 8:19 ` Patrik Eklund 2017-01-09 11:50 ` Graham White 1 sibling, 0 replies; 10+ messages in thread From: Patrik Eklund @ 2017-01-09 8:19 UTC (permalink / raw) To: Categories Russell's Paradox was quickly accepted as nothing but a Paradox since the community at that quickly realized that there cannot be only 'set' as one type of things in which things can enjoy membership. The idea for a solution was simple. Let there be a 'class', define it to differ from 'set', and see what happens. Another reason why this development took place was that the Paradox was so obvious, and that it didn't hide any smartness in it. It simply revealed that things do go wrong unless something is changed. In logic, "P true" and "(P provable) true" is mostly allowed to be of the same type. That type is not recognized or spelled out, and because of that not spelling it out, no Paradox is recognized. It's a self-referentiality, and it is connected with recursion, so it is generally not seen as paradoxical, or paratoxical, or paradoctrinal. I believe very few would disagree with me up to this point. In logic, P as a name for a proposition is still just an operator in a signature, so P(x) is still just a term. Once we put quantifiers in front of it, like Ex.P(x), it becomes something else. After that we have sentences, or statements, or predicates. Once we have terms and sentences, some have difficulties to treat P(x). Has it now changed to a predicate? We should note that the existence symbol is still just an informal symbol. Church called lambda an informal symbol. A similar identification happens in lambda-calculus. We identify terms with lambda-terms, and therefore we have some cleaning to do. I don't think we will formally prove the Kleene-Church-Post-Turing thesis before that apparently small issue has been properly recognized and solved. And the Post-Turing machine notation hides all these things anyway. --- To: John > ... sets the stage for modern developments Who or what sets that stage? G??del's result, after all, was no more than a few lines in the play as a whole. Still some time after his Princeton lectures, he wasn't convinced that his own definition of recursiveness was sufficiently general. I may see it so that the screenplay indeed is derived from results and papers, and then all the world's a stage. --- To: Saleh > I suggest Smullyan's treatment as opposed to the original paper. I am sorry but I generally do not like such suggestions. Originals are best, and must come first. I would certainly not like others to explain my papers. They may refer to them, critizice them, build upon them, tear them apart, or something similar, even rewrite them, but I would be offended if they re-explain them so that my original papers are supposed to become obsolete. The same, I would say, goes for papers that are one hundred years old. Having said that, Smullyan is fine. Nothing wrong with Smullyan. The risk in only reading papers (or books for that matter) about papers, is that detail in original papers may have been omitted for some reason, simply overlooked or even ignored. Even Smullyan didn't include everything from his papers into his book on diagonalization and self-reference. If he played just one prelude of Bach, you wouldn't necessarily know how good he might have been on fugues. And anyone playing a fugue by Bach on any instrument will certainly aim at not at all departing from the true original score, right? Otherwise it's just noise. --- To: Robert > PPS - you don't really think theorems "close development or debate", > now, do you?! Experience suggests otherwise I think Yes, book length it is, and actually several ones. My point is very simple. Of course, it's not just black and white about Theorem or Paradox, but it all boils down to recursion and typing, doesn't it? The history of recursion and typing is well-known. Recursion grew up more steadily even if by 1952 it still wasn't a closed deal. It still isn't. However, recursion as treated from 1928 by Ackermann (or earlier if you wish), through 1931, 1934, 1936, until we machine it and beyond that, could probably not have taken much different routes until 1952. But typing is different. If I recall correctly, in previous postings to this list I have mentioned Church's iota and o types from 1940. iota is basically what Martin-L??f called 'type', and then they did "type is type", and things go wrong for a while. HoTT is still off track, but they don't care. The o type is interesting I think. Nobody ever did anything about it. Types under iota are "normal" types, or sorts, so they type terms, and control substitution. The term functor is also extendable to a monad, so Kleisli is in there in a useful way. But sentences are different. Sentences are not terms, and sentence functors (whatever they are, by 2050, or beyond) cannot be extendable to monads, can they? Otherwise we only have terms, don't we? So that's where self-referentiality comes into play. Most of us think it's at least a bit peculiar to say that "P true" and "(|- P provable) true" are sibling statements. Cousins maybe, but not siblings, I think. G??del didn't care. Just throw every sentence in the same bag of sentences. Nobody is typing. Nobody is watching, right? That's my point. The argument may be valid in some sense, but it is untyped nevertheless. Or is it so that it was so fun to go up against Hilbert? What did he do wrong? After all, almost everybody were in G??ttingen. He was no longer in office by 1931. He was an old man. He was tired. G??del became the hero. G??del is also fine. Nothing wrong with G??del either. I'm sure he was a nice guy. But he did what he did maybe because that o type wasn't born, and wasn't watching him like a hawk. And when it was born, it was immediately orphaned. And came with no wings. What they didn't have back then was categories, and for sure, they didn't have monoidal closed ones. I've never seen recursive functors, by the way, and never seen recursion in monoidal closed categories. Don't know why, but my thoughts go a bit back to Thue and 1914. Isn't his grammar something about representing semigroups? Yes, there are books, but I fear that the authors of them didn't always check all detail in all papers. Boole is a good example. He didn't check anything. --- To: Vaughn Thank you, Vaughn. I like your paren-thesis. It's a bit of that stage, isn't it? From where you stand in the classroom, you see a couple of satchels, and faces all shining. No place for ballads, but some quick in quarrel. Some even opportunistic enough to seek the bubble reputation. On your side, true to form, expectedly full of wise saws and modern instances. This is how we play our parts, I think. We also see pantaloons become slippery, where world's a bit too wide, spectacles still on nose. "This is a Surprise" is really a good one. It's differently typed as compared to "This is a Falsity", I would say. But if you would ask me what those types are, I would say I don't know. But I sure would like to know. Is it maybe related to true/false, good/bad and right/wrong not having the same type. Suppose we would have "(|- P provable) right" instead of "(|- P provable) true", and, of course, "Screenplay good". Or "(Score) true" as different from "((Play Score) right) good". Thanks again! --- Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-08 23:30 ` Vaughan Pratt 2017-01-09 8:19 ` Patrik Eklund @ 2017-01-09 11:50 ` Graham White 2017-01-10 14:11 ` Paul B Levy 1 sibling, 1 reply; 10+ messages in thread From: Graham White @ 2017-01-09 11:50 UTC (permalink / raw) To: Vaughan Pratt, Categories One (rather trivial) reason why Goedel's Theorem isn't a paradox is because it's true, and there's a good argument for its truth, indeed one that can be formalised, but not in the system that the theorem is about. This differentiates it from paradoxes such as that of the liar, which can't consistently be assigned any truth value. However, there's something deeper here, which is that most paradoxes go against common sense, so that discovering them is a sort of self-limitation of reason (showing that something which seemed obvious is in fact false). And so was Goedel's theorem: nobody in the Hilbert school seems to have thought seriously that their program could fail, just that they hadn't quite got it right yet. And it says a great deal for Hilbert's personal qualities that he accepted Goedel's theorem when he saw it. (See Wilfried Sieg's wonderful book Hilbert's Programs and Beyond; a must read, in my opinion.) Graham On 08/01/17 23:30, Vaughan Pratt wrote: > What's in a name? > > A theorem is only paradoxical when it proves the inconsistency of an > otherwise plausible axiom system, for example one that assumes there is > a set of all sets with a well-defined cardinality, or Hilbert's > conviction that all formally definable problems are solvable, or the > "self-evident fact" that a dense linear order has no room to interpolate > another number, or that an open cover of the rationals must cover the > whole real line (as Pure Maths honours students in 1965 Henry Irgang and > I visited Max Kelly in his office after class to express our > incredulity), etc. etc. > > Any of these could have been officially called the such-and-such > paradox. Furthermore only some of them involve the Liar Paradox. > > (I taught a freshman seminar titled "Paradox: Bug or Feature?" many > years ago loosely based on Mark Sainsbury's book "Paradoxes". A basic > example of "Feature" is recursion, associated with the non-existence of > a largest integer. True to form I digressed with topics like surreal > numbers and other topics the class expressed interest in. The hardest > paradox we encountered was the Surprise Exam paradox where the teacher > says there will be an exam next week and it will be a surprise---to the > pupils' surprise it was given on Tuesday, contrary to a > reasonable-looking argument. None of us succeeded in analyzing it as > satisfactorily as the other paradoxes we treated. Sol Feferman taught a > similar seminar a couple of years later.) > > Vaughan Pratt > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-09 11:50 ` Graham White @ 2017-01-10 14:11 ` Paul B Levy 2017-01-13 7:22 ` Patrik Eklund 0 siblings, 1 reply; 10+ messages in thread From: Paul B Levy @ 2017-01-10 14:11 UTC (permalink / raw) To: Graham White, Categories On 09/01/17 11:50, Graham White wrote: > One (rather trivial) reason why Goedel's Theorem isn't a paradox is > because it's true, and there's a good argument for its truth, indeed one > that can be formalised, but not in the system that the theorem is about. > This differentiates it from paradoxes such as that of the liar, which > can't consistently be assigned any truth value. > > However, there's something deeper here, which is that most paradoxes go > against common sense, so that discovering them is a sort of > self-limitation of reason (showing that something which seemed obvious > is in fact false). And so was Goedel's theorem: nobody in the Hilbert > school seems to have thought seriously that their program could fail, > just that they hadn't quite got it right yet. And it says a great deal > for Hilbert's personal qualities that he accepted Goedel's theorem when > he saw it. What else could he have done, having read the proof? Paul > (See Wilfried Sieg's wonderful book Hilbert's Programs and > Beyond; a must read, in my opinion.) -- Paul Blain Levy School of Computer Science, University of Birmingham http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-10 14:11 ` Paul B Levy @ 2017-01-13 7:22 ` Patrik Eklund 2017-01-16 10:33 ` Steve Vickers 0 siblings, 1 reply; 10+ messages in thread From: Patrik Eklund @ 2017-01-13 7:22 UTC (permalink / raw) To: Categories; +Cc: P.B.Levy, graham.white > What else could he have done, having read the proof? > > Paul Dear Paul, Your question may turn out to be one of the most important questions in the history of mathematics, when looking back at it in 2103 (= 2017 + (2017 - 1931)). A sibling question, therefore, and for me a more important one, is "What else could we (= The Category Theory Community) do, having read the proof?". I have no interest to deeply analyze WHY G??del did what he did, even if I may be a bit curious about that as well. It relates to theatre and stage, or drama and logic. As far as I can tell, even Shakespeare did both. No, indeed not why, as I am more interested in how, and in showing that we need types, not just to distinguish terms, but also to distinguish sentences, and further to distinguish proofs from sentences, and so on. Category theory embraces tools to do that. We have already provided some first results in that direction. G??del didn't possess any of those tools. Neither did Kleene. Nor did any of the two contribute to creating those tools, I believe. I raised the seemingly harmless and philosophical question about theorem or paradox under this mailing list because I believe we [= The Category Theory Community) can settle this thesis by means of mathematics and category theory, and without philosophy, I would like to add, even if philosophers are welcome to learn more about mathematics and category theory in order to enrich their philosophical questions e.g. by the use of enriched categories. As you may have seen, I tend to believe that the thesis [G??del is wrong, so Hilbert's question remains open] is _right_, and indeed that "[G??del is wrong, so Hilbert's question remains open] is _right_" is well decidable. The thesis is still an open question, i.e., the thesis in the form presented here. I wouldn't interpret non-reply to the sibling question "What else could we do, having read the proof?" as a _good_ proof that "[G??del is wrong, so Hilbert's question remains open] is _wrong_". If it turns out that "[G??del is wrong, so Hilbert's question remains open] is _right_", also in the sense that there is a majority in a most important, well recognized and large mathematical community that agrees upon that, then I will be happy to refer to you, Paul, and to your question as having been the de facto starting point for the process leading to this dramatic and logical solution. On Friday the 13th, January, 2017, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Theorem or Paradox 2017-01-13 7:22 ` Patrik Eklund @ 2017-01-16 10:33 ` Steve Vickers 0 siblings, 0 replies; 10+ messages in thread From: Steve Vickers @ 2017-01-16 10:33 UTC (permalink / raw) To: Patrik Eklund; +Cc: Categories, joyal.andre Dear Patrik, There is a categorical account of Goedel's theorem, by Joyal, and dating back the 1980s (?). I first saw it presented by Gavin Wraith in 1985. The Goedel gap between truth and provability is presented as an issue of internalizability. The logic adequate for expressing arithmetic is obviously not ordinary finitary logic, which cannot characterize the natural numbers. Instead it is identified in categorical terms with "arithmetic universes". Categorically they have nnos and support free algebra constructions. But that is enough to show that an arithmetic universe has, internally, its own initial arithmetic universe. By nesting this construction, considering the initial arithmetic universe in the initial arithmetic universe, one can make the comparison between truth and provability and construct a Goedel sentence. At least, that's my understanding of it. As far as I know the work is still unpublished, and in the outline I have seen there are steps that I believe but don't know how to prove, even though I am actively working on arithmetic universes. I'm not the fastest of mathematicians. It's perhaps also worth noting that arithmetic universes support coherent logic, not full Boolean logic - no negation or implication. Anyway, what I'm saying is that if you want to see category theory evaluate Goedel, then you should probably start with Joyal's work. All the best, Steve. On 13 Jan 2017, at 07:22, Patrik Eklund <peklund@cs.umu.se> wrote: > > ... I believe we [= The Category > Theory Community) can settle this thesis by means of mathematics and > category theory, ... > > As you may have seen, I tend to believe that the thesis [G??del is wrong, > so Hilbert's question remains open] is _right_, ... > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
* RE: Theorem or Paradox 2017-01-08 12:39 Theorem or Paradox Patrik Eklund ` (2 preceding siblings ...) 2017-01-08 23:30 ` Vaughan Pratt @ 2017-01-09 1:09 ` Noson Yanofsky 3 siblings, 0 replies; 10+ messages in thread From: Noson Yanofsky @ 2017-01-09 1:09 UTC (permalink / raw) To: categories Hi, Nice question. A paradox is the final word about some assumption. Since it is the final word, we say it is a theorem. Here is what I what I wrote in "The Outer Limits of Reason: What Science, Mathematics, and Logic Cannot Tell Us": "In a way, the paradox is a test to see if an assumption is a legitimate addition to reason. If one can use valid reason and the assumption to derive a falsehood, then the assumption is wrong. The paradox shows that we have stepped beyond the boundaries of reason. A paradox in this sense is a pointer to an incorrect view. It points to the fact that the assumption is wrong. Since the assumption is wrong, it cannot be added to reason. This is a limitation of reason." For more, on paradoxes, please see Resolving Paradoxes (Philosophy Now 2015) http://www.sci.brooklyn.cuny.edu/~noson/PARADOXES.pdf and Paradoxes, Contradictions, and the Limits of Science (American Scientist 2016) http://www.sci.brooklyn.cuny.edu/~noson/2016-05Yanofsky.pdf All the best, Noson -----Original Message----- From: Patrik Eklund [mailto:peklund@cs.umu.se] Sent: Sunday, January 8, 2017 7:40 AM To: Categories Subject: categories: Theorem or Paradox Since the Incompleteness Theorem uses the Liar Paradox, why is it called the Incompleteness Theorem and not the Incompleteness Paradox? A Theorem closes a development or debate, and calls for admiration (because the inventor did something supposedly good), whereas a Paradox opens up development and debate (since the detector has pointed at something being wrong), and delays the call for admiration of the disruptively innovative solution until it is really deserved. Best, Patrik -- Prof. Patrik Eklund Ume?? University Department of Computing Science SE-90187 Ume?? Sweden ------------------------- mobile +46 70 586 4414 website www8.cs.umu.se/~peklund [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2017-01-16 10:33 UTC | newest] Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-01-08 12:39 Theorem or Paradox Patrik Eklund 2017-01-08 16:46 ` Robert Seely 2017-01-08 18:18 ` John Baez 2017-01-08 23:30 ` Vaughan Pratt 2017-01-09 8:19 ` Patrik Eklund 2017-01-09 11:50 ` Graham White 2017-01-10 14:11 ` Paul B Levy 2017-01-13 7:22 ` Patrik Eklund 2017-01-16 10:33 ` Steve Vickers 2017-01-09 1:09 ` Noson Yanofsky
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).