Proving that Diophantine sets are RE

Stream: new members

[Matt Diamond]

I was curious if it was possible to prove the following:

example {k : ℕ} (S : Set (Fin k → ℕ)) (h : Dioph S) : REPred fun n => n ∈ S := sorry

It seems like this should be simple (just iterate over all tuples until you happen to hit one that satisfies the polynomial), but docs#Dioph is defined using docs#Poly with no constraints on the index type. If the index type happened to be uncountable (or even just infinite), that would make things a bit difficult.

Should the definition of Dioph be modified or am I thinking about this incorrectly?

[Matt Diamond]

the other stumbling block is proving that Poly is primitive recursive since it involves integer math (though I'm hoping that's easier than it seems)