:: The canonical formulae
::  by Andrzej Trybulec
::
:: Received July 4, 2000
:: Copyright (c) 2000-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 INT_1, ABIAN, ARYTM_1, ZFMISC_1, FUNCT_1, RELAT_1, TARSKI,
      FUNCOP_1, FUNCT_2, FUNCT_6, XBOOLE_0, PBOOLE, SUBSET_1, NUMBERS, NAT_1,
      HILBERT1, CARD_1, FUNCT_3, CARD_3, MCART_1, PARTFUN1, FINSEQ_4, XBOOLEAN,
      QC_LANG1, HILBERT2, FUNCT_5, ARYTM_3, FUNCT_4, XXREAL_0, HILBERT3,
      XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      INT_1, RELAT_1, FUNCT_1, PBOOLE, CARD_1, CARD_3, ABIAN, PARTFUN1,
      FUNCT_2, BINOP_1, XXREAL_0, FUNCT_3, FUNCOP_1, FUNCT_4, FUNCT_5, FUNCT_6,
      PRALG_1, PRALG_2, MSUALG_3, HILBERT1, HILBERT2;
 constructors XXREAL_0, NAT_D, ABIAN, CAT_2, PRALG_1, PRALG_2, MSUALG_3,
      HILBERT2, RELSET_1, FUNCT_5, FUNCT_4;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
      FUNCT_2, FUNCOP_1, FUNCT_4, NUMBERS, XREAL_0, INT_1, PBOOLE, ABIAN,
      HILBERT1, RELSET_1, ZFMISC_1, MSSUBFAM, CARD_1;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

registration
  let m,n be non zero Nat;
  cluster (0,n)-->(m,0) -> one-to-one;
  cluster (n,0)-->(0,m) -> one-to-one;
end;

theorem :: HILBERT3:1
  for i being Integer holds i is even iff i-1 is odd;

theorem :: HILBERT3:2
  for i being Integer holds i is odd iff i-1 is even;

theorem :: HILBERT3:3
  for X being trivial set, x being set st x in X for f being
  Function of X,X holds x is_a_fixpoint_of f;

::$CT

theorem :: HILBERT3:5
  for A,B,x being set, f being Function st x in A & f in Funcs(A,B)
  holds f.x in B;

theorem :: HILBERT3:6
  for A,B,C being set st C = {} implies B = {} or A = {}
  for f being Function of A, Funcs(B,C) holds doms f = A --> B;

reserve n for Element of NAT,
  p,q,r,s for Element of HP-WFF;

theorem :: HILBERT3:7
  for x being set holds {}.x = {};

theorem :: HILBERT3:8
  for X being set, A being Subset of X holds
  ((0,1) --> (1,0))*chi(A,X) = chi(A`,X);

theorem :: HILBERT3:9
  for X being set, A being Subset of X holds
  ((0,1) --> (1,0))*chi(A`,X) = chi(A,X);

theorem :: HILBERT3:10
  for a,b,x,y,x9,y9 being set st a <> b &
  (a,b) --> (x,y) = (a,b) --> (x9,y9) holds x = x9 & y = y9;

theorem :: HILBERT3:11
  for a,b,x,y,X,Y being set st a<>b & x in X & y in Y holds
  (a,b) --> (x,y) in product((a,b) --> (X,Y));

theorem :: HILBERT3:12
  for D being non empty set for f being Function of 2, D ex d1,d2
  being Element of D st f = (0,1) --> (d1,d2);

theorem :: HILBERT3:13
  for a,b,c,d being set st a <> b holds
  ((a,b) --> (c,d)) * ((a,b)--> (b,a)) = (a,b) --> (d,c);

theorem :: HILBERT3:14
  for a,b,c,d being set, f being Function st a <> b & c in dom f &
  d in dom f holds f*((a,b) --> (c,d)) = (a,b) --> (f.c,f.d);

theorem :: HILBERT3:15
  (0,1) --> (1,0) is Permutation of 2;

begin :: the Cartesian product of functions and the Frege function

registration
  let f,g be one-to-one Function;
  cluster [:f,g:] -> one-to-one;
end;

theorem :: HILBERT3:16
  for A,B being non empty set, C,D being set,
      f being Function of C,A,
      g being Function of D,B holds pr1(A,B)*[:f,g:] = f*pr1(C,D);

