truth vs. provability for ordered fields

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.