HILBERT4

:: Pseudo-canonical Formulae are Classical
::  by Marco B. Caminati and Artur Korni{\l}owicz
:: 
:: Received May 25, 2014
:: Copyright (c) 2014-2026 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 TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1,
      FUNCT_1, XCMPLX_0, PARTFUN1, PBOOLE, FUNCT_4, OPOSET_1, FUNCOP_1,
      FOMODEL0, MCART_1, ABIAN, HILBERT1, HILBERT2, HILBERT3, XBOOLEAN,
      QC_LANG1, FUNCT_2, CARD_1, RELAT_2, HILBERT4;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, RELAT_1,
      FUNCT_1, RELSET_1, PARTFUN1, XXREAL_0, PBOOLE, FUNCT_4, PARTIT_2,
      XTUPLE_0, HILBERT1, HILBERT2, FUNCT_2, ABIAN, HILBERT3, FUNCT_3,
      DOMAIN_1, RELAT_2, XCMPLX_0, FUNCOP_1, BINOP_1, FOMODEL0;
 constructors SETFAM_1, FUNCT_4, PARTIT_2, BORSUK_7, ABIAN, HILBERT1, HILBERT2,
      FUNCT_2, MSUALG_3, RELAT_2, HILBERT3, FOMODEL0, NAT_D, FUNCT_3, RELSET_1,
      BINOP_1;
 registrations FOMODEL0, HILBERT3, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1,
      RELAT_1, RELAT_2, RELSET_1, SUBSET_1, XBOOLE_0, XTUPLE_0, ZFMISC_1,
      CARD_1;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, ABIAN, PARTIT_2, FUNCT_1;
 equalities BINOP_1, RELAT_1, FOMODEL0, FUNCOP_1, FUNCT_4, HILBERT3;
 expansions RELAT_1;
 theorems TARSKI, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1, XBOOLE_1, XBOOLE_0,
      XTUPLE_0, PARTFUN1, FUNCOP_1, PARTIT_2, ABIAN, HILBERT3, CARD_1, FUNCT_3,
      GRFUNC_1, FUNCT_4, ORDINAL1, PBOOLE, FOMODEL0;
 schemes ALTCAT_2, HILBERT2, FOMODEL0;

begin ::# Preliminaries about injectivity, involutiveness, fixpoints

set sw = (0,1)-->(1,0);
set I = id 1;

reserve
   a,b,c,x,y,z,A,B,C,X,Y for set,
   f,g for Function,
   V for SetValuation,
   P for Permutation of V,
   p,q,r,s for Element of HP-WFF,
   n for Element of NAT;

registration
  let X,Y;
  let f be Relation of X,Y;
  reduce (id X) * f to f;
  reducibility
  proof
    dom f c= X;
    hence (id X)*f = f by RELAT_1:51;
  end;
  reduce f * (id Y) to f;
  reducibility
  proof
    rng f c= Y;
    hence thesis by RELAT_1:53;
  end;
end;

theorem Th4:
  for f,g being one-to-one Function st f" = g" holds f = g
  proof
    let f,g be one-to-one Function;
    f"" = f & g"" = g by FUNCT_1:43;
    hence thesis;
  end;

registration
  cluster involutive for Function;
  existence
  proof
    take id 1;
    thus thesis;
  end;
  let A;
  cluster involutive for Permutation of A;
  existence
  proof
    take id A;
    thus thesis;
  end;
end;

theorem Th7:
  for f being involutive Function st rng f c= dom f holds
  f*f = id dom f
  proof
    let f be involutive Function;
    assume rng f c= dom f;
    then
A1: dom(f*f) = dom id dom f by RELAT_1:27;
    now
      let x be object;
      assume
A2:   x in dom(f*f);
      hence (f*f).x = f.(f.x) by FUNCT_1:12
      .= x by A1,A2,PARTIT_2:def 2
      .= (id dom f).x by A1,A2,FUNCT_1:18;
    end;
    hence thesis by A1, FUNCT_1:2;
  end;

theorem Th8:
  for f being Function st f*f = id dom f holds f is involutive
  proof
    let f be Function such that
A1: f*f = id dom f;
    let x be set;
    assume
A2: x in dom f;
    hence f.(f.x) = (f*f).x by FUNCT_1:13
    .= x by A1,A2,FUNCT_1:18;
  end;

theorem Th9:
  for f being involutive Function of A,A holds f*f = id A
  proof
    let f be involutive Function of A,A;
A1: dom f = A by FUNCT_2:52;
    then rng f c= dom f;
    hence thesis by A1,Th7;
  end;

theorem Th10:
  for f being Function of A,A st f*f = id A holds f is involutive
  proof
    let f be Function of A,A;
    dom f = A by FUNCT_2:52;
    hence thesis by Th8;
  end;

registration
  cluster involutive -> one-to-one for Function;
  coherence
  proof
    let f be Function;
    assume
A1: f is involutive;
    let x1,x2 be object;
    assume x1 in dom f & x2 in dom f;
    then f.(f.x1) = x1 & f.(f.x2) = x2 by A1,PARTIT_2:def 2;
    hence thesis;
  end;
end;

