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

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;

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

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

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;

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

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( p |- q iff {p} |- q );

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

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 :: CQC_THE3:8

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 )

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 :: CQC_THE3:12

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

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

definition

let A be QC-alphabet ;

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

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;
let X, Y be Subset of (CQC-WFF A);

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

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

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 ) )

for X, Y being Subset of (CQC-WFF A) holds

( X |-| Y iff ( X |- Y & Y |- X ) )

proof end;

theorem :: CQC_THE3:19

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 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))

for X, Y being Subset of (CQC-WFF A) holds Cn (X \/ Y) = Cn ((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

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

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

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;

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;
let p, q be Element of CQC-WFF A;

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

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

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( p |-| q iff ( p |- q & q |- p ) );

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

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;

for p, q being Element of CQC-WFF A holds {p,q} |-| {(p '&' q)} by CQC_THE2:89;

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

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

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 )

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

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)

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;

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

( 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) ) ) ) ) );

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

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

for p, q being Element of CQC-WFF A st p is_an_universal_closure_of q 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

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

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 )

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

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

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

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

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

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 )

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;

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;

reflexivity

for p being Element of CQC-WFF A holds p <=> p is valid

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

q <=> p is valid

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

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;

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

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 ) )

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

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

p <==> r

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

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

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

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

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

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)

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)

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)))

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}

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)

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}

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

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)

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;