The Mizar abstract of VALUAT

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Interpretation and Satisfiability in the First Order Logic
by
Edmund Woronowicz
Received June 1, 1990
MML identifier: VALUAT_1
[ Mizar article, MML identifier index ]
environ

 vocabulary FUNCT_2, QC_LANG1, FRAENKEL, FUNCT_1, RELAT_1, MARGREL1, BOOLE,
      ZF_LANG, CQC_LANG, FINSEQ_1, ARYTM_3, FUNCOP_1, ZF_MODEL, QC_LANG3,
      CAT_1, VALUAT_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, RELAT_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, FRAENKEL, QC_LANG1, QC_LANG3, CQC_LANG, MARGREL1;
 constructors QC_LANG3, CQC_LANG, MARGREL1, XREAL_0, XCMPLX_0, MEMBERED,
      XBOOLE_0;
 clusters RELSET_1, MARGREL1, CQC_LANG, QC_LANG1, ARYTM_3, FINSEQ_1, FUNCT_1,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;


begin

 reserve i,j,k for Nat,
         A,D for non empty set;

 definition let A be set;
   func Valuations_in A -> set equals
:: VALUAT_1:def 1
   Funcs(bound_QC-variables, A);
 end;

 definition let A;
  cluster Valuations_in A -> non empty functional;
 end;

canceled;

theorem :: VALUAT_1:2
  for x being set st x is Element of Valuations_in A holds
       x is Function of bound_QC-variables ,A;

definition
 let A;
 redefine func Valuations_in A -> FUNCTION_DOMAIN of bound_QC-variables, A;
end;

definition let f be Function;
 attr f is boolean-valued means
:: VALUAT_1:def 2
 rng f c= BOOLEAN;
end;

definition
 cluster boolean-valued Function;
end;

definition let f be boolean-valued Function, x be set;
 cluster f.x -> boolean;
end;

definition let A be set;
 cluster -> boolean-valued Element of Funcs(A,BOOLEAN);
end;

definition
 let p be boolean-valued Function;
  func 'not' p -> Function means
:: VALUAT_1:def 3
 dom it = dom p &
   for x being set st x in dom p holds it.x = 'not'(p.x);
 let q be boolean-valued Function;
  func p '&' q -> Function means
:: VALUAT_1:def 4
 dom it = dom p /\ dom q &
  for x being set st x in dom it holds it.x = (p.x) '&' (q.x);
 commutativity;
end;

definition
 let p be boolean-valued Function;
 cluster 'not' p -> boolean-valued;
 let q be boolean-valued Function;
  cluster p '&' q -> boolean-valued;
end;

 reserve f1,f2 for Element of Funcs(Valuations_in A,BOOLEAN),
         x,x1,y for bound_QC-variable,
         v,v1 for Element of Valuations_in A;

definition let A;
 redefine
 let p be Element of Funcs(A,BOOLEAN);
  func 'not' p -> Element of Funcs(A,BOOLEAN) means
:: VALUAT_1:def 5
 for x being Element of A holds it.x = 'not'(p.x);
 let q be Element of Funcs(A,BOOLEAN);
  func p '&' q -> Element of Funcs(A,BOOLEAN) means
:: VALUAT_1:def 6
 for x being Element of A holds it.x = (p.x) '&' (q.x);
end;

definition
 let A, x;
 let p be Element of Funcs(Valuations_in A,BOOLEAN);
  func FOR_ALL(x,p) -> Element of Funcs(Valuations_in A,BOOLEAN) means
