Reputation
7,135
Top tag
Next privilege 10,000 Rep.
Access moderator tools
Badges
1 25 49
Newest
 Yearling
Impact
~230k people reached

Apr
19
comment Difference between constructive Dedekind and Cauchy reals in computation
Moreover, the program of Proof Mining makes use of exactly the same framework, which is subsystems of higher-type classical and intuitionistic arithmetic, e.g. $\text{PA}^\omega$ and $\text{HA}^\omega$.
Apr
19
comment Difference between constructive Dedekind and Cauchy reals in computation
@Paul Taylor: the example is for decidable cuts, so the right side is just the complement of the left side, modulo possibly the rational value of the cut. But the example has open cuts. (You responded to that part of the comment). In any case, I do believe that people have seriously considered computing with Dedekind cuts in computable analysis and Reverse Mathematics, at least, and that cuts were abandoned exactly because they were not as convenient a framework as quickly converging Cauchy sequences. Whether cuts are more convenient in other areas is most likely a matter of opinion.
Apr
19
comment Difference between constructive Dedekind and Cauchy reals in computation
I am not sure if there is any evidence that can satisfy an opinion that computable analysis is not actually related to computational content, but at least I can point out that there are implementations of exact real arithmetic that are based on various representations from computable analysis.
Apr
19
comment Difference between constructive Dedekind and Cauchy reals in computation
It is very unclear. I also find it hard sometimes because the notion of "Dedekind cut" varies so much from place to place (e.g. in computable analysis we would treat the cut as decidable, while in some other places the cut is only assumed to be enumerated). So comparing results becomes challenging.
Apr
19
answered Difference between constructive Dedekind and Cauchy reals in computation
Apr
19
comment Difference between constructive Dedekind and Cauchy reals in computation
@Paul Taylor: there is no algorithm that, given any two left sides of Dedekind cuts, computes the left side Dedekind cut of their difference. The arithmetical operations on Dedekind cuts have several issues of this sort. This is why the formalization in Reverse Mathematics uses quickly converging Cauchy sequences, and why some other formulations use a kind of binary expansion with bits for $1$, $0$, and $-1$.
Apr
18
awarded  Yearling
Mar
17
comment Looking for a source for Intended Interpretation
"One can easily breeze through Kleene thinking that he is talking about the ZF semantic realisation of the syntax of the theory, rather than the familiar II. " That's a feature of the exposition - it seems maybe quixotic to look for something else. Most mathematical logic books are written in a way that is agnostic about whether the metatheory is formal or informal. They can be read both ways, depending on the taste of the reader. So one reader may view every result in e.g. Monk's logic book as a formal theorem of ZFC, while another may view the results as facts about a platonic universe.
Mar
17
answered A question on the provability predicate of Q
Mar
17
comment Looking for a source for Intended Interpretation
Of course, for the vast majority of mathematicians, the natural numbers are the ordinary/intuitive/informal counting numbers, and all those terms are synonymous. Only an author who wanted to make a distinction between two of them would worry about which word was used, and "natural number" is the most common one. So finding authors who go out of their way to emphasize the fact that two words mean the same thing may doom the search from the outset. The reason the "standard" model is "standard" is exactly that most mathematics is carried out in the standard model, rather than some other model.
Mar
17
awarded  set-theory
Mar
16
comment Looking for a source for Intended Interpretation
I have deleted several comments which I think are covered by the answer that I wrote.
Mar
16
comment Looking for a source for Intended Interpretation
A challenge for me is that Wang and Kleene both appear to be perfectly clear to me (I am also confused about a Wikipedia-like focus on finding a source that literally uses particular words). Kleene, in particular, identifies intended interpretations as using our informal or semiformal concepts as a model of a formal system, and views the standard model of arithmetic as such - so it seems that he clearly says that the intended interpretation of arithmetic uses our informal or semiformal notion of natural number to model system $N$. Don't the informal natural numbers form a set, informally?
Mar
16
revised Looking for a source for Intended Interpretation
added 29 characters in body
Mar
16
answered Looking for a source for Intended Interpretation
Mar
4
comment Theories of arithmetic from recursively inseparable sets
To clarify: are you asking whether, given a pair of recursively inseparable r.e. sets $X,Y$, there is a theory $T$ which is strong enough to satisfy the second incompleteness theorem, and so that $X$ consists of the provable statements of $T$ and $Y$ consists of the disprovable statements of $T$? I am not sure about the theories $T_X$ and $T_Y$ in the third paragraph.
Jan
28
comment Taller models of ZFC
@Asaf Karagila: I think you are thinking about the consistency of the statement (you are saying it is consistent relative to the existence of one inaccessible), but I was thinking about the provability of the statement. Is it consistent with ZFC that the collection of wordly cardinals is nonempty and bounded? In my earlier comment, I was trying to suggest that the axiom would follow from very mild large cardinal assumptions.
Jan
28
comment Taller models of ZFC
In (2), are you referring to transitive set models (so that the question is interpreted within a single class model of ZFC, so to speak) or are you asking about class models (so that the question is about the relationship between different class models of ZFC)? In the former case, doesn't (2) follow from the axiom that every set is contained in a transitive set model of ZFC, which in turn follows just from the existence of arbitrarily large inaccessible cardinals?
Jan
26
comment Is platonism regarding arithmetic consistent with the multiverse view in set theory?
I noticed this because I had originally hoped that the multiverse perspective would support position $P$, but I just don't see it after looking at the paper.
Jan
26
comment Is platonism regarding arithmetic consistent with the multiverse view in set theory?
@Nik Weaver: yes, I don't think the multiverse view is especially helpful for the position (which is very sympathetic) that $\omega$ has some real meaning but $2^\omega$ does not. Let's call that position $P$. The paper by Gitman and Hamkins has a list of multiverse axioms, including that the $\omega$ of any model is ill-founded in some other model. I don't see an obvious justification why one would accept all the other multiverse axioms of that paper, but not accept that particular multiverse axiom. It seems that position $P$ in the multiverse view would require such a justification.