categories - Category Theory list
 help / color / mirror / Atom feed
* 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 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

* 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

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).