:: Defining by structural induction in the positive propositional language :: 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 proofend; theorem Th2: :: HILBERT2:2 for x, y being set for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds f = g proofend; theorem Th3: :: HILBERT2:3 for x, X being set st <*x*> is FinSequence of X holds x in X proofend; 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*> proofend; theorem Th5: :: HILBERT2:5 for x being set for T1, T2 being Tree holds ( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) ) proofend; scheme :: HILBERT2:sch 1 InTreeInd{ F1() -> Tree, P1[ set ] } : for f being Element of F1() holds P1[f] provided A1: P1[ <*> NAT] and A2: for f being Element of F1() st P1[f] holds for n being Element of NAT st f ^ <*n*> in F1() holds P1[f ^ <*n*>] proofend; theorem Th6: :: HILBERT2:6 for x being set for T1, T2 being DecoratedTree holds (x -tree (T1,T2)) . {} = x proofend; 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 . {} ) proofend; 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 ) proofend; registration let x be set ; let p be non empty DTree-yielding FinSequence; clusterx -tree p -> non root ; coherence not x -tree p is trivial proofend; end; registration let x be set ; let T1 be DecoratedTree; clusterx -tree T1 -> non root ; coherence not x -tree T1 is trivial proofend; let T2 be DecoratedTree; clusterx -tree (T1,T2) -> non root ; coherence not x -tree (T1,T2) is trivial proofend; end; begin definition let n be Element of NAT ; func prop n -> Element of HP-WFF equals :: HILBERT2:def 1 <*(3 + n)*>; coherence <*(3 + n)*> is Element of HP-WFF by HILBERT1:def_4; end; :: deftheorem defines prop HILBERT2:def_1_:_ for n being Element of NAT holds prop n = <*(3 + n)*>; definition let D be set ; redefine attr D is with_VERUM means :Def2: :: HILBERT2:def 2 VERUM in D; 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 ( D is with_propositional_variables iff for n being Element of NAT holds prop n in D ) proofend; end; :: deftheorem Def2 defines with_VERUM HILBERT2:def_2_:_ 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 ); definition let D be Subset of HP-WFF; 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 ( 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 ) proofend; 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 ( 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 ) proofend; 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 ); :: 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 ); definition let p be Element of HP-WFF ; attrp is conjunctive means :Def6: :: HILBERT2:def 6 ex r, s being Element of HP-WFF st p = r '&' s; attrp is conditional means :Def7: :: HILBERT2:def 7 ex r, s being Element of HP-WFF st p = r => s; attrp is simple means :Def8: :: HILBERT2:def 8 ex n being Element of NAT st p = prop n; end; :: 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 ); :: 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 ); :: 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 ); scheme :: HILBERT2:sch 2 HPInd{ P1[ set ] } : for r being Element of HP-WFF holds P1[r] provided A1: P1[ VERUM ] and A2: for n being Element of NAT holds P1[ prop n] and A3: for r, s being Element of HP-WFF st P1[r] & P1[s] holds ( P1[r '&' s] & P1[r => s] ) proofend; 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 ) proofend; theorem Th10: :: HILBERT2:10 for p being Element of HP-WFF holds len p >= 1 proofend; theorem Th11: :: HILBERT2:11 for p being Element of HP-WFF st p . 1 = 1 holds p is conditional proofend; theorem Th12: :: HILBERT2:12 for p being Element of HP-WFF st p . 1 = 2 holds p is conjunctive proofend; theorem :: HILBERT2:13 for n being Element of NAT for p being Element of HP-WFF st p . 1 = 3 + n holds p is simple proofend; theorem :: HILBERT2:14 for p being Element of HP-WFF st p . 1 = 0 holds p = VERUM proofend; theorem Th15: :: HILBERT2:15 for p, q being Element of HP-WFF holds ( len p < len (p '&' q) & len q < len (p '&' q) ) proofend; theorem Th16: :: HILBERT2:16 for p, q being Element of HP-WFF holds ( len p < len (p => q) & len q < len (p => q) ) proofend; theorem Th17: :: HILBERT2:17 for p, q being Element of HP-WFF for t being FinSequence st p = q ^ t holds p = q proofend; theorem Th18: :: HILBERT2:18 for p, q, r, s being Element of HP-WFF st p ^ q = r ^ s holds ( p = r & q = s ) proofend; theorem Th19: :: HILBERT2:19 for p, q, r, s being Element of HP-WFF st p '&' q = r '&' s holds ( p = r & s = q ) proofend; theorem Th20: :: HILBERT2:20 for p, q, r, s being Element of HP-WFF st p => q = r => s holds ( p = r & s = q ) proofend; theorem Th21: :: HILBERT2:21 for n, m being Element of NAT st prop n = prop m holds n = m proofend; theorem Th22: :: HILBERT2:22 for p, q, r, s being Element of HP-WFF holds p '&' q <> r => s proofend; theorem Th23: :: HILBERT2:23 for p, q being Element of HP-WFF holds p '&' q <> VERUM proofend; theorem Th24: :: HILBERT2:24 for n being Element of NAT for p, q being Element of HP-WFF holds p '&' q <> prop n proofend; theorem Th25: :: HILBERT2:25 for p, q being Element of HP-WFF holds p => q <> VERUM proofend; theorem Th26: :: HILBERT2:26 for n being Element of NAT for p, q being Element of HP-WFF holds p => q <> prop n proofend; theorem Th27: :: HILBERT2:27 for p, q being Element of HP-WFF holds ( p '&' q <> p & p '&' q <> q ) proofend; theorem Th28: :: HILBERT2:28 for p, q being Element of HP-WFF holds ( p => q <> p & p => q <> q ) proofend; theorem Th29: :: HILBERT2:29 for n being Element of NAT holds VERUM <> prop n proofend; begin scheme :: HILBERT2:sch 3 HPMSSExL{ F1() -> set , F2( Element of NAT ) -> set , P1[ Element of HP-WFF , Element of HP-WFF , set , set , set ], P2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] } : ex M being ManySortedSet of HP-WFF st ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds ( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) ) provided A1: for p, q being Element of HP-WFF for a, b being set ex c being set st P1[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 P2[p,q,a,b,d] and A3: for p, q being Element of HP-WFF for a, b, c, d being set st P1[p,q,a,b,c] & P1[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 P2[p,q,a,b,c] & P2[p,q,a,b,d] holds c = d proofend; scheme :: HILBERT2:sch 4 HPMSSLambda{ F1() -> set , F2( Element of NAT ) -> set , F3( set , set ) -> set , F4( set , set ) -> set } : ex M being ManySortedSet of HP-WFF st ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds ( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) ) proofend; begin definition 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 ex b1 being ManySortedSet of HP-WFF st ( b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st ( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) ) proofend; uniqueness for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st ( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) & b2 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b2 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st ( p9 = b2 . p & q9 = b2 . q & b2 . (p '&' q) = (p '&' q) -tree (p9,q9) & b2 . (p => q) = (p => q) -tree (p9,q9) ) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines HP-Subformulae HILBERT2:def_9_:_ for b1 being ManySortedSet of HP-WFF holds ( b1 = HP-Subformulae iff ( b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st ( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) ) ); definition let p be Element of HP-WFF ; func Subformulae p -> DecoratedTree of HP-WFF equals :: HILBERT2:def 10 HP-Subformulae . p; correctness coherence HP-Subformulae . p is DecoratedTree of HP-WFF ; proofend; end; :: deftheorem defines Subformulae HILBERT2:def_10_:_ for p being Element of HP-WFF holds Subformulae p = HP-Subformulae . p; theorem Th30: :: HILBERT2:30 Subformulae VERUM = root-tree VERUM by Def9; theorem :: HILBERT2:31 for n being Element of NAT holds Subformulae (prop n) = root-tree (prop n) by Def9; theorem Th32: :: HILBERT2:32 for p, q being Element of HP-WFF holds Subformulae (p '&' q) = (p '&' q) -tree ((Subformulae p),(Subformulae q)) proofend; theorem Th33: :: HILBERT2:33 for p, q being Element of HP-WFF holds Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q)) proofend; theorem Th34: :: HILBERT2:34 for p being Element of HP-WFF holds (Subformulae p) . {} = p proofend; 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) proofend; 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 ) proofend;