:: 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 b₁ being Function st b₁ 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 b₁ being Permutation of A st b₁ 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 b₁ being Function st b₁ is involutive holds
b₁ 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 b₁ being Permutation of X st
( not b₁ is empty & b₁ 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 S₁[ 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 b₁ being ManySortedSet of HP-WFF st
( b₁ . VERUM = 1 & ( for n being Element of NAT holds b₁ . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b₁ . (p '&' q) = [:(b₁ . p),(b₁ . q):] & b₁ . (p => q) = Funcs ((b₁ . p),(b₁ . q)) ) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of HP-WFF st b₁ . VERUM = 1 & ( for n being Element of NAT holds b₁ . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b₁ . (p '&' q) = [:(b₁ . p),(b₁ . q):] & b₁ . (p => q) = Funcs ((b₁ . p),(b₁ . q)) ) ) & b₂ . VERUM = 1 & ( for n being Element of NAT holds b₂ . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b₂ . (p '&' q) = [:(b₂ . p),(b₂ . q):] & b₂ . (p => q) = Funcs ((b₂ . p),(b₂ . q)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines SetVal0 HILBERT4:def 8 :
for V being SetValuation0
for b₂ being ManySortedSet of HP-WFF holds
( b₂ = SetVal0 V iff ( b₂ . VERUM = 1 & ( for n being Element of NAT holds b₂ . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b₂ . (p '&' q) = [:(b₂ . p),(b₂ . q):] & b₂ . (p => q) = Funcs ((b₂ . p),(b₂ . 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 b₁ being Element of HP-WFF st b₁ is pseudo-canonical holds
b₁ 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;