:: Interpretation and Satisfiability in the First Order Logic
::  by Edmund Woronowicz
::
:: Received June 1, 1990
:: 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 SUBSET_1, NUMBERS, XBOOLE_0, FUNCT_2, QC_LANG1, FUNCT_1, RELAT_1,
      TARSKI, MARGREL1, XBOOLEAN, CQC_LANG, ARYTM_3, FINSEQ_1, NAT_1, XXREAL_0,
      ZF_LANG, FUNCOP_1, REALSET1, BVFUNC_2, ZF_MODEL, ZF_LANG1, QC_LANG3,
      CARD_1, CLASSES2, VALUAT_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
      FUNCT_2, FUNCT_7, NAT_1, FINSEQ_1, FUNCOP_1, QC_LANG1, QC_LANG3,
      CQC_LANG, MARGREL1, XXREAL_0;
 constructors XXREAL_0, MEMBERED, MARGREL1, QC_LANG3, CQC_LANG, FUNCOP_1,
      RELSET_1, FUNCT_7, NUMBERS;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, MARGREL1, QC_LANG1, CQC_LANG,
      XXREAL_0, FUNCT_2, ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE;


begin

reserve Al for QC-alphabet;
reserve i,j,k for Nat,
  A,D for non empty set;

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

registration
  let Al,A;
  cluster Valuations_in(Al,A) -> non empty functional;
end;

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

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

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

definition
  let Al, A, x;
  let p be Element of Funcs(Valuations_in(Al,A),BOOLEAN);
  func FOR_ALL(x,p) -> Element of Funcs(Valuations_in(Al,A),BOOLEAN) means
:: VALUAT_1:def 2

for v holds it.v =
   ALL{p.v9 where v9 is Element of Valuations_in(Al,A) :
       for y st x <> y holds v9.y = v.y};
end;

theorem :: VALUAT_1:2
  for p being Element of Funcs(Valuations_in(Al,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:3
  for p being Element of Funcs(Valuations_in(Al,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,Al;

notation
  let Al, A, k, ll, v;
  synonym v*'ll for v*ll;
end;

definition
  let Al;
  let A, k, ll, v;
  redefine func v*'ll -> FinSequence of A means
:: VALUAT_1:def 3

  len it = k & for i be Nat st
  1 <= i & i <= k holds it.i = v.(ll.i);
end;

definition
  let Al;
  let A, k, ll;
  let r be Element of relations_on A;
  func ll 'in' r -> Element of Funcs(Valuations_in(Al,A),BOOLEAN) means
:: VALUAT_1:def 4

  for
  v being Element of Valuations_in(Al,A) holds
   (v*'ll in r iff it.v = TRUE) & (not v*'ll in r iff it.v = FALSE);
end;

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

definition
  let Al, D;
  mode interpretation of Al,D -> Function of QC-pred_symbols(Al),
                                             relations_on D
    means
:: VALUAT_1:def 5
    for P being (Element of QC-pred_symbols(Al)),
    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(Al),
  J for interpretation of Al,A,
  P for QC-pred_symbol of k,Al,
  r for Element of relations_on A;

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

definition
  let Al, A, J, p;
  func Valid(p,J) -> Element of Funcs(Valuations_in(Al,A), BOOLEAN) means
:: VALUAT_1:def 6

ex F being Function of CQC-WFF(Al),Funcs(Valuations_in(Al,A), BOOLEAN)
st it = F.p & F.VERUM(Al) = Valuations_in(Al,A) --> TRUE &
for p,q being Element of CQC-WFF(Al), x being bound_QC-variable of Al,
k being Nat, ll being CQC-variable_list of k,Al, P
  being QC-pred_symbol of k,Al 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;

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

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

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

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

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

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

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

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

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

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

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

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

definition
  let Al, A, p, J, v;
  pred J,v |= p means
:: VALUAT_1:def 7

  Valid(p,J).v = TRUE;
end;

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

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

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

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

theorem :: VALUAT_1:20
  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:21
  Valid('not' 'not' p,J) = Valid(p,J);

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

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

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

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

definition
  let Al, A, J, p;
  pred J |= p means
:: VALUAT_1:def 8

  for v holds J,v |= p;
end;

reserve u,w,z for Element of BOOLEAN;

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

theorem :: VALUAT_1:26
  for A be non empty set, Y, Z be bound_QC-variable of Al,
   V1, V2 be Element of Valuations_in(Al,A)
  ex v being Element of Valuations_in(Al,A) st
   (for x being bound_QC-variable of Al st x <> Y holds v.x = V1.x) &
   v.Y = V2.Z;

theorem :: VALUAT_1:27
  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:28
  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:29
  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(Al,A);
reserve s9 for QC-formula of Al;

theorem :: VALUAT_1:30
  x <> y & p = s9.x & q = s9.y implies for v st v.x = v.y holds
  Valid(p,J).v = Valid(q,J).v;

theorem :: VALUAT_1:31
  x <> y & not x in still_not-bound_in s9 implies not x in
  still_not-bound_in (s9.y);

theorem :: VALUAT_1:32
  J,v |= VERUM(Al);

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

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

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

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

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

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

theorem :: VALUAT_1:39
  J |= VERUM(Al);

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

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

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

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

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

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

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

theorem :: VALUAT_1:47
  for s being QC-formula of Al st p = s.x & q = s.y & not x in
  still_not-bound_in s & J |= p holds J |= q;