:: Pseudo-canonical Formulae are Classical
:: by Marco B. Caminati and Artur Korni{\l}owicz
::
:: Received May 25, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


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

set I = id 1;

registration
let X, Y be set ;
let f be Relation of X,Y;
reduce (id X) * f to f;
reducibility
(id X) * f = f
proof end;
reduce f * (id Y) to f;
reducibility
f * (id Y) = f
proof end;
end;

theorem Th4: :: HILBERT4:1
for f, g being one-to-one Function st f " = g " holds
f = g
proof end;

registration
cluster Relation-like Function-like involutive for set ;
existence
ex b1 being Function st b1 is involutive
proof end;
let A be set ;
cluster Relation-like A -defined A -valued Function-like one-to-one total quasi_total onto bijective involutive oneone for Element of bool [:A,A:];
existence
ex b1 being Permutation of A st b1 is involutive
proof end;
end;

theorem Th7: :: HILBERT4:2
for f being involutive Function st rng f c= dom f holds
f * f = id (dom f)
proof end;

theorem Th8: :: HILBERT4:3
for f being Function st f * f = id (dom f) holds
f is involutive
proof end;

theorem Th9: :: HILBERT4:4
for A being set
for f being involutive Function of A,A holds f * f = id A
proof end;

theorem Th10: :: HILBERT4:5
for A being set
for f being Function of A,A st f * f = id A holds
f is involutive
proof end;

registration
cluster Relation-like Function-like involutive -> one-to-one for set ;
coherence
for b1 being Function st b1 is involutive holds
b1 is one-to-one
proof end;
end;

registration
let A be set ;
let f be involutive Permutation of A;
cluster f " -> involutive ;
coherence
f " is involutive
proof end;
end;

registration
let n be non zero Nat;
cluster (0,n) --> (n,0) -> without_fixpoints ;
coherence
not (0,n) --> (n,0) is with_fixpoint
proof end;
end;

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

registration
let X be non empty set ;
cluster non empty Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V67() oneone for Element of bool [:X,X:];
existence
ex b1 being Permutation of X st
( not b1 is empty & b1 is V67() )
proof end;
end;

registration
let A, B be set ;
let f be involutive Function of A,A;
let g be involutive Function of B,B;
cluster [:f,g:] -> involutive ;
coherence
[:f,g:] is involutive
proof end;
end;

registration
let A, B be non empty set ;
let f be V67() Permutation of A;
let g be V67() Permutation of B;
cluster f => g -> V67() ;
coherence
f => g is involutive
proof end;
end;

theorem Th14: :: HILBERT4:6
for x being set
for V being SetValuation
for P being Permutation of V
for p, q being Element of HP-WFF st x is_a_fixpoint_of Perm (P,q) holds
(SetVal (V,p)) --> x is_a_fixpoint_of Perm (P,(p => q))
proof end;

theorem Lm2: :: HILBERT4:7
for V being SetValuation
for P being Permutation of V
for p, q being Element of HP-WFF st Perm (P,q) is with_fixpoint holds
Perm (P,(p => q)) is with_fixpoint
proof end;

theorem Lm3: :: HILBERT4:8
for V being SetValuation
for P being Permutation of V
for p, q being Element of HP-WFF st Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints holds
Perm (P,(p => q)) is without_fixpoints
proof end;

::# 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 :: HILBERT4:def 1
{ [x, the Element of x] where x is Element of X \ {{}} : x in X \ {{}} } ;
coherence
{ [x, the Element of x] where x is Element of X \ {{}} : x in X \ {{}} } is set
;
end;

:: deftheorem defines ChoiceOn HILBERT4:def 1 :
for X being set holds ChoiceOn X = { [x, the Element of x] where x is Element of X \ {{}} : x in X \ {{}} } ;

registration
let X be set ;
cluster ChoiceOn X -> Relation-like Function-like ;
coherence
( ChoiceOn X is Relation-like & ChoiceOn X is Function-like )
proof end;
end;

Lm9: for a, X being set holds
( ( a in dom (ChoiceOn X) implies (ChoiceOn X) . a in a ) & dom (ChoiceOn X) = X \ {{}} )

