:: HILBERT2 semantic presentation

theorem Th1: :: HILBERT2:1

for b₁ being set
for b₂ being ManySortedSet of b₁ st ( for b₃ being set st b₃ in b₁ holds
b₂ . b₃ is ManySortedSet of b₃ ) holds
for b₃ being Function st b₃ = Union b₂ holds
dom b₃ = union b₁

proof end;

theorem Th2: :: HILBERT2:2

for b₁, b₂ being set
for b₃, b₄ being FinSequence st <*b₁*> ^ b₃ = <*b₂*> ^ b₄ holds
b₃ = b₄

proof end;

theorem Th3: :: HILBERT2:3

for b₁, b₂ being set st <*b₁*> is FinSequence of b₂ holds
b₁ in b₂

proof end;

theorem Th4: :: HILBERT2:4

for b₁ being set
for b₂ being FinSequence of b₁ st b₂ <> {} holds
ex b₃ being FinSequence of b₁ex b₄ being Element of b₁ st b₂ = b₃ ^ <*b₄*>

proof end;

theorem Th5: :: HILBERT2:5

for b₁ being set
for b₂, b₃ being Tree holds
( <*b₁*> in tree b₂,b₃ iff ( b₁ = 0 or b₁ = 1 ) )

proof end;

registration

cluster {} -> Tree-yielding ;
coherence by TREES_3:23;

end;

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

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

provided

E6: P₁[ <*> NAT ] and
E7: for b₁ being Element of F₁() st P₁[b₁] holds
for b₂ being Nat st b₁ ^ <*b₂*> in F₁() holds
P₁[b₁ ^ <*b₂*>]

proof end;

theorem Th6: :: HILBERT2:6

for b₁ being set
for b₂, b₃ being DecoratedTree holds (b₁ -tree b₂,b₃) . {} = b₁

proof end;

theorem Th7: :: HILBERT2:7

for b₁ being set
for b₂, b₃ being DecoratedTree holds
( (b₁ -tree b₂,b₃) . <*0*> = b₂ . {} & (b₁ -tree b₂,b₃) . <*1*> = b₃ . {} )

proof end;

theorem Th8: :: HILBERT2:8

for b₁ being set
for b₂, b₃ being DecoratedTree holds
( (b₁ -tree b₂,b₃) | <*0*> = b₂ & (b₁ -tree b₂,b₃) | <*1*> = b₃ )

proof end;

registration

let c₁ be set ;
let c₂ be non empty DTree-yielding FinSequence;
cluster a₁ -tree a₂ -> non root ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be DecoratedTree;
cluster a₁ -tree a₂ -> non root ;
coherence

proof end;

let c₃ be DecoratedTree;
cluster a₁ -tree a₂,a₃ -> non root ;
coherence

proof end;

end;

definition

let c₁ be Nat;
func prop c₁ -> Element of HP-WFF equals :: HILBERT2:def 1
<*(3 + a₁)*>;
coherence by HILBERT1:def 4;

end;

:: deftheorem Def1 defines prop HILBERT2:def 1 :

definition

let c₁ be set ;
redefine attr a₁ is with_VERUM means :: HILBERT2:def 2
VERUM in a₁;
compatibility by HILBERT1:def 1;
redefine attr a₁ is with_propositional_variables means :: HILBERT2:def 3
for b₁ being Nat holds prop b₁ in a₁;
compatibility

proof end;

end;

:: deftheorem Def2 defines with_VERUM HILBERT2:def 2 :

:: deftheorem Def3 defines with_propositional_variables HILBERT2:def 3 :

definition

let c₁ be Subset of HP-WFF ;
redefine attr a₁ is with_implication means :: HILBERT2:def 4
for b₁, b₂ being Element of HP-WFF st b₁ in a₁ & b₂ in a₁ holds
b₁ => b₂ in a₁;
compatibility

proof end;

redefine attr a₁ is with_conjunction means :: HILBERT2:def 5
for b₁, b₂ being Element of HP-WFF st b₁ in a₁ & b₂ in a₁ holds
b₁ '&' b₂ in a₁;
compatibility

proof end;

end;

:: deftheorem Def4 defines with_implication HILBERT2:def 4 :

:: deftheorem Def5 defines with_conjunction HILBERT2:def 5 :

definition

