begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
begin
:: deftheorem defines prop HILBERT2:def 1 :
:: deftheorem Def2 defines with_VERUM HILBERT2:def 2 :
:: deftheorem defines with_propositional_variables HILBERT2:def 3 :
:: deftheorem defines with_implication HILBERT2:def 4 :
:: deftheorem defines with_conjunction HILBERT2:def 5 :
:: deftheorem Def6 defines conjunctive HILBERT2:def 6 :
:: deftheorem Def7 defines conditional HILBERT2:def 7 :
:: deftheorem Def8 defines simple HILBERT2:def 8 :
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
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 Element of 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' ) ) )
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 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 Element of 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
end;
:: deftheorem Def9 defines HP-Subformulae HILBERT2:def 9 :
:: deftheorem defines Subformulae HILBERT2:def 10 :
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem