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
    Commented 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$

You must log in to answer this question.

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