PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 82(96) (2007), 155–163 DOI 102298/PIM0796155P

FIN-SET: A SYNTACTICAL DEFINITION OF FINITE SETS

Slaviša B. Prešić

Abstract. We state Fin-set, by which one founds the notion of finite sets in a syntactical way. Any finite set {a_{1}, a_{2}, …, a_{n}} is defined as a well formed term of the form S(a_{1} + (a_{2} + (⋯ + (a_{n−1} + a_{n}) ⋯))), where + is a binary and S a unary operational symbol. Related to the operational symbol + the term-substitutions (1) are introduced. Definition of finite sets is called syntactical because by two algorithms Set-alg and Calc one can effectively establish whether any given set-terms are equal or not equal.

All other notions related to finite sets, like ∈, ordered pair, Cartesian product, relation, function, cardinal number are defined as terms as well. Each of these definitions is recursive. For instance, ∈ is defined by

x ∈ S(a_{1}) iff x = a_{1}

x ∈ S(a_{1} + ⋯ + a_{n}) iff x = a_{1} or x ∈ S(a_{2} + ⋯ + a_{n})

x ∉ ∅ (∅ denotes the empty set)

1. The key idea

Finite sets are usually expressed by some set-terms like {a}, {a, {b, c}}, {a_{1}, …, a_{n}}. Related to such terms there are infinite number of ‘algebraic laws’ like

(∗)  {x, x} = {x}, {x, y} = {y, x}, {x, y, z} = {z, x, y}

which express various properties of finite sets. In order to state all such algebraic laws we use the following idea: We ‘divide’ the notion of finite set into two ‘parts’. The first one is the preset, formalized by means of a binary operational symbol +. The second one is the set-maker, formalized by an unary operational symbol S.

For instance, using S and + the ordinary set-terms {a}, {{a, b}, c}, {a_{1}, …, a_{n}} are represented by the following (S, +)-terms

S(a), S(S(a + b) + c), S(a_{1} + (a_{2} + ⋯ + (a_{n−1} + a_{n}) + ⋯))

respectively. Having in mind (∗) for + we put term-substitutions (1) (below).

2000 Mathematics Subject Classification: 03E30. Key words and phrases: finite set, algorithm, syntactical definition.

2. (+, S)−terms

Denote by Γ a collection of constant symbols, called initial elements. Symbol ∅ is also an element of Γ. Let L be a language whose elements are all elements of Γ and also the operational symbols + and S (+ is a binary, S a unary operational symbol). The symbols x, y, z, u, x′, y′, z′, u′, … are used as variables. We define terms by the generalized inductive definition:

(i) Any element of Γ is a term.

(ii) A variable is a term.

(iii) If A, B are terms, then the words (A + B), S(A) are terms. Next we introduce the following term-substitutions

(1)  \begin{aligned}(i) & (τ_{1} + τ_{1}) & → τ_{1} \\ (i′) & τ_{1} & → (τ_{1} + τ_{1}) \\ (ii) & (τ_{1} + τ_{2}) & → (τ_{2} + τ_{1}) \\ (iii) & ((τ_{1} + τ_{2}) + τ_{3}) & → (τ_{1} + (τ_{2} + τ_{3})) \\ (iii′) & (τ_{1} + (τ_{2} + τ_{3})) & → ((τ_{1} + τ_{2}) + τ_{3}) \\ (iv) & τ_{1} & → τ_{1} \end{aligned}

where τ_{1}, τ_{2}, τ_{3} are any terms.

Let σ_{1} → σ_{2} be a substitution. Suppose that t_{1} is a term which contains, at some place^{1} a subterm of the form σ_{1}. Replacing σ_{1} with σ_{2} at such a place from t_{1} we obtain a new term denoted by t_{2}. We shall say that t_{2} is neighbouring to t_{1}. For the sentence: t_{2} is neighbouring to t_{1} we shall use the following notation: t_{1} → t_{2}. For instance, let t_{1} be a term