proof end;

definition
let f be Function;
func FieldCover f -> set equals :: HILBERT4:def 2
{ {x,(f . x)} where x is Element of dom f : x in dom f } ;
coherence
{ {x,(f . x)} where x is Element of dom f : x in dom f } is set
;
end;

:: deftheorem defines FieldCover HILBERT4:def 2 :
for f being Function holds FieldCover f = { {x,(f . x)} where x is Element of dom f : x in dom f } ;

definition
let f be Function;
func SomePoints f -> set equals :: HILBERT4:def 3
(field f) \ (rng (ChoiceOn (FieldCover f)));
coherence
(field f) \ (rng (ChoiceOn (FieldCover f))) is set
;
end;

:: deftheorem defines SomePoints HILBERT4:def 3 :
for f being Function holds SomePoints f = (field f) \ (rng (ChoiceOn (FieldCover f)));

definition
let f be Function;
func OtherPoints f -> set equals :: HILBERT4:def 4
((field f) \ (fixpoints f)) \ (SomePoints f);
coherence
((field f) \ (fixpoints f)) \ (SomePoints f) is set
;
end;

:: deftheorem defines OtherPoints HILBERT4:def 4 :
for f being Function holds OtherPoints f = ((field f) \ (fixpoints f)) \ (SomePoints f);

registration
let g be Function;
cluster (OtherPoints g) /\ (SomePoints g) -> empty ;
coherence
(OtherPoints g) /\ (SomePoints g) is empty
proof end;
end;

Lm23: for f being Function st f is involutive holds
f .: (SomePoints f) c= OtherPoints f

proof end;

Lm24: for f being Function st f is involutive holds
f .: (OtherPoints f) c= SomePoints f

proof end;

Lm30: for f being Function st f is involutive & rng f c= dom f holds
( f .: (OtherPoints f) = SomePoints f & f .: (SomePoints f) = OtherPoints f )

proof end;

Lm25: for g being Function st g is involutive & (field g) \ (fixpoints g) <> {} & rng g c= dom g holds
SomePoints g <> {}

proof end;

Lm26: for g being Function st (rng g) \ (dom g) = {} & g is involutive & (field g) \ (fixpoints g) <> {} holds
( SomePoints g <> {} & OtherPoints g <> {} )

proof end;

::# 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 be set ;
::# Constructive definition of the object uniquely described by Lm17 & Lm18
func x tohilb -> set equals :: HILBERT4:def 5
((id 1) +* ([:1,(Funcs (x,{})):] * [:(Funcs (x,{})),{1}:])) +* ([:{1},(Funcs (x,{})):] * [:(Funcs (x,{})),{0}:]);
coherence
((id 1) +* ([:1,(Funcs (x,{})):] * [:(Funcs (x,{})),{1}:])) +* ([:{1},(Funcs (x,{})):] * [:(Funcs (x,{})),{0}:]) is set
;
end;

:: deftheorem defines tohilb HILBERT4:def 5 :
for x being set holds x tohilb = ((id 1) +* ([:1,(Funcs (x,{})):] * [:(Funcs (x,{})),{1}:])) +* ([:{1},(Funcs (x,{})):] * [:(Funcs (x,{})),{0}:]);

registration
let x be set ;
cluster x tohilb -> Relation-like Function-like ;
coherence
( x tohilb is Function-like & x tohilb is Relation-like )
;
end;

theorem Lm18: :: HILBERT4:9
for x being set st x <> {} holds
x tohilb = id 1
proof end;

theorem Lm17: :: HILBERT4:10
{} tohilb = (0,1) --> (1,0)
proof end;

definition
let v be Function;
func v tohilbperm -> set equals :: HILBERT4:def 6
{ [n,((v . n) tohilb)] where n is Element of NAT : verum } ;
coherence
{ [n,((v . n) tohilb)] where n is Element of NAT : verum } is set
;
end;

:: deftheorem defines tohilbperm HILBERT4:def 6 :
for v being Function holds v tohilbperm = { [n,((v . n) tohilb)] where n is Element of NAT : verum } ;

