:: HILBERT2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: HILBERT2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds
f = g
proof end;

theorem Th3: :: HILBERT2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set st <*x*> is FinSequence of X holds
x in X
proof end;

theorem Th4: :: HILBERT2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{} is Tree-yielding
by TREES_3:23;
end;

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 Nat st f ^ <*n*> in F1() holds
P1[f ^ <*n*>]
proof end;

theorem Th6: :: HILBERT2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for T1, T2 being DecoratedTree holds (x -tree T1,T2) . {} = x
proof end;

theorem Th7: :: HILBERT2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 root
proof end;
end;

registration
let x be set ;
let T1 be DecoratedTree;
cluster x -tree T1 -> non root ;
coherence
not x -tree T1 is root
proof end;
let T2 be DecoratedTree;
cluster x -tree T1,T2 -> non root ;
coherence
not x -tree T1,T2 is root
proof end;
end;

definition
let n be 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 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 )
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
( D is with_propositional_variables iff for n being 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 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 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 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 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] )
proof end;

theorem Th9: :: HILBERT2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF holds len p >= 1
proof end;

theorem Th11: :: HILBERT2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF st p . 1 = 1 holds
p is conditional
proof end;

theorem Th12: :: HILBERT2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF st p . 1 = 2 holds
p is conjunctive
proof end;

theorem :: HILBERT2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF st p . 1 = 0 holds
p = VERUM
proof end;

theorem Th15: :: HILBERT2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st prop n = prop m holds
n = m
proof end;

theorem Th22: :: HILBERT2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r, s being Element of HP-WFF holds p '&' q <> r => s
proof end;

theorem Th23: :: HILBERT2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds p '&' q <> VERUM
proof end;

theorem Th24: :: HILBERT2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being Element of HP-WFF holds p '&' q <> prop n
proof end;

theorem Th25: :: HILBERT2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds p => q <> VERUM
proof end;

theorem Th26: :: HILBERT2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being Element of HP-WFF holds p => q <> prop n
proof end;

theorem Th27: :: HILBERT2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds
( p '&' q <> p & p '&' q <> q )
proof end;

theorem Th28: :: HILBERT2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds
( p => q <> p & p => q <> q )
proof end;

theorem Th29: :: HILBERT2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds VERUM <> prop n
proof end;

scheme :: HILBERT2:sch 3
HPMSSExL{ F1() -> set , F2( 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 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
proof end;

scheme :: HILBERT2:sch 4
HPMSSLambda{ F1() -> set , F2( Nat) -> set , F3( set , set ) -> set , F4( set , set ) -> set } :
ex M being ManySortedSet of HP-WFF st
( M . VERUM = F1() & ( for n being 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)) ) ) )
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
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = root-tree VERUM & ( for n being Nat holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of HP-WFF st
( p' = b1 . p & q' = b1 . q & b1 . (p '&' q) = (p '&' q) -tree p',q' & b1 . (p => q) = (p => q) -tree p',q' ) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = root-tree VERUM & ( for n being Nat holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of HP-WFF st
( p' = b1 . p & q' = b1 . q & b1 . (p '&' q) = (p '&' q) -tree p',q' & b1 . (p => q) = (p => q) -tree p',q' ) ) & b2 . VERUM = root-tree VERUM & ( for n being Nat holds b2 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of HP-WFF st
( p' = b2 . p & q' = b2 . q & b2 . (p '&' q) = (p '&' q) -tree p',q' & b2 . (p => q) = (p => q) -tree p',q' ) ) holds
b1 = b2
proof end;
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 Nat holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of HP-WFF st
( p' = b1 . p & q' = b1 . q & b1 . (p '&' q) = (p '&' q) -tree p',q' & b1 . (p => q) = (p => q) -tree p',q' ) ) ) );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Subformulae VERUM = root-tree VERUM by Def9;

theorem Th31: :: HILBERT2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds Subformulae (prop n) = root-tree (prop n) by Def9;

theorem Th32: :: HILBERT2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF holds (Subformulae p) . {} = p
proof end;

theorem Th35: :: HILBERT2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds
( not p in Leaves (Subformulae q) or p = VERUM or p is simple )
proof end;