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
-ary relation symbols
, and the sets
-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
. 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
, 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
", to be
", to be
, "there exists an
", 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
. 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
-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
. (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
- iff .
- iff and
- iff implies
- iff for all we have , where
For a theory
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
. Furthermore, we definde
for a formula
now finally means that
, which is what we wanted to achieve.
There are some well-known theories like ZFC, NGB
. 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
. 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
, and a model of
which does not satisfy
, 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.