begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
begin
:: deftheorem defines prop HILBERT2:def 1 :
for n being Element of NAT holds prop n = <*(3 + n)*>;
:: 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 );
:: 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 );
:: 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 );
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
scheme
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 ] } :
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
begin
definition
func HP-Subformulae -> ManySortedSet of
HP-WFF means :
Def9:
(
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) ) ) )
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
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) ) ) ) );
:: deftheorem defines Subformulae HILBERT2:def 10 :
for p being Element of HP-WFF holds Subformulae p = HP-Subformulae . p;
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem