3 ms·

As a human this explanation is emotionally satisfying. It appeals to my sense of human exceptionalism. However how many true but unprovable theorems do we know

As a human this explanation is emotionally satisfying. It appeals to my sense of human exceptionalism. However how many true but unprovable theorems do we know about? Has anyone ever bothered to compile a list of true but unprovable under the axioms xyz? I would think it is exceedingly hard to manage such research as every axiom set xyz would require companion axioms abc to be provable, and such theorems (at least the non-trivial interesting ones) are possibly hard to reach. This intuition for unprovableness may just be a mechanism for escaping local minima that gets lucky often enough.

wisnesky 6y ago
Many such lists exist. For example: https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC https://en.wikipedia.org/wiki/List_of_statements_independent...
- __MatrixMan__ 6y ago
  That's certainly true, but Godel-type unprovability is separate from logical independence, and indeed much harder to make lists of. My earlier point is not that we could know for sure that our struggles are due to being up against such a wall--just that our ability to suspect as much is relevant to how we allocate our time.
  - wisnesky 6y ago
    Oh, such as a list of statements unprovable under a specific Godel numbering? Definitely much more difficult - I never saw such a list in grad school, although I wouldn't rule out the existence of one.
  - p0llard 6y ago
    > Godel-type unprovability is separate from logical independence What do you mean by this? The Goedel sentence of a system is logically independent from the system by the standard meaning of "logical independence".
p0llard 6y ago
> true but unprovable under the axioms xyz? Careful: we don't really talk about things which are "true but unprovable" in first-order logics. By Goedel's completeness theorem, if a statement is true in all models of a first-order theory then it is provable. For any recursively axiomisable first-order theory of sufficient complexity, there exists some sentence which isn't provable [Goedel's First Incompleteness Theorem]: by contraposition of completeness, there exist models of the theory where the sentence is true, and models where the sentence is false. So when you say "true but unprovable", you're probably talking about truth in the so-called "intended model": if something is independent of the first-order system (e.g. ZF) you're using as a foundation of mathematics, then you get to decide whether it's true or not! Once you've proven independence via e.g. forcing, it's up to you to decide whether the sentence should hold in your intended model: then you can add the appropriate axiom to your system. Choice is independent from ZF: most mathematicians are OK with choice, so they chose to work in ZFC, but some aren't. Neither is "more valid" or "more true" from a purely logical perspective.

wisnesky 6y ago

Many such lists exist. For example: https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC https://en.wikipedia.org/wiki/List_of_statements_independent...

__MatrixMan__ 6y ago
That's certainly true, but Godel-type unprovability is separate from logical independence, and indeed much harder to make lists of. My earlier point is not that we could know for sure that our struggles are due to being up against such a wall--just that our ability to suspect as much is relevant to how we allocate our time.
- wisnesky 6y ago
  Oh, such as a list of statements unprovable under a specific Godel numbering? Definitely much more difficult - I never saw such a list in grad school, although I wouldn't rule out the existence of one.
- p0llard 6y ago
  > Godel-type unprovability is separate from logical independence What do you mean by this? The Goedel sentence of a system is logically independent from the system by the standard meaning of "logical independence".

p0llard 6y ago

> true but unprovable under the axioms xyz? Careful: we don't really talk about things which are "true but unprovable" in first-order logics. By Goedel's completeness theorem, if a statement is true in all models of a first-order theory then it is provable. For any recursively axiomisable first-order theory of sufficient complexity, there exists some sentence which isn't provable [Goedel's First Incompleteness Theorem]: by contraposition of completeness, there exist models of the theory where the sentence is true, and models where the sentence is false. So when you say "true but unprovable", you're probably talking about truth in the so-called "intended model": if something is independent of the first-order system (e.g. ZF) you're using as a foundation of mathematics, then you get to decide whether it's true or not! Once you've proven independence via e.g. forcing, it's up to you to decide whether the sentence should hold in your intended model: then you can add the appropriate axiom to your system. Choice is independent from ZF: most mathematicians are OK with choice, so they chose to work in ZFC, but some aren't. Neither is "more valid" or "more true" from a purely logical perspective.