Properties of ZF Models

Summary. The article deals with the concepts of satisfiability of ZF set theory language formulae in a model (a non-empty family of sets) and the axioms of ZF theory introduced in [6]. It is shown that the transitive model satisfies the axiom of extensionality and that it satisfies the axiom of pairs if and only if it is closed to pair operation; it satisfies the axiom of unions if and only if it is closed to union operation, ect. The conditions which are satisfied by arbitrary model of ZF set theory are also shown. Besides introduced are definable and parametrically definable functions. MML Identifier: ZFMODEL1. The notation and terminology used in this paper are introduced in the following papers: [8], [4], [1], [5], [7], [3], and [2]. For simplicity we follow a convention: x, y, z will be variables, H will be a ZF-formula, E will be a non-empty family of sets, X, Y, Z will be sets, u, v, w will be elements of E, and f, g will be functions from VAR into E. One can prove the following propositions: (1) If E is transitive, then E | = theaxiom of extensionality. (2) If E is transitive, then E | = theaxiom of pairs if and only if for all u, v holds {u,v} ∈ E. (3) If E is transitive, then E | = theaxiom of pairs if and only if for all X, Y such that X ∈ E and Y ∈ E holds {X,Y} ∈ E. (4) If E is transitive, then E | = theaxiom of unions if and only if for every u holds � u ∈ E. (5) If E is transitive, then E | = theaxiom of unions if and only if for every X such that X ∈ E holds � X ∈ E. (6) If E is transitive, then E | = theaxiom of infinity if and only if there exists u such that u � = ∅ and for every v such that v ∈ u there exists w such that v ⊆ w and v � = w and w ∈ u. (7) If E is transitive, then E | = theaxiom of infinity if and only if there exists X such that X ∈ E and X � = ∅ and for every Y such that Y ∈ X there exists Z such that Y ⊆ Z and Y � = Z and Z ∈ X