Skip to main content
MathOverflow

Return to Question

added 200 characters in body
Source Link
coder
coder
  • 31
  • 2

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.

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

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.

Source Link
coder
coder
  • 31
  • 2

Translate ZFC statements into systems of Diophantine equations compatibly with geometry

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