CQC_THE3: Logical Equivalence of Formulae

:: Logical Equivalence of Formulae
:: by Oleg Okhotnikov
::
:: Received January 24, 1995
:: Copyright (c) 1995-2011 Association of Mizar Users

begin

theorem Th1: :: CQC_THE3:1

for p being Element of CQC-WFF
for X being Subset of CQC-WFF st p in X holds
X |- p

proof end;

theorem Th2: :: CQC_THE3:2

for X, Y being Subset of CQC-WFF st X c= Cn Y holds
Cn X c= Cn Y by CQC_THE1:36, CQC_THE1:37;

theorem Th3: :: CQC_THE3:3

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p & {p} |- q holds
X |- q

proof end;

theorem Th4: :: CQC_THE3:4

for p being Element of CQC-WFF
for X, Y being Subset of CQC-WFF st X |- p & X c= Y holds
Y |- p

proof end;

definition

let p, q be Element of CQC-WFF ;
pred p |- q means :Def1: :: CQC_THE3:def 1
{p} |- q;

end;

:: deftheorem Def1 defines |- CQC_THE3:def 1 :

theorem Th5: :: CQC_THE3:5

for p being Element of CQC-WFF holds p |- p

proof end;

theorem Th6: :: CQC_THE3:6

for p, q, r being Element of CQC-WFF st p |- q & q |- r holds
p |- r

proof end;

definition

let X, Y be Subset of CQC-WFF;
pred X |- Y means :Def2: :: CQC_THE3:def 2
for p being Element of CQC-WFF st p in Y holds
X |- p;

end;

:: deftheorem Def2 defines |- CQC_THE3:def 2 :

theorem Th7: :: CQC_THE3:7

for X, Y being Subset of CQC-WFF holds
( X |- Y iff Y c= Cn X )

proof end;

theorem :: CQC_THE3:8

for X being Subset of CQC-WFF holds X |- X

proof end;

theorem Th9: :: CQC_THE3:9

for X, Y, Z being Subset of CQC-WFF st X |- Y & Y |- Z holds
X |- Z

proof end;

theorem Th10: :: CQC_THE3:10

for p being Element of CQC-WFF
for X being Subset of CQC-WFF holds
( X |- {p} iff X |- p )

proof end;

theorem Th11: :: CQC_THE3:11

for p, q being Element of CQC-WFF holds
( {p} |- {q} iff p |- q )

proof end;

theorem :: CQC_THE3:12

for X, Y being Subset of CQC-WFF st X c= Y holds
Y |- X

proof end;

theorem Th13: :: CQC_THE3:13

for X being Subset of CQC-WFF holds X |- TAUT

proof end;

theorem Th14: :: CQC_THE3:14

{} CQC-WFF |- TAUT by Th13;

definition

let X be Subset of CQC-WFF;
pred |- X means :Def3: :: CQC_THE3:def 3
for p being Element of CQC-WFF st p in X holds
p is valid ;

end;

:: deftheorem Def3 defines |- CQC_THE3:def 3 :

theorem Th15: :: CQC_THE3:15

for X being Subset of CQC-WFF holds
( |- X iff {} CQC-WFF |- X )

proof end;

theorem :: CQC_THE3:16

|- TAUT by Th14, Th15;

theorem :: CQC_THE3:17

for X being Subset of CQC-WFF holds
( |- X iff X c= TAUT )

proof end;

definition

let X, Y be Subset of CQC-WFF;
pred X |-| Y means :Def4: :: CQC_THE3:def 4
for p being Element of CQC-WFF holds
( X |- p iff Y |- p );
reflexivity ;
symmetry ;

end;

:: deftheorem Def4 defines |-| CQC_THE3:def 4 :

theorem Th18: :: CQC_THE3:18

for X, Y being Subset of CQC-WFF holds
( X |-| Y iff ( X |- Y & Y |- X ) )

proof end;

theorem Th19: :: CQC_THE3:19

for X, Y, Z being Subset of CQC-WFF st X |-| Y & Y |-| Z holds
X |-| Z

proof end;

theorem Th20: :: CQC_THE3:20

for X, Y being Subset of CQC-WFF holds
( X |-| Y iff Cn X = Cn Y )

proof end;

Lm1: for X, Y being Subset of CQC-WFF holds X \/ Y c= (Cn X) \/ (Cn Y)

proof end;

