:: by Andrzej Trybulec

::

:: Received April 23, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

theorem Th1: :: HILBERT2:1

for Z being set

for M being ManySortedSet of Z st ( for x being set st x in Z holds

M . x is ManySortedSet of x ) holds

for f being Function st f = Union M holds

dom f = union Z

for M being ManySortedSet of Z st ( for x being set st x in Z holds

M . x is ManySortedSet of x ) holds

for f being Function st f = Union M holds

dom f = union Z

proof end;

theorem Th4: :: HILBERT2:4

for X being set

for f being FinSequence of X st f <> {} holds

ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>

for f being FinSequence of X st f <> {} holds

ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>

proof end;

theorem Th7: :: HILBERT2:7

for x being set

for T1, T2 being DecoratedTree holds

( (x -tree (T1,T2)) . <*0*> = T1 . {} & (x -tree (T1,T2)) . <*1*> = T2 . {} )

for T1, T2 being DecoratedTree holds

( (x -tree (T1,T2)) . <*0*> = T1 . {} & (x -tree (T1,T2)) . <*1*> = T2 . {} )

proof end;

theorem Th8: :: HILBERT2:8

for x being set

for T1, T2 being DecoratedTree holds

( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )

for T1, T2 being DecoratedTree holds

( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )

proof end;

registration

let x be set ;

let p be non empty DTree-yielding FinSequence;

coherence

not x -tree p is trivial

end;
let p be non empty DTree-yielding FinSequence;

coherence

not x -tree p is trivial

proof end;

registration

let x be set ;

let T1 be DecoratedTree;

coherence

not x -tree T1 is trivial

coherence

not x -tree (T1,T2) is trivial

end;
let T1 be DecoratedTree;

coherence

not x -tree T1 is trivial

proof end;

let T2 be DecoratedTree;coherence

not x -tree (T1,T2) is trivial

proof end;

begin

definition
end;

definition

let D be set ;

compatibility

( D is with_VERUM iff VERUM in D ) by HILBERT1:def 1;

( D is with_propositional_variables iff for n being Element of NAT holds prop n in D )

end;
compatibility

( D is with_VERUM iff VERUM in D ) by HILBERT1:def 1;

redefine attr D is with_propositional_variables means :: HILBERT2:def 3

for n being Element of NAT holds prop n in D;

compatibility for n being Element of NAT holds prop n in D;

( D is with_propositional_variables iff for n being Element of NAT holds prop n in D )

proof end;

:: deftheorem Def2 defines with_VERUM HILBERT2:def 2 :

for D being set holds

( D is with_VERUM iff VERUM in D );

for D being set holds

( D is with_VERUM iff VERUM in D );

:: deftheorem defines with_propositional_variables HILBERT2:def 3 :

for D being set holds

( D is with_propositional_variables iff for n being Element of NAT holds prop n in D );

for D being set holds

( D is with_propositional_variables iff for n being Element of NAT holds prop n in D );

definition

let D be Subset of HP-WFF;

( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds

p => q in D )

( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds

p '&' q in D )

end;
redefine attr D is with_implication means :: HILBERT2:def 4

for p, q being Element of HP-WFF st p in D & q in D holds

p => q in D;

compatibility for p, q being Element of HP-WFF st p in D & q in D holds

p => q in D;

( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds

p => q in D )

proof end;

redefine attr D is with_conjunction means :: HILBERT2:def 5

for p, q being Element of HP-WFF st p in D & q in D holds

p '&' q in D;

compatibility for p, q being Element of HP-WFF st p in D & q in D holds

p '&' q in D;

( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds

p '&' q in D )

proof end;

:: deftheorem defines with_implication HILBERT2:def 4 :

for D being Subset of HP-WFF holds

( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds

p => q in D );

for D being Subset of HP-WFF holds

( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds

p => q in D );

:: deftheorem defines with_conjunction HILBERT2:def 5 :

for D being Subset of HP-WFF holds

( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds

p '&' q in D );

for D being Subset of HP-WFF holds

( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds

p '&' q in D );

definition

let p be Element of HP-WFF ;

end;
attr p is conjunctive means :Def6: :: HILBERT2:def 6

ex r, s being Element of HP-WFF st p = r '&' s;

ex r, s being Element of HP-WFF st p = r '&' s;

:: deftheorem Def6 defines conjunctive HILBERT2:def 6 :

for p being Element of HP-WFF holds

( p is conjunctive iff ex r, s being Element of HP-WFF st p = r '&' s );

for p being Element of HP-WFF holds

( p is conjunctive iff ex r, s being Element of HP-WFF st p = r '&' s );

:: deftheorem Def7 defines conditional HILBERT2:def 7 :

for p being Element of HP-WFF holds

( p is conditional iff ex r, s being Element of HP-WFF st p = r => s );

for p being Element of HP-WFF holds

( p is conditional iff ex r, s being Element of HP-WFF st p = r => s );

:: deftheorem Def8 defines simple HILBERT2:def 8 :

for p being Element of HP-WFF holds

( p is simple iff ex n being Element of NAT st p = prop n );

for p being Element of HP-WFF holds

( p is simple iff ex n being Element of NAT st p = prop n );

theorem Th9: :: HILBERT2:9

for p being Element of HP-WFF holds

( p is conjunctive or p is conditional or p is simple or p = VERUM )

( p is conjunctive or p is conditional or p is simple or p = VERUM )

proof end;

begin

scheme :: HILBERT2:sch 3

HPMSSExL{ F_{1}() -> set , F_{2}( Element of NAT ) -> set , P_{1}[ Element of HP-WFF , Element of HP-WFF , set , set , set ], P_{2}[ Element of HP-WFF , Element of HP-WFF , set , set , set ] } :

