Construction of the Hereditarily Finite Sets model

This discussion briefly describes how we encode finite and discrete model X with a computable n-ary relation R into an hereditary finite set (hfs) with to elements l and r, l representing the points in X and r representing the n-tuples in R. Because X is finite and discrete, one can compute a bijection X <~> pos n where n is the cardinal of X. Hence we assume that X = pos n and the ternary relation is R : pos n -> pos n -> pos n -> Prop 1) We find a transitive hfs l such that pos n bijects with the elements of l (transitive means ∀x, x∈l -> x⊆l). Hence pos n <-> { x | x ∈ l } For this, we use the encoding of natural numbers into sets, ie 0 := ø and 1+i := {i} U i and choose l to be the encoding of n (the cardinal of X=pos n above). Notice that since l is transitive then so is P(l) (powerset) and hence P^i(l) for any i. 2) forall x,y ∈ l, both {x} and {x,y} belong to P(l) hence (x,y) = ,{x,y} ∈ P(P(l))=P^2(l) 3) P^1(l) = P(l) contains the empty set 4) Hence P^(2n+1)(l) contains all n-tuples build from the elements of l by induction on n 5) So we can encode R as hfs r ∈ p := P^(2n+2)(l) = P(P^(2n+1)(l)) and p serves as our model, ie Y := { x : hfs | x ∈b p } where x ∈b p is the Boolean encoding of x ∈ p to ensure uniqueness of witnesses/proofs. 6) In the logic, we replace any R v by v ∈ r encoded according to the above description. We have computed the transitive closure, spec'ed and proved finite

First a surjective map from some transitive set l to X

Now we build P^5 l that contains all the set of triples of l

We encode R as a subset of tuples of elements of l in p

The Boolean encoding of x ∈ p

Membership equivalence is identity in the model

For finite and discrete type X, non empty (as witnessed by a given element) equipped with a Boolean ternary relation R, one can compute a type Y, finite and discrete, equipped with a Boolean binary membership predicate ∈ which is extensional. Y is a finite (set like) model which contains two sets yl and yr and there is a bijection between X and (the elements of) yl. All ordered triples build from elements of yl exist in Y, and yr encodes R in the set of (ordered) triples it contains. Finally, membership equivalence (≈) is the same as identity (=) in Y. Membership equivalence : x ≈ y := ∀z, z∈x <-> z∈y Membership extensional : x ≈ y -> ∀z, x∈z -> y∈z Triples are build the usual way (in set theory)

• z ∈ {x,y} := z ≈ x \/ z ≈ y
• ordered pairs: (x,y) is ,{x,y}
• ordered triples: (x,y,z) is ((x,y),z)

Non-emptyness is not really necessary but then bijection between X=ø and yl has to be implemented with dependent functions, more cumbersome to work with. And first order models can never be empty because one has to be able to interpret variables. Maybe a discussion on the case of empty models could be necessary, the logic been reduced to True/False in that case. Any ∀ formula is True, any ∃ is False and no atomic formula can ever be evaluated (because it contains terms that cannot be interpreted). Only closed formula have a meaning in the empty model