registration
  let A;
  let f be involutive Permutation of A;
  cluster f" -> involutive;
  coherence
  proof
    set h = f";
    h" = f by FUNCT_1:43;
    then (h*h)" = f*f by FUNCT_1:44
    .= id A by Th9
    .= (id A)" by FUNCT_1:45;
    hence thesis by Th4,Th10;
  end;
end;

registration
  let n be non zero Nat;
  cluster (0,n) --> (n,0) -> without_fixpoints;
  coherence
  proof
    set f = (0,n) --> (n,0);
    assume f is with_fixpoint;
    then consider x being object such that
A1: x is_a_fixpoint_of f by ABIAN:def 5;
A2: x in dom f by A1,ABIAN:def 3;
A3: f.x = x by A1,ABIAN:def 3;
    dom f = {0,n} by FUNCT_4:62;
    then x = 0 or x = n by A2,TARSKI:def 2;
    hence contradiction by A3,FUNCT_4:63;
  end;
end;

registration
  let n be non zero Nat, z be zero Nat;
  cluster fixpoints ((z,n) --> (n,z)) -> empty;
  coherence;
end;

registration
  let X be non empty set;
  cluster non empty involutive for Permutation of X;
  existence proof take id X; thus thesis; end;
end;

registration
  let A,B;
  let f be involutive Function of A,A;
  let g be involutive Function of B,B;
  cluster [:f,g:] -> involutive;
  coherence
  proof
    let x;
    set h = [:f,g:];
A1: dom h = [:dom f,dom g:] by FUNCT_3:def 8;
    assume x in dom h;
    then consider a,b being object such that
A2: a in dom f and
A3: b in dom g and
A4: x = [a,b] by A1,ZFMISC_1:def 2;
A5: f.(f.a) = a & g.(g.b) = b by A2,A3,PARTIT_2:def 2;
A6: dom f = A & dom g = B by FUNCT_2:52;
A7: f.a in rng f & g.b in rng g by A2,A3,FUNCT_1:def 3;
    h.(a,b) = [f.a,g.b] by A2,A3,FUNCT_3:def 8;
    hence h.(h.x) = h.(f.a,g.b) by A4
    .= x by A4,A5,A6,A7,FUNCT_3:def 8;
  end;
end;

registration
  let A,B be non empty set;
  let f be involutive Permutation of A, g be involutive Permutation of B;
  cluster f => g -> involutive;
  coherence
  proof
    set h = f=>g;
    let x be Element of Funcs(A,B);
