:: Defining by structural induction in the positive propositional language
:: by Andrzej Trybulec
::
:: Received April 23, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem Th1: :: HILBERT2:1
theorem Th2: :: HILBERT2:2
theorem Th3: :: HILBERT2:3
theorem Th4: :: HILBERT2:4
theorem Th5: :: HILBERT2:5
theorem Th6: :: HILBERT2:6
theorem Th7: :: HILBERT2:7
theorem Th8: :: HILBERT2:8
:: deftheorem defines prop HILBERT2:def 1 :
:: deftheorem 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: :: HILBERT2:9
theorem Th10: :: HILBERT2:10
theorem Th11: :: HILBERT2:11
theorem Th12: :: HILBERT2:12
theorem :: HILBERT2:13
theorem :: HILBERT2:14
theorem Th15: :: HILBERT2:15
theorem Th16: :: HILBERT2:16
theorem Th17: :: HILBERT2:17
theorem Th18: :: HILBERT2:18
theorem Th19: :: HILBERT2:19
theorem Th20: :: HILBERT2:20
theorem Th21: :: HILBERT2:21
theorem Th22: :: HILBERT2:22
theorem Th23: :: HILBERT2:23
theorem Th24: :: HILBERT2:24
theorem Th25: :: HILBERT2:25
theorem Th26: :: HILBERT2:26
theorem Th27: :: HILBERT2:27
theorem Th28: :: HILBERT2:28
theorem Th29: :: HILBERT2:29
scheme :: HILBERT2:sch 3
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
definition
func HP-Subformulae -> ManySortedSet of
HP-WFF means :
Def9:
:: HILBERT2:def 9
(
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: :: HILBERT2:30
theorem :: HILBERT2:31
theorem Th32: :: HILBERT2:32
theorem Th33: :: HILBERT2:33
theorem Th34: :: HILBERT2:34
theorem Th35: :: HILBERT2:35
theorem :: HILBERT2:36