A permutation metatheorem

This is one of a series of draft papers on set theory that I did in the late 1960’s. None were ever published. This one covers a small hole in Gödel’s axiomatization of abstract set theory.

In Gödel’s system of abstract set theory [1] propositional functions are represented by classes of ordered n-tuple. One of the first things shown in the development is a general existence theorem to the effect that every primitive propositional function has a representation; i.e if α(x₁,…,x_n) is a primitive propositional function in which ∈ is the only primitive predicate, then
(∃X)(x₁,…,x_n)([x₁,…,x_n])∈X ⇔ α(x₁,…,x_n).
The proof for this metatheorem is by induction on the number of logical operators in α, the critical point in the proof being the case of 0 logical operators. The proof for the case of 0 logical operators depends on three requirements being fulfilled:

• Firstly, the primitive predicate ∈ must be representable; there must be a class X such that (∀x,y)([x,y]∈X⇔x∈y).
• Secondly, it must be possible to add free variables so that the two place predicate ∈ can be considered as a propositional function in n variables; this is achieved by the cartesian product axiom.
• Finally, it must be possible to reorder subscripts of classes of ordered n-tuples so that for all i and j less than or equal to n
  (∃X)(∀ x₁,…,x_n)(x_i∈x_j ⇔ [x₁,…,x_n];
  this is made possible by the converse axioms.

It is clear from the way that the proof is carried out that it could be extended to a more general representation theorem. This theorem says that if α is a propositional function such that the only primitive predicates in α are predicates that have representations and that are one or two place predicates, then α has a representation. The restriction that the predicates be one or two place cannot be removed; the permutation axioms that Gödel gives (axioms 1-3 below) are not strong enough to fulfill the third requirement for m place predicates when m is greater than 2. This paper shows that a single axiom may be added that is equivalent to a general permutation metatheorem that does not have this restriction. (But see below What is proved.)

The result we shall prove is independent of everything in Gödel’s axiomization except the recursive definiton of ordered n-tuples and the axioms given below. In particular it is independent of what definition of the ordered pair [x,y] is used, provided that it is one that meets the usual requirements. We will assume that ordered n-tuples are defined recursively by:
(1) [x₁,x₂,…,x_n] = [x₁,[x₂,…,x_n]] .

From definition (1) it can easily be shown by induction that
(2) [x₁,…,x_k,[x_k+1,…,x_n]] = [x₁,…,x_k,x_k+1,…,x_n] .

We shall assume the following four axioms:

1. (∀x)(∃y)(∀x₁,x₂)([x₁,x₂]∈x⇔[x₂,x₁]∈y)
2. (∀x)(∃y)(∀x₁,x₂,x₃)([x₁,x₂,x₃]∈x⇔[x₁,x₃,x₂]∈y)
3. (∀x)(∃y)(∀x₁,x₂,x₃)([x₁,x₂,x₃]∈x⇔[x₂,x₃,x₁]∈y)
4. (∀x)(∃y)(∀x₁,x₂,x₃,x₄)([x₁,x₂,x₃,x₄]∈x⇔[x₁,x₃,x₂,x₄]∈y)

Theorem: If π is any permutation on n letters then
(∀X)(∃y)(∀x₁,…,x_n)([x₁,…,x_n]∈x ⇔ [x_π(1),…,x_π(n)]∈y)

Proof: The proof is by complete induction on n. The cases n=2 and n=3 follow immediately from axioms 1-3. The general case depends on the fact that an ordered n-tuple is also an ordered pair, triple, etc. Hence, if x is a class of ordered n-tuples and A is a theorem about classes of ordered pairs then A applies to x considered as a class of ordered pairs. For example, it follows from axiom 1 and (2) that
(∀x)(∃y)(∀x₁,x₂,x₃)([x₁,x₂,x₃]∈x⇔[[x₂,x₃],x₁]∈y)
We shall indicate that we are going to treat an ordered n-tuple as an n-k tuple by saying that we are closing brackets around the last k+1 elements. Similarly, if x is a set n-k tuples and the last element of each n-k tuple is a k+1 tuple then we can treat x as a set of n-tuples. We shall indicate that we are doing so by saying that we opening brackets around the last k+1 elements.

If n=4 there are 24 permutations. It can be shown by a direct enumeration that applying (2) and axioms 1-3 to a class x of ordered quadruples yields 40 classes, (see below for a listing) of which eight are classes of ordered quadruples corresponding to the eight permutations of the subscripts for which the first two subscripts are 1 and 2 (in either order) or are 3 and 4 (in either order), these being the only classes of ordered 4-tuples produced by applying (2) and axioms 1-3. Adding axiom 4 permits us change which two subscripts are first and hence provides for the remaining 16 permutations. Hence axiom 4 is necessary for the theorem.

To prove the general case suppose that the theorem is true for all m less then n where n is greater than 4. Depending on how the permutation π action on the last two letters we can classify it as being one of three cases:

Case a: π(n-1),π(n) = (n-1),n

By the inductive hypothesis the theorem holds for n-1. Hence , closing brackets around the last two elements, there is a set y₁ such that
[[x_n-1,x_n],x_π(1),…,x_π(n-2)]∈y₁⇔[x₁,…,x_n]∈x.
We may then close brackets around the last n-2 and apply the inductive hypothesis to get a set y₂ such that
[[x_π(1),…,x_π(n-2)],[x_n-1,x_n]]∈y₂⇔[x₁,…,x_n]∈x.
Proceeding in a similar fashion we can obtain y₃, y₃, and y such that
[[x_π(1),…,x_π(n-2)],[x_π(n-1),x_π(n)]]∈y₃⇔[x₁,…,x_n]∈x,
[[x_π(n-1),x_π(n)],x_π(1),…,x_π(n-2)]∈y₃⇔[x₁,…,x_n]∈x,
[x_π(1),…,x_π(n)]∈y⇔[x₁,…,x_n]∈x

Case b: π(n-1)=i, π(n)=j, i,j ≠ (n-1),n

In this case we may close brackets around the last two elements and form the set y₁ with elements x_i and x_j permuted to the right. We can then close brackets around them and form the set y₂ with the element [x_n-1,x_n] back at the right. We can then open the brackets around [x_n-1,x_n], permute all elements to the desired positions and finally open the brackets around [x_i and x_j] to get y.

Case c: Precisely one of π(n-1), π(n) is a member of {n-1,n}

Let i be the integer such that i is either π(n-1)or π(n) and is neither n-1 nor n. Since is n is greater than 4 there are two distinct integers j and k such that j,k ≠ i,n-1,n. We may then close brackets on x_n-1 and x_n and then get a set y₁ that has x_j and x_k permuted to the right. We may then close brackets on them and get a set y₃ that has [x_n-1,x_n] on the right. We may then open brackets and get a set y₄ that has x_π(n-1) and x_π(n) on the right. We may then close brackets on them and get as set y₅ with [x_j,x_k] on the right. Finally we may open brackets and permute all elements to the desired position to get the set y.

Q.E.D

References:

Gödel, K: “The consistency of the Continuum Hypothesis,” Annals of Matheamtics Studies, No. #, Princeton University Press, Princeton, N.J., 1940

All that this paper actually proves is the permutation metatheorem. The claim is made that (a) without axiom 4 primitive propositional functions that contain a primitive predicate with more than two places are not guaranteed a representation, and (b) with axiom 4 they are. The claim relies on Gödel’s construction. This would be all right if only sufficient detail were given to outline the argument. As it is, the argument for the broader claim is too vague.

2. The 40 classes

The original paper did not list the 40 classes; the predicates for them are listed in the table below:

[x1[x2[x3x4]]] [x3[x4[x1x2]]] [x4[x3[x2x1]]] [x2[x1[x4x3]]] 
[x2[x1[x3x4]]] [x4[x3[x1x2]]] [x3[x4[x2x1]]] [x1[x2[x4x3]]]
[x1[[x3x4]x2]] [x3[[x1x2]x4]] [x4[[x2x1]x3]] [x2[[x4x3]x1]]
[x2[[x3x4]x1]] [x4[[x1x2]x3]] [x3[[x2x1]x4]] [x1[[x4x3]x2]]
[[x3x4][x1x2]] [[x1x2][x3x4]] [[x2x1][x4x3]] [[x4x3][x2x1]]
[[x3x4][x2x1]] [[x1x2][x4x3]] [[x2x1][x3x4]] [[x3x4][x1x2]]
[[x2[x3x4]]x1] [[x4[x1x2]]x3] [[x3[x2x1]]x4] [[x1[x4x3]]x2] 
[[[x3x4]x2]x1] [[[x1x2]x4]x3] [[[x2x1]x3]x4] [[[x4x3]x1]x2]
[[[x3x4]x1]x2] [[[x1x2]x3]x4] [[[x2x1]x4]x3] [x1[[x4x3]x2]]
[[x1[x3x4]]x2] [[x3[x1x2]]x4] [[x4[x2x1]]x3] [[x2[x4x3]]x1]

Although the paper is framed in terms of a particular axiomatic set theory the theorem proved can be considered as a theorem in graph theory. As defined an ordered n-tuple is a binary tree that forms a right-handed vine, e.g.

o--o--o...o--xn
|  |  |   |
x1 x2 x3  xn-1

The result has no particular importance in the context of Gödel’s set/class theory in which the only primitive predicate is ∈. However it is of interest in theories that have a generality of primitive predicates.