:: by Marco B. Caminati and Artur Korni{\l}owicz

::

:: Received May 25, 2014

:: Copyright (c) 2014-2019 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;

reducibility

(id X) * f = f

f * (id Y) = f

end;
let f be Relation of X,Y;

reducibility

(id X) * f = f

proof end;

reducibility f * (id Y) = f

proof end;

registration

existence

ex b_{1} being Function st b_{1} is involutive

ex b_{1} being Permutation of A st b_{1} is involutive

end;
ex b

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

proof end;

registration
end;

registration
end;

registration
end;

registration

let X be non empty set ;

ex b_{1} being Permutation of X st

( not b_{1} is empty & b_{1} is V67() )

end;
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

( not b

proof end;

registration

let A, B be set ;

let f be involutive Function of A,A;

let g be involutive Function of B,B;

coherence

[:f,g:] is involutive

end;
let f be involutive Function of A,A;

let g be involutive Function of B,B;

coherence

[:f,g:] is involutive

proof end;

registration

let A, B be non empty set ;

let f be V67() Permutation of A;

let g be V67() Permutation of B;

coherence

f => g is involutive

end;
let f be V67() Permutation of A;

let g be V67() Permutation of B;

coherence

f => g is involutive

proof 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))

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

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

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;

definition

let X be set ;

{ [x, the Element of x] where x is Element of X \ {{}} : x in X \ {{}} } is set ;

end;
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 \ {{}} } ;

{ [x, the Element of x] where x is Element of X \ {{}} : x in X \ {{}} } is set ;

:: 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 \ {{}} } ;

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

registration
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;

{ {x,(f . x)} where x is Element of dom f : x in dom f } is set ;

end;
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 } ;

{ {x,(f . x)} where x is Element of dom f : x in dom f } is set ;

:: 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 } ;

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

:: deftheorem defines SomePoints HILBERT4:def 3 :

for f being Function holds SomePoints f = (field f) \ (rng (ChoiceOn (FieldCover f)));

for f being Function holds SomePoints f = (field f) \ (rng (ChoiceOn (FieldCover f)));

:: deftheorem defines OtherPoints HILBERT4:def 4 :

for f being Function holds OtherPoints f = ((field f) \ (fixpoints f)) \ (SomePoints f);

for f being Function holds OtherPoints f = ((field f) \ (fixpoints f)) \ (SomePoints f);

registration
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).

::# 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 ;

((id 1) +* ([:1,(Funcs (x,{})):] * [:(Funcs (x,{})),{1}:])) +* ([:{1},(Funcs (x,{})):] * [:(Funcs (x,{})),{0}:]) is set ;

end;
::# 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}:]);

((id 1) +* ([:1,(Funcs (x,{})):] * [:(Funcs (x,{})),{1}:])) +* ([:{1},(Funcs (x,{})):] * [:(Funcs (x,{})),{0}:]) is set ;

:: 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}:]);

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

registration
end;

definition

let v be Function;

{ [n,((v . n) tohilb)] where n is Element of NAT : verum } is set ;

end;
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 } ;

{ [n,((v . n) tohilb)] where n is Element of NAT : verum } is set ;

:: deftheorem defines tohilbperm HILBERT4:def 6 :

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

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

definition

let v be Function;

{ [n,(dom ((v . n) tohilb))] where n is Element of NAT : verum } is set ;

end;
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 } ;

{ [n,(dom ((v . n) tohilb))] where n is Element of NAT : verum } is set ;

:: 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 } ;

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

defpred S

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;

coherence

( v tohilbval is Function-like & v tohilbval is Relation-like ) by Lm15;

coherence

( v tohilbperm is Function-like & v tohilbperm is Relation-like ) by Lm15;

coherence

v tohilbval is NAT -defined by Lm15;

coherence

v tohilbval is total

v tohilbperm is NAT -defined by Lm15;

coherence

v tohilbperm is total

end;
coherence

( v tohilbval is Function-like & v tohilbval is Relation-like ) by Lm15;

coherence

( v tohilbperm is Function-like & v tohilbperm is Relation-like ) by Lm15;

coherence

v tohilbval is NAT -defined by Lm15;

coherence

v tohilbval is total

proof end;

coherence v tohilbperm is NAT -defined by Lm15;

coherence

v tohilbperm is total

proof 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
end;

Lm37: for x being set holds

( x tohilb is symmetric & dom (x tohilb) = rng (x tohilb) )

proof end;

registration
end;

definition

let v be Function;

:: original: tohilbperm

redefine func v tohilbperm -> Permutation of v tohilbval ;

coherence

v tohilbperm is Permutation of v tohilbval

end;
:: original: tohilbperm

redefine func v tohilbperm -> Permutation of v tohilbval ;

coherence

v tohilbperm is Permutation of v tohilbval

proof end;

registration

let p be Element of HP-WFF ;

let v be SetValuation0;

coherence

Perm ((v tohilbperm),p) is involutive

end;
let v be SetValuation0;

coherence

Perm ((v tohilbperm),p) is involutive

proof end;

::# Classical semantics via SetVal0, an extension of SetVal.

::# Thus, we can state and prove the main result:

::# pseudo-canonical implies classical.

::# Thus, we can state and prove the main result:

::# pseudo-canonical implies classical.

definition

let V be SetValuation0;

ex b_{1} being ManySortedSet of HP-WFF st

( b_{1} . VERUM = 1 & ( for n being Element of NAT holds b_{1} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{1} . (p '&' q) = [:(b_{1} . p),(b_{1} . q):] & b_{1} . (p => q) = Funcs ((b_{1} . p),(b_{1} . q)) ) ) )

for b_{1}, b_{2} being ManySortedSet of HP-WFF st b_{1} . VERUM = 1 & ( for n being Element of NAT holds b_{1} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{1} . (p '&' q) = [:(b_{1} . p),(b_{1} . q):] & b_{1} . (p => q) = Funcs ((b_{1} . p),(b_{1} . q)) ) ) & b_{2} . VERUM = 1 & ( for n being Element of NAT holds b_{2} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{2} . (p '&' q) = [:(b_{2} . p),(b_{2} . q):] & b_{2} . (p => q) = Funcs ((b_{2} . p),(b_{2} . q)) ) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) ) );

ex b

( b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def2 defines SetVal0 HILBERT4:def 8 :

for V being SetValuation0

for b_{2} being ManySortedSet of HP-WFF holds

( b_{2} = SetVal0 V iff ( b_{2} . VERUM = 1 & ( for n being Element of NAT holds b_{2} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{2} . (p '&' q) = [:(b_{2} . p),(b_{2} . q):] & b_{2} . (p => q) = Funcs ((b_{2} . p),(b_{2} . q)) ) ) ) );

for V being SetValuation0

for b

( b

( b

definition
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;

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 ;

end;
attr p is classical means :DefClassical: :: HILBERT4:def 10

for v being SetValuation0 holds SetVal0 (v,p) <> {} ;

for v being SetValuation0 holds SetVal0 (v,p) <> {} ;

:: 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) <> {} );

for p being Element of HP-WFF holds

( p is classical iff for v being SetValuation0 holds SetVal0 (v,p) <> {} );

registration

coherence

for b_{1} being Element of HP-WFF st b_{1} is pseudo-canonical holds

b_{1} is classical

end;
for b

b

proof end;

registration

let v be SetValuation0;

let p be classical Element of HP-WFF ;

coherence

not SetVal0 (v,p) is empty by DefClassical;

end;
let p be classical Element of HP-WFF ;

coherence

not SetVal0 (v,p) is empty by DefClassical;

::# 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.