In Propositions equivalent to the completeness of the real numbers I started by asking "Can anyone point me to a reasonably comprehensive article (or book chapter) explaining which basic theorems of calculus are equivalent to the completeness axiom of the reals and which ones aren't?" and ended by speculating "Perhaps somebody wrote a beautiful Monthly article a few decades ago that explained things so clearly as to make the whole matter seem trivial, with the result that the article was forgotten? :-)"

Since the article I was looking for doesn't seem to exist, I decided to write one myself; the current draft can be found at http://jamespropp.org/reverse.pdf .

One issue I'm a little confused about is the relationship between truth and provability in this context. As I ask on the bottom of page 2 and the top of page 3, is saying "Every ordered ring $R$ satisfying property $P$ satisfies property $P'$" the same as saying "From the ordered field axioms plus the assumption that $P$ holds one can prove that $P'$ holds"?

I believe that they're not the same (because for instance the Riemann Hypothesis might be true but unprovable), but I'd like to hear from people who know more about foundations and model theory than I do.

All kinds of comments on the article are welcome, but comments on the truth-versus-provability issue are especially sought.

  • $\begingroup$ Well, on the one hand, this is true if $P, P'$ are both first-order by the completeness theorem. On the other hand, you seem to be dealing with properties that aren't first-order... $\endgroup$ – Qiaochu Yuan Jul 26 '11 at 19:46
  • $\begingroup$ No they are not. Consider rephrasing: every ring satisfies P implies P'. Then P implies P' is a true statement, but the chosen axiom system may lead to a logically incomplete theory, and the above statement may lie outside that theory. I think the general theory of rings may be undecidable, while certain extensions such as alg. Closed fields of a given characteristic are complete, and hence decidable. Gerhard "Ask Me About System Design" Paseman, 2011.07.26 $\endgroup$ – Gerhard Paseman Jul 26 '11 at 19:53
  • $\begingroup$ Apparent typo on page 2: "much of a muchness"? $\endgroup$ – user5810 Jul 26 '11 at 19:55
  • $\begingroup$ On page 7, a sequence of Laurent polynomials converges if and only if the principal (en.wikipedia.org/wiki/Principal_part#Laurent_series_definition) part stabilizes and for every non-negative integer $n$, the sequence of coefficients of $\epsilon^n$ stabilizes. $\endgroup$ – user5810 Jul 26 '11 at 20:06
  • $\begingroup$ On page 9, $f$ isn't even defined at $0_R$, so it can't be continuous on $R$. $\endgroup$ – user5810 Jul 26 '11 at 20:10

In your draft paper, you are using second-order logic with standard semantics over the (first-order) theory of ordered fields. What this means is that your structures are ordered fields (with the usual axioms) augmented with extra second-order structure: sets, functions, sequences, etc. You are using standard semantics because you are always considering all possible sets, functions, sequences, etc. For example, your continuous functions from an ordered field $R$ to itself are all possible functions from $R$ to $R$ that are continuous with respect to the order topology of $R$.

Unfortunately, there is no reasonable proof theory for second-order logic with standard semantics. More precisely, there is no deductive system which is simultaneously

  • sound — every statement which is provable is valid in all models;

  • complete — every statement which is valid in all models is provable; and

  • effective — the validity of a proof can be checked by an idealized computer (or an idealized human).

By contrast, first-order logic has all three of these properties.

There is an alternative view of second-order logic that does admit a reasonable proof theory. This alternative is to use Henkin semantics instead of standard semantics. With Henkin semantics, one is not required to always consider all possible second-order objects. Second-order objects are simply regarded as another sort of the language, which effectively makes this a first-order system (with multiple sorts). This is the usual approach used by logicians since Henkin semantics does have a sound, complete, and effective deductive system.

However, there are drawbacks to this approach. In order to ensure that sets do look and behave like sets, one must prescribe additional axioms for these: extensionality, comprehension, choice, etc. Similarly for functions. For sequences, one needs to add yet another sort for natural numbers and axioms for these as well. This adds an extra layer of complications since Henkin semantics allows such natural numbers to be nonstandard.

  • $\begingroup$ We can think of second-order logic with standard semantics as a two sorted first-order logic (one sort for objects, one sort for sets of objects) with a non-recursive set of axioms for the sort of sets. $\endgroup$ – Kaveh Jul 26 '11 at 20:51
  • 4
    $\begingroup$ @James Propp: François is correct, but in case you did not follow everything he said, the short answer is that your initial instinct is basically correct: There may be instances where two propositions are equivalent but you have no effective means of proving it. This is because you're interested in properties of the ordered field that may not be first-order. In my opinion, that's all you need to say, and it can be relegated to a footnote. Going into technical details about the difficulties of working with second-order logic will be an unenlightening digression in the context of your paper. $\endgroup$ – Timothy Chow Jul 27 '11 at 3:02
  • 1
    $\begingroup$ In many cases, the properties we want are first order, though, in second-order arithmetic. This is one of the morals of reverse mathematics. There are many results there that can be viewed as showing that certain results require certain fragments of completeness. For example, ACAo can be understood as limit-point completeness, while WKLo can be understood as compactness in the Heine-Borel sense, which turns out to be weaker. $\endgroup$ – Carl Mummert Jul 27 '11 at 11:54
  • 1
    $\begingroup$ On the other hand, if we worry about truth instead of provability, then of course there are equivalent statements that we can't prove equivalent in some particular system. All true statements are equivalent to each other, and all false statements are equivalent to each other, and these are the only equivalence classes with respect to truth. A key reason to look at provable equivalence is this triviality of equivalence of truth values. $\endgroup$ – Carl Mummert Jul 27 '11 at 11:57
  • 1
    $\begingroup$ I think natural numbers are definable in the theory of ordered fields using second order quantification, so I guess it is not necessary to add a sort for natural numbers: $$n \in \mathbb{N} := \forall X \ [(0 \in X \land \forall x \ x \in X \rightarrow x+1 \in X) \rightarrow n \in X]$$ $\endgroup$ – Kaveh Jul 27 '11 at 20:38

In general, the way that people approach these things is to look at provable equivalences over some fixed theory. So, for example, you could prove results of the following form:

Theory $T$ proves that any object satisfying the ordered field axioms will satisfy property $P$ if and only if it satisfies property $P'$.

The theory $T$ could be ZFC set theory, or it could be a weaker theory such as second-order arithmetic. The main point of the theory is to give some syntactical tools for manipulating the ordered field axioms and the statements of $P$ and $P'$. For example, if $P$ is the axiom of completeness (every nonempty bonded set has an supremum), the theory $T$ needs to guarantee some sets exist.

To establish positive results of the quoted form, you simply write a proof in $T$ of the desired result. The more difficult thing is to establish negative results, and this is the first time you have to think about semantics. To prove the negation of the quoted statement, it suffices to have:

  • A class of interpretations of $T$ such that a statement is provable in $T$ if and only if it is true in every one of these interpretations

  • And an example of one of these interpretations in which there is an ordered field satisfying $P$ but not $P'$, or vice versa.

It's clear on a moment's thought that the class of structures we want only really depends on the proof rules we have in $T$, not on our intended interpretation of $T$. In the case that the proof rules are the usual ones, we have a general theorem that the set of all "first-order stuctures" is a sufficient class of interpretations to achieve the first bullet. This works not only for first-order logic, but also higher-order logic and set theory, which have the same sort of proof system.

Finally, let me point out a trivial exercise that underscores the need to look at provability rather than truth. For any effective, consistent theory $T$ that is sufficiently strong, and any statement $\phi$ provable in $T$, there is a statement $\phi'$ that is equivalent to $\phi$ but so that $T$ does not prove $\phi \leftrightarrow \phi'$. Namely, $\phi'$ says "$\phi$ and $T$ is consistent". This sort of method shows that the question in the third paragraph of the question has a negative answer, and this would be true no matter what effective consistent proof system we choose.


To be meaningful the question needs to assume that $P$ and $P'$ is expressible in the language (otherwise proving it does not have meaning). In that case your question is equivalent to the following:

Is $$\forall M, \ M \vDash P + T_{or} \Rightarrow \ M \vDash P'$$ the same as $$P + T_{or} \vdash P'$$

Note that $$\forall M, \ M \vDash P + T_{or} \Rightarrow \ M \vDash P'$$ is equivalent to $$P + T_{or} \vDash P'$$ therefore the answer is yes, by the completeness of first order logic.

  • $\begingroup$ Well, but it seems to me that (as per the discussion in the comments) the properties the OP is interested in are not first-order. $\endgroup$ – Qiaochu Yuan Jul 26 '11 at 20:25
  • $\begingroup$ @Qiaochu, if we cannot express them in the language that proofs are being written proving them (in the logical/formal sense) is obviously impossible. $\endgroup$ – Kaveh Jul 26 '11 at 20:30
  • $\begingroup$ @Qiaochu, the same thing works for other logics if we choose the correct semantics for them. Unfortunately the terminology "first-order" has a frightful number of meanings. $\endgroup$ – Carl Mummert Jul 27 '11 at 12:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.