# AC is not refutable in ZF - Part 1Sat, 01 Oct 2011 22:00:00 GMT

This is the first of four parts of my posts about the irrefutability of AC in ZF.

It will be about the basic logical background.

Canonically, an alphabet is a set of symbols. It is not necessarily finite. A string is a finite sequence of symbols. A language is a set of strings.

Let us fix the alphabet of logical symbols . Furthermore, we define the sets of -ary relation symbols for , and the sets of -ary function symbols, and the set of variable symbols. Of course, they will stand for relations, functions and variables, but so far, they are only symbols with no meaning.

We define the set , the language of terms, as the smallest superset of satisfying the closure condition for all . This resembles terms in polish notation, but still, so far is just a set of strings with no specified meaning.

We define the set , the language of formulae, as the smallest set containing all strings of the form for for all , and satisfying the closure conditions

stands for the falsum, the proposition which is always false.

This intuitively resembles logical formulae built up from relations between terms and their conjunctions, implications and quantifications. In most theories, we have term symbols different from , and we may safely use these instead of , same for relation symbols, same for variable symbols. Some binary function symbols and relation symbols use infix notation, and we may as well allow these and brackets to change the precedence as usual. So for example, instead of we may write , as it is clear how to convert this formula into our defined notation.

Furthermore, we define , "not ", to be , and , " or ", to be , and , "there exists an satisfying ", to be .

A set of such formulae is called (first-order) theory. Intuitively, a formula follows from a theory , if all structures satisfying the formulae in also satisfy . Make sure that you understood this intuition, it is crucial for the further definitions. It motivates to define what exactly a structure is, and what it means for a structure to satisfy a formula.

We define the concept of an interpretation , which maps function symbols and relation symbols to functions and relations, and bounds quantifiers. Mathematical structures usually have relations and functions on a domain, for example for arithmetic this is the set of natural numbers. So an interpretation has a domain . Having fixed this domain, we need a rather unintuitive object, a function , the valuation. This function is only a "helper" for some edge cases in our setting. And then finally, we need two functions and , mapping and to -ary functions and relations on . We unite these functions into a single function , as it is clear which one of them we mean by the argument we give to it. Now, an interpretation is a triple of these functions and a domain.

An example would be , , , , which would give a standard interpretation of the above formula.

We can extend to general terms by for variables , and . (As you can see, the valuation's purpose is mainly to give a value to free variables.)

Now we can define what it means for an interpretation to satisfy a formula . For this, we write , saying models , or that is a model of :

• iff .
• iff and
• iff implies
• iff for all we have , where
For a theory we define by for all .

To add an additional level of confusion, we define a second meaning for , namely a relation between theories. Let be theories. Then iff for all models , implies . Furthermore, we definde for a formula to be . now finally means that follows from , which is what we wanted to achieve.

There are some well-known theories like ZFC, NGB and PA. But there are also simpler theories like the theory of groups, . Every group is a model of .

Theories which have at least one model are called satisfiable, it is provable that this implies that no contradiction can be derived from them, that is, they are also consistent. There are some theories which do not have a model, for example, trivially does not have one. Less trivial, we can define the theory of fields similar to the theory of groups. Then is not satisfiable, as it can only be satisfied by a field with exactly six elements, which clearly does not exist.

The other question, which will be relevant in the next parts, is the question whether formulae are decided by a theory anyway, that is, whether or . Gödel proved that this is not the case when the theory is of sufficient complexity. Furthermore, there is a proof that this does not hold for the theory of ZF and the axiom of choice. Such propositions are called independent.

But there are much simpler examples. Consider again, and the formula . is independent from : There is a model of which satisfies , and a model of which does not satisfy .

For example, , since the group of integers is abelian. But for example, the multiplicative group of invertible matrices is not commutative.

In the end, the independence proof of AC from ZFC is not different from this: A model of set theory is given which satisfies AC, and another model is given which satisfies the negation of AC.