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


begin

theorem Th1: :: CQC_THE3:1
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p in X holds
X |- p
proofend;

theorem Th2: :: CQC_THE3:2
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) st X c= Cn Y holds
Cn X c= Cn Y by CQC_THE1:15, CQC_THE1:16;

theorem Th3: :: CQC_THE3:3
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p & {p} |- q holds
X |- q
proofend;

theorem Th4: :: CQC_THE3:4
for A being QC-alphabet
for p being Element of CQC-WFF A
for X, Y being Subset of (CQC-WFF A) st X |- p & X c= Y holds
Y |- p
proofend;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
predp |- q means :Def1: :: CQC_THE3:def 1
{p} |- q;
end;

:: deftheorem Def1 defines |- CQC_THE3:def_1_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p |- q iff {p} |- q );

theorem Th5: :: CQC_THE3:5
for A being QC-alphabet
for p being Element of CQC-WFF A holds p |- p
proofend;

theorem Th6: :: CQC_THE3:6
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p |- q & q |- r holds
p |- r
proofend;

definition
let A be QC-alphabet ;
let X, Y be Subset of (CQC-WFF A);
predX |- Y means :Def2: :: CQC_THE3:def 2
 for p being Element of CQC-WFF A st p in Y holds
X |- p;
end;

:: deftheorem Def2 defines |- CQC_THE3:def_2_:_
 for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |- Y iff for p being Element of CQC-WFF A st p in Y holds
X |- p );

theorem Th7: :: CQC_THE3:7
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |- Y iff Y c= Cn X )
proofend;

theorem :: CQC_THE3:8
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds X |- X
proofend;

theorem Th9: :: CQC_THE3:9
for A being QC-alphabet
for X, Y, Z being Subset of (CQC-WFF A) st X |- Y & Y |- Z holds
X |- Z
proofend;

theorem Th10: :: CQC_THE3:10
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- {p} iff X |- p )
proofend;

theorem Th11: :: CQC_THE3:11
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( {p} |- {q} iff p |- q )
proofend;

theorem :: CQC_THE3:12
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) st X c= Y holds
Y |- X
proofend;

theorem Th13: :: CQC_THE3:13
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds X |- TAUT A
proofend;

theorem :: CQC_THE3:14
for A being QC-alphabet holds {} (CQC-WFF A) |- TAUT A by Th13;

definition
let A be QC-alphabet ;
let X be Subset of (CQC-WFF A);
pred |- X means :Def3: :: CQC_THE3:def 3
 for p being Element of CQC-WFF A st p in X holds
p is valid ;
end;

:: deftheorem Def3 defines |- CQC_THE3:def_3_:_
 for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff for p being Element of CQC-WFF A st p in X holds
p is valid );

theorem Th15: :: CQC_THE3:15
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff {} (CQC-WFF A) |- X )
proofend;

theorem :: CQC_THE3:16
for A being QC-alphabet holds |- TAUT A
proofend;

theorem :: CQC_THE3:17
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff X c= TAUT A )
proofend;

definition
let A be QC-alphabet ;
let X, Y be Subset of (CQC-WFF A);
predX |-| Y means :Def4: :: CQC_THE3:def 4
 for p being Element of CQC-WFF A holds
( X |- p iff Y |- p );
reflexivity
 for X being Subset of (CQC-WFF A)
for p being Element of CQC-WFF A holds
( X |- p iff X |- p ) ;
symmetry
 for X, Y being Subset of (CQC-WFF A) st ( for p being Element of CQC-WFF A holds
( X |- p iff Y |- p ) ) holds
for p being Element of CQC-WFF A holds
( Y |- p iff X |- p ) ;
end;

:: deftheorem Def4 defines |-| CQC_THE3:def_4_:_
 for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff for p being Element of CQC-WFF A holds
( X |- p iff Y |- p ) );

theorem Th18: :: CQC_THE3:18
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff ( X |- Y & Y |- X ) )
proofend;

