Timeline for Is it decidable whether a statement about reals (in the language of ordered rings) is constructively provable?
Current License: CC BY-SA 4.0
25 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 13 at 12:28 | comment | added | Paul Taylor | I confess I don't follow the model-theoretic subtleties of this question, but since it seems to have reaches an impasse you might like to consider my similar question which arose from the practical question of computing (with) Dedekind cuts that @AndrejBauer and I were working on. If you know about semi-algebraic geometry you might be able to help with this. Please contact me privately by email. | |
| Apr 12 at 18:51 | comment | added | aws | I don’t really follow what’s going on in the paper I linked to before, but I think it has to somehow be using the fact that there are sentences not provable for their formulation of rcf that will hold for the reals. Something like $x < 1 \vee x > 0$ for all x. | |
| Apr 12 at 15:28 | comment | added | Christopher King | @AndrejBauer vouching for why this question is interesting: (1) what makes Tarski's result interesting isn't that some oddly specific set of axioms implies all the first-order properties of the reals, but the corollary that the first-order properties of the reals are computable (2) you can quickly check if something is a constructive taboo and (3) an algorithm like this would be a pretty cool feature in a constructive proof assistant | |
| Apr 12 at 15:15 | comment | added | Christopher King | @aws yeah that sounds right. I changed the question to say "language of ordered rings" since that's a little clearer. | |
| Apr 12 at 15:07 | history | edited | Christopher King | CC BY-SA 4.0 |
added 220 characters in body
|
| Apr 12 at 14:57 | comment | added | Andrej Bauer | @aws: Thanks! I find this formulation to be very strange, as it drags in higher-order logic etc., and it must somehow reduce to Tarski's result in the cases of boolean toposes, anyhow. | |
| Apr 12 at 14:53 | comment | added | aws | @AndrejBauer if I understand right, the precise question would be "which sentences in the language of ordered rings hold for the Dedekind real number object in every topos with n.n.o." | |
| Apr 12 at 14:50 | comment | added | Andrej Bauer | The standard axioms for a real-closed field are: the axioms of an ordered field, and for every $n$, the intermediate value theorem for polynomials of degree $n$. This is a first-order axiomatization. It is independent of any foundation or logic because it is a syntactic object. See for instance the introduction to doi.org/10.2307/2274424 | |
| Apr 12 at 14:30 | comment | added | Christopher King | @aws maybe there is a way to reduce it. To determine if $\phi$ follows from RCF^H, just check if "$\text{RCF^H} \implies \phi$" is constructively provable. The main question is just if it is finitely axiomatizable. | |
| Apr 12 at 14:22 | comment | added | Christopher King | @AndrejBauer If you want a set of axioms in the language of real closed fields, it would be any phi such that "Neutral constructive mathematics proves that the Dedekind reals satisfy phi" is an axiom. I do not know any other way to describe this set of axioms. Perhaps I should specify specifically which foundation of constructive mathematics? 🤔 | |
| Apr 12 at 14:15 | comment | added | Andrej Bauer | Well, I give up. | |
| Apr 12 at 13:35 | comment | added | Christopher King | @AndrejBauer "neutral constructive mathematics", so like HoTT without univalence or the free topos or something. I doubt which version of neutral constructive mathematics will make much difference. But in any case $<$ will be defined relation, not a primitive getting axiomatized. | |
| Apr 12 at 8:21 | comment | added | aws | According to the paper doi.org/10.2307/2271730 the intuitionistic theory of real closed fields is not decidable, although the proof doesn't apply to the set of sentences in the language that hold for $\mathbb{R}_d$, because it goes via adding a fairly strong version of division that doesn't hold constructively for the reals. | |
| Apr 12 at 5:35 | comment | added | Andrej Bauer | So, you say you'd like to decide whether a proof exists. In what theory? What are the axioms? Let me explain why I am being difficult. I am waiting for you to produce a set of axioms (hoping to see the theory of the real closed field), and then look carefully how you axiomatized $<$. It's going to matter, because you might put in the trichotomy law in its classical form. | |
| Apr 12 at 5:34 | comment | added | Andrej Bauer | Are we talking about Tarski's theorem that the theory of a real closed field is decidable? If so, that result is purely proof-theoretic. In the context of Tarski's result CAD is not about "truth" but about proving theorems in the theory of real-closed field. Mentioning ZFC just causes confusion, because it has nothing to do with Tarski's result. I speak formally and I am nit-picking but I am really trying to understand what the question is. Also,, as a logician I feel entitled to nitpick more than normal mathematicians. | |
| Apr 12 at 1:27 | comment | added | Christopher King | @AndrejBauer decide whether a proof exists, not whether the statement is true. ie is the set of provable statements computable. (Using CAD to compute truth is just one step of the algorithm in the classical case, because if CAD determines it is true, a proof exists in ZFC, but if CAD determines it is false, ZFC definitely does not prove it since ZFC is sound. This does not work for the set of constructive proofs because you can't convert CAD's results into constructive proofs, as shown in the WLPO case.) "Prove 'phi' for the Dedekind real numbers" = "Prove 'phi is true for the Dedekind reals'" | |
| Apr 11 at 23:39 | comment | added | Andrej Bauer | Are we talking about decidability of a theory, or about the decidability of validity in a particular model? Whatever it is, you should not be saying things like "classically proven for real numbers" because "proven" makes sense with respect to a theory but "real numbers" is not a theory, it's a model (or a structure). And then a little later you say "use CAD to compute whether it is true or not". So which is it going to be, "prove" or "true"? Do you understand what confuses me? | |
| Apr 11 at 22:21 | comment | added | Christopher King | (In particular, I think the classical and constructive case coincide for the algebraic numbers.) | |
| Apr 11 at 21:51 | comment | added | Christopher King | @AndrejBauer "is the theory of intuitionistic real-closed field (whatever that is) decidable?" I mean, I'm pretty sure the answer is yes for, say, the algebraic numbers. The case of the Dedekind reals is more interesting. | |
| Apr 11 at 21:17 | comment | added | Andrej Bauer | The question seems oddly phrased to me. The classical result by Tarski is that the theory of real-closed field is decidable. There is no ZFC anywhere, nor any models, just a first-order classical theory. So wouldn't the intuitionistic question be: is the theory of intuitionistic real-closed field (whatever that is) decidable? Why are we dragging in Dedekind reals? | |
| Apr 11 at 19:12 | history | edited | Christopher King | CC BY-SA 4.0 |
edited body
|
| Apr 11 at 19:00 | history | edited | Christopher King | CC BY-SA 4.0 |
added 151 characters in body
|
| Apr 11 at 18:39 | comment | added | Christopher King | @JamesHanson I'm not sure. I think neutral constructive mathematics coincides with the free topos tho (in general, not just on the reals). | |
| Apr 11 at 18:10 | comment | added | James E Hanson | Do you know if there's a sheaf topos in which the theory of the Dedekind reals is the same as the 'neutral constructive theory' of the Dedekind reals? | |
| Apr 11 at 17:34 | history | asked | Christopher King | CC BY-SA 4.0 |