theorem :: HILBERT3:17
  for A,B being non empty set, C,D being set, f being Function of C,A,
      g being Function of D,B holds pr2(A,B)*[:f,g:] = g*pr2(C,D);

theorem :: HILBERT3:18
  for g being Function holds ({})..g = {};

theorem :: HILBERT3:19
  for f being Function-yielding Function, g,h being Function
    st dom f = dom g holds (f..g)*h = (f*h)..(g*h);

theorem :: HILBERT3:20
  for C being set, A being non empty set
  for f being Function of A,Funcs({} qua set,C),
      g being Function of A,{} holds rng (f..g) = {};

theorem :: HILBERT3:21
  for A,B,C being set st (B = {} implies A = {}) & (C = {} implies B = {})
  for f being Function of A, Funcs(B,C),
      g being Function of A,B holds rng(f..g) c= C;

theorem :: HILBERT3:22
  for A,B,C being set st C = {} implies B = {} or A = {}
  for f being Function of A, Funcs(B,C) holds dom Frege f = Funcs(A,B);

theorem :: HILBERT3:23
  for A,B,C being set st C = {} implies B = {} or A = {}
  for f being Function of A, Funcs(B,C) holds rng Frege f c= Funcs(A,C);

theorem :: HILBERT3:24
  for A,B,C being set st C = {} implies B = {} or A = {}
  for f being Function of A, Funcs(B,C) holds
    Frege f is Function of Funcs(A,B), Funcs(A,C);

begin :: about permutations

registration
  let A,B be set, P be Permutation of A, Q be Permutation of B;
  cluster [:P,Q:] -> bijective for Function of [:A,B:],[:A,B:];
end;

theorem :: HILBERT3:25
  for A,B being set, P being Permutation of A, Q being Permutation of B holds
  [:P,Q:] is bijective;

definition
  let A,B be non empty set;
  let P be Permutation of A, Q be Function of B,B;
  func P => Q -> Function of Funcs(A,B), Funcs(A,B) means
:: HILBERT3:def 1

  for f being Function of A,B holds it.f = Q*f*P";
end;

registration
  let A,B be non empty set;
  let P be Permutation of A, Q be Permutation of B;
  cluster P => Q -> bijective;
end;

theorem :: HILBERT3:26
  for A,B being non empty set for P being Permutation of A,
      Q being Permutation of B for f being Function of A,B holds
    (P => Q)".f = Q"*f*P;