HPMSSExL{ F

ex M being ManySortedSet of HP-WFF st

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

( P_{1}[p,q,M . p,M . q,M . (p '&' q)] & P_{2}[p,q,M . p,M . q,M . (p => q)] ) ) )

provided( M . VERUM = F

( P

A1:
for p, q being Element of HP-WFF

for a, b being set ex c being set st P_{1}[p,q,a,b,c]
and

A2: for p, q being Element of HP-WFF

for a, b being set ex d being set st P_{2}[p,q,a,b,d]
and

A3: for p, q being Element of HP-WFF

for a, b, c, d being set st P_{1}[p,q,a,b,c] & P_{1}[p,q,a,b,d] holds

c = d and

A4: for p, q being Element of HP-WFF

for a, b, c, d being set st P_{2}[p,q,a,b,c] & P_{2}[p,q,a,b,d] holds

c = d

for a, b being set ex c being set st P

A2: for p, q being Element of HP-WFF

for a, b being set ex d being set st P

A3: for p, q being Element of HP-WFF

for a, b, c, d being set st P

c = d and

A4: for p, q being Element of HP-WFF

for a, b, c, d being set st P

c = d

proof end;

scheme :: HILBERT2:sch 4

HPMSSLambda{ F_{1}() -> set , F_{2}( Element of NAT ) -> set , F_{3}( set , set ) -> set , F_{4}( set , set ) -> set } :

HPMSSLambda{ F

ex M being ManySortedSet of HP-WFF st

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

( M . (p '&' q) = F_{3}((M . p),(M . q)) & M . (p => q) = F_{4}((M . p),(M . q)) ) ) )

( M . VERUM = F

( M . (p '&' q) = F

proof end;

begin

definition

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

( b_{1} . VERUM = root-tree VERUM & ( for n being Element of NAT holds b_{1} . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st

( p9 = b_{1} . p & q9 = b_{1} . q & b_{1} . (p '&' q) = (p '&' q) -tree (p9,q9) & b_{1} . (p => q) = (p => q) -tree (p9,q9) ) ) )

for b_{1}, b_{2} being ManySortedSet of HP-WFF st b_{1} . VERUM = root-tree VERUM & ( for n being Element of NAT holds b_{1} . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st

( p9 = b_{1} . p & q9 = b_{1} . q & b_{1} . (p '&' q) = (p '&' q) -tree (p9,q9) & b_{1} . (p => q) = (p => q) -tree (p9,q9) ) ) & b_{2} . VERUM = root-tree VERUM & ( for n being Element of NAT holds b_{2} . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st

( p9 = b_{2} . p & q9 = b_{2} . q & b_{2} . (p '&' q) = (p '&' q) -tree (p9,q9) & b_{2} . (p => q) = (p => q) -tree (p9,q9) ) ) holds

b_{1} = b_{2}
end;

func HP-Subformulae -> ManySortedSet of HP-WFF means :Def9: :: HILBERT2:def 9

( it . VERUM = root-tree VERUM & ( for n being Element of NAT holds it . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st

( p9 = it . p & q9 = it . q & it . (p '&' q) = (p '&' q) -tree (p9,q9) & it . (p => q) = (p => q) -tree (p9,q9) ) ) );

existence ( it . VERUM = root-tree VERUM & ( for n being Element of NAT holds it . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st

( p9 = it . p & q9 = it . q & it . (p '&' q) = (p '&' q) -tree (p9,q9) & it . (p => q) = (p => q) -tree (p9,q9) ) ) );

ex b

( b

( p9 = b

proof end;

uniqueness for b

( p9 = b

( p9 = b

b

proof end;

:: deftheorem Def9 defines HP-Subformulae HILBERT2:def 9 :

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

( b_{1} = HP-Subformulae iff ( b_{1} . VERUM = root-tree VERUM & ( for n being Element of NAT holds b_{1} . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st

( p9 = b_{1} . p & q9 = b_{1} . q & b_{1} . (p '&' q) = (p '&' q) -tree (p9,q9) & b_{1} . (p => q) = (p => q) -tree (p9,q9) ) ) ) );

for b

( b

( p9 = b

definition

let p be Element of HP-WFF ;

correctness

coherence

HP-Subformulae . p is DecoratedTree of HP-WFF ;

end;
correctness

coherence

HP-Subformulae . p is DecoratedTree of HP-WFF ;

proof end;

:: deftheorem defines Subformulae HILBERT2:def 10 :

for p being Element of HP-WFF holds Subformulae p = HP-Subformulae . p;

for p being Element of HP-WFF holds Subformulae p = HP-Subformulae . p;

theorem :: HILBERT2:31

theorem Th32: :: HILBERT2:32

for p, q being Element of HP-WFF holds Subformulae (p '&' q) = (p '&' q) -tree ((Subformulae p),(Subformulae q))

proof end;

theorem Th33: :: HILBERT2:33

for p, q being Element of HP-WFF holds Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q))

proof end;

theorem Th35: :: HILBERT2:35

for p being Element of HP-WFF

for f being Element of dom (Subformulae p) holds (Subformulae p) | f = Subformulae ((Subformulae p) . f)

for f being Element of dom (Subformulae p) holds (Subformulae p) | f = Subformulae ((Subformulae p) . f)

proof end;

theorem :: HILBERT2:36

for p, q being Element of HP-WFF holds

( not p in Leaves (Subformulae q) or p = VERUM or p is simple )

( not p in Leaves (Subformulae q) or p = VERUM or p is simple )

proof end;