S(S(x + S(a + (b + c))) + S(a + (b + c)))

and let the substitution σ_{1} → σ_{2} be of the form (τ_{1} + τ_{2}) → (τ_{2} + τ_{1}). In the given term t_{1} there are six subterms of the form (τ_{1} + τ_{2}), since the symbol + appears in t_{1} just six times. Let us consider the subterm (a + (b + c)), at its first occurrence. Then τ_{1} is a, and τ_{2} is (b + c). By applying the substitution (τ_{1} + τ_{2}) → (τ_{2} + τ_{1}) from term t_{1} we obtain the term t_{2}

S(S(x + S((b + c) + a)) + S(a + (b + c)))

which is neighbouring to t_{1}. Due to (1)(iv) any term t is neighbouring to t, i.e., t → t. Next, we shall define a relation = (‘equality’) between two terms t_{1}, t_{2}. Namely:

(2) We shall say that t_{1} = t_{2} holds iff either the word t_{1} is literally equal to the word t_{2} or there are terms τ_{1}, τ_{2}, …, τ_{k} such that τ_{1} is t_{1}, τ_{k} is t_{2}, and each τ_{i} (1 < i ⩽ k) is neighbouring to τ_{i−1} In other words, t_{1} = t_{2} holds iff we have the following ‘substitutional chain’

(3′)  τ_{1} → τ_{2} → τ_{3} → ⋯ → τ_{k} (τ_{1} is t_{1}, τ_{k} is t_{2})

1Starting, say, with certain i-th letter of the word t_{1}

If the relation t_{1} = t_{2} holds we shall say that t_{1} is equal to t_{2}. Obviously relation = has the following properties

τ_{1} = τ_{1}
If τ_{1} = τ_{2}, then τ_{2} = τ_{1}
(3)  If τ_{1} = τ_{2} and τ_{2} = τ_{3}, then τ_{1} = τ_{3}
If τ_{1} = τ_{2}, then S(τ_{1}) = S(τ_{2})
If τ_{1} = τ_{2} and τ_{3} = τ_{4}, then (τ_{1} + τ_{3}) = (τ_{2} + τ_{4})

Remark 1. Relation = can be defined by equational axioms x+x = x, x+y = y +x, (x+y)+z = x+(y +z). Namely, it can be easily proved that relation t_{1} = t_{2} holds iff formula t_{1} = t_{2} is an equational consequence of the axioms, where x, y, z can be any (S, +)-terms.

Now we consider terms of the form

A_{1}, (A_{1} + A_{2}), ((A_{1} + A_{2}) + A_{3}), (((A_{1} + A_{2}) + A_{3}) + A_{4}), …

For them we shall use the notation

A_{1}, A_{1} + A_{2}, A_{1} + A_{2} + A_{3}, A_{1} + A_{2} + A_{3} + A_{4}, …

respectively and call them sum-terms. Suppose that by term(+, A_{1}, …, A_{k}) any term is denoted which is built up from its subterms A_{1}, …, A_{k} by use of the operational symbol + only. The order of these A_{i} is not important. Then the following equality holds:

(∗_{1})  term(+, A_{1}, …, A_{k}) = A_{1} + ⋯ + A_{k}

This equality holds in virtue of substitutions (1) of the form (ii), (iii), (iii′). For instance, the equality ((A + (C + B)) + (E + D)) = A + B + C + D + E is true.

Let A_{1} + ⋯ + A_{k}, B_{1} + ⋯ + B_{q} be any sum-terms. We define relation =_{S} between them:

(4) A_{1} + ⋯ + A_{p} =_{S} B_{1} + ⋯ + B_{q} holds iff each A_{i} is equal to some B_{j} and
each B_{k} is equal to some A_{l}

The relation =_{S} has the following properties

(5) (i) A_{1}+⋯+A_{p} =_{S} A_{f(1)}+⋯+A_{f(p)}, where f is any permutation of indexes