theorem :: HILBERT3:27
  for A,B being non empty set for P being Permutation of A,
      Q being Permutation of B holds (P => Q)" = P" => (Q");

theorem :: HILBERT3:28
  for A,B,C being non empty set, f being Function of A, Funcs(B,C),
      g being Function of A,B,
      P being Permutation of B, Q being Permutation of C
  holds ((P => Q)*f)..(P*g) = Q*(f..g);

begin ::  set valuations

definition
  mode SetValuation is non-empty ManySortedSet of NAT;
end;

reserve V for SetValuation;

definition
  let V;
  func SetVal V -> ManySortedSet of HP-WFF means
:: HILBERT3:def 2

  it.VERUM = 1 & (for n holds it.prop n = V.n) &
  for p,q holds it.(p '&' q) = [:it.p, it.q:] & it.(p =>q) = Funcs(it.p,it.q);
end;

definition
  let V,p;
  func SetVal(V,p) -> set equals
:: HILBERT3:def 3
  (SetVal V).p;
end;

registration
  let V,p;
  cluster SetVal(V,p) -> non empty;
end;

theorem :: HILBERT3:29
  SetVal(V,VERUM) = 1;

theorem :: HILBERT3:30
  SetVal(V,prop n) = V.n;

theorem :: HILBERT3:31
  SetVal(V,p '&' q) = [:SetVal(V,p), SetVal(V,q):];

theorem :: HILBERT3:32
  SetVal(V,p => q) = Funcs(SetVal(V,p),SetVal(V,q));

registration
  let V,p,q;
  cluster SetVal(V,p => q) -> functional;
end;

registration
  let V,p,q,r;
  cluster -> Function-yielding for Element of SetVal(V,p => (q => r));
end;

registration
  let V,p,q,r;
  cluster Function-yielding for Function of SetVal(V,p => q),SetVal(V,p => r);
  cluster Function-yielding for Element of SetVal(V,p => (q => r));
end;

begin :: permuting set valuations

definition
  let V;
  mode Permutation of V -> Function means
:: HILBERT3:def 4

  dom it = NAT & for n holds it .n is Permutation of V.n;
end;

reserve P for Permutation of V;

definition
  let V,P;
  func Perm P -> ManySortedFunction of SetVal V, SetVal V means
:: HILBERT3:def 5

  it.VERUM = id 1 & (for n holds it.prop n = P.n) &
  for p,q ex p9 being Permutation of SetVal(V,p),
      q9 being Permutation of SetVal(V,q) st p9 = it.p & q9 = it.q &
  it.(p '&' q) = [:p9,q9:] & it.(p => q) = p9 => q9;
end;

definition
  let V,P,p;
  func Perm(P,p) -> Function of SetVal(V,p), SetVal(V,p) equals
:: HILBERT3:def 6
  (Perm P).p;
end;

theorem :: HILBERT3:33
  Perm(P,VERUM) = id SetVal(V,VERUM);

theorem :: HILBERT3:34
  Perm(P,prop n) = P.n;

theorem :: HILBERT3:35
  Perm(P,p '&' q) = [:Perm(P,p),Perm(P,q):];

theorem :: HILBERT3:36
  for p9 being Permutation of SetVal(V,p), q9 being Permutation of
SetVal(V,q) st p9 = Perm(P,p) & q9 = Perm(P,q) holds Perm(P,p => q) = p9 => q9;

registration
  let V,P,p;
  cluster Perm(P,p) -> bijective;
end;

theorem :: HILBERT3:37
  for g being Function of SetVal(V,p), SetVal(V,q) holds Perm(P,p
  => q).g = Perm(P,q)*g*Perm(P,p)";

theorem :: HILBERT3:38
  for g being Function of SetVal(V,p), SetVal(V,q) holds Perm(P,p
  => q)".g = Perm(P,q)"*g*Perm(P,p);

theorem :: HILBERT3:39
  for f,g being Function of SetVal(V,p), SetVal(V,q) st f = Perm(P
  ,p => q).g holds Perm(P,q)*g = f*Perm(P,p);

theorem :: HILBERT3:40
  for V for P being Permutation of V for x being set st x
is_a_fixpoint_of Perm(P,p) for f being Function st f is_a_fixpoint_of Perm(P,p
  => q) holds f.x is_a_fixpoint_of Perm(P,q);

begin :: canonical formulae

definition
  let p;
  attr p is canonical means
:: HILBERT3:def 7
  for V ex x being set st for P being Permutation of V holds
  x is_a_fixpoint_of Perm(P,p);
end;

registration
  cluster VERUM -> canonical;
end;

registration
  let p,q;
  cluster p => (q => p) -> canonical;
  cluster (p '&' q) => p -> canonical;
  cluster (p '&' q) => q -> canonical;
  cluster p => (q => (p '&' q)) -> canonical;
end;

registration
  let p,q,r;
  cluster (p => (q => r)) => ((p => q) => (p => r)) -> canonical;
end;

theorem :: HILBERT3:41
  p is canonical & p => q is canonical implies q is canonical;

theorem :: HILBERT3:42
  p in HP_TAUT implies p is canonical;

registration
  cluster canonical for Element of HP-WFF;
end;

begin :: pseudo-canonical formulae

definition
  let p;
  attr p is pseudo-canonical means
:: HILBERT3:def 8
  for V for P being Permutation of V
  ex x being set st x is_a_fixpoint_of Perm(P,p);
end;

registration
  cluster canonical -> pseudo-canonical for Element of HP-WFF;
end;

theorem :: HILBERT3:43
  p is pseudo-canonical & p => q is pseudo-canonical implies
  q is pseudo-canonical;

theorem :: HILBERT3:44
  for p,q for V for P being Permutation of V st (ex f being set st
f is_a_fixpoint_of Perm(P,p)) & not (ex f being set st f is_a_fixpoint_of Perm(
  P,q)) holds p => q is not pseudo-canonical;

theorem :: HILBERT3:45
  for a, b being Element of NAT st a <> b holds
  (prop a) => (prop b) => (prop a) => (prop a) is non pseudo-canonical;