let c₁ be Element of HP-WFF ;
attr a₁ is conjunctive means :Def6: :: HILBERT2:def 6
ex b₁, b₂ being Element of HP-WFF st a₁ = b₁ '&' b₂;
attr a₁ is conditional means :Def7: :: HILBERT2:def 7
ex b₁, b₂ being Element of HP-WFF st a₁ = b₁ => b₂;
attr a₁ is simple means :Def8: :: HILBERT2:def 8
ex b₁ being Nat st a₁ = prop b₁;

end;

:: deftheorem Def6 defines conjunctive HILBERT2:def 6 :

:: deftheorem Def7 defines conditional HILBERT2:def 7 :

:: deftheorem Def8 defines simple HILBERT2:def 8 :

scheme :: HILBERT2:sch 2
s2{ P₁[ set ] } :

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

provided

E12: P₁[ VERUM ] and
E13: for b₁ being Nat holds P₁[ prop b₁] and
E14: for b₁, b₂ being Element of HP-WFF st P₁[b₁] & P₁[b₂] holds
( P₁[b₁ '&' b₂] & P₁[b₁ => b₂] )

proof end;

theorem Th9: :: HILBERT2:9

for b₁ being Element of HP-WFF holds
( b₁ is conjunctive or b₁ is conditional or b₁ is simple or b₁ = VERUM )

proof end;

theorem Th10: :: HILBERT2:10

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

proof end;

theorem Th11: :: HILBERT2:11

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

proof end;

theorem Th12: :: HILBERT2:12

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

proof end;

theorem Th13: :: HILBERT2:13

for b₁ being Nat
for b₂ being Element of HP-WFF st b₂ . 1 = 3 + b₁ holds
b₂ is simple

proof end;

theorem Th14: :: HILBERT2:14

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

proof end;

theorem Th15: :: HILBERT2:15

for b₁, b₂ being Element of HP-WFF holds
( len b₁ < len (b₁ '&' b₂) & len b₂ < len (b₁ '&' b₂) )

proof end;

theorem Th16: :: HILBERT2:16

for b₁, b₂ being Element of HP-WFF holds
( len b₁ < len (b₁ => b₂) & len b₂ < len (b₁ => b₂) )

proof end;

theorem Th17: :: HILBERT2:17

for b₁, b₂ being Element of HP-WFF
for b₃ being FinSequence st b₁ = b₂ ^ b₃ holds
b₁ = b₂

proof end;

theorem Th18: :: HILBERT2:18

for b₁, b₂, b₃, b₄ being Element of HP-WFF st b₁ ^ b₂ = b₃ ^ b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th19: :: HILBERT2:19

for b₁, b₂, b₃, b₄ being Element of HP-WFF st b₁ '&' b₂ = b₃ '&' b₄ holds
( b₁ = b₃ & b₄ = b₂ )

proof end;

theorem Th20: :: HILBERT2:20

for b₁, b₂, b₃, b₄ being Element of HP-WFF st b₁ => b₂ = b₃ => b₄ holds
( b₁ = b₃ & b₄ = b₂ )

proof end;

theorem Th21: :: HILBERT2:21

for b₁, b₂ being Nat st prop b₁ = prop b₂ holds
b₁ = b₂

proof end;

theorem Th22: :: HILBERT2:22

for b₁, b₂, b₃, b₄ being Element of HP-WFF holds b₁ '&' b₂ <> b₃ => b₄

proof end;

theorem Th23: :: HILBERT2:23

for b₁, b₂ being Element of HP-WFF holds b₁ '&' b₂ <> VERUM

proof end;

theorem Th24: :: HILBERT2:24

for b₁ being Nat
for b₂, b₃ being Element of HP-WFF holds b₂ '&' b₃ <> prop b₁

proof end;

theorem Th25: :: HILBERT2:25

for b₁, b₂ being Element of HP-WFF holds b₁ => b₂ <> VERUM

proof end;

theorem Th26: :: HILBERT2:26

for b₁ being Nat
for b₂, b₃ being Element of HP-WFF holds b₂ => b₃ <> prop b₁

proof end;

theorem Th27: :: HILBERT2:27

for b₁, b₂ being Element of HP-WFF holds
( b₁ '&' b₂ <> b₁ & b₁ '&' b₂ <> b₂ )

proof end;

theorem Th28: :: HILBERT2:28

for b₁, b₂ being Element of HP-WFF holds
( b₁ => b₂ <> b₁ & b₁ => b₂ <> b₂ )

proof end;

theorem Th29: :: HILBERT2:29

