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.