[FOM] First, second order theories, second order characterizations

[Joe Shipman]

I agree with these distinctions. What I am asking for isn't complicated:

1) I want a version of HOL which comes with a powerful deductive calculus that allows one to formulate and prove theorems in "ordinary mathematics". I don't care about distinguishing between "mathematical" and "logical" axioms, nor do I demand completeness or other proof-theoretical desiderata, I just want to do mathematics in it (the set of theorems that can be generated will of course be recursively enumerable, that is what I mean by "deductive calculus").

2) There are certain formulations of the above in which the "axioms" can be regarded as "logical" rather than "mathematical", which already suffice to establish most of "ordinary mathematics". I can create additional more powerful formulations by adding specifically mathematical axioms.

3) I am asking what is the most powerful deductive calculus for HOL which is used in practice, so I can evaluate it with respect to 1) and 2). A test case should be whether Con(Zermelo Set Theory) is a theorem, because I believe that the usual calculi do not allow one to get this far, although they can reach the theorems derivable in Type Theory. 

The best proposal I have seen so far is Peter Homeier's HOL-Omega logic. It appears to be less powerful than ZFC, but it can formalize category-theoretic and type-theoretic arguments. Can anyone give an estimate of its proof-theoretic strength?

-- JS

Sent from my iPhone

On Sep 7, 2013, at 9:27 PM, Harvey Friedman <hmflogic at gmail.com> wrote:

In http://www.cs.nyu.edu/pipermail/fom/2013-August/017552.html

I asked

1. Is CH an axiom of ZFC?
2. Is CH an "axiom" of second order ZFC"?
3. Is CH a theorem of ZFC?
4. Is CH an "axiom of second order ZFC"?
The main point of these questions is to flesh out apparent confusions I am seeing on the FOM concerning so called  "second order systems". 

On Thu, Sep 5, 2013 at 7:28 PM, Harry Deutsch <hdeutsch at ilstu.edu> wrote:
> Here's a stab at answering Harvey's question as asked.  No. Ch is not an axiom of ZFC.  No, it is not an axiom of ZFC second order, since this is not axiomatizable.  That's just part of the test, and I'm hardly an expert.  Harry
> On Sep 5, 2013, at 12:31 PM, Cole Leahy wrote:
This is of course a natural  response by those who do not view "2nd order ZFC" as having any axioms at all - in contrast to "first order ZFC". 

Now look at, for example, Hewitt:

"[Dedekind 1888] and [Peano 1889] thought they had achieved success because they had presented axioms for natural numbers and real numbers such that models of these axioms are unique up to isomorphism with a unique isomorphism.  And later generations of mathematicians were happy to use these axioms."

Here confusions between various notions of "axioms" and "axiom systems" and "characterizations" are apparent, and are best fleshed out by answering 1-4. 

Another way of getting to the bottom of these kinds of confusions is to ask for all full description of just what "use of these axioms" we are talking about. 

In such cases, it is only various associated first order *formal systems* that are in use for the mathematical reasoning, whereas various 2nd order "characterizations" are in in the underlying mathematics. 

This distinction becomes very clear as one deals with 1-4 above. 

Another good exercise is to discuss the relationships between 

1. First order arithmetic (PA).
2. Second order arithmetic (Z_2).
3. Second order theory of the natural numbers.

WHen reading several of the recent FOM postings, I get the impression that the authors have not paid sufficient attention to 1-4 and 1-3. 

A good test question is: is Con(ZFC) an axiom or a theorem of any of 1 - 3?

Harvey Friedman



_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130908/99b604f2/attachment-0001.html>