1, …, p. (ii) A_{1} + ⋯ + A_{i} + ⋯ + A_{p} =_{S} A_{1} + ⋯ + A_{i} + A_{i} + ⋯ + A_{p}, where the right hand side is obtained from the left hand side by replacing A_{i} by A_{i} + A_{i} (ii′) A_{1} + ⋯ + A_{i} + A_{i} + ⋯ + A_{p} =_{S} A_{1} + ⋯ + A_{i} + ⋯ + A_{p}, where the left hand side is obtained from the right hand side by replacing A_{i} by A_{i} + A_{i} (iii) If A_{1} + ⋯ + A_{p} =_{S} B_{1} + ⋯ + B_{q}, then B_{1} + ⋯ + B_{q} =_{S} A_{1} + ⋯ + A_{p} (iv) If A_{1} + ⋯ + A_{p} =_{S} B_{1} + ⋯ + B_{q} and B_{1} + ⋯ + B_{q} =_{S} C_{1} + ⋯ + C_{r},

then A_{1} + ⋯ + A_{p} =_{S} C_{1} + ⋯ + C_{r}

(v) A_{1} + ⋯ + A_{i} + ⋯ + A_{p} =_{S} A_{1} + ⋯ + B + ⋯ + A_{p} assuming that A_{i} is replaced by B and A_{i} = B

Assertion (5) is an immediate consequence of definition (4). Relation =_{S} has also this property

(∗_{2}) If A_{1} + ⋯ + A_{p} =_{S} B_{1} + ⋯ + B_{q}, then A_{1} + ⋯ + A_{p} = B_{1} + ⋯ + B_{q}

which is an immediate consequence of (4) and definition of =, i.e., of (2). For instance, A + B + C =_{S} B + C + A + C holds. Also A + B + C = B + C + A + C holds, which can be proved easily by substitutions (1).

Related to implication (∗_{2}) it is important to know when the opposite implication is true too. In connection with it we introduce the notion of full sum-term. Namely, we shall say that A_{1} + ⋯ + A_{k} is a full sum-term if none of A_{i} is of the form (P + Q) for some P, Q. Obviously, any sum-term is equal to certain full sum-term.

Now we shall prove

(∗_{3}) If B_{1} + ⋯ + B_{q} is a full sum-term, which is neighbouring to a full sum-term A_{1} + ⋯ + A_{p}, then A_{1} + ⋯ + A_{p} =_{S} B_{1} + ⋯ + B_{q} holds.

Indeed, denote by σ a substitution of type (1) by which from A_{1} + ⋯ + A_{p} we obtain B_{1} + ⋯ + B_{q}. We distinguish two cases: 1^{∘} σ is related to some subterm of A_{1} ⋯ + A_{p} whose + is inside one A_{i}. 2^{∘} σ is related to one of p−1 symbols + occuring in the sum-term A_{1}+A_{2}+⋯+A_{p} In the first case applying σ to A_{i} we obtain some B, such that A_{i} = B. Then in virtue of (5)(v) we conclude that

A_{1} + ⋯ + A_{i−1} + A_{i} + ⋯ + A_{p} =_{S} A_{1} + ⋯ + A_{i−1} + B + ⋯ + A_{p}

and proof is complete in the first case.

In the second case, having in mind (5)(i), (ii), (ii′) the proof completes.

Now we shall prove a generalization of (∗_{3})

(∗_{4}) If A_{1} + ⋯ + A_{p} = B_{1} + ⋯ + B_{q} holds, where A_{1} + ⋯ + A_{p}, B_{1} + ⋯ + B_{q} are full sum-terms, then also A_{1} + ⋯ + A_{p} =_{S} B_{1} + ⋯ + B_{q} holds.

Indeed, let A_{1} + ⋯ + A_{p} = B_{1} + ⋯ + B_{q}. Then, like (3′), there is certain substitutional chain

τ_{1} → τ_{2} → ⋯ → τ_{k} (τ_{1} is A_{1} + ⋯ + A_{p}, τ_{k} is B_{1} + ⋯ + B_{q})