theorem Th21: :: CQC_THE3:21

for X, Y being Subset of CQC-WFF holds (Cn X) \/ (Cn Y) c= Cn (X \/ Y)

proof end;

theorem Th22: :: CQC_THE3:22

for X, Y being Subset of CQC-WFF holds Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))

proof end;

theorem :: CQC_THE3:23

for X being Subset of CQC-WFF holds X |-| Cn X

proof end;

theorem :: CQC_THE3:24

for X, Y being Subset of CQC-WFF holds X \/ Y |-| (Cn X) \/ (Cn Y)

proof end;

theorem Th25: :: CQC_THE3:25

for X1, X2, Y being Subset of CQC-WFF st X1 |-| X2 holds
X1 \/ Y |-| X2 \/ Y

proof end;

theorem Th26: :: CQC_THE3:26

for X1, X2, Y, Z being Subset of CQC-WFF st X1 |-| X2 & X1 \/ Y |- Z holds
X2 \/ Y |- Z

proof end;

theorem Th27: :: CQC_THE3:27

for X1, X2, Y being Subset of CQC-WFF st X1 |-| X2 & Y |- X1 holds
Y |- X2

proof end;

definition

let p, q be Element of CQC-WFF ;
pred p |-| q means :Def5: :: CQC_THE3:def 5
( p |- q & q |- p );
reflexivity by Th5;
symmetry ;

end;

:: deftheorem Def5 defines |-| CQC_THE3:def 5 :

theorem Th28: :: CQC_THE3:28

for p, q, r being Element of CQC-WFF st p |-| q & q |-| r holds
p |-| r

proof end;

theorem Th29: :: CQC_THE3:29

for p, q being Element of CQC-WFF holds
( p |-| q iff {p} |-| {q} )

proof end;

theorem :: CQC_THE3:30

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st p |-| q & X |- p holds
X |- q

proof end;

theorem Th31: :: CQC_THE3:31

for p, q being Element of CQC-WFF holds {p,q} |-| {(p '&' q)}

proof end;

theorem :: CQC_THE3:32

for p, q being Element of CQC-WFF holds p '&' q |-| q '&' p

proof end;

Lm2: for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p & X |- q holds
X |- p '&' q

proof end;

Lm3: for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p '&' q holds
( X |- p & X |- q )

proof end;

theorem :: CQC_THE3:33

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds
( X |- p '&' q iff ( X |- p & X |- q ) ) by Lm2, Lm3;

Lm4: for p, q, r, s being Element of CQC-WFF st p |-| q & r |-| s holds
p '&' r |- q '&' s

proof end;

theorem :: CQC_THE3:34

for p, q, r, s being Element of CQC-WFF st p |-| q & r |-| s holds
p '&' r |-| q '&' s

proof end;

theorem Th35: :: CQC_THE3:35

for p being Element of CQC-WFF
for X being Subset of CQC-WFF
for x being bound_QC-variable holds
( X |- All (x,p) iff X |- p )

proof end;

theorem Th36: :: CQC_THE3:36

for p being Element of CQC-WFF
for x being bound_QC-variable holds All (x,p) |-| p

proof end;

theorem :: CQC_THE3:37

for p, q being Element of CQC-WFF
for x, y being bound_QC-variable st p |-| q holds
All (x,p) |-| All (y,q)

proof end;

definition

let p, q be Element of CQC-WFF ;
pred p is_an_universal_closure_of q means :Def6: :: CQC_THE3:def 6
( p is closed & ex n being Element of NAT st
( 1 <= n & ex L being FinSequence st
( len L = n & L . 1 = q & L . n = p & ( for k being Element of NAT st 1 <= k & k < n holds
ex x being bound_QC-variable ex r being Element of CQC-WFF st
( r = L . k & L . (k + 1) = All (x,r) ) ) ) ) );

end;

:: deftheorem Def6 defines is_an_universal_closure_of CQC_THE3:def 6 :

theorem Th38: :: CQC_THE3:38

for p, q being Element of CQC-WFF st p is_an_universal_closure_of q holds
p |-| q

proof end;

theorem Th39: :: CQC_THE3:39

for p, q being Element of CQC-WFF st p => q is valid holds
p |- q

proof end;

theorem Th40: :: CQC_THE3:40

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => q holds
X \/ {p} |- q

proof end;

theorem Th41: :: CQC_THE3:41

