:: Models and Satisfiability. Defining by Structural Induction and
:: Free Variables in ZF-formulae
::  by Grzegorz Bancerek
::
:: Received April 14, 1989
:: Copyright (c) 1990-2021 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;