definition
let v be Function;
func v tohilbval -> set equals :: HILBERT4:def 7
{ [n,(dom ((v . n) tohilb))] where n is Element of NAT : verum } ;
coherence
{ [n,(dom ((v . n) tohilb))] where n is Element of NAT : verum } is set
;
end;

:: deftheorem defines tohilbval HILBERT4:def 7 :
for v being Function holds v tohilbval = { [n,(dom ((v . n) tohilb))] where n is Element of NAT : verum } ;

defpred S1[ set ] means verum;

Lm15: for v being Function holds
( v tohilbval is Function & v tohilbperm is Function & proj1 (v tohilbval) = NAT & proj1 (v tohilbperm) = NAT )

proof end;

registration
let v be Function;
cluster v tohilbval -> Relation-like Function-like ;
coherence
( v tohilbval is Function-like & v tohilbval is Relation-like )
by Lm15;
cluster v tohilbperm -> Relation-like Function-like ;
coherence
( v tohilbperm is Function-like & v tohilbperm is Relation-like )
by Lm15;
cluster v tohilbval -> NAT -defined ;
coherence
v tohilbval is NAT -defined
by Lm15;
cluster v tohilbval -> total ;
coherence
v tohilbval is total
proof end;
cluster v tohilbperm -> NAT -defined ;
coherence
v tohilbperm is NAT -defined
by Lm15;
cluster v tohilbperm -> total ;
coherence
v tohilbperm is total
proof end;
end;

Lm34: for x being set
for g being Function st x is Nat holds
( (g tohilbperm) . x = (g . x) tohilb & (g tohilbval) . x = dom ((g . x) tohilb) )

proof end;

registration
let v be Function;
cluster v tohilbval -> V8() ;
coherence
v tohilbval is non-empty
proof end;
end;

Lm37: for x being set holds
( x tohilb is symmetric & dom (x tohilb) = rng (x tohilb) )

proof end;

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

definition
let v be Function;
:: original: tohilbperm
redefine func v tohilbperm -> Permutation of v tohilbval ;
coherence
v tohilbperm is Permutation of v tohilbval
proof end;
end;

definition
mode SetValuation0 is ManySortedSet of NAT ;
end;

registration
let p be Element of HP-WFF ;
let v be SetValuation0;
cluster Perm ((v tohilbperm),p) -> V67() ;
coherence
Perm ((v tohilbperm),p) is involutive
proof end;
end;

::# 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: :: HILBERT4:def 8
( it . VERUM = 1 & ( for n being Element of NAT holds it . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( it . (p '&' q) = [:(it . p),(it . q):] & it . (p => q) = Funcs ((it . p),(it . q)) ) ) );
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) & b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SetVal0 HILBERT4:def 8 :
for V being SetValuation0
for b2 being ManySortedSet of HP-WFF holds
( b2 = SetVal0 V iff ( b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) ) );

definition
let v be SetValuation0;
let p be Element of HP-WFF ;
func SetVal0 (v,p) -> set equals :: HILBERT4:def 9
(SetVal0 v) . p;
correctness
coherence
(SetVal0 v) . p is set
;
;
end;

:: deftheorem defines SetVal0 HILBERT4:def 9 :
for v being SetValuation0
for p being Element of HP-WFF holds SetVal0 (v,p) = (SetVal0 v) . p;

Lm100: for p being Element of HP-WFF
for v being SetValuation0 holds
( fixpoints (Perm ((v tohilbperm),p)) <> {} iff SetVal0 (v,p) <> {} )

proof end;

definition
let p be Element of HP-WFF ;
attr p is classical means :DefClassical: :: HILBERT4:def 10
for v being SetValuation0 holds SetVal0 (v,p) <> {} ;
end;

:: deftheorem DefClassical defines classical HILBERT4:def 10 :
for p being Element of HP-WFF holds
( p is classical iff for v being SetValuation0 holds SetVal0 (v,p) <> {} );

registration
cluster pseudo-canonical -> classical for Element of HP-WFF ;
coherence
for b1 being Element of HP-WFF st b1 is pseudo-canonical holds
b1 is classical
proof end;
end;

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