:: Hilbert Positive Propositional Calculus
:: by Adam Grabowski
::
:: Received February 20, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

definition

let D be set ;

attr D is with_VERUM means :Def1: :: HILBERT1:def 1
<*0*> in D;

end;

:: deftheorem Def1 defines with_VERUM HILBERT1:def 1 :
for D being set holds
( D is with_VERUM iff <*0*> in D );

definition

let D be set ;

attr D is with_implication means :Def2: :: HILBERT1:def 2
for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D;

end;

:: deftheorem Def2 defines with_implication HILBERT1:def 2 :
for D being set holds
( D is with_implication iff for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D );

definition

let D be set ;

attr D is with_conjunction means :Def3: :: HILBERT1:def 3
for p, q being FinSequence st p in D & q in D holds
(<*2*> ^ p) ^ q in D;

end;

:: deftheorem Def3 defines with_conjunction HILBERT1:def 3 :
for D being set holds
( D is with_conjunction iff for p, q being FinSequence st p in D & q in D holds
(<*2*> ^ p) ^ q in D );

definition

let D be set ;

attr D is with_propositional_variables means :Def4: :: HILBERT1:def 4
for n being Element of NAT holds <*(3 + n)*> in D;

end;

:: deftheorem Def4 defines with_propositional_variables HILBERT1:def 4 :
for D being set holds
( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D );

definition

let D be set ;

attr D is HP-closed means :Def5: :: HILBERT1:def 5
( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables );

end;

:: deftheorem Def5 defines HP-closed HILBERT1:def 5 :
for D being set holds
( D is HP-closed iff ( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables ) );

Lm1: for D being set st D is HP-closed holds
not D is empty

proof end;

registration

cluster HP-closed -> non empty with_VERUM with_implication with_conjunction with_propositional_variables for set ;

coherence
for b₁ being set st b₁ is HP-closed holds
( b₁ is with_VERUM & b₁ is with_implication & b₁ is with_conjunction & b₁ is with_propositional_variables & not b₁ is empty ) by Lm1;

cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed for Element of K16((NAT *));

coherence
for b₁ being Subset of (NAT *) st b₁ is with_VERUM & b₁ is with_implication & b₁ is with_conjunction & b₁ is with_propositional_variables holds
b₁ is HP-closed ;

end;

definition

func HP-WFF -> set means :Def6: :: HILBERT1:def 6
( it is HP-closed & ( for D being set st D is HP-closed holds
it c= D ) );

existence
ex b₁ being set st
( b₁ is HP-closed & ( for D being set st D is HP-closed holds
b₁ c= D ) )

proof end;

uniqueness
for b₁, b₂ being set st b₁ is HP-closed & ( for D being set st D is HP-closed holds
b₁ c= D ) & b₂ is HP-closed & ( for D being set st D is HP-closed holds
b₂ c= D ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines HP-WFF HILBERT1:def 6 :
for b₁ being set holds
( b₁ = HP-WFF iff ( b₁ is HP-closed & ( for D being set st D is HP-closed holds
b₁ c= D ) ) );

registration

cluster HP-WFF -> HP-closed ;

coherence
HP-WFF is HP-closed by Def6;

end;

registration

cluster non empty HP-closed for set ;

existence
ex b₁ being set st
( b₁ is HP-closed & not b₁ is empty )

proof end;

end;

registration

cluster HP-WFF -> functional ;

coherence
HP-WFF is functional

proof end;

end;

registration

cluster -> FinSequence-like for Element of HP-WFF ;

coherence
for b₁ being Element of HP-WFF holds b₁ is FinSequence-like

proof end;

end;

definition

mode HP-formula is Element of HP-WFF ;

end;

definition

func VERUM -> HP-formula equals :: HILBERT1:def 7
<*0*>;

correctness
coherence
<*0*> is HP-formula;
by Def1;
let p, q be Element of HP-WFF ;

func p => q -> HP-formula equals :: HILBERT1:def 8
(<*1*> ^ p) ^ q;

coherence
(<*1*> ^ p) ^ q is HP-formula by Def2;

func p '&' q -> HP-formula equals :: HILBERT1:def 9
(<*2*> ^ p) ^ q;

correctness
coherence
(<*2*> ^ p) ^ q is HP-formula;
by Def3;

end;

:: deftheorem defines VERUM HILBERT1:def 7 :
VERUM = <*0*>;

:: deftheorem defines => HILBERT1:def 8 :
for p, q being Element of HP-WFF holds p => q = (<*1*> ^ p) ^ q;

:: deftheorem defines '&' HILBERT1:def 9 :
for p, q being Element of HP-WFF holds p '&' q = (<*2*> ^ p) ^ q;

definition

let T be Subset of HP-WFF;

attr T is Hilbert_theory means :Def10: :: HILBERT1:def 10
( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) );