In virtue of (∗_{3}) we have τ_{1} =_{S} τ_{2}, τ_{2} =_{S} τ_{3}, …, τ_{k−1} =_{S} τ_{k}. Having in mind (5)(iv) we conclude τ_{1} =_{S} τ_{k} and the proof completes.

Lemma 1. Suppose that A_{1} + ⋯ + A_{p}, B_{1} + ⋯ + B_{q} are full sum-terms. Then the following equivalence is true

A_{1} + ⋯ + A_{p} = B_{1} + ⋯ + B_{q} holds iff each A_{i} is equal to some B_{j} and
each B_{k} is equal to some A_{l}

Proof. Proof follows immediately from (∗_{3}) and (4). For instance, if p = 2, q = 2 then we have the following equivalence

(∗_{5}) A_{1} + A_{2} = B_{1} + B_{2} iff (A_{1} = B_{1} ∧ A_{2} = B_{2}) ∨ (A_{1} = B_{2} ∧ A_{2} = B_{1}) □

Lemma 2. S(A) = S(B) iff A = B.

Proof follows directly from the definition (1).

Now we define the notion of monomial. This is a term t which is not of the form (P +Q) for some P, Q. Let t be any term. It is a monomial just in three cases: t is an initial element or t is a variable or t has the form S(P) for some P. Term of the form S(P) will be called S-monomial. An equality of the form m_{1} = m_{2}, where m_{1}, m_{2} are monomials will be called a monomial equality. Such an equality will be called a reduced monomial equality if at least one of m_{1}, m_{2} is not an S-monomial.

Lemma 3. Let m_{1} = m_{2} be a reduced monomial equality. This equality holds iff m_{1}, m_{2} are equal as words.

As a matter of fact, Lemma 1, Lemma 2 and Lemma 3 describe an algorithm, called Set-alg, by which one can decide whether any given terms t_{1}, t_{2} are equal or not. Namely, to given equality t_{1} = t_{2} we apply Lemma 1 or Lemma 2 as many times as possible. At the end we obtain some logical expression Expr, built from certain reduced monomial equations m_{i} = m_{j} using logical connectives ∧ and ∨. Having in mind Lemma 3 we can calculate logical value of Expr. If the obtained value is ⊤, then the equality t_{1} = t_{2} holds. If the value is ⊥, then the equality t_{1} = t_{2} does not hold. We shall illustrate this algorithm by some examples.

Example 1. Let a, b, c, d be some initial elements. Calculate the logical value of a given equality:

1^{∘} S(a + b) = S(b + a), 2^{∘} S(a + b) = S(b + ∅)
3^{∘} S(a + S(b + c + d) + b) = S(b + a + S(d + c + b))

Solution. 1^{∘} We have the following equivalence-chain

S(a + b) = S(b + a)

iff a + b = b + a (By Lemma 2)

iff (a = b ∧ b = a) ∨ (a = a ∧ b = b) (By (∗_{5}), i.e. by Lemma 1)

The answer is yes since by Lemma 3 the equalities a = a and b = b are true.

2^{∘} We have the following equivalence-chain

S(a + b) = S(b + ∅)

iff a + b = b + ∅ (By Lemma 2)

iff (a = b ∧ b = ∅) ∨ (a = ∅ ∧ b = b) (By (∗), i.e. by Lemma 1)

The answer is no since by Lemma 3 equalities a = b, a = ∅ and b = ∅ are false.

3^{∘} By Lemma 2 we see that the given equality reduces to

a + S(b + c + d) + b = b + a + S(d + c + b)

Applying Lemma 1 this equality reduces to S(b + c + d) = S(d + c + b). Applying Lemma 2 this equality reduces to b + c + d = d + c + b. Finally applying Lemma 1 and Lemma 3 we conclude that the answer is yes.