A1: f"*f" = id A & g*g = id B by Th9;
    thus h.(h.x) = h.(g*x*f") by HILBERT3:def 1
    .= g*(g*x*f")*f" by HILBERT3:def 1
    .= g*(g*x)*f"*f" by RELAT_1:36
    .= g*g*x*f"*f" by RELAT_1:36
    .= x*id A by A1,RELAT_1:36
    .= x;
  end;
end;

begin ::# Facts about Perm's fixed points

theorem Th14:
  x is_a_fixpoint_of Perm(P,q) implies
  SetVal(V,p) --> x is_a_fixpoint_of Perm(P,p=>q)
  proof
    assume
A1: x is_a_fixpoint_of Perm(P,q);
    set F = SetVal(V,p) --> x;
A2: dom Perm(P,p=>q) = SetVal(V,p=>q) by FUNCT_2:def 1;
A3: SetVal(V,p=>q) = Funcs(SetVal(V,p),SetVal(V,q)) by HILBERT3:32;
    x in dom Perm(P,q) by A1,ABIAN:def 3;
    then
A4: F is Function of SetVal(V,p),SetVal(V,q) by FUNCOP_1:46;
    hence
A5: F in dom Perm(P,p=>q) by A2,A3,FUNCT_2:8;
A6: Perm(P,p=>q) = Perm(P,p)=>Perm(P,q) by HILBERT3:36;
    Perm(P,p=>q).F in SetVal(V,p=>q) by A5,FUNCT_2:5;
    then
A7: dom (Perm(P,p=>q).F) = SetVal(V,p) by A3,FUNCT_2:92;
    now
      let z be object such that
A8:   z in dom (Perm(P,p=>q).F);
      (Perm(P,p)=>Perm(P,q)).F =
      Perm(P,q)*F*Perm(P,p)" by A4,HILBERT3:def 1;
      hence Perm(P,p=>q).F.z = (Perm(P,q)*F).((Perm(P,p)").z)
      by A6,A8,FUNCT_1:12
      .= Perm(P,q).(F.(Perm(P,p)".z)) by A7,A8,FUNCT_2:5,15
      .= Perm(P,q).x by A7,A8,FUNCT_2:5,FUNCOP_1:7
      .= x by A1,ABIAN:def 3;
    end;
    hence thesis by A7,FUNCOP_1:11;
  end;

theorem Lm2:
  Perm(P,q) is with_fixpoint implies Perm(P,p=>q) is with_fixpoint
  proof
    given x being object such that
A1: x is_a_fixpoint_of Perm(P,q);
    reconsider xx=x as set by TARSKI:1;
    take SetVal(V,p) --> xx;
    thus thesis by A1,Th14;
  end;

theorem Lm3:
  Perm(P,p) is with_fixpoint & Perm(P,q) is without_fixpoints implies
  Perm(P,p=>q) is without_fixpoints
  proof
    given x1 being object such that
A1: x1 is_a_fixpoint_of Perm(P,p);
    reconsider xx1=x1 as set by TARSKI:1;
    assume
A2: for x2 being object holds not x2 is_a_fixpoint_of Perm(P,q);
    let x be object;
    assume
A3: x is_a_fixpoint_of Perm(P,p=>q);
A4: x in dom Perm(P,p=>q) by A3,ABIAN:def 3;
    SetVal(V,p=>q) = Funcs(SetVal(V,p),SetVal(V,q)) by HILBERT3:32;
    then consider f being Function such that
A5: x = f and
    dom f = SetVal(V,p) & rng f c= SetVal(V,q) by A4,FUNCT_2:def 2;
    f.xx1 is_a_fixpoint_of Perm(P,q) by A3,A1,A5,HILBERT3:40;
    hence contradiction by A2;
  end;

begin
::# Axiom of choice in functional form via Fr\{ae}nkel operator
::# It is used to arbitrarily partition the field of a function f
::# into three parts, one of which is made of the fixpoints.
::# We will use this construction in Lm100 for the case of f
::# being a permutation, hence some elementary properties are shown
::# for that case.

definition
  let X be set;
  func ChoiceOn X -> set equals
  {[x, the Element of x] where x is Element of X\{{}}: x in X\{{}}};
  coherence;
end;

registration
  let X be set;
  cluster ChoiceOn X -> Relation-like Function-like;
  coherence
  proof
    deffunc F(set) = the Element of $1;
    defpred P[set] means $1 in X\{{}};
    {[x,F(x)] where x is Element of X\{{}}:P[x]} is Function
    from FOMODEL0:sch 3;
    hence thesis;
  end;
end;

Lm9: (a in dom ChoiceOn X implies (ChoiceOn X).a in a)
& dom ChoiceOn X = X\{{}}
proof
set f=ChoiceOn X, E={{}}, LH=dom f, RH=X\E;
A1: x in LH implies (x in RH & f.x in x)
proof
  assume x in LH; then
  [x,f.x] in f by FUNCT_1:def 2; then
  consider x1 being Element of RH such that
  B0: [x,f.x]=[x1,the Element of x1] & x1 in RH;
  B1: x= [x1,the Element of x1]`1 by B0 .= x1;
  hence x in RH by B0; not x1 in {{}} by B0, XBOOLE_0:def 5; then
  reconsider xx1=x1 as non empty set by TARSKI:def 1;
  f.x=[x1,the Element of x1]`2 by B0 .= the Element of xx1;
  hence thesis by B1;
end;
hence a in LH implies f.a in a;
for x being object holds x in LH implies x in RH by A1; then
A2: LH c= RH by TARSKI:def 3;
now
  let x be object; assume AA: x in RH;
  reconsider xx = x as set by TARSKI:1;
  [x,the Element of xx] in f by AA;
  hence x in LH by XTUPLE_0:def 12;
end; then
RH c= LH by TARSKI:def 3; hence
LH=RH by XBOOLE_0:def 10, A2;
end;

definition
::# When f is a permutation, call each {x, f.x} a switchpair.
::# In that case, FieldCover
::# covers the permuted set with the set of (unordered) switchpairs.
  let f;
  func FieldCover f -> set equals
  {{x,f.x} where x is Element of dom f: x in dom f};
  coherence;
end;

definition
::# When f is a permutation, we arbitrarily choose one element of the
::# switchpair.
::# Except that we are avoiding fixpoints:
::# switchpairs become singletons
::# exactly in the case of fixpoints,
::# hence the latter never belong to SomePoints.
  let f;
  func SomePoints f -> set equals
  (field f) \ rng ChoiceOn FieldCover f;
  coherence;
end;

definition
::# Again, we restrict our comments to the case of f being a permutation.
::# Then, by construction, we are splitting its domain into three subsets:
::# that of fixpoints, and two arbitrary "halves"
::# (called SomePoints and OtherPoints) of the remaining points.
  let f;
  func OtherPoints f -> set equals
  ((field f) \ (fixpoints f)) \ (SomePoints f);
  coherence;
end;

registration
let g;
cluster (OtherPoints g) /\ SomePoints g -> empty;
coherence
proof
  set S=SomePoints g;
  ((field g\fixpoints g)\S)/\(S/\S)={}; hence thesis;
end;
end;

Lm23: f is involutive implies f.:SomePoints f c= OtherPoints f
proof
set F=FieldCover f,
A1=SomePoints f,
A2=OtherPoints f,
B1=f.:A1,
ch=ChoiceOn F,
A=dom f,
FP=fixpoints f;
B1 \ rng f = {} &
  A2 \+\ ((field f \FP qua Subset of field f) /\ rng ch)={}; then
B4: B1 c= rng f & A2= (field f \ FP) /\ rng ch by FOMODEL0:29;
assume
B2: f is involutive;
let y be object; assume
B3: y in B1; then
consider x being object such that
B0: x in A & x in A1 & y=f.x by FUNCT_1:def 6;
set X={x,f.x};
X in F & not X in {{}} by B0; then
X in F\{{}} by XBOOLE_0:def 5; then
B1: X in dom ch by Lm9; then
ch.X in rng ch & not x in rng ch by B0, XBOOLE_0:def 5, FUNCT_1:def 3;
then ch.X <> x & ch.X in X by B1, Lm9; then
ch.X=y & x<>f.x & f.y=x by B0, B2, TARSKI:def 2, PARTIT_2:def 2; then
y in rng ch & not y is_a_fixpoint_of f by B1, FUNCT_1:def 3, ABIAN:def 3; then
y in rng ch & y in rng f null dom f & not y in FP by FOMODEL0:69, B3, B4; then
y in (field f \ FP) & y in rng ch by XBOOLE_0:def 5;
hence y in A2 by B4, XBOOLE_0:def 4;
end;

Lm24: f is involutive implies f.:OtherPoints f c= SomePoints f
proof
set F=FieldCover f,
S=SomePoints f,
O=OtherPoints f,
ch=ChoiceOn F,
A=field f,
FP=fixpoints f,
E={{}};
assume
B5: f is involutive;
let y be object;
assume
B7: y in f.:O; then
consider x being object such that
B0: x in dom f & x in O & y=f.x by FUNCT_1:def 6;
reconsider xx=x as set by TARSKI:1;
f.:O \ rng f = {}; then
f.:O c= rng f & rng f null dom f c= A by FOMODEL0:29; then
B8: y in A by B7, TARSKI:def 3;
O \+\ (A\FP)/\rng ch={}; then
B66: x in (A\FP) /\ rng ch by B0, FOMODEL0:29;
consider X1 being object such that
B1: X1 in dom ch & x=ch.X1 by B66, FUNCT_1:def 3;
X1 in F\E by B1, Lm9; then
X1 in F; then
consider x1 being Element of dom f such that
B2: X1={x1,f.x1} & x1 in dom f;
B3: {x,f.x}={x1,f.x1} by FOMODEL0:70, B5, B2,B1,Lm9;
f.x in rng ch implies x in FP
proof
  assume f.x in rng ch; then
  consider X2 being object such that
  C0: X2 in dom ch & f.x=ch.X2 by FUNCT_1:def 3;
  reconsider X22=X2 as set by TARSKI:1;
  X2 in F\E by C0, Lm9; then
  X2 in F; then
  consider x2 being Element of dom f such that
  C1: X2={x2,f.x2} & x2 in dom f;
  f.x in X22 by C0,Lm9; then
  ch.X1=ch.X2 by B3,B2,C1,FOMODEL0:71,B5,B0; then
  xx is_a_fixpoint_of f by C0, B0, B1, ABIAN:def 3; hence
  thesis by FOMODEL0:69;
end;
hence y in S by B0, B8, XBOOLE_0:def 5;
end;

Lm30: f is involutive & rng f c= dom f implies
(f.:OtherPoints f = SomePoints f & f.:SomePoints f = OtherPoints f)
proof
assume f is involutive; then
reconsider ff=f as involutive Function;
set D=dom ff,
C=rng ff,
S=SomePoints ff,
O=OtherPoints ff,
F=fixpoints ff,
I=id D;
reconsider g=ff*ff as Function-like Relation-like Subset of I by FOMODEL0:72;
assume rng f c= dom f; then
reconsider C as Subset of D;
C c= D & D null C c= field f; then
reconsider CC=C as Subset of field f;
set D2=dom g;
field ff=D null C; then
reconsider SS=S, OO=O as Subset of D;
C c= D; then
reconsider SSS=SS, OOO=OO as Subset of D2 by RELAT_1:27;
g=I|D2 by GRFUNC_1:23; then
g | SS = I | (SSS null D2) by RELAT_1:71; then
B0: g .: SS = I .: SS .= S;
g|OO = I|D2|OO by GRFUNC_1:23; then
g|OO = I|(OOO null D2) by RELAT_1:71; then
B1: g.:OO = I.:OO .= O;
ff.:(ff.:S) c= ff.:O by Lm23, RELAT_1:123; then
S c= ff.:O & ff.:O c= S by B0, Lm24, RELAT_1:126;
hence f.:OtherPoints f = SomePoints f by XBOOLE_0:def 10;
ff.:(ff.:O) c= ff.:S by Lm24, RELAT_1:123; then
O c= ff.:S & ff.:S c= O by B1, Lm23, RELAT_1:126;
hence thesis by XBOOLE_0:def 10;
end;

Lm25: g is involutive & field g \ fixpoints g<>{} &
rng g c= dom g implies SomePoints g <> {}
proof
assume g is involutive;
then reconsider gg=g as involutive Function;
set G=field gg,
F=fixpoints gg,
S=SomePoints gg,
O=OtherPoints gg;
assume
B0:field g\fixpoints g<>{}; then
reconsider G as non empty set;
reconsider X=G\F as non empty Subset of G by B0; assume
B2: rng g c= dom g;
assume SomePoints g={}; then
reconsider S as empty Subset of G; X\S<>{}; then
reconsider O as non empty Subset of G; gg.:S=O by B2, Lm30;
hence contradiction;
end;

Lm26: rng g \ dom g={} & g is involutive & field g \ fixpoints g<>{}
implies (SomePoints g <> {} & OtherPoints g <> {})
proof
assume rng g \ dom g={}; then
B0: rng g c= dom g by FOMODEL0:29; assume
B1: g is involutive & field g \ fixpoints g<>{}; hence
SomePoints g <> {} by Lm25, B0; then
g.:(OtherPoints g) <> {} by Lm30, B0, B1; hence
thesis;
end;

begin
::# Building the needed SetValuation (tohilbval), and the
::# needed permutation of it, called tohilbperm.
::# They are specifically built so to enjoy the right fixpoints properties
::# in order to prove the main theorem (Lm100).

definition
  let x;
  ::# Constructive definition of the object uniquely described by Lm17 & Lm18
  func x tohilb -> set equals
  (id 1) +*
  ([:1, Funcs(x,{}):] * [:Funcs(x,{}),{1}:]) +*
  ([:{1}, Funcs(x,{}):] * [:Funcs(x,{}),{0}:]);
  coherence;
end;

registration
let x;
cluster x tohilb -> Function-like Relation-like;
coherence;
end;

theorem Lm18: x<>{} implies x tohilb=id 1
proof
assume x<>{}; then
reconsider xx=x as non empty set;
xx tohilb=id 1;
hence thesis;
end;

theorem Lm17: {} tohilb = (0,1) --> (1,0)
proof
reconsider X=Funcs({},{}) as non empty set;
reconsider I=id 1 as 1-defined Function;
set f=[:1,X:]*[:X,{1}:],
g=[:{1},X:]*[:X,{0}:],
ff=1-->1,
gg={1}-->0;
B0: ff=f & gg=g by FOMODEL0:73;
I +* ff +* gg = sw by CARD_1:49;
hence thesis by B0;
end;

definition
  let v be Function;
  func v tohilbperm -> set equals
  the set of all [n, v.n tohilb] where n is Element of NAT;
  coherence;
end;

definition
  let v be Function;
  func v tohilbval -> set equals
  the set of all [n, dom (v.n tohilb)] where n is Element of NAT;
  coherence;
end;

defpred P [set] means not contradiction;

Lm15: for v being Function holds
v tohilbval is Function & v tohilbperm is Function &
(proj1 (v tohilbval)=NAT & proj1 (v tohilbperm)=NAT)
proof
let v be Function; set f=v tohilbval, g=v tohilbperm;
deffunc Ff (set)= dom (v.$1 tohilb); deffunc Fg (set) = v.$1 tohilb;
set ff={[n, Ff(n)] where n is Element of NAT:P[n]},
gg={[n, Fg(n)] where n is Element of NAT:P[n]},
N={n where n is Element of NAT:P[n]};
B10: ff is Function from FOMODEL0:sch 3; hence f is Function;
reconsider f as Function by B10;
B11: gg is Function from FOMODEL0:sch 3; hence g is Function;
reconsider g as Function by B11;
B0: f=ff;
BB2: dom f=N from ALTCAT_2:sch 2(B0);
B1: g=gg; dom g=N from ALTCAT_2:sch 2(B1);
hence thesis by BB2, FOMODEL0:74;
end;

registration let v be Function;
  cluster v tohilbval -> Function-like Relation-like;
  coherence by Lm15;
  cluster v tohilbperm -> Function-like Relation-like;
  coherence by Lm15;
  cluster v tohilbval -> NAT-defined;
  coherence by Lm15;
  cluster v tohilbval -> total;
  coherence
  proof
    dom (v tohilbval) = NAT by Lm15;
    hence thesis by PARTFUN1:def 2;
  end;
  cluster v tohilbperm -> NAT-defined;
  coherence by Lm15;
  cluster v tohilbperm -> total;
  coherence
  proof
    dom (v tohilbperm) = NAT by Lm15;
    hence thesis by PARTFUN1:def 2;
  end;
end;

Lm34: x is Nat implies
(g tohilbperm.x=g.x tohilb & (g tohilbval).x=dom (g.x tohilb))
proof
set fv=g tohilbval,
fp=g tohilbperm;
assume x is Nat; then
reconsider n=x as Element of NAT by ORDINAL1:def 12;
deffunc F(set)=(g.$1) tohilb;
B0: P[n];
B1: fp={[o,F(o)] where o is Element of NAT:P[o]};
fp.n=F(n) from ALTCAT_2:sch 3(B1,B0);
hence fp.x=g.x tohilb;
deffunc G(set)=dom F($1);
B2: fv={[o,G(o)] where o is Element of NAT:P[o]};
fv.n=G(n) from ALTCAT_2:sch 3(B2,B0);
hence thesis;
end;

registration
  let v be Function;
  cluster v tohilbval -> non-empty;
  coherence
proof
  set f=v tohilbval, D=dom f, C=rng f;
  assume not f is non-empty;
  then consider x being object such that
B0: x in D & {}=f.x by FUNCT_1:def 3;
  reconsider n=x as Element of NAT by B0;
  f.n=dom ((v.n)tohilb) by Lm34;
  hence contradiction by CARD_1:49, B0;
end;
end;

Lm37: x tohilb is symmetric & dom (x tohilb) = rng (x tohilb)
proof
set g=x tohilb;
per cases;
suppose
  C00: x<>{};
  then
  C0: g=I by Lm18;
  thus g is symmetric by C00;
  thus thesis by C0;
end;
suppose
  C1: x={};
  thus g is symmetric by C1, Lm17;
  dom sw={0,1} & rng sw={0,1} by FUNCT_4:62,64;
  hence thesis by C1, Lm17;
end;
end;

registration let x;
  cluster x tohilb -> symmetric;
  coherence by Lm37;
end;

definition
let v be Function;
redefine func v tohilbperm -> Permutation of v tohilbval;  :: redefines tohilbperm (HILBERT4, definition)
coherence
proof
set fP=v tohilbperm,
fV=v tohilbval;
B0: now
  dom fP \+\ NAT={};
  hence dom fP=NAT by FOMODEL0:29;
end;
now
  let n be Element of NAT;
  D0: fP.n=v.n tohilb & fV.n=dom (v.n tohilb) by Lm34; then
  reconsider y=fP.n as symmetric Function;
  dom y=fV.n & rng y=dom y by D0, Lm37; then
  y is onto Function of fV.n, fV.n by FOMODEL0:75;
  hence fP.n is Permutation of fV.n;
end;
hence thesis by HILBERT3:def 4, B0;
end;
end;

definition
  mode SetValuation0 is ManySortedSet of NAT;
end;

reserve v for SetValuation0;

registration
let p,v;
cluster Perm (v tohilbperm,p) -> involutive;
coherence
proof
set P=v tohilbperm,
V=v tohilbval,
fP=Perm P;
defpred P[set] means
for f being Function st f=fP.$1 holds f is involutive;
A0: P[VERUM] by HILBERT3:def 5;
A1: for n being Element of NAT holds P[prop n]
proof
  let n be Element of NAT;
  let f be Function;
  assume f=fP.prop n;
  then f=P.n by HILBERT3:def 5 .= v.n tohilb by Lm34;
  hence thesis;
end;
A2: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
  let r, s;
  set a=r '&' s,
  i=r => s,
  f=Perm(P,r),
  h=Perm(P,s),
  F=SetVal(V,r),
  H=SetVal(V,s);
  assume
  B1: P[r] & P[s];
  reconsider f as involutive Permutation of F by B1;
  reconsider h as involutive Permutation of H by B1;
  thus P[a]
  proof
    let g;
    assume g=fP.a; then
    g=Perm(P,a) .= [:f,h:] by HILBERT3:35;
    hence thesis;
  end;
  let F be Function;
  assume F=fP.i; then
  F=Perm(P,i) .= f => h by HILBERT3:36;
  hence thesis;
end;
for p holds P[p] from HILBERT2:sch 2(A0,A1,A2);
hence thesis;
end;
end;

begin
::# Classical semantics via SetVal0, an extension of SetVal.
::# Thus, we can state and prove the main result:
::# pseudo-canonical implies classical.

definition
  let V be SetValuation0;
  func SetVal0 V -> ManySortedSet of HP-WFF means
  :Def2:
  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);
  existence
  proof
    deffunc F(Element of NAT)=V.$1;
    consider M being ManySortedSet of HP-WFF such that
A1: ( M.VERUM = 1 & for n holds M.prop n = F(n) ) &
    for p,q holds M.(p '&' q) = [:M.p,M.q:] &
    M.(p => q) = Funcs(M.p,M.q)
    from HILBERT2:sch 4;
    take M;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let M1,M2 be ManySortedSet of HP-WFF such that
A2: M1.VERUM = 1 and
A3: for n holds M1.prop n = V.n and
A4: for p,q holds
    M1.(p '&' q) = [:M1.p, M1.q:] & M1.(p => q) = Funcs(M1.p,M1.q) and
A5: M2.VERUM = 1 and
A6: for n holds M2.prop n = V.n and
A7: for p,q holds
    M2.(p '&' q) = [:M2.p, M2.q:] & M2.(p => q) = Funcs(M2.p,M2.q);
    defpred P[Element of HP-WFF] means M1.$1 = M2.$1;
A8: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
    proof
      let r,s such that
A9:   M1.r=M2.r & M1.s = M2.s;
      thus M1.(r '&' s) = [:M2.r, M2.s:] by A4,A9
        .= M2.(r '&' s) by A7;
      thus M1.(r => s) = Funcs(M2.r,M2.s) by A4,A9
        .= M2.(r => s) by A7;
    end;
A10: for n holds P[prop n]
    proof
      let n;
      thus M1.prop n = V.n by A3
        .= M2.prop n by A6;
    end;
A11: P[VERUM] by A2,A5;
    for r holds P[r] from HILBERT2:sch 2(A11,A10,A8);
    then for r being object st r in HP-WFF holds M1.r = M2.r;
    hence M1 = M2 by PBOOLE:3;
  end;
end;

definition
  let v,p;
  func SetVal0(v,p) -> set equals
  (SetVal0 v).p;
  correctness;
end;

Lm100: fixpoints Perm(v tohilbperm,p) <> {} iff SetVal0(v,p) <> {}
proof
set V=v tohilbval,
P=v tohilbperm,
fP=Perm P,
fv=SetVal0 v,
fV=SetVal V,
I=id 1;
defpred Z[set] means fv.$1={} iff fixpoints (fP.$1)={};
A1: Z[VERUM]
proof
  fixpoints (fP.VERUM)=fixpoints I by HILBERT3:def 5 .= 1;
  hence thesis by Def2;
end;
A2: for n being Element of NAT holds Z[prop n]
proof
  let n be Element of NAT;
  set l=prop n,
  x=fv.n,
  X=fV.n;
  B0: fP.l=P.n & fv.l=v.n by Def2, HILBERT3:def 5;
  thus fv.l={} implies fixpoints (fP.l)={}
  proof
    assume fv.l={}; then
    P.n=sw by B0, Lm34, Lm17;
    hence thesis by B0;
  end;
  assume
  B1: fixpoints (fP.l)={};
  assume fv.l<>{}; then
  v.n<>{} & P.n=v.n tohilb by Def2, Lm34; then
  P.n=I by Lm18;
  hence contradiction by CARD_1:49,B1,B0;
end;
A3: for r, s st Z[r] & Z[s] holds Z[r '&' s] & Z[r => s]
proof
  let r,s;
  set a=r '&' s,
  i=r=>s;
  set F=SetVal(V,r),
  H=SetVal(V,s);
  set f=Perm(P,r),
  h=Perm(P,s);
  reconsider h as non empty involutive Permutation of H;
  reconsider ff=f" as non empty involutive Permutation of F;
  set S=SomePoints ff, O=OtherPoints ff;
  reconsider S,O as Subset of field ff;
  set f1=ff|S,
  f2=ff|O; assume
  B0: Z[r] & Z[s];
  reconsider Sr = SetVal0(v,r), Ss = SetVal0(v,s) as set;
  SetVal0(v,a)=[:Sr, Ss:] by Def2; then
  SetVal0(v,a)={} iff [:fixpoints Perm(P,r), fixpoints Perm(P,s):]={}
  by B0; then
  SetVal0(v,a)={} iff fixpoints [:Perm(P,r), Perm(P,s):]={}
  by FOMODEL0:76; then
  SetVal0(v,a)={} iff fixpoints Perm(P,a)={} by HILBERT3:35; hence
  fv.a={} iff fixpoints fP.a={};
  thus fv.i={} implies fixpoints(fP.i)={}
  proof
    assume fv.i={}; then
    {} = Funcs(fv.r, fv.s) by Def2; then
    f is with_fixpoint & h is without_fixpoints by B0; then
    Perm(P,i) is without_fixpoints by Lm3;
    hence thesis;
  end;
  assume
  B2: fixpoints (fP.i)={};
  assume
  B3: fv.i<>{};
  per cases;
  suppose
    fv.s<>{};then
    h is with_fixpoint by B0; then
    Perm(P,i) is with_fixpoint by Lm2;
    hence contradiction by B2;
  end;
  suppose
    CCCC20: fv.s={}; then
    Funcs(fv.r, fv.s)<>{} & fv.s={} by B3, Def2;
    then
    CC20: fv.s={} & fv.r={} & fixpoints ff \+\ fixpoints f ={};
    C00: dom ff=F & dom h=H & rng h c= H & rng ff c= F by PARTFUN1:def 2;
    C01: field ff=F null rng ff & field h=H null rng h by PARTFUN1:def 2;
    C0: dom ff=F & dom h=H & rng h c= H & rng ff c= F &
    field ff=F & field h=H & dom f1=S & dom f2=O &
    ff.:O=S & ff.:S=O & rng f1=ff.:S & rng f2=ff.:O by C00, C01, Lm30; then
    C2: rng f1 /\ rng f2={} & rng f1 = dom f2 & rng f2=dom f1;
    reconsider S,O as Subset of dom ff by PARTFUN1:def 2, C01;
    rng h \ dom h={} & field h \ fixpoints h<>{} by CCCC20, B0;
    then reconsider SH=SomePoints h, OH=OtherPoints h as non empty Subset
      of dom h by PARTFUN1:def 2, C01, Lm26;
    set b1=the Element of SH, b2=h.b1;
    b2 in h.:SH & h.:SH c= OH by Lm23, FUNCT_1:108; then
    b2 in OH & not b2 in OH/\SH; then
    C21: b1<>b2 by XBOOLE_0:def 4;
    reconsider b1 as Element of dom h;
    set b2=h.b1, ha=(b1,b2)-->(b2,b1), hb=h\ha,
    g1=[:rng f1,{b2}:], g2=[:rng f2,{b1}:],
    g=g1\/g2, h1=b1.-->b2, h2=b2.-->b1;
    h.b2=b1 & b2 in dom h by C00; then
    reconsider h1,h2 as Function-like Relation-like Subset of h
    by FUNCT_4:85;
    h1\/h2 c= h & h1 +*1 h2 c= h1\/h2; then
    reconsider hha=ha as Function-like Relation-like Subset of h
    by XBOOLE_1:1;
    h=h/\ha\/hb; then
    C14: (f1\/f2)*g*h = ((f1\/f2)*g*(hha null h)) \/ ((f1\/f2)*g*hb)
    by RELAT_1:32;
    CC13: dom ha={b1,b2} &
    dom(h\hha)=dom h \ dom ha by FOMODEL0:78, FUNCT_4:62;
    rng g1 c= {b2} & {b2}\{b1,b2}={}; then
    rng g1 c= {b2} & {b2} c= {b1,b2} by FOMODEL0:29; then
    reconsider rg1=rng g1 as Subset of {b1,b2} by XBOOLE_1:1;
    rng g2 c= {b1} & {b1}\{b1,b2}={}; then
    rng g2 c= {b1} & {b1} c= {b1,b2} by FOMODEL0:29; then
    reconsider rg2=rng g2 as Subset of {b1,b2} by XBOOLE_1:1;
    rg1\/rg2 \+\ rng g = {} & rg1\/rg2 \ {b1,b2} = {}; then
    reconsider rg=rng g as Subset of {b1,b2} by FOMODEL0:29;
    rng ((f1\/f2) >*> g) c= rg by RELAT_1:26; then
    reconsider R=rng((f1\/f2) >*> g) as Subset of {b1,b2} by XBOOLE_1:1;
    dom hb /\R ={} by CC13; then
    (f1\/f2)>*>g>*>hb={} by XBOOLE_0:def 7, RELAT_1:44; then
    C15: g c= (f1\/f2)>*>g>*>h by C14, C2, FOMODEL0:77, C21;
    CC3: S/\O={};
    CC8: dom g1 \ dom g2=dom g1 & dom f1 \ dom f2=dom f1
    by C0, CC3, XBOOLE_0:def 7, XBOOLE_1:83;
    reconsider rff=rng ff as Subset of F;
    C10: F=field ff\S \/ (field ff/\S) by C01 .=
    field ff\S \/ (dom ff/\S) by C01, PARTFUN1:def 2 .=
    O null dom ff \/ S by CC20, B0;
    f1\/f2 \ ff={} & dom f1 \/ dom f2 \+\ dom (f1\/f2)={}; then
    f1\/f2 c= ff & dom (f1\/f2)=F by C10, FOMODEL0:29; then
    f1\/f2=ff by C00, FOMODEL0:68; then
    C12: g1+*g2 c= h * (g1+*g2) * ff by CC8, C15, RELAT_1:36;
    dom g1 \/ dom g2 \+\ dom (g1\/g2)={}; then
    C11: dom (g1+*g2) = F by C0, C10, CC8, FOMODEL0:29;
    dom (h *(g1+*g2)*ff) c= dom (g1+*g2) by C11; then
    C17: g1+*g2 = h*(g1+*g2)*ff by C12, FOMODEL0:68;
    reconsider bb1=b1, bb2=b2 as Element of H;
    reconsider B={bb1,bb2} as non empty Subset of H;
    rg c= {b1,b2}; then
    reconsider gg=g1+*g2 as Element of Funcs(F,B) by CC8, C11, FUNCT_2:def 2;
    {gg} \ Funcs(F,H)={}; then
    reconsider gg as Element of Funcs(F,H) by FOMODEL0:29;
    (Perm(P,i)).gg=gg & gg<>{} by C17, HILBERT3:37; then
    Perm(P,i).gg=gg & gg in dom Perm(P,i) by FUNCT_1:def 2; then
    gg is_a_fixpoint_of Perm(P,i) by ABIAN:def 3;
    hence contradiction by B2, FOMODEL0:69;
  end;
end;
for r holds Z[r] from HILBERT2:sch 2(A1,A2,A3);
hence thesis;
end;

definition
  let p;
  attr p is classical means :DefClassical:
  SetVal0 (v,p) <> {};
::# The idea is that the three set-theoretical entities
::# {}, [:,:], Funcs
::# behave respectively like
::# 0, AND, =>
::# of classical logic.
::# For example Funcs(x,y)={} iff (x<>{}, y={}). And so on...
::# To enforce this scheme, a slight modification of SetValuation into
::# the ancestor mode SetValuation0, allowing empty truth values, was needed.
::# Initially, the immaterial restriction of 2-valuedness was considered
::# to ease the work; however, upon rethinking tohilb definition, it
::# was no longer needed.
end;

registration
  cluster pseudo-canonical -> classical for Element of HP-WFF;
  coherence
  proof
    let p;
    assume
AA: p is pseudo-canonical;
    defpred IT[Function] means
    ex x being set st x is_a_fixpoint_of $1;
    assume not p is classical; then consider v such that
B0: SetVal0(v,p)={};
    set P=v tohilbperm, V=v tohilbval;
    fixpoints Perm(P,p)={} by Lm100, B0; then
    not IT[Perm(P,p)] by FOMODEL0:69;
    hence thesis by AA,HILBERT3:def 8;
  end;
end;

registration
  let v;
  let p be classical Element of HP-WFF;
  cluster SetVal0 (v,p) -> non empty;
  coherence by DefClassical;
end;