:: VALUAT_1:def 7
 for v holds
        it.v = ALL{p.v' where v' is Element of Valuations_in A:
                       for y st x <> y holds v'.y = v.y};
end;

canceled 4;

theorem :: VALUAT_1:7
  for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
  FOR_ALL(x,p).v = FALSE iff ex v1 st p.v1 = FALSE &
                          for y st x <> y holds v1.y = v.y;

 theorem :: VALUAT_1:8
  for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
  FOR_ALL(x,p).v = TRUE iff for v1 st for y st x <> y holds v1.y = v.y holds
      p.v1 = TRUE;

reserve ll for CQC-variable_list of k;

definition
 let A, k, ll, v;
  redefine
  func v*ll -> FinSequence of A means
:: VALUAT_1:def 8
 len it = k & for i st 1 <= i & i <= k holds it.i = v.(ll.i);
 synonym v*'ll;
end;

definition
 let A, k, ll;
 let r be Element of relations_on A;
  func ll 'in' r -> Element of Funcs(Valuations_in A,BOOLEAN) means
:: VALUAT_1:def 9
 for v being Element of Valuations_in A holds
       (v*'ll in r implies it.v = TRUE) &
       (not v*'ll in r implies it.v = FALSE);
end;

definition
 let A;
 let F be Function of CQC-WFF,Funcs(Valuations_in A, BOOLEAN);
 let p be Element of CQC-WFF;
 redefine func F.p -> Element of Funcs(Valuations_in A, BOOLEAN);
end;

definition
 let D;
   mode interpretation of D -> Function of QC-pred_symbols, relations_on D
     means
:: VALUAT_1:def 10
      for P being (Element of QC-pred_symbols),
      r being Element of relations_on D st it.P = r holds
      r = empty_rel(D) or the_arity_of P = the_arity_of r;
 end;

reserve
     p,q,s,t for Element of CQC-WFF,
     J for interpretation of A,
     P for QC-pred_symbol of k,
     r for Element of relations_on A;

definition let A, k, J, P;
  redefine func J.P -> Element of relations_on A;
end;

definition let A, J, p;
  func Valid(p,J) -> Element of Funcs(Valuations_in A, BOOLEAN) means
:: VALUAT_1:def 11
 ex F being Function of CQC-WFF,Funcs(Valuations_in A, BOOLEAN) st
    it = F.p &
    F.VERUM = (Valuations_in A --> TRUE) &
       for p,q being Element of CQC-WFF,
       x being bound_QC-variable, k being Nat,
       ll being CQC-variable_list of k,
       P being QC-pred_symbol of k holds
    F.(P!ll) = (ll 'in' (J.P)) &
    F.('not' p) = 'not'(F.p) &
    (F.(p '&' q)) = ((F.p) '&' (F.q)) &
    F.(All(x,p)) = (FOR_ALL(x,F.p));
end;

canceled 4;

theorem :: VALUAT_1:13
    Valid(VERUM,J) = Valuations_in A --> TRUE;

theorem :: VALUAT_1:14
   Valid(VERUM,J).v = TRUE;

theorem :: VALUAT_1:15
     Valid(P!ll,J) = ll 'in' (J.P);

theorem :: VALUAT_1:16
   p = P!ll & r = J.P implies (v*'ll in r iff Valid(p,J).v = TRUE);

theorem :: VALUAT_1:17
   p = P!ll & r = J.P implies (not (v*'ll in r) iff Valid(p,J).v = FALSE);

canceled;

theorem :: VALUAT_1:19
    Valid('not' p,J) = 'not' Valid(p,J);

theorem :: VALUAT_1:20
   Valid('not' p,J).v = 'not'(Valid(p,J).v);

theorem :: VALUAT_1:21
    Valid(p '&'q ,J) = Valid(p,J) '&' Valid(q,J);

theorem :: VALUAT_1:22
   Valid(p '&'q ,J).v = (Valid(p,J).v) '&' (Valid(q,J).v);

theorem :: VALUAT_1:23
    Valid(All(x,p),J) = FOR_ALL(x,Valid(p,J));

theorem :: VALUAT_1:24
   Valid(p '&' 'not' p,J).v = FALSE;

theorem :: VALUAT_1:25
     Valid('not'(p '&' 'not' p),J).v = TRUE;

definition
 let A, p, J, v;
  pred J,v |= p means
:: VALUAT_1:def 12
 Valid(p,J).v = TRUE;
end;

canceled;

theorem :: VALUAT_1:27
    J,v |= P!ll iff (ll 'in' (J.P)).v = TRUE;

theorem :: VALUAT_1:28
    J,v |= 'not' p iff not J,v |= p;

theorem :: VALUAT_1:29
    J,v |= (p '&' q) iff J,v |= p & J,v |= q;

theorem :: VALUAT_1:30
   J,v |= All(x,p) iff FOR_ALL(x,Valid(p,J)).v = TRUE;

theorem :: VALUAT_1:31
   J,v |= All(x,p) iff
        for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE;

 theorem :: VALUAT_1:32
     Valid('not' 'not' p,J) = Valid(p,J);

theorem :: VALUAT_1:33
  Valid(p '&' p,J) = Valid(p,J);

canceled;

theorem :: VALUAT_1:35
  J,v |= p => q iff
          Valid(p, J).v = FALSE or Valid(q, J).v = TRUE;

theorem :: VALUAT_1:36
   J,v |= p => q iff (J,v |= p implies J,v |= q);

theorem :: VALUAT_1:37
   for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
         FOR_ALL(x,p).v = TRUE implies p.v = TRUE;

definition
 let A, J, p;
  pred J |= p means
:: VALUAT_1:def 13
 for v holds J,v |= p;
end;

reserve u,w,z for Element of BOOLEAN;

reserve w,v2 for Element of Valuations_in A,
        z for bound_QC-variable;

scheme Lambda_Val {A() -> non empty set, Y, Z() -> bound_QC-variable,
                     V1, V2() -> Element of Valuations_in A()}:
 ex v being Element of Valuations_in A() st
  (for x being bound_QC-variable st x <> Y() holds v.x = V1().x) &
                                                 v.Y() = V2().Z();

canceled;

theorem :: VALUAT_1:39

  not x in still_not-bound_in p implies
    for v,w st for y st x<>y holds w.y = v.y holds Valid(p,J).v = Valid(p,J).w;

theorem :: VALUAT_1:40

  J,v |= p & not x in still_not-bound_in p implies
     for w st for y st x<>y holds w.y = v.y holds J,w |= p;

theorem :: VALUAT_1:41

  J,v |= All(x,p) iff
   for w st for y st x<>y holds w.y = v.y holds J,w |= p;

reserve u,w for Element of Valuations_in A;
reserve s' for QC-formula;

theorem :: VALUAT_1:42

  x <> y & p = s'.x & q = s'.y implies for v st v.x = v.y holds
      Valid(p,J).v = Valid(q,J).v;

theorem :: VALUAT_1:43

  x <> y & not x in still_not-bound_in s' implies
    not x in still_not-bound_in (s'.y);

theorem :: VALUAT_1:44
   J,v |= VERUM;

theorem :: VALUAT_1:45
   J,v |= p '&' q => q '&' p;

theorem :: VALUAT_1:46
   J,v |= ('not' p => p) => p;

theorem :: VALUAT_1:47
   J,v |= p => ('not' p => q);

theorem :: VALUAT_1:48
   J,v |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t));

theorem :: VALUAT_1:49
    J,v |= p & J,v |= (p => q) implies J,v |= q;

theorem :: VALUAT_1:50
   J,v |= All(x,p) => p;


theorem :: VALUAT_1:51
    J |= VERUM;

theorem :: VALUAT_1:52
    J |= p '&' q => q '&' p;

theorem :: VALUAT_1:53
    J |= ('not' p => p) => p;

theorem :: VALUAT_1:54
    J |= p => ('not' p => q);

theorem :: VALUAT_1:55
    J |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t));

theorem :: VALUAT_1:56
    J |= p & J |= (p => q) implies J |= q;

theorem :: VALUAT_1:57
    J |= All(x,p) => p;

theorem :: VALUAT_1:58
    (J |= p => q) & not x in still_not-bound_in p implies J |= p => All(x,q);

theorem :: VALUAT_1:59
    for s being QC-formula st p = s.x & q = s.y & not x in still_not-bound_in s
&
   J |= p holds J |= q;
The abstract of the Mizar article:

Interpretation and Satisfiability in the First Order Logic
