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/ ]