for b₁ being Nat holds VERUM <> prop b₁

proof end;

scheme :: HILBERT2:sch 3
s3{ F₁() -> set , F₂( 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 b₁ being ManySortedSet of HP-WFF st
( b₁ . VERUM = F₁() & ( for b₂ being Nat holds b₁ . (prop b₂) = F₂(b₂) ) & ( for b₂, b₃ being Element of HP-WFF holds
( P₁[b₂,b₃,b₁ . b₂,b₁ . b₃,b₁ . (b₂ '&' b₃)] & P₂[b₂,b₃,b₁ . b₂,b₁ . b₃,b₁ . (b₂ => b₃)] ) ) )

provided

E31: for b₁, b₂ being Element of HP-WFF
for b₃, b₄ being set ex b₅ being set st P₁[b₁,b₂,b₃,b₄,b₅] and
E32: for b₁, b₂ being Element of HP-WFF
for b₃, b₄ being set ex b₅ being set st P₂[b₁,b₂,b₃,b₄,b₅] and
E33: for b₁, b₂ being Element of HP-WFF
for b₃, b₄, b₅, b₆ being set st P₁[b₁,b₂,b₃,b₄,b₅] & P₁[b₁,b₂,b₃,b₄,b₆] holds
b₅ = b₆ and
E34: for b₁, b₂ being Element of HP-WFF
for b₃, b₄, b₅, b₆ being set st P₂[b₁,b₂,b₃,b₄,b₅] & P₂[b₁,b₂,b₃,b₄,b₆] holds
b₅ = b₆

proof end;

scheme :: HILBERT2:sch 4
s4{ F₁() -> set , F₂( Nat) -> set , F₃( set , set ) -> set , F₄( set , set ) -> set } :

ex b₁ being ManySortedSet of HP-WFF st
( b₁ . VERUM = F₁() & ( for b₂ being Nat holds b₁ . (prop b₂) = F₂(b₂) ) & ( for b₂, b₃ being Element of HP-WFF holds
( b₁ . (b₂ '&' b₃) = F₃((b₁ . b₂),(b₁ . b₃)) & b₁ . (b₂ => b₃) = F₄((b₁ . b₂),(b₁ . b₃)) ) ) )

proof end;

definition

func HP-Subformulae -> ManySortedSet of HP-WFF means :Def9: :: HILBERT2:def 9
( a₁ . VERUM = root-tree VERUM & ( for b₁ being Nat holds a₁ . (prop b₁) = root-tree (prop b₁) ) & ( for b₁, b₂ being Element of HP-WFF ex b₃, b₄ being DecoratedTree of HP-WFF st
( b₃ = a₁ . b₁ & b₄ = a₁ . b₂ & a₁ . (b₁ '&' b₂) = (b₁ '&' b₂) -tree b₃,b₄ & a₁ . (b₁ => b₂) = (b₁ => b₂) -tree b₃,b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be Element of HP-WFF ;
func Subformulae c₁ -> DecoratedTree of HP-WFF equals :: HILBERT2:def 10
HP-Subformulae . a₁;
correctness

proof end;

end;

:: deftheorem Def10 defines Subformulae HILBERT2:def 10 :

theorem Th30: :: HILBERT2:30

Subformulae VERUM = root-tree VERUM by Def9;

theorem Th31: :: HILBERT2:31

for b₁ being Nat holds Subformulae (prop b₁) = root-tree (prop b₁) by Def9;

theorem Th32: :: HILBERT2:32

for b₁, b₂ being Element of HP-WFF holds Subformulae (b₁ '&' b₂) = (b₁ '&' b₂) -tree (Subformulae b₁),(Subformulae b₂)

proof end;

theorem Th33: :: HILBERT2:33

for b₁, b₂ being Element of HP-WFF holds Subformulae (b₁ => b₂) = (b₁ => b₂) -tree (Subformulae b₁),(Subformulae b₂)

proof end;

theorem Th34: :: HILBERT2:34

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

proof end;

theorem Th35: :: HILBERT2:35

for b₁ being Element of HP-WFF
for b₂ being Element of dom (Subformulae b₁) holds (Subformulae b₁) | b₂ = Subformulae ((Subformulae b₁) . b₂)

proof end;

theorem Th36: :: HILBERT2:36

for b₁, b₂ being Element of HP-WFF holds
( not b₁ in Leaves (Subformulae b₂) or b₁ = VERUM or b₁ is simple )

proof end;