Remark 2. Here, in brief, we describe an algorithm, called Calc, which is simpler than Set-alg. Let a term S_{1} have the form S(p_{1} + p_{2} + ⋯ + p_{m}), where p_{i} are some initial elements. We shall say that such a term is countable. Term S_{1} can be equal to certain other countable term, say S(q_{1} + q_{2} + ⋯ + q_{n}), where q_{j} are some initial elements. In such case each element p_{i} must be the same as some q_{j} and also each q_{k} must be the same as some p_{r}. For instance, if a, b, c are initial elements we have equality

S(a + b + a + b + c) = S(c + b + a + a)

Suppose now that a term t_{1} has certain countable subterm S_{1}, and that a ‘list’ S_{1}, S_{2}, … S_{p} contains all countable subterms of t, which are equal to S_{1}. Suppose that t_{1} equals t_{2}. Then like (3′) we have the following substitutional chain

(σ_{1})  τ_{1} → τ_{2} → τ_{3} → ⋯ → τ_{s}  (τ_{1} is t_{1}, τ_{s} is t_{2})

In the first step τ_{1} → τ_{2} of this chain, any S_{i} remains unchanged or transforms to some countable term S′_{i}, which is equal to S_{i}. The same holds for other steps. Denote by S_{1}, … S_{p}, … S_{P} all terms occurring in (σ_{1}) which are equal to S_{1}.

Let C be an initial element not occurring in the chain (σ_{1}). In this chain replace all S_{1}, … S_{p}, … S_{P} by C. If t is any term, by t⟨C⟩ we denote the term obtained by that replacement. In such a way from (σ_{1}) we obtain the following ‘formal chain’

(σ_{2})  τ_{1}⟨C⟩ → τ_{2}⟨C⟩ → τ_{3}⟨C⟩ → ⋯ → τ_{s}⟨C⟩

Obviously τ_{1}⟨C⟩, … τ_{s}⟨C⟩ are well-formed (S, +)-terms and in addition to that (σ_{2}) is a valid substitutional chain. So we conclude the following

If t_{1} = t_{2}, then t_{1}⟨C⟩ = t_{2}⟨C⟩.

Now suppose that in (σ_{2}) every C is replaced by any terms S_{1}, … S_{p}, … S_{P}. Then from (σ_{2}) we shall obtain a chain which can be easily extended to a valid substitutional chain^{2}. So, we conclude also

If t_{1}⟨C⟩ = t_{2}⟨C⟩, then t_{1} = t_{2}.

The mentioned algorithm Calc is based on the equivalence

(Cal)  t_{1} = t_{2} iff t_{1}⟨C⟩ = t_{2}⟨C⟩

We illustrate Calc by two examples. First one is: prove or disprove the equality

S(a + S(S(a) + b) + S(b + S(a)) + c) = S(a + c + S(b + S(a)))

Using (Cal) we have the following equivalence-chain

S(a + S(S(a) + b) + S(b + S(a)) + c) = S(a + c + S(b + S(a)))

iff S(a + S(p + b) + S(b + p) + c) = S(a + c + S(b + p)) (S(a) is replaced by p)

iff S(a + q + q + c) = S(a + c + q) (S(p + b), S(b + p) are replaced by q)

iff r = r (S(a + q + q + c), S(a + c + q) are replaced by r)

2For instance, if in the chain S(a + C) → S(C + a) we replace the first C by S(p + q) and the second by S(q + p) we obtain S(a + S(p + q)) → S(S(q + p) + a), which can be extended to this valid substitutional chain S(a + S(p + q)) → S(S(p + q) + a) → S(S(q + p) + a).

So, the given equality is proven. Here p, q, r are initial elements.

The second example is: prove or disprove the equality

S(a + S(S(b)) + c) = S(c + a + S(S(b) + d))

Using (Cal) we have the following equivalence-chain

S(a + S(S(b)) + c) = S(c + a + S(S(b) + d))

iff S(a + S(p) + c) = S(c + a + S(p + d)) (S(b) is replaced by p)