theorem Th19: :: CQC_THE3:19
for A being QC-alphabet
for X, Y, Z being Subset of (CQC-WFF A) st X |-| Y & Y |-| Z holds
X |-| Z
proofend;

theorem Th20: :: CQC_THE3:20
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff Cn X = Cn Y )
proofend;

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

theorem Th21: :: CQC_THE3:21
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds (Cn X) \/ (Cn Y) c= Cn (X \/ Y)
proofend;

theorem Th22: :: CQC_THE3:22
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))
proofend;

theorem :: CQC_THE3:23
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds X |-| Cn X
proofend;

theorem :: CQC_THE3:24
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds X \/ Y |-| (Cn X) \/ (Cn Y)
proofend;

theorem Th25: :: CQC_THE3:25
for A being QC-alphabet
for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 holds
X1 \/ Y |-| X2 \/ Y
proofend;

theorem Th26: :: CQC_THE3:26
for A being QC-alphabet
for X1, X2, Y, Z being Subset of (CQC-WFF A) st X1 |-| X2 & X1 \/ Y |- Z holds
X2 \/ Y |- Z
proofend;

theorem Th27: :: CQC_THE3:27
for A being QC-alphabet
for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 & Y |- X1 holds
Y |- X2
proofend;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
predp |-| q means :Def5: :: CQC_THE3:def 5
( p |- q & q |- p );
reflexivity
 for p being Element of CQC-WFF A holds
( p |- p & p |- p ) by Th5;
symmetry
 for p, q being Element of CQC-WFF A st p |- q & q |- p holds
( q |- p & p |- q ) ;
end;

:: deftheorem Def5 defines |-| CQC_THE3:def_5_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p |-| q iff ( p |- q & q |- p ) );

theorem Th28: :: CQC_THE3:28
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p |-| q & q |-| r holds
p |-| r
proofend;

theorem Th29: :: CQC_THE3:29
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p |-| q iff {p} |-| {q} )
proofend;

theorem :: CQC_THE3:30
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p |-| q & X |- p holds
X |- q
proofend;

theorem Th31: :: CQC_THE3:31
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds {p,q} |-| {(p '&' q)}
proofend;

theorem :: CQC_THE3:32
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p '&' q |-| q '&' p
proofend;

Lm2:  for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p & X |- q holds
X |- p '&' q
proofend;

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

theorem :: CQC_THE3:33
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- p '&' q iff ( X |- p & X |- q ) ) by Lm2, Lm3;

Lm4:  for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |- q '&' s
proofend;

theorem :: CQC_THE3:34
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |-| q '&' s
proofend;

theorem Th35: :: CQC_THE3:35
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A)
for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
proofend;

theorem Th36: :: CQC_THE3:36
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds All (x,p) |-| p
proofend;

theorem :: CQC_THE3:37
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x, y being bound_QC-variable of A st p |-| q holds
All (x,p) |-| All (y,q)
proofend;

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

:: deftheorem Def6 defines is_an_universal_closure_of CQC_THE3:def_6_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p is_an_universal_closure_of q iff ( p is closed &amp; ex n being Element of NAT st
( 1 <= n &amp; ex L being FinSequence st
( len L = n &amp; L . 1 = q &amp; L . n = p &amp; ( for k being Element of NAT st 1 <= k &amp; k < n holds
ex x being bound_QC-variable of A ex r being Element of CQC-WFF A st
( r = L . k &amp; L . (k + 1) = All (x,r) ) ) ) ) ) );

theorem Th38: :: CQC_THE3:38
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is_an_universal_closure_of q holds
p |-| q
proofend;

theorem Th39: :: CQC_THE3:39
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p => q is valid holds
p |- q
proofend;

theorem Th40: :: CQC_THE3:40
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => q holds
X \/ {p} |- q
proofend;

theorem Th41: :: CQC_THE3:41
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed &amp; p |- q holds
p => q is valid
proofend;