for p, q being Element of CQC-WFF st p is closed & p |- q holds
p => q is valid

proof end;

theorem :: CQC_THE3:42

for p1, p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )

proof end;

theorem Th43: :: CQC_THE3:43

for p, q being Element of CQC-WFF st p is closed & p |- q holds
'not' q |- 'not' p

proof end;

theorem :: CQC_THE3:44

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st p is closed & X \/ {p} |- q holds
X \/ {('not' q)} |- 'not' p

proof end;

theorem Th45: :: CQC_THE3:45

for p, q being Element of CQC-WFF st p is closed & 'not' p |- 'not' q holds
q |- p

proof end;

theorem :: CQC_THE3:46

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st p is closed & X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p

proof end;

theorem :: CQC_THE3:47

for p, q being Element of CQC-WFF st p is closed & q is closed holds
( p |- q iff 'not' q |- 'not' p ) by Th43, Th45;

theorem Th48: :: CQC_THE3:48

for p1, p, q1, q being Element of CQC-WFF st p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q holds
( p |- q iff 'not' q1 |- 'not' p1 )

proof end;

theorem :: CQC_THE3:49

for p1, p, q1, q being Element of CQC-WFF st p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q holds
( p |-| q iff 'not' p1 |-| 'not' q1 )

proof end;

definition

let p, q be Element of CQC-WFF ;
pred p <==> q means :Def7: :: CQC_THE3:def 7
p <=> q is valid ;
reflexivity

proof end;

proof end;

end;

:: deftheorem Def7 defines <==> CQC_THE3:def 7 :

theorem Th50: :: CQC_THE3:50

for p, q being Element of CQC-WFF holds
( p <==> q iff ( p => q is valid & q => p is valid ) )

proof end;

theorem :: CQC_THE3:51

for p, q, r being Element of CQC-WFF st p <==> q & q <==> r holds
p <==> r

proof end;

theorem :: CQC_THE3:52

for p, q being Element of CQC-WFF st p <==> q holds
p |-| q

proof end;

Lm5: for p, q being Element of CQC-WFF st p <==> q holds
'not' p <==> 'not' q

proof end;

Lm6: for p, q being Element of CQC-WFF st 'not' p <==> 'not' q holds
p <==> q

proof end;

theorem :: CQC_THE3:53

for p, q being Element of CQC-WFF holds
( p <==> q iff 'not' p <==> 'not' q ) by Lm5, Lm6;

theorem Th54: :: CQC_THE3:54

for p, q, r, s being Element of CQC-WFF st p <==> q & r <==> s holds
p '&' r <==> q '&' s

proof end;

theorem Th55: :: CQC_THE3:55

for p, q, r, s being Element of CQC-WFF st p <==> q & r <==> s holds
p => r <==> q => s

proof end;

theorem :: CQC_THE3:56

for p, q, r, s being Element of CQC-WFF st p <==> q & r <==> s holds
p 'or' r <==> q 'or' s

proof end;

theorem :: CQC_THE3:57

for p, q, r, s being Element of CQC-WFF st p <==> q & r <==> s holds
p <=> r <==> q <=> s

proof end;

theorem Th58: :: CQC_THE3:58

for p, q being Element of CQC-WFF
for x being bound_QC-variable st p <==> q holds
All (x,p) <==> All (x,q)

proof end;

theorem :: CQC_THE3:59

for p, q being Element of CQC-WFF
for x being bound_QC-variable st p <==> q holds
Ex (x,p) <==> Ex (x,q)

proof end;

theorem :: CQC_THE3:60

canceled;

theorem Th61: :: CQC_THE3:61

for k being Element of NAT
for l being QC-variable_list of k
for a being free_QC-variable
for x being bound_QC-variable holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))

proof end;

theorem Th62: :: CQC_THE3:62

for k being Element of NAT
for l being QC-variable_list of k
for a being free_QC-variable
for x being bound_QC-variable holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}

proof end;

theorem Th63: :: CQC_THE3:63

for x being bound_QC-variable
for h being QC-formula holds still_not-bound_in h c= still_not-bound_in (h . x)

proof end;

theorem Th64: :: CQC_THE3:64

for x being bound_QC-variable
for h being QC-formula holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x}

proof end;

theorem Th65: :: CQC_THE3:65

for p being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p

proof end;

theorem :: CQC_THE3:66

for p, q being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)

proof end;