iff S(a + q + c) = S(c + a + S(p + d)) (S(p) is replaced by q.)

As a matter of fact, because S(p) does not appear on the right hand side we conclude that the last equality is false. Consequently the given equality is false.

Notice that the name Calc is related to the fact that this algorithm in some sense ‘calculates’ the given terms. Terms of the form S(p_{1} + p_{2} + ⋯ + p_{m}), where p_{i} are some initial elements, are called countable, since the algorithm Calc is ‘able to calculate just them’.

3. Definition of finite sets

A ground term is a term not containing variables. Now we define the notion of a finite set:

(6) A finite set is either ∅ (called the empty set) or a ground term

of the form S(A) (called a non-empty set).

According to Lemma 1 any set A can be expressed in one of the forms

(∗_{6})  1^{∘}: ∅,  2^{∘}: S(A_{1} + ⋯ + A_{n})

where n = 1, 2, … and A_{1} + ⋯ + A_{n} is a full sum-term. One may suppose that A_{i} are pairwise different terms. These forms are called the canonical forms for set A. By virtue of Lemma 1 the form (∗_{6}) 2^{∘} is unique up to the order of A_{1}, A_{2}, …, A_{n}. In the sequel we always assume that finite sets are given in a canonical form.

Example 2. Let 1, 2, 3 be initial elements. Then the ground term S((1 + 3) + (2 + 3)) is a finite set. One of its canonical forms is S(1 + 2 + 3). Besides this there are also 5 others canonical forms

S(1 + 3 + 2), S(2 + 1 + 3), S(2 + 3 + 1), S(3 + 1 + 2), S(3 + 2 + 1)

which differ only in the order of 1, 2, 3.

Concerning the given definition (6) of a finite set we point out that a finite set is defined as a well defined term. Consequently, we can produce various recursive definitions for them.

First, we define the relation ∈:

(7) x ∈ S(A) iff x = A
x ∈ S(A_{1} + A_{2} + ⋯ + A_{n}) iff x = A_{1} or x ∈ S(A_{2} + ⋯ + A_{n}) (n > 1)
x ∉ ∅

For instance, 2 ∈ S(1 + 2 + 3). Indeed:

2 ∈ S(1 + 2 + 3) iff 2 = 1 or 2 ∈ S(2 + 3)

iff 2 ∈ S(2 + 3) (Since 2 = 1 is false)

iff 2 = 2 or 2 ∈ S(3)

iff 2 = 2 (Since 2 = 2 is true)

So, it is true that 2 ∈ S(1 + 2 + 3). But, for instance 2 ∉ S(1 + 3). Indeed:

2 ∈ S(1 + 3) iff 2 = 1 or 2 ∈ S(3)

iff 2 ∈ S(3) (Since 2 = 1 is false) iff 2 = 3

Since the equality 2 = 3 is false we conclude that 2 ∈ S(1 + 3) is false too.

Notice that in general if A_{1}, …, A_{n} are some given ground terms then S(A_{1} + ⋯ + A_{n}) is the set whose all elements are A_{1},…,A_{n}.

Bearing in mind Lemma 1 and the definition (7) one can easily prove the following well known equivalence (Extensionality axiom in ZF set theory)

A = B ↔ (∀x)(x ∈ A ↔ x ∈ B)

where A, B are any finite sets and the variable x ranges over ground terms only.

The next step is to define |A|–the cardinal number of the set A. By use of the ‘ordinary’ notion of natural number we have the inductive definition

|∅| = 0, |S(A)| = 1, |S(A_{1} + A_{2} + ⋯ + A_{n})| = 1 + |S(A_{2} + ⋯ + A_{n})|.

Now we give several definitions, and each of them will be syntactical; in other words for each of them we can make a corresponding decision algorithm.

(Relation ⊆) A ⊆ B iff (∀x)(x ∈ A ⇒ x ∈ B) (Operation ∪) ∅ ∪ x = x (x is any finite set)

