:: Defining by structural induction in the positive propositional language
:: by Andrzej Trybulec
::
:: Received April 23, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

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

proof end;

theorem Th2: :: HILBERT2:2

for x, y being set
for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds
f = g

proof end;

theorem Th3: :: HILBERT2:3

for X being set
for x being object st <*x*> is FinSequence of X holds
x in X

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*>

proof end;

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

proof end;

scheme :: HILBERT2:sch 1
InTreeInd{ F₁() -> Tree, P₁[ set ] } :

for f being Element of F₁() holds P₁[f]

provided

A1: P₁[ <*> NAT] and
A2: for f being Element of F₁() st P₁[f] holds
for n being Element of NAT st f ^ <*n*> in F₁() holds
P₁[f ^ <*n*>]

proof end;

theorem Th6: :: HILBERT2:6

for x being set
for T1, T2 being DecoratedTree holds (x -tree (T1,T2)) . {} = x

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 . {} )

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 )

proof end;

registration

let x be set ;
let p be non empty DTree-yielding FinSequence;

cluster x -tree p -> non root ;

coherence
not x -tree p is trivial

proof end;

end;

registration

let x be set ;
let T1 be DecoratedTree;

cluster x -tree T1 -> non root ;

coherence
not x -tree T1 is trivial

proof end;

let T2 be DecoratedTree;

cluster x -tree (T1,T2) -> non root ;

coherence
not x -tree (T1,T2) is trivial

proof end;

end;

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 :: HILBERT2:def 2
VERUM in D;

compatibility
( D is with_VERUM iff VERUM in D ) ;

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 )

proof end;

end;

:: deftheorem 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 )

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

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 ;

attr p is conjunctive means :Def6: :: HILBERT2:def 6
ex r, s being Element of HP-WFF st p = r '&' s;

attr p is conditional means :Def7: :: HILBERT2:def 7
ex r, s being Element of HP-WFF st p = r => s;

attr p 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{ P₁[ set ] } :

for r being Element of HP-WFF holds P₁[r]

provided

A1: P₁[ VERUM ] and
A2: for n being Element of NAT holds P₁[ prop n] and
A3: for r, s being Element of HP-WFF st P₁[r] & P₁[s] holds
( P₁[r '&' s] & P₁[r => s] )

proof end;

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 )

proof end;

theorem Th10: :: HILBERT2:10

for p being Element of HP-WFF holds len p >= 1

proof end;

theorem Th11: :: HILBERT2:11

for p being Element of HP-WFF st p . 1 = 1 holds
p is conditional

proof end;

theorem Th12: :: HILBERT2:12

for p being Element of HP-WFF st p . 1 = 2 holds
p is conjunctive

proof end;

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

proof end;

theorem :: HILBERT2:14

for p being Element of HP-WFF st p . 1 = 0 holds
p = VERUM

proof end;

theorem Th15: :: HILBERT2:15

for p, q being Element of HP-WFF holds
( len p < len (p '&' q) & len q < len (p '&' q) )

proof end;

theorem Th16: :: HILBERT2:16

for p, q being Element of HP-WFF holds
( len p < len (p => q) & len q < len (p => q) )

proof end;

theorem Th17: :: HILBERT2:17

for p, q being Element of HP-WFF
for t being FinSequence st p = q ^ t holds
p = q

proof end;

theorem Th18: :: HILBERT2:18

for p, q, r, s being Element of HP-WFF st p ^ q = r ^ s holds
( p = r & q = s )

proof end;

theorem Th19: :: HILBERT2:19

for p, q, r, s being Element of HP-WFF st p '&' q = r '&' s holds
( p = r & s = q )

proof end;

theorem Th20: :: HILBERT2:20

for p, q, r, s being Element of HP-WFF st p => q = r => s holds
( p = r & s = q )

proof end;

theorem Th21: :: HILBERT2:21

for m, n being Element of NAT st prop n = prop m holds
n = m

proof end;

theorem Th22: :: HILBERT2:22

for p, q, r, s being Element of HP-WFF holds p '&' q <> r => s

proof end;

theorem Th23: :: HILBERT2:23

for p, q being Element of HP-WFF holds p '&' q <> VERUM

proof end;

theorem Th24: :: HILBERT2:24

for n being Element of NAT
for p, q being Element of HP-WFF holds p '&' q <> prop n

proof end;

theorem Th25: :: HILBERT2:25

for p, q being Element of HP-WFF holds p => q <> VERUM

proof end;

theorem Th26: :: HILBERT2:26

for n being Element of NAT
for p, q being Element of HP-WFF holds p => q <> prop n

proof end;

theorem Th27: :: HILBERT2:27

for p, q being Element of HP-WFF holds
( p '&' q <> p & p '&' q <> q )

proof end;

theorem Th28: :: HILBERT2:28

for p, q being Element of HP-WFF holds
( p => q <> p & p => q <> q )

proof end;

theorem Th29: :: HILBERT2:29

for n being Element of NAT holds VERUM <> prop n

proof end;

scheme :: HILBERT2:sch 3
HPMSSExL{ F₁() -> set , F₂( Element of NAT ) -> set , P₁[ Element of HP-WFF , Element of HP-WFF , set , set , set ], P₂[ Element of HP-WFF , Element of HP-WFF , set , set , set ] } :

ex M being ManySortedSet of HP-WFF st
( M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(n) ) & ( for p, q being Element of HP-WFF holds
( P₁[p,q,M . p,M . q,M . (p '&' q)] & P₂[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 P₁[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₂[p,q,a,b,d] and
A3: for p, q being Element of HP-WFF
for a, b, c, d being set st P₁[p,q,a,b,c] & P₁[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₂[p,q,a,b,c] & P₂[p,q,a,b,d] holds
c = d

proof end;

scheme :: HILBERT2:sch 4
HPMSSLambda{ F₁() -> set , F₂( Element of NAT ) -> set , F₃( set , set ) -> set , F₄( set , set ) -> set } :

ex M being ManySortedSet of HP-WFF st
( M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F₃((M . p),(M . q)) & M . (p => q) = F₄((M . p),(M . q)) ) ) )

proof end;

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 b₁ being ManySortedSet of HP-WFF st
( b₁ . VERUM = root-tree VERUM & ( for n being Element of NAT holds b₁ . (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₁ . p & q9 = b₁ . q & b₁ . (p '&' q) = (p '&' q) -tree (p9,q9) & b₁ . (p => q) = (p => q) -tree (p9,q9) ) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of HP-WFF st b₁ . VERUM = root-tree VERUM & ( for n being Element of NAT holds b₁ . (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₁ . p & q9 = b₁ . q & b₁ . (p '&' q) = (p '&' q) -tree (p9,q9) & b₁ . (p => q) = (p => q) -tree (p9,q9) ) ) & b₂ . VERUM = root-tree VERUM & ( for n being Element of NAT holds b₂ . (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₂ . p & q9 = b₂ . q & b₂ . (p '&' q) = (p '&' q) -tree (p9,q9) & b₂ . (p => q) = (p => q) -tree (p9,q9) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines HP-Subformulae HILBERT2:def 9 :
for b₁ being ManySortedSet of HP-WFF holds
( b₁ = HP-Subformulae iff ( b₁ . VERUM = root-tree VERUM & ( for n being Element of NAT holds b₁ . (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₁ . p & q9 = b₁ . q & b₁ . (p '&' q) = (p '&' q) -tree (p9,q9) & b₁ . (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 ;

proof end;

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

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 Th34: :: HILBERT2:34

for p being Element of HP-WFF holds (Subformulae p) . {} = p

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)

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 )

proof end;