:: HILBERT2 semantic presentation

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, X being set 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;

registration

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

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

proof end;

end;

registration

let x be set ;
let T1 be DecoratedTree;
cluster x -tree T1 -> non root ;
coherence

proof end;

let T2 be DecoratedTree;
cluster x -tree T1,T2 -> non root ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem defines prop HILBERT2:def 1 :

definition

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

proof end;

end;

:: deftheorem defines with_VERUM HILBERT2:def 2 :

:: deftheorem defines with_propositional_variables HILBERT2:def 3 :

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

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

proof end;

end;

:: deftheorem defines with_implication HILBERT2:def 4 :

:: deftheorem defines with_conjunction HILBERT2:def 5 :

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 Nat st p = prop n;

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

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

provided

A1: P₁[ VERUM ] and
A2: for n being 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 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 n, m being 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 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 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 Nat holds VERUM <> prop n

proof end;

scheme :: HILBERT2:sch 3
HPMSSExL{ 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 M being ManySortedSet of HP-WFF st
( M . VERUM = F₁() & ( for n being 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₂( Nat) -> set , F₃( set , set ) -> set , F₄( set , set ) -> set } :

ex M being ManySortedSet of HP-WFF st
( M . VERUM = F₁() & ( for n being 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 Nat holds it . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of HP-WFF st
( p' = it . p & q' = it . q & it . (p '&' q) = (p '&' q) -tree p',q' & it . (p => q) = (p => q) -tree p',q' ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

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

proof end;

end;

:: deftheorem defines Subformulae HILBERT2:def 10 :

theorem Th30: :: HILBERT2:30

Subformulae VERUM = root-tree VERUM by Def9;

theorem Th31: :: HILBERT2:31

for n being 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;