S(A_{1}) ∪ S(B_{1} + ⋯ + B_{m}) is S(A_{1} + B_{1} + ⋯ + B_{m}) S(A_{1}+⋯+A_{n})∪S(B_{1}+⋯+B_{m}) is S(A_{2}+⋯+A_{n})∪S(B_{1}+⋯+B_{m}) if A_{1} ∈ S(B_{1} + ⋯ + B_{m}), otherwise it is S(A_{1}) ∪ (S(A_{2} + ⋯ + A_{n}) ∪ S(B_{1} + ⋯ + B_{m}))

(Operation ∩) ∅ ∩ x = ∅ (x is any finite set) S(A_{1}+⋯+A_{n})∩S(B_{1}+⋯+B_{m}) is S(A_{2}+⋯+A_{n})∩S(B_{1}+⋯+B_{m}) if A_{1} ∉ S(B_{1} + ⋯ + B_{m}), otherwise it is S(A_{1}) ∪ (S(A_{2} + ⋯ + A_{n}) ∩ S(B_{1} + ⋯ + B_{m}))

(Operation ∖) ∅ ∖ x = ∅ (x is any finite set) S(A_{1}+⋯+A_{n})∖S(B_{1}+⋯+B_{m}) is S(A_{2}+⋯+A_{n})∖S(B_{1}+⋯+B_{m}) if A_{1} ∈ S(B_{1} + ⋯ + B_{m}), otherwise it is S(A_{1}) ∪ (S(A_{2} + ⋯ + A_{n}) ∖ S(B_{1} + ⋯ + B_{m}))

Now we shall define the ordered pair of two member terms x, y, in symbols Π(x, y). There are two ways to do this: one is to extend Ω by a new binary operational symbol Π and to add no new axiom concerning Π, and to regard term Π(x, y) as the ordered pair of x and y. The alternative way is to adopt Wiener– Kuratowski idea, i.e., to introduce the following definition

Π(x, y) = S(S(x) + S(x + y))

Further, we can in the usual way define cartesian product X × Y of two sets, of more sets, a binary, ternary,… relation, a function f : X → Y, etc. Again and again each of such notions is determined by some ground term.

Example 3. Let A = S(1 + 2 + 3), B = S(a + b). Then

A × B = S(Π(1, a) + Π(1, b) + Π(2, a) + Π(2, b) + Π(3, a) + Π(3, b))

The term S(Π(1, a) + Π(2, b) + Π(3, a)) determines a function f : A → B such that f(1) = a, f(2) = b, f(3) = a.

We have already mentioned that the finite sets defined by (6) satisfy Extensionality axiom of ZF set theory. It is not difficult to see that, in Fin-set, except Axiom of infinity, all other axioms of ZF theory can be proved in a simple way. Moreover, if some axioms say that there exist some sets x, y, …, then one can make ‘algorithmic proof’, which effectively construct such sets x, y, …

We illustrate this idea by considering Subset axioms. So, let t = S(a_{1}+⋯+a_{n}) be a given set and ϕ(x) any given formula, condition containing x as a free variable. Suppose that for each a_{i} we can determine whether ϕ(a_{i}) is true or false. We should prove that there exists a set T such that: x ∈ T iff x ∈ t ∧ ϕ(x).

Denote by b_{1}, …, b_{k} all of those a_{i} for which ϕ(a_{i}) is true. If k = 0, then T = ∅, otherwise T = S(b_{1} + ⋯ + b_{k}). The proof is complete.

Example 4. Let t = S(1+2+3+4+5) and let ϕ(x) be the following condition x ∈ S(1 + 4 + 8 + 9). Then T = S(1 + 4). However, suppose that we extend the language Ω by a relation symbol ev (‘to be even’) and also add the following new axioms ev(2), ev(4), ev(6). Let ϕ(x) be the formula ev(x). Then the corresponding T is S(2 + 4).

Matematički fakultet

11000 Beograd

Serbia

    spresic@matf.bg.ac.yu