:: 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
proof end;

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
proof end;

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
proof end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
pred p |- 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
proof end;

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
proof end;

definition
let A be QC-alphabet ;
let X, Y be Subset of (CQC-WFF A);
pred X |- 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 )
proof end;

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

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
proof end;

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 )
proof end;

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 )
proof end;

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
proof end;

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

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 )
proof end;

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

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

definition
let A be QC-alphabet ;
let X, Y be Subset of (CQC-WFF A);
pred X |-| 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 ) )
proof end;

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
proof end;

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 )
proof end;

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

proof end;

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)
proof end;

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))
proof end;

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

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)
proof end;

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
proof end;

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
proof end;

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
proof end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
pred p |-| 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
proof end;

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} )
proof end;

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
proof end;

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

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

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

proof end;

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 )

proof end;

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

proof end;

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
proof end;

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 )
proof end;

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
proof end;

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)
proof end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
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 of A ex r being Element of CQC-WFF A st
( r = L . k & 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 & 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 of A ex r being Element of CQC-WFF A st
( r = L . k & 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
proof end;

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
proof end;

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
proof end;

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

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 )
proof end;

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

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 & X \/ {p} |- q holds
X \/ {('not' q)} |- 'not' p
proof end;

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

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 & X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p
proof end;

theorem :: CQC_THE3:47
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed & 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 & q1 is_an_universal_closure_of q holds
( p |- q iff 'not' q1 |- 'not' p1 )
proof end;

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 & q1 is_an_universal_closure_of q holds
( p |-| q iff 'not' p1 |-| 'not' q1 )
proof end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
pred p <==> 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
proof end;
symmetry
for p, q being Element of CQC-WFF A st p <=> q is valid holds
q <=> p is valid
proof end;
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 & q => p is valid ) )
proof end;

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

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

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

proof end;

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

proof end;

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 & r <==> s holds
p '&' r <==> q '&' s
proof end;

theorem Th55: :: CQC_THE3:55
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
proof end;

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

theorem :: CQC_THE3:57
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
proof end;

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)
proof end;

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)
proof end;

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)))
proof end;

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}
proof end;

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)
proof end;

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}
proof end;

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 & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
proof end;

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 & 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;