:: Models and Satisfiability. Defining by Structural Induction and :: Free Variables in ZF-formulae :: by Grzegorz Bancerek :: :: Received April 14, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ZF_LANG, XXREAL_0, CLASSES2, XBOOLE_0, FUNCT_1, CARD_1, TARSKI, SUBSET_1, XBOOLEAN, BVFUNC_2, FUNCT_4, ORDINAL1, ZF_MODEL, FUNCT_2; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, FUNCT_1, ZF_LANG, FUNCT_2, ORDINAL1, NUMBERS, FUNCT_7; constructors ENUMSET1, FUNCT_2, ZF_LANG, FUNCT_7, NUMBERS; registrations XBOOLE_0, RELSET_1, ZF_LANG; requirements NUMERALS, SUBSET, BOOLE; begin reserve F,H,H9 for ZF-formula, x,y,z,t for Variable, a,b,c,d,A,X for set; scheme :: ZF_MODEL:sch 1 ZFschex { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3(set)-> set, F4(set,set)->set, F5(Variable,set)->set, H()->ZF-formula } : ex a,A st ( for x,y holds [x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)] in A) & [H(),a] in A & for H,a st [H,a] in A holds (H is being_equality implies a = F1(Var1 H,Var2 H ) ) & (H is being_membership implies a = F2(Var1 H,Var2 H) ) & (H is negative implies ex b st a = F3(b) & [the_argument_of H,b] in A) & (H is conjunctive implies ex b,c st a = F4(b,c) & [the_left_argument_of H,b] in A & [ the_right_argument_of H,c] in A) & (H is universal implies ex b st a = F5( bound_in H,b) & [the_scope_of H,b] in A); scheme :: ZF_MODEL:sch 2 ZFschuniq { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3(set) ->set, F4(set,set)->set, F5(Variable,set)->set, H()->ZF-formula, a()->set, b() ->set } : a() = b() provided ex A st (for x,y holds [x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)] in A) & [H(),a()] in A & for H,a st [H,a] in A holds (H is being_equality implies a = F1(Var1 H,Var2 H) ) & (H is being_membership implies a = F2(Var1 H, Var2 H) ) & (H is negative implies ex b st a = F3(b) & [the_argument_of H,b] in A) & (H is conjunctive implies ex b,c st a = F4(b,c) & [the_left_argument_of H, b] in A & [the_right_argument_of H,c] in A) & (H is universal implies ex b st a = F5(bound_in H,b) & [the_scope_of H,b] in A) and ex A st (for x,y holds [x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)] in A) & [H(),b()] in A & for H,a st [H,a] in A holds (H is being_equality implies a = F1(Var1 H,Var2 H) ) & (H is being_membership implies a = F2(Var1 H, Var2 H) ) & (H is negative implies ex b st a = F3(b) & [the_argument_of H,b] in A) & (H is conjunctive implies ex b,c st a = F4(b,c) & [the_left_argument_of H, b] in A & [the_right_argument_of H,c] in A) & (H is universal implies ex b st a = F5(bound_in H,b) & [the_scope_of H,b] in A); scheme :: ZF_MODEL:sch 3 ZFschresult { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3(set )->set, F4(set,set)->set, F5(Variable,set)->set, H()->ZF-formula, f(ZF-formula) ->set } : ( H() is being_equality implies f(H()) = F1(Var1 H(),Var2 H()) ) & ( H() is being_membership implies f(H()) = F2(Var1 H(),Var2 H()) ) & ( H() is negative implies f(H()) = F3(f(the_argument_of H())) ) & ( H() is conjunctive implies for a,b st a = f(the_left_argument_of H()) & b = f( the_right_argument_of H()) holds f(H()) = F4(a,b) ) & ( H() is universal implies f(H()) = F5(bound_in H(),f(the_scope_of H())) ) provided for H9,a holds a = f(H9) iff ex A st (for x,y holds [x '=' y,F1(x,y) ] in A & [x 'in' y,F2(x,y)] in A) & [H9,a] in A & for H,a st [H,a] in A holds ( H is being_equality implies a = F1(Var1 H,Var2 H) ) & (H is being_membership implies a = F2(Var1 H,Var2 H) ) & (H is negative implies ex b st a = F3(b) & [ the_argument_of H,b] in A) & (H is conjunctive implies ex b,c st a = F4(b,c) & [the_left_argument_of H,b] in A & [the_right_argument_of H,c] in A) & (H is universal implies ex b st a = F5(bound_in H,b) & [the_scope_of H,b] in A); scheme :: ZF_MODEL:sch 4 ZFschproperty { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3( set)->set, F4(set,set)->set, F5(Variable,set)->set, f(ZF-formula)->set, H()-> ZF-formula, P[set] } : P[f(H())] provided for H9,a holds a = f(H9) iff ex A st (for x,y holds [x '=' y,F1(x,y) ] in A & [x 'in' y,F2(x,y)] in A) & [H9,a] in A & for H,a st [H,a] in A holds ( H is being_equality implies a = F1(Var1 H,Var2 H) ) & (H is being_membership implies a = F2(Var1 H,Var2 H) ) & (H is negative implies ex b st a = F3(b) & [ the_argument_of H,b] in A) & (H is conjunctive implies ex b,c st a = F4(b,c) & [the_left_argument_of H,b] in A & [the_right_argument_of H,c] in A) & (H is universal implies ex b st a = F5(bound_in H,b) & [the_scope_of H,b] in A) and for x,y holds P[F1(x,y)] & P[F2(x,y)] and for a st P[a] holds P[F3(a)] and for a,b st P[a] & P[b] holds P[F4(a,b)] and for a,x st P[a] holds P[F5(x,a)]; definition let H; func Free H -> set means :: ZF_MODEL:def 1 ex A st (for x,y holds [x '=' y,{ x,y }] in A & [x 'in' y,{ x,y }] in A) & [H,it] in A & for H9,a st [H9,a] in A holds (H9 is being_equality implies a = { Var1 H9,Var2 H9 }) & (H9 is being_membership implies a = { Var1 H9,Var2 H9 }) & (H9 is negative implies ex b st a = b & [ the_argument_of H9,b] in A) & (H9 is conjunctive implies ex b,c st a = union { b,c } & [the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9 is universal implies ex b st a = b \ { bound_in H9 } & [ the_scope_of H9,b] in A); end; definition let H; redefine func Free H -> Subset of VAR; end; theorem :: ZF_MODEL:1 for H holds (H is being_equality implies Free H = { Var1 H,Var2 H }) & (H is being_membership implies Free H = { Var1 H,Var2 H }) & (H is negative implies Free H = Free the_argument_of H) & (H is conjunctive implies Free H = Free the_left_argument_of H \/ Free the_right_argument_of H) & (H is universal implies Free H = (Free the_scope_of H) \ { bound_in H }); :: The set of all valuations of variables in a model definition let D be non empty set; func VAL D -> set equals :: ZF_MODEL:def 2 Funcs(VAR,D); end; registration let D be non empty set; cluster VAL D -> non empty; end; reserve E for non empty set, f,g,h for Function of VAR,E, v1,v2,v3,v4,v5,u5 for Element of VAL E; :: The set of all valuations which satisfy a ZF-formula in a model definition let H,E; func St(H,E) -> set means :: ZF_MODEL:def 3 ex A st (for x,y holds [x '=' y,{ v1 : for f st f = v1 holds f.x = f.y }] in A & [x 'in' y,{ v2 : for f st f = v2 holds f. x in f.y }] in A) & [H,it] in A & for H9,a st [H9,a] in A holds (H9 is being_equality implies a = { v3 : for f st f = v3 holds f.(Var1 H9) = f.(Var2 H9) }) & (H9 is being_membership implies a = { v4 : for f st f = v4 holds f.( Var1 H9) in f.(Var2 H9) }) & (H9 is negative implies ex b st a = (VAL E) \ b & [the_argument_of H9,b] in A ) & (H9 is conjunctive implies ex b,c st a = b /\ c & [the_left_argument_of H9,b] in A & [ the_right_argument_of H9,c] in A) & (H9 is universal implies ex b st a = { v5 : for X,f st X = b & f = v5 holds f in X & for g st for y st g.y <> f.y holds bound_in H9 = y holds g in X } & [the_scope_of H9,b] in A); end; definition let H,E; redefine func St(H,E) -> Subset of VAL E; end; theorem :: ZF_MODEL:2 for x,y,f holds f.x = f.y iff f in St(x '=' y,E); theorem :: ZF_MODEL:3 for x,y,f holds f.x in f.y iff f in St(x 'in' y,E); theorem :: ZF_MODEL:4 for H,f holds not f in St(H,E) iff f in St('not' H,E); theorem :: ZF_MODEL:5 for H,H9,f holds f in St(H,E) & f in St(H9,E) iff f in St(H '&' H9,E); theorem :: ZF_MODEL:6 for x,H,f holds ( f in St(H,E) & for g st for y st g.y <> f.y holds x = y holds g in St(H,E) ) iff f in St(All(x,H),E); theorem :: ZF_MODEL:7 H is being_equality implies for f holds f.(Var1 H) = f.(Var2 H) iff f in St(H,E); theorem :: ZF_MODEL:8 H is being_membership implies for f holds f.(Var1 H) in f.(Var2 H) iff f in St(H,E); theorem :: ZF_MODEL:9 H is negative implies for f holds not f in St(the_argument_of H,E) iff f in St(H,E); theorem :: ZF_MODEL:10 H is conjunctive implies for f holds f in St(the_left_argument_of H,E) & f in St(the_right_argument_of H,E) iff f in St(H,E); theorem :: ZF_MODEL:11 H is universal implies for f holds (f in St(the_scope_of H,E) & for g st for y st g.y <> f.y holds bound_in H = y holds g in St(the_scope_of H,E) ) iff f in St(H,E); :: The satisfaction of a ZF-formula in a model by a valuation definition let D be non empty set; let f be Function of VAR,D; let H; pred D,f |= H means :: ZF_MODEL:def 4 f in St(H,D); end; theorem :: ZF_MODEL:12 for E,f,x,y holds E,f |= x '=' y iff f.x = f.y; theorem :: ZF_MODEL:13 for E,f,x,y holds E,f |= x 'in' y iff f.x in f.y; theorem :: ZF_MODEL:14 for E,f,H holds E,f |= H iff not E,f |= 'not' H; theorem :: ZF_MODEL:15 for E,f,H,H9 holds E,f |= H '&' H9 iff E,f |= H & E,f |= H9; theorem :: ZF_MODEL:16 for E,f,H,x holds E,f |= All(x,H) iff for g st for y st g.y <> f .y holds x = y holds E,g |= H; theorem :: ZF_MODEL:17 for E,f,H,H9 holds E,f |= H 'or' H9 iff E,f |= H or E,f |= H9; theorem :: ZF_MODEL:18 for E,f,H,H9 holds E,f |= H => H9 iff (E,f |= H implies E,f |= H9); theorem :: ZF_MODEL:19 for E,f,H,H9 holds E,f |= H <=> H9 iff (E,f |= H iff E,f |= H9); theorem :: ZF_MODEL:20 for E,f,H,x holds E,f |= Ex(x,H) iff ex g st (for y st g.y <> f. y holds x = y) & E,g |= H; theorem :: ZF_MODEL:21 E,f |= All(x,y,H) iff for g st for z st g.z <> f.z holds x = z or y = z holds E,g |= H; theorem :: ZF_MODEL:22 E,f |= Ex(x,y,H) iff ex g st (for z st g.z <> f.z holds x = z or y = z ) & E,g |= H; :: The satisfaction of a ZF-formula in a model definition let E,H; pred E |= H means :: ZF_MODEL:def 5 for f holds E,f |= H; end; theorem :: ZF_MODEL:23 E |= All(x,H) iff E |= H; :: The axioms of ZF-language definition func the_axiom_of_extensionality -> ZF-formula equals :: ZF_MODEL:def 6 All(x.0,x.1,All(x.2,x. 2 'in' x.0 <=> x.2 'in' x.1) => x.0 '=' x.1); func the_axiom_of_pairs -> ZF-formula equals :: ZF_MODEL:def 7 All(x.0,x.1,Ex(x.2,All(x.3, x.3 'in' x.2 <=> (x.3 '=' x.0 'or' x.3 '=' x.1) ))); func the_axiom_of_unions -> ZF-formula equals :: ZF_MODEL:def 8 All(x.0,Ex(x.1,All(x.2, x.2 'in' x.1 <=> Ex(x.3,x.2 'in' x.3 '&' x.3 'in' x.0) ))); func the_axiom_of_infinity -> ZF-formula equals :: ZF_MODEL:def 9 Ex(x.0,x.1,x.1 'in' x.0 '&' All(x.2,x.2 'in' x.0 => Ex(x.3,x.3 'in' x.0 '&' 'not' x.3 '=' x.2 '&' All(x.4, x.4 'in' x.2 => x.4 'in' x.3) ))); func the_axiom_of_power_sets -> ZF-formula equals :: ZF_MODEL:def 10 All(x.0,Ex(x.1,All(x.2, x. 2 'in' x.1 <=> All(x.3,x.3 'in' x.2 => x.3 'in' x.0) ))); end; definition let H be ZF-formula; func the_axiom_of_substitution_for H -> ZF-formula equals :: ZF_MODEL:def 11 All(x.3,Ex(x.0,All (x.4,H <=> x.4 '=' x.0))) => All(x.1,Ex(x.2,All(x.4,x.4 'in' x.2 <=> Ex(x.3,x.3 'in' x.1 '&' H)))); end; definition let E; attr E is being_a_model_of_ZF means :: ZF_MODEL:def 12 E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & for H st { x.0,x.1,x.2 } misses Free H holds E |= the_axiom_of_substitution_for H; end;