correctness
;

end;

:: deftheorem Def10 defines Hilbert_theory HILBERT1:def 10 :
for T being Subset of HP-WFF holds
( T is Hilbert_theory iff ( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) ) );

definition

let X be Subset of HP-WFF;

func CnPos X -> Subset of HP-WFF means :Def11: :: HILBERT1:def 11
for r being Element of HP-WFF holds
( r in it iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T );

existence
ex b₁ being Subset of HP-WFF st
for r being Element of HP-WFF holds
( r in b₁ iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T )

proof end;

uniqueness
for b₁, b₂ being Subset of HP-WFF st ( for r being Element of HP-WFF holds
( r in b₁ iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) & ( for r being Element of HP-WFF holds
( r in b₂ iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines CnPos HILBERT1:def 11 :
for X, b₂ being Subset of HP-WFF holds
( b₂ = CnPos X iff for r being Element of HP-WFF holds
( r in b₂ iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) );

definition

func HP_TAUT -> Subset of HP-WFF equals :: HILBERT1:def 12
CnPos ({} HP-WFF);

correctness
coherence
CnPos ({} HP-WFF) is Subset of HP-WFF;
;

end;

:: deftheorem defines HP_TAUT HILBERT1:def 12 :
HP_TAUT = CnPos ({} HP-WFF);

theorem Th1: :: HILBERT1:1

for X being Subset of HP-WFF holds VERUM in CnPos X

proof end;

theorem Th2: :: HILBERT1:2

for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X

proof end;

theorem Th3: :: HILBERT1:3

for X being Subset of HP-WFF
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X

proof end;

theorem Th4: :: HILBERT1:4

for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => p) in CnPos X

proof end;

theorem Th5: :: HILBERT1:5

for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X

proof end;

theorem Th6: :: HILBERT1:6

for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X

proof end;

theorem Th7: :: HILBERT1:7

for X being Subset of HP-WFF
for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds
q in CnPos X

proof end;

theorem Th8: :: HILBERT1:8

for T, X being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
CnPos X c= T by Def11;

theorem Th9: :: HILBERT1:9

for X being Subset of HP-WFF holds X c= CnPos X

proof end;

theorem Th10: :: HILBERT1:10

for X, Y being Subset of HP-WFF st X c= Y holds
CnPos X c= CnPos Y

proof end;

Lm2: for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X

proof end;

theorem :: HILBERT1:11

for X being Subset of HP-WFF holds CnPos (CnPos X) = CnPos X

proof end;

Lm3: for X being Subset of HP-WFF holds CnPos X is Hilbert_theory
by Th1, Th4, Th3, Th5, Th6, Th2, Th7;

registration

let X be Subset of HP-WFF;

cluster CnPos X -> Hilbert_theory ;

coherence
CnPos X is Hilbert_theory by Lm3;

end;

theorem Th12: :: HILBERT1:12

for T being Subset of HP-WFF holds
( T is Hilbert_theory iff CnPos T = T )

proof end;

theorem :: HILBERT1:13

for T being Subset of HP-WFF st T is Hilbert_theory holds
HP_TAUT c= T

proof end;

registration

cluster HP_TAUT -> Hilbert_theory ;

coherence
HP_TAUT is Hilbert_theory ;

end;

theorem Th14: :: HILBERT1:14

for p being Element of HP-WFF holds p => p in HP_TAUT

proof end;

theorem Th15: :: HILBERT1:15

for p, q being Element of HP-WFF st q in HP_TAUT holds
p => q in HP_TAUT

proof end;

theorem :: HILBERT1:16

for p being Element of HP-WFF holds p => VERUM in HP_TAUT by Th1, Th15;

theorem :: HILBERT1:17

for p, q being Element of HP-WFF holds (p => q) => (p => p) in HP_TAUT by Th14, Th15;

theorem :: HILBERT1:18

for p, q being Element of HP-WFF holds (q => p) => (p => p) in HP_TAUT by Th14, Th15;

theorem Th19: :: HILBERT1:19

for p, q, r being Element of HP-WFF holds (q => r) => ((p => q) => (p => r)) in HP_TAUT

proof end;

theorem Th20: :: HILBERT1:20

for p, q, r being Element of HP-WFF st p => (q => r) in HP_TAUT holds
q => (p => r) in HP_TAUT

proof end;

theorem Th21: :: HILBERT1:21

for p, q, r being Element of HP-WFF holds (p => q) => ((q => r) => (p => r)) in HP_TAUT

proof end;

theorem Th22: :: HILBERT1:22

for p, q, r being Element of HP-WFF st p => q in HP_TAUT holds
(q => r) => (p => r) in HP_TAUT

proof end;

theorem Th23: :: HILBERT1:23

for p, q, r being Element of HP-WFF st p => q in HP_TAUT & q => r in HP_TAUT holds
p => r in HP_TAUT

proof end;

Lm4: for p, q, r, s being Element of HP-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT

proof end;

theorem Th24: :: HILBERT1:24

for p, q, r, s being Element of HP-WFF holds (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT

proof end;

theorem :: HILBERT1:25

for p, q, r being Element of HP-WFF holds ((p => q) => r) => (q => r) in HP_TAUT

proof end;

theorem Th26: :: HILBERT1:26

for p, q, r being Element of HP-WFF holds (p => (q => r)) => (q => (p => r)) in HP_TAUT

proof end;

theorem Th27: :: HILBERT1:27

for p, q being Element of HP-WFF holds (p => (p => q)) => (p => q) in HP_TAUT

proof end;

theorem :: HILBERT1:28

for p, q being Element of HP-WFF holds q => ((q => p) => p) in HP_TAUT

proof end;

theorem Th29: :: HILBERT1:29

for p, q, s being Element of HP-WFF st s => (q => p) in HP_TAUT & q in HP_TAUT holds
s => p in HP_TAUT

proof end;

theorem Th30: :: HILBERT1:30

for p being Element of HP-WFF holds p => (p '&' p) in HP_TAUT

proof end;

theorem Th31: :: HILBERT1:31

for p, q being Element of HP-WFF holds
( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )

proof end;

theorem :: HILBERT1:32

for p, q being Element of HP-WFF st p '&' q in HP_TAUT holds
q '&' p in HP_TAUT

proof end;

theorem Th33: :: HILBERT1:33

for p, q, r being Element of HP-WFF holds ((p '&' q) => r) => (p => (q => r)) in HP_TAUT

proof end;

theorem Th34: :: HILBERT1:34

for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p '&' q) => r) in HP_TAUT

proof end;

theorem Th35: :: HILBERT1:35

for p, q, r being Element of HP-WFF holds (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT

proof end;

theorem Th36: :: HILBERT1:36

for p, q being Element of HP-WFF holds ((p => q) '&' p) => q in HP_TAUT

proof end;

theorem :: HILBERT1:37

for p, q, s being Element of HP-WFF holds (((p => q) '&' p) '&' s) => q in HP_TAUT

proof end;

theorem :: HILBERT1:38

for p, q, s being Element of HP-WFF holds (q => s) => ((p '&' q) => s) in HP_TAUT

proof end;

theorem Th39: :: HILBERT1:39

for p, q, s being Element of HP-WFF holds (q => s) => ((q '&' p) => s) in HP_TAUT

proof end;

theorem Th40: :: HILBERT1:40

for p, q, s being Element of HP-WFF holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT

proof end;

theorem Th41: :: HILBERT1:41

for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT

proof end;

theorem Th42: :: HILBERT1:42

for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT

proof end;

theorem Th43: :: HILBERT1:43

for p, q being Element of HP-WFF holds (p '&' q) => (q '&' p) in HP_TAUT

proof end;

theorem Th44: :: HILBERT1:44

for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT

proof end;

theorem Th45: :: HILBERT1:45

for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT

proof end;

theorem Th46: :: HILBERT1:46

for p, q, s being Element of HP-WFF holds (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT

proof end;

theorem :: HILBERT1:47

for p, q, s being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT

proof end;

theorem :: HILBERT1:48

for p, q, s being Element of HP-WFF holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT

proof end;

Lm5: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT

proof end;

Lm6: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT

proof end;

Lm7: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT

proof end;

Lm8: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT

proof end;

Lm9: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT

proof end;

Lm10: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT

proof end;

Lm11: for p, q, s being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT

proof end;

Lm12: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT

proof end;

Lm13: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT

proof end;

Lm14: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT

proof end;

Lm15: for p, q, s being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT

proof end;

theorem :: HILBERT1:49

for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT

proof end;

Lm16: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT

proof end;

Lm17: for p, q, s being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT

proof end;

Lm18: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT

proof end;

Lm19: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT

proof end;

Lm20: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT

proof end;

theorem :: HILBERT1:50

for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT

proof end;