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

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 :: CQC_THE3:def 1
{p} |- q;

end;

:: deftheorem 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 by CQC_THE2:87;

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 by Th3;

definition

let A be QC-alphabet ;
let X, Y be Subset of (CQC-WFF A);

pred X |- Y means :: CQC_THE3:def 2
for p being Element of CQC-WFF A st p in Y holds
X |- p;

end;

:: deftheorem 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 by Th1;

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 ) by Th10;

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 by Th1;

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 :: CQC_THE3:def 3
for p being Element of CQC-WFF A st p in X holds
p is valid ;

end;

:: deftheorem 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 :: 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 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 :: 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 ;

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 Y, X1, X2 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 Y, Z, X1, X2 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 Y, X1, X2 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 :: 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 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 by Th6;

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)} by CQC_THE2:89;

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 by Lm4;

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 :: 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 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 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 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 p, q, p1 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 p, q, p1, q1 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 p, q, p1, q1 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 ) by Th48;

definition

let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;

pred p <==> q means :: 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 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 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 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;