theorem :: CQC_THE3:42
for A being QC-alphabet
for p1, p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )
proofend;

theorem Th43: :: CQC_THE3:43
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed &amp; p |- q holds
'not' q |- 'not' p
proofend;

theorem :: CQC_THE3:44
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p is closed &amp; X \/ {p} |- q holds
X \/ {('not' q)} |- 'not' p
proofend;

theorem Th45: :: CQC_THE3:45
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed &amp; 'not' p |- 'not' q holds
q |- p
proofend;

theorem :: CQC_THE3:46
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p is closed &amp; X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p
proofend;

theorem :: CQC_THE3:47
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed &amp; q is closed holds
( p |- q iff 'not' q |- 'not' p ) by Th43, Th45;

theorem Th48: :: CQC_THE3:48
for A being QC-alphabet
for p1, p, q1, q being Element of CQC-WFF A st p1 is_an_universal_closure_of p &amp; q1 is_an_universal_closure_of q holds
( p |- q iff 'not' q1 |- 'not' p1 )
proofend;

theorem :: CQC_THE3:49
for A being QC-alphabet
for p1, p, q1, q being Element of CQC-WFF A st p1 is_an_universal_closure_of p &amp; q1 is_an_universal_closure_of q holds
( p |-| q iff 'not' p1 |-| 'not' q1 )
proofend;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
predp <==> q means :Def7: :: CQC_THE3:def 7
p <=> q is valid ;
reflexivity
 for p being Element of CQC-WFF A holds p <=> p is valid
proofend;
symmetry
 for p, q being Element of CQC-WFF A st p <=> q is valid holds
q <=> p is valid
proofend;
end;

:: deftheorem Def7 defines <==> CQC_THE3:def_7_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p <==> q iff p <=> q is valid );

theorem Th50: :: CQC_THE3:50
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p <==> q iff ( p => q is valid &amp; q => p is valid ) )
proofend;

theorem :: CQC_THE3:51
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p <==> q &amp; q <==> r holds
p <==> r
proofend;

theorem :: CQC_THE3:52
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <==> q holds
p |-| q
proofend;

Lm5:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <==> q holds
'not' p <==> 'not' q
proofend;

Lm6:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st 'not' p <==> 'not' q holds
p <==> q
proofend;

theorem :: CQC_THE3:53
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p <==> q iff 'not' p <==> 'not' q ) by Lm5, Lm6;

theorem Th54: :: CQC_THE3:54
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q &amp; r <==> s holds
p '&amp;' r <==> q '&amp;' s
proofend;

theorem Th55: :: CQC_THE3:55
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q &amp; r <==> s holds
p => r <==> q => s
proofend;

theorem :: CQC_THE3:56
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q &amp; r <==> s holds
p 'or' r <==> q 'or' s
proofend;

theorem :: CQC_THE3:57
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q &amp; r <==> s holds
p <=> r <==> q <=> s
proofend;

theorem Th58: :: CQC_THE3:58
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
All (x,p) <==> All (x,q)
proofend;

theorem :: CQC_THE3:59
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
proofend;

theorem Th60: :: CQC_THE3:60
for A being QC-alphabet
for k being Element of NAT
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
proofend;

theorem Th61: :: CQC_THE3:61
for A being QC-alphabet
for k being Element of NAT
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
proofend;

theorem Th62: :: CQC_THE3:62
for A being QC-alphabet
for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in h c= still_not-bound_in (h . x)
proofend;

theorem Th63: :: CQC_THE3:63
for A being QC-alphabet
for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x}
proofend;

theorem Th64: :: CQC_THE3:64
for A being QC-alphabet
for p being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; x <> y &amp; not y in still_not-bound_in h holds
not y in still_not-bound_in p
proofend;

theorem :: CQC_THE3:65
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; q = h . y &amp; not x in still_not-bound_in h &amp; not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
proofend;