ZFC Axioms to be extended?

Question

Sorry if this is going to be a really loaded question.

I was told several times that for virtually all theorems/corollaries/propositions of mathematics (except those cases not compatible with ZFC or not expressed in FOL) we can turn it into a first order language, and obtain a formal proof of it from the logical axioms of first order logic (propositional logic tautologies, first order tautologies, axiom of equality) along with the axioms of ZFC, by using a proof calculi of our choice.
So for example, that means that if I have a theorem that states $A → C$ (and is compatible with ZFC), then its corresponding formula in first order logic is provable (from logical axioms + ZFC). At the same time, this would also make $C$ be deduced from $A$ (by deduction theorem).

On the semantical side, by soundness of first order logic, we would have that $A → C$ is true in every interpretation where all our initial axioms (logical ones and ZFC ones) are true, that is, for all models of our initial axioms. And along with that we could infer that $C$ is true in every interpretation where $A$ is true, that is, $C$ is a semantical consequence of $A$.

If i'm wrong in something until now, it would be good to know.

My question is about the role of the additional (or extended) axioms like Peano axioms ,Group axioms, etc in theorems of the kind $A → C$ that use concepts defined by them.
Do they really act like axioms, or more like definitions?

I know that its shown that in any model of ZFC, there exists exactly one set that satisfy the Peano axioms, and a bunch of sets that satisfy the group axioms.

For example, suppose a theorem $A → C$ involves a fact about a natural number (or a group). ie : some basic theorem in elementary number theory or the theorem that states that every cyclic group is abelian.
Would the theorem be saying something about the set(s) ( inside a model of the ZFC ) which was "defined" by the Peano or Group axioms ?

What would mean to be saying that $A → C$ is provable , in light of its reference to some specific sets of ZFC ( defined by the Peano or Group axioms ) ? Would it still be true that $A → C$ is provable from our initial axioms (logical ones) ?

Would we need to consider the validity of the Peano axioms (or group axioms, respectively) to say that $A → C$ is provable?
Would it still be provable from ZFC + logical axioms only?
Or would we have to augment ZFC + logical axioms with peano axioms (or group axioms)?
Or would it be provable directly from Peano (or group axioms), maybe with logical axioms, withouth reference to ZFC?

I hope i could deliver the essence of my doubt. Thanks in advance.

Answer 1

Okay, first off the bat, let me correct something here. In every model of $\sf ZFC$ there is only one model (up to isomorphism) of the second-order version of the Peano axioms. This is important, because the first-order theory is subjected to things like compactness and Lowenheim-Skolem which ensure that there are models of arbitrary cardinality.

But now that we have relaxed about this point, let's get back to the actual question at hand. What is the role of the additional axioms.

I want to answer a whole other question, which in turn is actually the more important question that you've asked (without asking). What is the role of $\sf ZFC$ in the additional axioms and mathematics?

We can develop first-order logic without $\sf ZFC$, perhaps we won't have the model theory and the semantics of logic, but we can talk about languages, terms, formulas, proofs and so on and so forth. We can even do all that in a fairly finitary theory like $\sf PRA$.

Why is that important? Because we want some sort of one "processor" for our mathematics, that will be able to tell us whether or not we are doing okay, and will allow some sort of compatibility between our theories (for example, we want our meta-theory to be able and translate statements about rings to statements about modules, even if those are completely different objects).

So without ever using any axiom of $\sf ZFC$ we can start with $\sf PRA$ and talk about the theory of groups, or abelian groups, and prove all sort of things that we would prove usually about groups. But this will be harder because we are used to taking an "actual" group and arguing the existence, or non-existence of certain objects which would satisfy certain properties. Sometimes we would take ultrapowers, or want to use advanced model theoretic arguments. And these require semantics which we might not have in $\sf PRA$.

The solution is simple. If we want a "processing unit" for mathematics, which can encode and decode internally "pretty much everything we want" -- which include interpretation of objects like the real numbers or very large objects, and if we want model theoretic tools, then we have a good incentive to use set theory instead of arithmetic. And $\sf ZFC$ makes a relatively natural theory to use (for myriad of reasons, for example it doesn't require us to keep track of the syntax of its own meta-theory like in $\sf NF$).

If so, the role of $\sf ZFC$ is to allow us to build mathematical objects. But building them requires logic, and since mathematical logic is also a mathematical object, we can begin by building a "copy" of first-order logic within $\sf ZFC$ and then use that to talk about proofs from $\sf PA$ or group theory, or whatever. And later on we can formalize $\sf ZFC$ within something like $\sf PRA$ and then have something like "$\sf ZFC$ proves that group theory proves that there is exactly one elements such that $\forall x(x\cdot e=x)$". But that's not important right now.

So, to your question. The working mathematician (read: not a set theorist) is not working within $\sf ZFC$. It is working within her own settings, whatever they might be: group theory, measure theory, low-dimensional topology, etc. Each of these have their own "usual" axioms and their own "commonplace logic" (sometimes it's first-order logic, sometimes it's another thing). And they all do what they want to do: prove things using the rules of that logic and the axioms of these theories. And the proofs are proofs from that theory, with that specific logic.

The role of $\sf ZFC$ is to take all that, and translate it back to a unifying mechanism which allows us to worry (from a foundational point of view) about just one theory, rather than many theories.

So when you prove a statement in number theory about the prime numbers, you don't prove it from $\sf ZFC$. You prove it in, say, second-order logic and the axioms of $\sf PA_2$ (second-order Peano). But somewhere in the back of your mind, if you care enough about these things at all, you know that all that is in fact a theorem that $\sf ZFC$ proves that in second-order arithmetic it is true that this and that theory is true.

Answer 2

Let's take the "every cyclic group is abelian" proposition as an example. It's easy to express abelianess in a first-order language of groups, that $gh=hg$ for all $g,h$ (in your group).

It's less easy to express that a group is cyclic. Set theory, or at least some inductive scheme, would be a natural way to express that every group element can be generated by some fixed element.

Thus much of what is considered elementary group theory needs more infrastructure than just logical axioms. To get a handle on "normal subgroups" or "exact sequences" takes us beyond the operations on group elements themselves to a discussion of sets and functions, etc.

Answer 3

We have two cases to consider.

(1) First-order theory of arithmetic, with first-order version of Peano Axioms.

In this theory, with f-o logical axioms and rules of inference [see e.g.Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)] you can prove usual "facts" about natural numbers, like :

$\lnot (1 = 0)$

or :

$\forall x \forall y [ x \ne 0 \rightarrow \exists q \exists r (y = xq+r \land r < x) ]$,

where $x \ne y$ is an abbreviation for : $\lnot x = y$ and $x < y$ is an abbreviation for : $\exists z (S(z) + x = y)$ .

These are theorems of first-order arithmetic, i.e.we can prove in f-o logic that e.g.:

$\Gamma \vdash \forall x \forall y [ x \ne 0 \rightarrow \exists q \exists r (y = xq+r \land r < x) ]$

where $\Gamma$ is the set of f-o arithmetical axioms (i.e. $\Gamma$ includes : $\forall x \lnot (S(x) = 0)$, and so on).

(2) In $\mathsf {ZFC}$ [see for example : Patrick Suppes, Axiomatic set theory (ed or 1960 - Dover reprint)] we have set axioms (like Axiom of extensionality, Axiom schema of separation, and so on).

In $\mathsf {ZFC}$ it is not necessary to "add" axioms for natural numbers, because the axioms of $\mathsf {ZFC}$ guarantee the existence of a structure with the familiar properties we expect the natural numbers to have.

We define what is a natural number (of course, it is a set : a specific one) and define "proxy" for natural numbers as :

$0 = \emptyset$,

$S(0) = \emptyset \cup \{ \emptyset \} = \{ \emptyset \} = 1$,

$S(1)= \{ \emptyset \} \cup \{ \{ \emptyset \} \} = \{ \emptyset, \{ \emptyset \} \} =2$,

and so on.

We can prove that these set satisfy Peano's axioms (see Suppes, page 135), like :

Theorem 17. $0$ is a natural number.

Theorem 19. There is no natural number $n$ such that $S(n) = 0$.