2
$\begingroup$

For any ZFC statement we can build a Turing machine that enumerates all proofs in ZFC and halts if and when it finds a proof of the statement. Then we can find a system of Diophantine equations that has an integer solution iff the Turing machine halts.

Can this encoding be done in a more natural way? Like "AND" corresponds to direct product of varieties, "OR" corresponds to disjoint union and if there is a deduction between two statements there is also a map between the corresponding varieties (that takes a roughly similar number of bits to define)?

It probably should be impossible (because the variety corresponding to FLT would be mapping to an awful lot of varieties); I would be interested in a meaningful negative result in this direction.

Improve this question
$\endgroup$
1
  • 3
    $\begingroup$ I do not think this question is clearly stated enough to be answered positively, much less with an impossibility result as you suspect. $\endgroup$
    – LSpice
    Sep 22, 2021 at 16:59

1 Answer 1

Reset to default
3
$\begingroup$

Andrey Bovykin used to work on this kind of topic until ten (?) years ago:

formulate unprovable statements in terms of some kind of polynomial equations, possibly involving quantifiers.

Here you can find a researchgate page. I do not know if anything came out of this work.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.