Axioms of set theory and logic

Question

Zermelo–Fraenkel set theory is the most common foundation of mathematics with eight axioms and axiom of choice (ZFC):

http://plato.stanford.edu/entries/set-theory/ZF.html

But one can see that the statement of ZFC depends on first-order logic symbols and definitions, for example $=, \in, \forall, \exists$, predicate, formula, etc... And in many books, they didn't concept clearly about axioms of first-order logic, even through use set theory definition.

My question is how set theory and first-order logic can combine in a unique system of axioms as the foundation of Mathematics.

For example,

1. There are objects called sets, denote by $X,Y,Z,..., A,B,C$

2. There are symbols $=, \in, \forall, \exists$

3. Symbols $=, \in$ can be put between two any sets $X,Y$ to be (primary) propositionals: $X\in Y$, $X=Y$.

4. There are two logic values: $T$ (true), $F$ (false).

5. Each propositional has a unique value, $T$ or $F$.

6. There are logic operators $\neg, \vee, \wedge, \rightarrow, \leftrightarrow$

7. Logic operators can combine propositionals to create new propositionals, their logic values follow the standard logic rules.

8. For a set $A$ and a propositional $P$, then $\forall A, P,\ \exists A, P$ are propositionals.

etc...

There must have a system of axioms for propositionals and sets (include ZFC) and how can we make them be minimal?

Answer 1

The usual approach is to define a concept of a first order language $\mathcal{L}$. They are usually specified by the nonlogical symbols. Well-formed formulas in the language $\mathfrak{L}$ are strings of symbols of $\mathfrak{L}$ along with the logical symbols such as $($, $)$, $\wedge$, $\neg$, variables etc. You can look up in a logic textbook the inductive definition of well-formed formulas, but something like $x \wedge y$ is a well-formed formula, but $(()\neg\wedge xy \neg$ is not a well-formed formula.

A first order theory $T$ in the language $\mathfrak{L}$ is then a collection of well-formed sentences (no free variable) in the language $\mathfrak{L}$. You would then define the deduce relation $T \vdash \varphi$ to mean that there exists a proof of $\varphi$ using $T$. A proof is just a string of of sentences $\phi_1, ..., \phi_n$ such that $\phi_n = \varphi$, each $\phi_i$ is in $T$, a logical axiom of first order logic, follows from modus ponen or generalization using previous $\phi_j$, where $j < i$.

So the above is the definition of a arbitrary first order theory in an arbitrary first order language $\mathfrak{L}$. Now let $\mathfrak{L} = \{\in\}$ a first order language consisting a single binary relation. $ZFC$ is then the first order theory in the language $\mathfrak{L}$ consisting of the "eight axioms" you mentioned above. (Note that ZFC has infinitely may axioms. For example, the axiom schema of specification is actually one axiom for each formula.)

The benefit of this approach where the general definition of first order logic is developed first is that you apply this to study first order logic in general and other first order theories such that the theory of groups, rings, vector space, random graphs, etc. Also first order logic is developed in the metatheory. That is for example, a theorem of ZFC (even if it is about infinite cardinals greater than $\aleph_1$) has a finite proof in the metatheory. However, within ZFC you can formalize first order logic. Then you can consider question about whether $ZFC$ can prove it own consistency.

By taking the approach of developing first order theories in general, you also gain a certain perspective. Some people think that ZFC is something special since it can serve as a foundation for much of mathematics. Through this approach, $ZFC$ is really just another first order theory in a very simple language consisting of a single non-logical symbol. People often have a hard time grasping the idea that $ZFC$ can have different models, for instance one where the continuum hypothesis holds and one where it does not. However, almost everyone would agree that that there exists more than one model of group theory (i.e. more than one group). Sometimes it is helpful to know that results about arbitrary first order theory still apply when one is working in ZFC set theory.

Answer 2

Note that before talking about theories and provability we need to first select a language to express formulas/statements. Here the language is the language of first-order logic.

A language is just a set of symbols and how we can combine those symbols to create meaningful expressions (well-founded formulas).

After selecting a language we can start talking about proof systems (mathematical reasoning systems). A proof system is an (efficient) algorithmic way of checking if a given string is a proof of a given formula (encodes as a string). Think of it as an algorithm that getes two inputs $P(\pi,\varphi)$ (a binary computable predicate) which is true if and only if string $\pi$ is a proof of formula $\varphi$ in $P$. People sometimes write $\pi : P \vdash \varphi$ or omit $\pi$ and write $P \vdash \varphi$. Often the $P$ is put below the symbol like $\vdash_P \varphi$, and when it is clear from the context it is omitted completely $\vdash \varphi$.

What is $P$? We would like that $P$ captures our intuitive notion, i.e. we would like it to satisfy the following conditions:

• soundness: $P$ accepts $\pi$ and $\varphi$, then $\varphi$ is true.

• completeness: if $\varphi$ is true, then $P$ accepts $\pi$ and $\varphi$.

The conditions above presume a notion of semantic truth and are what ties a syntactic objects like proofs to the semantic notion of truth. For validity in first-order logic we can satisfy these conditions, i.e. first-order logic has a sound and complete proof system. However this is not the case for stronger systems like PA or ZF where by incompleteness theorem there is no way of algorithmicly enumerating the true statements (in dependent of the way you define the truth as long as we agree that some basic statements are true, e.g. Robinson's arithmetic theory $Q$).

It is usual in mathematics to take $P$ to be proofs in first-order logic + some first-order theory. ZF is one of such theories. William explains some reasons for this in his answer. A key point here is that first-order logic is very simple and intuitive. It is simpler than the amount of mathematics that one needs to do the stuff I explained above. It is seldom disputed (at least not classical mathematics). By separating the first-order logic part from the first-order theory part we can focus on the disputed part of reasoning. There are mathematicians who would not accept ZF and but you will have a difficulty finding anyone who doesn't accept first-order logic.

If you remove the axioms for first-order logic, then you cannot prove even simple things because the axioms for first-order logic are the part that give us the meaning of the symbols. For example, we have axioms $P \land Q$ implies $P$, $P \land Q$ implies $Q$, and $P$ and $Q$ imply $P \land Q$. If you don't have these axiom, then meaning of the symbol $\land$ can be arbitrary. There is nothing forcing it to act as "and" other than these axioms. Same applies to other axioms of first-order logic. I would suggest that you have a look at a proof system for first-order logic to understand (e.g. LK) to understand that the meaning and use of the symbols is a result of these axioms and without them the symbol is meaningless.

Let me add something that confuses people who are new to mathematical logic. Logic is not build on nothing! We are already assuming a considerable amount of arithmetic in manipulating symbols. For example, if $f$ is a function symbol and $x$ is a variable, we assume that we can create $f(x)$, $f(f(x))$, etc. and this can be views as similar to the successor function over natural numbers. The minimum amount that is needed not too much, but it at least will contain a form of induction over natural numbers. The usual theory that people assume for this meta theory when talking about strong theories is PRA (but there are weaker theories that are sufficient, the bounded arithmetic theory VTC is the weakest meta-theory that I know which allows relatively easy development, see "Logical Foundations of Proof Complexity" for more detail.) Also see Petr Hajek and Pavel Pudlak's book "Metamathematics of First-Order Arithmetic".