23
$\begingroup$

It is well known that some problems in functional analysis and in general topology are independent from ZFC: to name a few, Kaplansky's conjecture, the existence of outer automorphisms of the Calkin algebra, the existence of a Suslin line etc. This is not too surprising, since many results in this fields require a nontrivial amount of set theory to be proved. On the other hand, differential geometry seems to be "higher up" in mathematical complexity (i.e., further away from set theoretical questions) and so it seems reasonable to me that no "natural" statement in diff. geom. is independent from ZFC.

Is that the case? That is, are there some statements which are independent from ZFC (or are conjectured to be)?

Edit: many comments (and the only, at the moment, answer) focused on computably undecidable problems. While this does indeed answer the question as formulated (because at least one instance of the problem must be independent), it is not exactly what I had in mind in that it does not offer an explicit example of an independent statement, or at least I don't see how to get one. So a more precise reformulation of my question is (but I am also very interested in more examples of computably indecidable problems): is there an explicit (in some sense of the word) statement in differential geometry that is (or is conjectured to be) independent from ZFC?

Improve this question
$\endgroup$
15
  • 10
    $\begingroup$ Does "are these two 4-manifolds diffeomorphic" count as differential geometry? Andrei Markov Jr showed how to take two finite group presentations and build two 4-manifolds that are diffeomorphic iff the corresponding groups are isomorphic. It is possible to construct a finite presentation that presents the trivial group iff $\mathrm{Con}(\mathrm{ZFC})$ is true. By Gödel's second incompleteness theorem, it is therefore independent of ZFC if the two 4-manifolds are diffeomorphic. $\endgroup$
    – Robert Furber
    Commented Jan 25, 2023 at 12:34
  • 1
    $\begingroup$ @RobertFurber I'd say it counts, although it feels a bit like cheating the question (in that one is basically "embedding" some group theory in diff. geom.) $\endgroup$
    – Pelota
    Commented Jan 25, 2023 at 13:04
  • 1
    $\begingroup$ In a similar vein to Robert Furber's comment: Matt Foreman has does some work recently showing, for example, that there are diffeomorphisms of the torus such that the question of whether they one is isomorphic to its inverse (in the sense of dynamical systems) is undecidable in ZFC. He does this, roughly, by coding undecidable arithmetic statements into the problem of deciding whether such an isomorphism exists. $\endgroup$
    – Will Brian
    Commented Jan 25, 2023 at 13:10
  • 2
    $\begingroup$ @BenjaminSteinberg I thought someone might say that. ZFC has a recursively enumerable set of axioms, so we can make a Turing machine $T$ that enumerates all formal proofs starting from the ZFC axioms and halts if it reaches a proof of $0 = 1$. Then $\mathrm{Con}(\mathrm{ZFC})$ is equivalent to the halting problem for $T$. $\endgroup$
    – Robert Furber
    Commented Jan 25, 2023 at 13:15
  • 11
    $\begingroup$ @BenjaminSteinberg Every computably undecidable decision problem is saturated with logical undecidability, over any base theory, since otherwise we could solve the problem by searching for proofs. In this sense, any computably undecidable problem of differential geometry will provide an answer to the question, even if one uses much stronger theories than ZFC. $\endgroup$
    – Joel David Hamkins
    Commented Jan 25, 2023 at 13:20

2 Answers 2

Reset to default
19
$\begingroup$

[Using the comments for context on undecidability/independence of ZFC]

A computably undecidable problem is whether or not a homology sphere has a metric of positive scalar curvature [Page 79 of Computers, Rigidity, and Moduli].

Improve this answer
$\endgroup$
1
  • $\begingroup$ Great answer, thank you! I'll wait a few more days to see if somebody else has something to add before accepting. $\endgroup$
    – Pelota
    Commented Jan 26, 2023 at 16:10
4
$\begingroup$

An explicit construction from the undecidability problem is this. There is a computer program $C$ that can check whether a (completely formal) proof in ZFC is valid, i.e. whether each step is either an axiom or follows from previous steps by a set of logical rules. Proofs are simply finite length strings drawn from a finite alphabet, so there is a program $S$ that outputs every (valid or invalid) proof one by one, ordered by length and alphabetical order. Now use $C$ to filter out the invalid proofs. This gives you a program that outputs every valid proof. Program $H$ runs through every proof, and when it encounters a proof of $p \land \neg p$, it halts. All of these are very easy but tedious to write out, if you have some basic programming knowledge. Whether this program halts is obviously independent of ZFC.

There is a very constructive proof that constructs a finite presentation of a group, such that whether a particular element $w$ is equal to the identity is equivalent to some program halting. This is done by using a lot of generators to guard the boundaries of symbols, so that there is only one potential path of equational reasoning that the given element is the identity. This path mimics the execution of a program. This construction is explicit, and you can check all the construction details if you have enough time.

Finally, there are ways to construct a 4-manifold for any given finite presentation of a group, so that it is diffeomorphic to another 4-manifold if and only if adding the equation $w = 1$ gives an isomorphic group. This result is mentioned in the comments.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .