:: CQC_THE3 semantic presentation 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 let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for X being Subset of (CQC-WFF A) st p in X holds X |- p let p be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p in X holds X |- p let X be Subset of (CQC-WFF A); ::_thesis: ( p in X implies X |- p ) X c= Cn X by CQC_THE1:17; hence ( p in X implies X |- p ) by CQC_THE1:def_8; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p & {p} |- q holds X |- q let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p & {p} |- q implies X |- q ) assume that A1: X |- p and A2: {p} |- q ; ::_thesis: X |- q p in Cn X by A1, CQC_THE1:def_8; then {p} c= Cn X by ZFMISC_1:31; then A3: Cn {p} c= Cn X by CQC_THE1:15, CQC_THE1:16; q in Cn {p} by A2, CQC_THE1:def_8; hence X |- q by A3, CQC_THE1:def_8; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p be Element of CQC-WFF A; ::_thesis: for X, Y being Subset of (CQC-WFF A) st X |- p & X c= Y holds Y |- p let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |- p & X c= Y implies Y |- p ) assume that A1: X |- p and A2: X c= Y ; ::_thesis: Y |- p A3: p in Cn X by A1, CQC_THE1:def_8; Cn X c= Cn Y by A2, CQC_THE1:18; hence Y |- p by A3, CQC_THE1:def_8; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p |- p let p be Element of CQC-WFF A; ::_thesis: p |- p {p} |- p by CQC_THE2:87; hence p |- p by Def1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p |- q & q |- r holds p |- r let p, q, r be Element of CQC-WFF A; ::_thesis: ( p |- q & q |- r implies p |- r ) assume that A1: p |- q and A2: q |- r ; ::_thesis: p |- r A3: {q} |- r by A2, Def1; {p} |- q by A1, Def1; then {p} |- r by A3, Th3; hence p |- r by Def1; ::_thesis: verum end; 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 ) proof let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds ( X |- Y iff Y c= Cn X ) let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |- Y iff Y c= Cn X ) A1: now__::_thesis:_(_X_|-_Y_implies_Y_c=_Cn_X_) assume A2: X |- Y ; ::_thesis: Y c= Cn X now__::_thesis:_for_p_being_set_st_p_in_Y_holds_ p_in_Cn_X let p be set ; ::_thesis: ( p in Y implies p in Cn X ) assume A3: p in Y ; ::_thesis: p in Cn X then reconsider p9 = p as Element of CQC-WFF A ; X |- p9 by A2, A3, Def2; hence p in Cn X by CQC_THE1:def_8; ::_thesis: verum end; hence Y c= Cn X by TARSKI:def_3; ::_thesis: verum end; now__::_thesis:_(_Y_c=_Cn_X_implies_X_|-_Y_) assume Y c= Cn X ; ::_thesis: X |- Y then for p being Element of CQC-WFF A st p in Y holds X |- p by CQC_THE1:def_8; hence X |- Y by Def2; ::_thesis: verum end; hence ( X |- Y iff Y c= Cn X ) by A1; ::_thesis: verum end; theorem :: CQC_THE3:8 for A being QC-alphabet for X being Subset of (CQC-WFF A) holds X |- X proof let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds X |- X let X be Subset of (CQC-WFF A); ::_thesis: X |- X for p being Element of CQC-WFF A st p in X holds X |- p by Th1; hence X |- X by Def2; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y, Z being Subset of (CQC-WFF A) st X |- Y & Y |- Z holds X |- Z let X, Y, Z be Subset of (CQC-WFF A); ::_thesis: ( X |- Y & Y |- Z implies X |- Z ) assume that A1: X |- Y and A2: Y |- Z ; ::_thesis: X |- Z for p being Element of CQC-WFF A st p in Z holds X |- p proof let p be Element of CQC-WFF A; ::_thesis: ( p in Z implies X |- p ) assume p in Z ; ::_thesis: X |- p then Y |- p by A2, Def2; then A3: p in Cn Y by CQC_THE1:def_8; Y c= Cn X by A1, Th7; then Cn Y c= Cn X by CQC_THE1:15, CQC_THE1:16; hence X |- p by A3, CQC_THE1:def_8; ::_thesis: verum end; hence X |- Z by Def2; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for X being Subset of (CQC-WFF A) holds ( X |- {p} iff X |- p ) let p be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) holds ( X |- {p} iff X |- p ) let X be Subset of (CQC-WFF A); ::_thesis: ( X |- {p} iff X |- p ) A1: now__::_thesis:_(_X_|-_p_implies_X_|-_{p}_) assume X |- p ; ::_thesis: X |- {p} then for q being Element of CQC-WFF A st q in {p} holds X |- q by TARSKI:def_1; hence X |- {p} by Def2; ::_thesis: verum end; now__::_thesis:_(_X_|-_{p}_implies_X_|-_p_) A2: p in {p} by TARSKI:def_1; assume X |- {p} ; ::_thesis: X |- p hence X |- p by A2, Def2; ::_thesis: verum end; hence ( X |- {p} iff X |- p ) by A1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ( {p} |- {q} iff p |- q ) let p, q be Element of CQC-WFF A; ::_thesis: ( {p} |- {q} iff p |- q ) A1: now__::_thesis:_(_p_|-_q_implies_{p}_|-_{q}_) assume p |- q ; ::_thesis: {p} |- {q} then {p} |- q by Def1; hence {p} |- {q} by Th10; ::_thesis: verum end; now__::_thesis:_(_{p}_|-_{q}_implies_p_|-_q_) assume {p} |- {q} ; ::_thesis: p |- q then {p} |- q by Th10; hence p |- q by Def1; ::_thesis: verum end; hence ( {p} |- {q} iff p |- q ) by A1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) st X c= Y holds Y |- X let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X c= Y implies Y |- X ) assume X c= Y ; ::_thesis: Y |- X then for p being Element of CQC-WFF A st p in X holds Y |- p by Th1; hence Y |- X by Def2; ::_thesis: verum end; theorem Th13: :: CQC_THE3:13 for A being QC-alphabet for X being Subset of (CQC-WFF A) holds X |- TAUT A proof let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds X |- TAUT A let X be Subset of (CQC-WFF A); ::_thesis: X |- TAUT A TAUT A c= Cn X by CQC_THE1:39; hence X |- TAUT A by Th7; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds ( |- X iff {} (CQC-WFF A) |- X ) let X be Subset of (CQC-WFF A); ::_thesis: ( |- X iff {} (CQC-WFF A) |- X ) A1: now__::_thesis:_(_{}_(CQC-WFF_A)_|-_X_implies_|-_X_) assume A2: {} (CQC-WFF A) |- X ; ::_thesis: |- X now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_ p_is_valid let p be Element of CQC-WFF A; ::_thesis: ( p in X implies p is valid ) assume p in X ; ::_thesis: p is valid then {} (CQC-WFF A) |- p by A2, Def2; hence p is valid by CQC_THE1:def_9; ::_thesis: verum end; hence |- X by Def3; ::_thesis: verum end; now__::_thesis:_(_|-_X_implies_{}_(CQC-WFF_A)_|-_X_) assume A3: |- X ; ::_thesis: {} (CQC-WFF A) |- X now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_ {}_(CQC-WFF_A)_|-_p let p be Element of CQC-WFF A; ::_thesis: ( p in X implies {} (CQC-WFF A) |- p ) assume p in X ; ::_thesis: {} (CQC-WFF A) |- p then p is valid by A3, Def3; hence {} (CQC-WFF A) |- p by CQC_THE1:def_9; ::_thesis: verum end; hence {} (CQC-WFF A) |- X by Def2; ::_thesis: verum end; hence ( |- X iff {} (CQC-WFF A) |- X ) by A1; ::_thesis: verum end; theorem :: CQC_THE3:16 for A being QC-alphabet holds |- TAUT A proof let A be QC-alphabet ; ::_thesis: |- TAUT A A1: ( |- TAUT A iff {} (CQC-WFF A) |- TAUT A ) by Th15; {} (CQC-WFF A) |- TAUT A by Th13; hence |- TAUT A by A1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds ( |- X iff X c= TAUT A ) let X be Subset of (CQC-WFF A); ::_thesis: ( |- X iff X c= TAUT A ) A1: now__::_thesis:_(_|-_X_implies_X_c=_TAUT_A_) assume A2: |- X ; ::_thesis: X c= TAUT A now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_ p_in_TAUT_A let p be Element of CQC-WFF A; ::_thesis: ( p in X implies p in TAUT A ) assume p in X ; ::_thesis: p in TAUT A then p is valid by A2, Def3; hence p in TAUT A by CQC_THE1:def_10; ::_thesis: verum end; hence X c= TAUT A by SUBSET_1:2; ::_thesis: verum end; now__::_thesis:_(_X_c=_TAUT_A_implies_|-_X_) assume X c= TAUT A ; ::_thesis: |- X then for p being Element of CQC-WFF A st p in X holds p is valid by CQC_THE1:def_10; hence |- X by Def3; ::_thesis: verum end; hence ( |- X iff X c= TAUT A ) by A1; ::_thesis: verum end; 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 ) ) proof let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds ( X |-| Y iff ( X |- Y & Y |- X ) ) let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |-| Y iff ( X |- Y & Y |- X ) ) A1: now__::_thesis:_(_X_|-_Y_&_Y_|-_X_implies_X_|-|_Y_) assume that A2: X |- Y and A3: Y |- X ; ::_thesis: X |-| Y now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_holds_ (_X_|-_p_iff_Y_|-_p_) let p be Element of CQC-WFF A; ::_thesis: ( X |- p iff Y |- p ) A4: now__::_thesis:_(_Y_|-_p_implies_X_|-_p_) assume Y |- p ; ::_thesis: X |- p then Y |- {p} by Th10; then X |- {p} by A2, Th9; hence X |- p by Th10; ::_thesis: verum end; now__::_thesis:_(_X_|-_p_implies_Y_|-_p_) assume X |- p ; ::_thesis: Y |- p then X |- {p} by Th10; then Y |- {p} by A3, Th9; hence Y |- p by Th10; ::_thesis: verum end; hence ( X |- p iff Y |- p ) by A4; ::_thesis: verum end; hence X |-| Y by Def4; ::_thesis: verum end; now__::_thesis:_(_X_|-|_Y_implies_(_X_|-_Y_&_Y_|-_X_)_) assume A5: X |-| Y ; ::_thesis: ( X |- Y & Y |- X ) now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_Y_holds_ X_|-_p let p be Element of CQC-WFF A; ::_thesis: ( p in Y implies X |- p ) assume p in Y ; ::_thesis: X |- p then Y |- p by Th1; hence X |- p by A5, Def4; ::_thesis: verum end; hence X |- Y by Def2; ::_thesis: Y |- X now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_ Y_|-_p let p be Element of CQC-WFF A; ::_thesis: ( p in X implies Y |- p ) assume p in X ; ::_thesis: Y |- p then X |- p by Th1; hence Y |- p by A5, Def4; ::_thesis: verum end; hence Y |- X by Def2; ::_thesis: verum end; hence ( X |-| Y iff ( X |- Y & Y |- X ) ) by A1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y, Z being Subset of (CQC-WFF A) st X |-| Y & Y |-| Z holds X |-| Z let X, Y, Z be Subset of (CQC-WFF A); ::_thesis: ( X |-| Y & Y |-| Z implies X |-| Z ) assume that A1: X |-| Y and A2: Y |-| Z ; ::_thesis: X |-| Z A3: Z |- Y by A2, Th18; Y |- X by A1, Th18; then A4: Z |- X by A3, Th9; A5: Y |- Z by A2, Th18; X |- Y by A1, Th18; then X |- Z by A5, Th9; hence X |-| Z by A4, Th18; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds ( X |-| Y iff Cn X = Cn Y ) let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |-| Y iff Cn X = Cn Y ) A1: now__::_thesis:_(_X_|-|_Y_implies_Cn_X_=_Cn_Y_) assume A2: X |-| Y ; ::_thesis: Cn X = Cn Y then Y |- X by Th18; then X c= Cn Y by Th7; then A3: Cn X c= Cn Y by CQC_THE1:15, CQC_THE1:16; X |- Y by A2, Th18; then Y c= Cn X by Th7; then Cn Y c= Cn X by CQC_THE1:15, CQC_THE1:16; hence Cn X = Cn Y by A3, XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_(_Cn_X_=_Cn_Y_implies_X_|-|_Y_) assume A4: Cn X = Cn Y ; ::_thesis: X |-| Y X c= Cn X by CQC_THE1:17; then A5: Y |- X by A4, Th7; Y c= Cn Y by CQC_THE1:17; then X |- Y by A4, Th7; hence X |-| Y by A5, Th18; ::_thesis: verum end; hence ( X |-| Y iff Cn X = Cn Y ) by A1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds X \/ Y c= (Cn X) \/ (Cn Y) let X, Y be Subset of (CQC-WFF A); ::_thesis: X \/ Y c= (Cn X) \/ (Cn Y) A1: Y c= Cn Y by CQC_THE1:17; X c= Cn X by CQC_THE1:17; hence X \/ Y c= (Cn X) \/ (Cn Y) by A1, XBOOLE_1:13; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds (Cn X) \/ (Cn Y) c= Cn (X \/ Y) let X, Y be Subset of (CQC-WFF A); ::_thesis: (Cn X) \/ (Cn Y) c= Cn (X \/ Y) A1: Cn Y c= Cn (X \/ Y) by CQC_THE1:18, XBOOLE_1:7; Cn X c= Cn (X \/ Y) by CQC_THE1:18, XBOOLE_1:7; hence (Cn X) \/ (Cn Y) c= Cn (X \/ Y) by A1, XBOOLE_1:8; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) let X, Y be Subset of (CQC-WFF A); ::_thesis: Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) A1: Cn (X \/ Y) c= Cn ((Cn X) \/ (Cn Y)) by Lm1, CQC_THE1:18; Cn ((Cn X) \/ (Cn Y)) c= Cn (X \/ Y) by Th2, Th21; hence Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CQC_THE3:23 for A being QC-alphabet for X being Subset of (CQC-WFF A) holds X |-| Cn X proof let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds X |-| Cn X let X be Subset of (CQC-WFF A); ::_thesis: X |-| Cn X Cn X = Cn (Cn X) by CQC_THE1:19; hence X |-| Cn X by Th20; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds X \/ Y |-| (Cn X) \/ (Cn Y) let X, Y be Subset of (CQC-WFF A); ::_thesis: X \/ Y |-| (Cn X) \/ (Cn Y) Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) by Th22; hence X \/ Y |-| (Cn X) \/ (Cn Y) by Th20; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 holds X1 \/ Y |-| X2 \/ Y let X1, X2, Y be Subset of (CQC-WFF A); ::_thesis: ( X1 |-| X2 implies X1 \/ Y |-| X2 \/ Y ) assume X1 |-| X2 ; ::_thesis: X1 \/ Y |-| X2 \/ Y then Cn X1 = Cn X2 by Th20; then Cn (X1 \/ Y) = Cn ((Cn X2) \/ (Cn Y)) by Th22 .= Cn (X2 \/ Y) by Th22 ; hence X1 \/ Y |-| X2 \/ Y by Th20; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X1, X2, Y, Z being Subset of (CQC-WFF A) st X1 |-| X2 & X1 \/ Y |- Z holds X2 \/ Y |- Z let X1, X2, Y, Z be Subset of (CQC-WFF A); ::_thesis: ( X1 |-| X2 & X1 \/ Y |- Z implies X2 \/ Y |- Z ) assume that A1: X1 |-| X2 and A2: X1 \/ Y |- Z ; ::_thesis: X2 \/ Y |- Z X1 \/ Y |-| X2 \/ Y by A1, Th25; then Cn (X1 \/ Y) = Cn (X2 \/ Y) by Th20; then Z c= Cn (X2 \/ Y) by A2, Th7; hence X2 \/ Y |- Z by Th7; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 & Y |- X1 holds Y |- X2 let X1, X2, Y be Subset of (CQC-WFF A); ::_thesis: ( X1 |-| X2 & Y |- X1 implies Y |- X2 ) assume that A1: X1 |-| X2 and A2: Y |- X1 ; ::_thesis: Y |- X2 X1 |- X2 by A1, Th18; hence Y |- X2 by A2, Th9; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p |-| q & q |-| r holds p |-| r let p, q, r be Element of CQC-WFF A; ::_thesis: ( p |-| q & q |-| r implies p |-| r ) assume that A1: p |-| q and A2: q |-| r ; ::_thesis: p |-| r A3: r |- q by A2, Def5; q |- p by A1, Def5; then A4: r |- p by A3, Th6; A5: q |- r by A2, Def5; p |- q by A1, Def5; then p |- r by A5, Th6; hence p |-| r by A4, Def5; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ( p |-| q iff {p} |-| {q} ) let p, q be Element of CQC-WFF A; ::_thesis: ( p |-| q iff {p} |-| {q} ) A1: now__::_thesis:_(_{p}_|-|_{q}_implies_p_|-|_q_) assume A2: {p} |-| {q} ; ::_thesis: p |-| q then {q} |- {p} by Th18; then A3: q |- p by Th11; {p} |- {q} by A2, Th18; then p |- q by Th11; hence p |-| q by A3, Def5; ::_thesis: verum end; now__::_thesis:_(_p_|-|_q_implies_{p}_|-|_{q}_) assume A4: p |-| q ; ::_thesis: {p} |-| {q} then q |- p by Def5; then A5: {q} |- {p} by Th11; p |- q by A4, Def5; then {p} |- {q} by Th11; hence {p} |-| {q} by A5, Th18; ::_thesis: verum end; hence ( p |-| q iff {p} |-| {q} ) by A1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p |-| q & X |- p holds X |- q let X be Subset of (CQC-WFF A); ::_thesis: ( p |-| q & X |- p implies X |- q ) assume that A1: p |-| q and A2: X |- p ; ::_thesis: X |- q A3: X |- {p} by A2, Th10; {p} |-| {q} by A1, Th29; then X |- {q} by A3, Th27; hence X |- q by Th10; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds {p,q} |-| {(p '&' q)} let p, q be Element of CQC-WFF A; ::_thesis: {p,q} |-| {(p '&' q)} for r being Element of CQC-WFF A holds ( {p,q} |- r iff {(p '&' q)} |- r ) by CQC_THE2:89; hence {p,q} |-| {(p '&' q)} by Def4; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p '&' q |-| q '&' p let p, q be Element of CQC-WFF A; ::_thesis: p '&' q |-| q '&' p A1: {q,p} |-| {(q '&' p)} by Th31; {(p '&' q)} |-| {q,p} by Th31; then {(p '&' q)} |-| {(q '&' p)} by A1, Th19; hence p '&' q |-| q '&' p by Th29; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p & X |- q holds X |- p '&' q let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p & X |- q implies X |- p '&' q ) assume that A1: X |- p and A2: X |- q ; ::_thesis: X |- p '&' q for r being Element of CQC-WFF A st r in {p,q} holds X |- r by A1, A2, TARSKI:def_2; then X |- {p,q} by Def2; then X |- {(p '&' q)} by Th27, Th31; hence X |- p '&' q by Th10; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 ) let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p '&' q holds ( X |- p & X |- q ) let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p '&' q implies ( X |- p & X |- q ) ) assume X |- p '&' q ; ::_thesis: ( X |- p & X |- q ) then A1: X |- {(p '&' q)} by Th10; {p,q} |-| {(p '&' q)} by Th31; then A2: X |- {p,q} by A1, Th27; p in {p,q} by TARSKI:def_2; hence X |- p by A2, Def2; ::_thesis: X |- q q in {p,q} by TARSKI:def_2; hence X |- q by A2, Def2; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds p '&' r |- q '&' s let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p |-| q & r |-| s implies p '&' r |- q '&' s ) assume that A1: p |-| q and A2: r |-| s ; ::_thesis: p '&' r |- q '&' s r |- s by A2, Def5; then {r} |- s by Def1; then A3: {p,r} |- s by Th4, ZFMISC_1:7; {p,r} |-| {(p '&' r)} by Th31; then A4: {(p '&' r)} |- {p,r} by Th18; p |- q by A1, Def5; then {p} |- q by Def1; then {p,r} |- q by Th4, ZFMISC_1:7; then {p,r} |- q '&' s by A3, Lm2; then {p,r} |- {(q '&' s)} by Th10; then {(p '&' r)} |- {(q '&' s)} by A4, Th9; hence p '&' r |- q '&' s by Th11; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds p '&' r |-| q '&' s let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p |-| q & r |-| s implies p '&' r |-| q '&' s ) assume that A1: p |-| q and A2: r |-| s ; ::_thesis: p '&' r |-| q '&' s A3: q '&' s |- p '&' r by A1, A2, Lm4; p '&' r |- q '&' s by A1, A2, Lm4; hence p '&' r |-| q '&' s by A3, Def5; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 ) let p be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) for x being bound_QC-variable of A holds ( X |- All (x,p) iff X |- p ) let X be Subset of (CQC-WFF A); ::_thesis: for x being bound_QC-variable of A holds ( X |- All (x,p) iff X |- p ) let x be bound_QC-variable of A; ::_thesis: ( X |- All (x,p) iff X |- p ) thus ( X |- All (x,p) implies X |- p ) ::_thesis: ( X |- p implies X |- All (x,p) ) proof A1: X |- (All (x,p)) => p by CQC_THE1:56; assume X |- All (x,p) ; ::_thesis: X |- p hence X |- p by A1, CQC_THE1:55; ::_thesis: verum end; thus ( X |- p implies X |- All (x,p) ) by CQC_THE2:90; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds All (x,p) |-| p let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds All (x,p) |-| p let x be bound_QC-variable of A; ::_thesis: All (x,p) |-| p {(All (x,p))} |- (All (x,p)) => p by CQC_THE1:56; then {(All (x,p))} |- p by CQC_THE1:55, CQC_THE2:87; hence All (x,p) |- p by Def1; :: according to CQC_THE3:def_5 ::_thesis: p |- All (x,p) {p} |- p by CQC_THE2:87; then {p} |- All (x,p) by Th35; hence p |- All (x,p) by Def1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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) let p, q be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A st p |-| q holds All (x,p) |-| All (y,q) let x, y be bound_QC-variable of A; ::_thesis: ( p |-| q implies All (x,p) |-| All (y,q) ) assume A1: p |-| q ; ::_thesis: All (x,p) |-| All (y,q) A2: q |-| All (y,q) by Th36; All (x,p) |-| p by Th36; then All (x,p) |-| q by A1, Th28; hence All (x,p) |-| All (y,q) by A2, Th28; ::_thesis: verum end; 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 & 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is_an_universal_closure_of q holds p |-| q let p, q be Element of CQC-WFF A; ::_thesis: ( p is_an_universal_closure_of q implies p |-| q ) assume p is_an_universal_closure_of q ; ::_thesis: p |-| q then consider n being Element of NAT such that A1: 1 <= n and A2: 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) ) ) ) by Def6; consider L being FinSequence such that len L = n and A3: L . 1 = q and A4: L . n = p and A5: 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) ) by A2; for k being Element of NAT st 1 <= k & k <= n holds ex r being Element of CQC-WFF A st ( r = L . k & q |-| r ) proof defpred S1[ Element of NAT ] means ( 1 <= \$1 & \$1 <= n implies ex r being Element of CQC-WFF A st ( r = L . \$1 & q |-| r ) ); A6: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_1_<=_k_+_1_&_k_+_1_<=_n_&_not_(_k_=_0_&_ex_p,_r_being_Element_of_CQC-WFF_A_st_ (_r_=_L_._(k_+_1)_&_q_|-|_r_)_)_implies_(_1_<=_k_&_k_<_n_&_ex_s_being_Element_of_CQC-WFF_A_st_ (_s_=_L_._(k_+_1)_&_q_|-|_s_)_)_) assume that 1 <= k + 1 and A8: k + 1 <= n ; ::_thesis: ( ( k = 0 & ex p, r being Element of CQC-WFF A st ( r = L . (k + 1) & q |-| r ) ) or ( 1 <= k & k < n & ex s being Element of CQC-WFF A st ( s = L . (k + 1) & q |-| s ) ) ) percases ( k = 0 or ( 1 <= k & k < n ) ) by A8, NAT_1:13, NAT_1:14; caseA9: k = 0 ; ::_thesis: ex p, r being Element of CQC-WFF A st ( r = L . (k + 1) & q |-| r ) take p = q; ::_thesis: ex r being Element of CQC-WFF A st ( r = L . (k + 1) & q |-| r ) thus ex r being Element of CQC-WFF A st ( r = L . (k + 1) & q |-| r ) by A3, A9; ::_thesis: verum end; caseA10: ( 1 <= k & k < n ) ; ::_thesis: ex s being Element of CQC-WFF A st ( s = L . (k + 1) & q |-| s ) then consider x being bound_QC-variable of A, r being Element of CQC-WFF A such that A11: r = L . k and A12: L . (k + 1) = All (x,r) by A5; consider s being Element of CQC-WFF A such that A13: s = All (x,r) ; s |-| r by A13, Th36; hence ex s being Element of CQC-WFF A st ( s = L . (k + 1) & q |-| s ) by A7, A10, A11, A12, A13, Th28; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A14: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A14, A6); ::_thesis: verum end; then ex r being Element of CQC-WFF A st ( r = L . n & q |-| r ) by A1; hence p |-| q by A4; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p => q is valid holds p |- q let p, q be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies p |- q ) assume p => q is valid ; ::_thesis: p |- q then {p} |- p => q by CQC_THE1:59; then {p} |- q by CQC_THE1:55, CQC_THE2:87; hence p |- q by Def1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => q holds X \/ {p} |- q let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => q implies X \/ {p} |- q ) p in {p} by TARSKI:def_1; then p in X \/ {p} by XBOOLE_0:def_3; then A1: X \/ {p} |- p by Th1; assume X |- p => q ; ::_thesis: X \/ {p} |- q then X \/ {p} |- p => q by Th4, XBOOLE_1:7; hence X \/ {p} |- q by A1, CQC_THE1:55; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is closed & p |- q holds p => q is valid let p, q be Element of CQC-WFF A; ::_thesis: ( p is closed & p |- q implies p => q is valid ) assume that A1: p is closed and A2: p |- q ; ::_thesis: p => q is valid ({} (CQC-WFF A)) \/ {p} |- q by A2, Def1; then {} (CQC-WFF A) |- p => q by A1, CQC_THE2:92; hence p => q is valid by CQC_THE1:def_9; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 ) let p1, p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p1 is_an_universal_closure_of p holds ( X \/ {p} |- q iff X |- p1 => q ) let X be Subset of (CQC-WFF A); ::_thesis: ( p1 is_an_universal_closure_of p implies ( X \/ {p} |- q iff X |- p1 => q ) ) assume A1: p1 is_an_universal_closure_of p ; ::_thesis: ( X \/ {p} |- q iff X |- p1 => q ) now__::_thesis:_(_X_\/_{p}_|-_q_implies_X_|-_p1_=>_q_) assume X \/ {p} |- q ; ::_thesis: X |- p1 => q then A2: X \/ {p} |- {q} by Th10; p |-| p1 by A1, Th38; then {p} |-| {p1} by Th29; then X \/ {p1} |- {q} by A2, Th26; then A3: X \/ {p1} |- q by Th10; p1 is closed by A1, Def6; hence X |- p1 => q by A3, CQC_THE2:92; ::_thesis: verum end; hence ( X \/ {p} |- q implies X |- p1 => q ) ; ::_thesis: ( X |- p1 => q implies X \/ {p} |- q ) now__::_thesis:_(_X_|-_p1_=>_q_implies_X_\/_{p}_|-_q_) assume X |- p1 => q ; ::_thesis: X \/ {p} |- q then X \/ {p1} |- q by Th40; then A4: X \/ {p1} |- {q} by Th10; p |-| p1 by A1, Th38; then {p} |-| {p1} by Th29; then X \/ {p} |- {q} by A4, Th26; hence X \/ {p} |- q by Th10; ::_thesis: verum end; hence ( X |- p1 => q implies X \/ {p} |- q ) ; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is closed & p |- q holds 'not' q |- 'not' p let p, q be Element of CQC-WFF A; ::_thesis: ( p is closed & p |- q implies 'not' q |- 'not' p ) assume that A1: p is closed and A2: p |- q ; ::_thesis: 'not' q |- 'not' p p => q is valid by A1, A2, Th41; then ('not' q) => ('not' p) is valid by LUKASI_1:52; hence 'not' q |- 'not' p by Th39; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p is closed & X \/ {p} |- q holds X \/ {('not' q)} |- 'not' p let X be Subset of (CQC-WFF A); ::_thesis: ( p is closed & X \/ {p} |- q implies X \/ {('not' q)} |- 'not' p ) assume that A1: p is closed and A2: X \/ {p} |- q ; ::_thesis: X \/ {('not' q)} |- 'not' p X |- p => q by A1, A2, CQC_THE2:92; then X |- ('not' q) => ('not' p) by LUKASI_1:69; hence X \/ {('not' q)} |- 'not' p by Th40; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is closed & 'not' p |- 'not' q holds q |- p let p, q be Element of CQC-WFF A; ::_thesis: ( p is closed & 'not' p |- 'not' q implies q |- p ) assume that A1: p is closed and A2: 'not' p |- 'not' q ; ::_thesis: q |- p 'not' p is closed by A1, QC_LANG3:21; then ('not' p) => ('not' q) is valid by A2, Th41; then q => p is valid by LUKASI_1:52; hence q |- p by Th39; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p is closed & X \/ {('not' p)} |- 'not' q holds X \/ {q} |- p let X be Subset of (CQC-WFF A); ::_thesis: ( p is closed & X \/ {('not' p)} |- 'not' q implies X \/ {q} |- p ) assume that A1: p is closed and A2: X \/ {('not' p)} |- 'not' q ; ::_thesis: X \/ {q} |- p 'not' p is closed by A1, QC_LANG3:21; then X |- ('not' p) => ('not' q) by A2, CQC_THE2:92; then X |- q => p by LUKASI_1:69; hence X \/ {q} |- p by Th40; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 ) let p1, p, q1, q be Element of CQC-WFF A; ::_thesis: ( p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies ( p |- q iff 'not' q1 |- 'not' p1 ) ) assume that A1: p1 is_an_universal_closure_of p and A2: q1 is_an_universal_closure_of q ; ::_thesis: ( p |- q iff 'not' q1 |- 'not' p1 ) now__::_thesis:_(_p_|-_q_implies_'not'_q1_|-_'not'_p1_) q |-| q1 by A2, Th38; then A3: q |- q1 by Def5; p1 |-| p by A1, Th38; then A4: p1 |- p by Def5; assume p |- q ; ::_thesis: 'not' q1 |- 'not' p1 then p1 |- q by A4, Th6; then A5: p1 |- q1 by A3, Th6; p1 is closed by A1, Def6; hence 'not' q1 |- 'not' p1 by A5, Th43; ::_thesis: verum end; hence ( p |- q implies 'not' q1 |- 'not' p1 ) ; ::_thesis: ( 'not' q1 |- 'not' p1 implies p |- q ) now__::_thesis:_(_'not'_q1_|-_'not'_p1_implies_p_|-_q_) q1 |-| q by A2, Th38; then A6: q1 |- q by Def5; p1 |-| p by A1, Th38; then A7: p |- p1 by Def5; assume A8: 'not' q1 |- 'not' p1 ; ::_thesis: p |- q q1 is closed by A2, Def6; then p1 |- q1 by A8, Th45; then p |- q1 by A7, Th6; hence p |- q by A6, Th6; ::_thesis: verum end; hence ( 'not' q1 |- 'not' p1 implies p |- q ) ; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 ) let p1, p, q1, q be Element of CQC-WFF A; ::_thesis: ( p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies ( p |-| q iff 'not' p1 |-| 'not' q1 ) ) assume that A1: p1 is_an_universal_closure_of p and A2: q1 is_an_universal_closure_of q ; ::_thesis: ( p |-| q iff 'not' p1 |-| 'not' q1 ) now__::_thesis:_(_p_|-|_q_implies_'not'_p1_|-|_'not'_q1_) assume A3: p |-| q ; ::_thesis: 'not' p1 |-| 'not' q1 then p |- q by Def5; then A4: 'not' q1 |- 'not' p1 by A1, A2, Th48; q |- p by A3, Def5; then 'not' p1 |- 'not' q1 by A1, A2, Th48; hence 'not' p1 |-| 'not' q1 by A4, Def5; ::_thesis: verum end; hence ( p |-| q implies 'not' p1 |-| 'not' q1 ) ; ::_thesis: ( 'not' p1 |-| 'not' q1 implies p |-| q ) now__::_thesis:_(_'not'_p1_|-|_'not'_q1_implies_p_|-|_q_) assume A5: 'not' p1 |-| 'not' q1 ; ::_thesis: p |-| q then 'not' q1 |- 'not' p1 by Def5; then A6: p |- q by A1, A2, Th48; 'not' p1 |- 'not' q1 by A5, Def5; then q |- p by A1, A2, Th48; hence p |-| q by A6, Def5; ::_thesis: verum end; hence ( 'not' p1 |-| 'not' q1 implies p |-| q ) ; ::_thesis: verum end; 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 proof let p be Element of CQC-WFF A; ::_thesis: p <=> p is valid {} (CQC-WFF A) |- p => p by CQC_THE1:def_9; then {} (CQC-WFF A) |- (p => p) '&' (p => p) by Lm2; then (p => p) '&' (p => p) is valid by CQC_THE1:def_9; hence p <=> p is valid by QC_LANG2:def_4; ::_thesis: verum end; symmetry for p, q being Element of CQC-WFF A st p <=> q is valid holds q <=> p is valid proof let p, q be Element of CQC-WFF A; ::_thesis: ( p <=> q is valid implies q <=> p is valid ) assume p <=> q is valid ; ::_thesis: q <=> p is valid then (p => q) '&' (q => p) is valid by QC_LANG2:def_4; then A1: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def_9; then A2: {} (CQC-WFF A) |- q => p by Lm3; {} (CQC-WFF A) |- p => q by A1, Lm3; then {} (CQC-WFF A) |- (q => p) '&' (p => q) by A2, Lm2; then (q => p) '&' (p => q) is valid by CQC_THE1:def_9; hence q <=> p is valid by QC_LANG2:def_4; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ( p <==> q iff ( p => q is valid & q => p is valid ) ) let p, q be Element of CQC-WFF A; ::_thesis: ( p <==> q iff ( p => q is valid & q => p is valid ) ) A1: now__::_thesis:_(_p_=>_q_is_valid_&_q_=>_p_is_valid_implies_p_<==>_q_) assume that A2: p => q is valid and A3: q => p is valid ; ::_thesis: p <==> q A4: {} (CQC-WFF A) |- q => p by A3, CQC_THE1:def_9; {} (CQC-WFF A) |- p => q by A2, CQC_THE1:def_9; then {} (CQC-WFF A) |- (p => q) '&' (q => p) by A4, Lm2; then (p => q) '&' (q => p) is valid by CQC_THE1:def_9; then p <=> q is valid by QC_LANG2:def_4; hence p <==> q by Def7; ::_thesis: verum end; now__::_thesis:_(_p_<==>_q_implies_(_p_=>_q_is_valid_&_q_=>_p_is_valid_)_) assume p <==> q ; ::_thesis: ( p => q is valid & q => p is valid ) then p <=> q is valid by Def7; then (p => q) '&' (q => p) is valid by QC_LANG2:def_4; then A5: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def_9; then A6: {} (CQC-WFF A) |- q => p by Lm3; {} (CQC-WFF A) |- p => q by A5, Lm3; hence ( p => q is valid & q => p is valid ) by A6, CQC_THE1:def_9; ::_thesis: verum end; hence ( p <==> q iff ( p => q is valid & q => p is valid ) ) by A1; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p <==> q & q <==> r holds p <==> r let p, q, r be Element of CQC-WFF A; ::_thesis: ( p <==> q & q <==> r implies p <==> r ) assume that A1: p <==> q and A2: q <==> r ; ::_thesis: p <==> r A3: r => q is valid by A2, Th50; q => p is valid by A1, Th50; then A4: r => p is valid by A3, LUKASI_1:42; A5: q => r is valid by A2, Th50; p => q is valid by A1, Th50; then p => r is valid by A5, LUKASI_1:42; hence p <==> r by A4, Th50; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p <==> q holds p |-| q let p, q be Element of CQC-WFF A; ::_thesis: ( p <==> q implies p |-| q ) assume p <==> q ; ::_thesis: p |-| q then p <=> q is valid by Def7; then (p => q) '&' (q => p) is valid by QC_LANG2:def_4; then A1: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def_9; then {} (CQC-WFF A) |- q => p by Lm3; then A2: q => p is valid by CQC_THE1:def_9; {} (CQC-WFF A) |- p => q by A1, Lm3; then p => q is valid by CQC_THE1:def_9; hence ( p |- q & q |- p ) by A2, Th39; :: according to CQC_THE3:def_5 ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p <==> q holds 'not' p <==> 'not' q let p, q be Element of CQC-WFF A; ::_thesis: ( p <==> q implies 'not' p <==> 'not' q ) assume A1: p <==> q ; ::_thesis: 'not' p <==> 'not' q then q => p is valid by Th50; then A2: ('not' p) => ('not' q) is valid by LUKASI_1:52; p => q is valid by A1, Th50; then ('not' q) => ('not' p) is valid by LUKASI_1:52; hence 'not' p <==> 'not' q by A2, Th50; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st 'not' p <==> 'not' q holds p <==> q let p, q be Element of CQC-WFF A; ::_thesis: ( 'not' p <==> 'not' q implies p <==> q ) assume A1: 'not' p <==> 'not' q ; ::_thesis: p <==> q then ('not' q) => ('not' p) is valid by Th50; then A2: p => q is valid by LUKASI_1:52; ('not' p) => ('not' q) is valid by A1, Th50; then q => p is valid by LUKASI_1:52; hence p <==> q by A2, Th50; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds p '&' r <==> q '&' s let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p '&' r <==> q '&' s ) assume that A1: p <==> q and A2: r <==> s ; ::_thesis: p '&' r <==> q '&' s s => r is valid by A2, Th50; then A3: s => r in TAUT A by CQC_THE1:def_10; q => p is valid by A1, Th50; then q => p in TAUT A by CQC_THE1:def_10; then (q '&' s) => (p '&' r) in TAUT A by A3, PROCAL_1:56; then A4: (q '&' s) => (p '&' r) is valid by CQC_THE1:def_10; r => s is valid by A2, Th50; then A5: r => s in TAUT A by CQC_THE1:def_10; p => q is valid by A1, Th50; then p => q in TAUT A by CQC_THE1:def_10; then (p '&' r) => (q '&' s) in TAUT A by A5, PROCAL_1:56; then (p '&' r) => (q '&' s) is valid by CQC_THE1:def_10; hence p '&' r <==> q '&' s by A4, Th50; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds p => r <==> q => s let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p => r <==> q => s ) assume that A1: p <==> q and A2: r <==> s ; ::_thesis: p => r <==> q => s 'not' r <==> 'not' s by A2, Lm5; then p '&' ('not' r) <==> q '&' ('not' s) by A1, Th54; then A3: 'not' (p '&' ('not' r)) <==> 'not' (q '&' ('not' s)) by Lm5; p => r = 'not' (p '&' ('not' r)) by QC_LANG2:def_2; hence p => r <==> q => s by A3, QC_LANG2:def_2; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds p 'or' r <==> q 'or' s let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p 'or' r <==> q 'or' s ) assume that A1: p <==> q and A2: r <==> s ; ::_thesis: p 'or' r <==> q 'or' s s => r is valid by A2, Th50; then A3: s => r in TAUT A by CQC_THE1:def_10; q => p is valid by A1, Th50; then q => p in TAUT A by CQC_THE1:def_10; then (q 'or' s) => (p 'or' r) in TAUT A by A3, PROCAL_1:57; then A4: (q 'or' s) => (p 'or' r) is valid by CQC_THE1:def_10; r => s is valid by A2, Th50; then A5: r => s in TAUT A by CQC_THE1:def_10; p => q is valid by A1, Th50; then p => q in TAUT A by CQC_THE1:def_10; then (p 'or' r) => (q 'or' s) in TAUT A by A5, PROCAL_1:57; then (p 'or' r) => (q 'or' s) is valid by CQC_THE1:def_10; hence p 'or' r <==> q 'or' s by A4, Th50; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds p <=> r <==> q <=> s let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p <=> r <==> q <=> s ) assume that A1: p <==> q and A2: r <==> s ; ::_thesis: p <=> r <==> q <=> s A3: r => p <==> s => q by A1, A2, Th55; A4: p <=> r = (p => r) '&' (r => p) by QC_LANG2:def_4; p => r <==> q => s by A1, A2, Th55; then (p => r) '&' (r => p) <==> (q => s) '&' (s => q) by A3, Th54; hence p <=> r <==> q <=> s by A4, QC_LANG2:def_4; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p <==> q holds All (x,p) <==> All (x,q) let x be bound_QC-variable of A; ::_thesis: ( p <==> q implies All (x,p) <==> All (x,q) ) assume A1: p <==> q ; ::_thesis: All (x,p) <==> All (x,q) then q => p is valid by Th50; then All (x,(q => p)) is valid by CQC_THE2:23; then A2: (All (x,q)) => (All (x,p)) is valid by CQC_THE2:31; p => q is valid by A1, Th50; then All (x,(p => q)) is valid by CQC_THE2:23; then (All (x,p)) => (All (x,q)) is valid by CQC_THE2:31; hence All (x,p) <==> All (x,q) by A2, Th50; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p <==> q holds Ex (x,p) <==> Ex (x,q) let x be bound_QC-variable of A; ::_thesis: ( p <==> q implies Ex (x,p) <==> Ex (x,q) ) assume p <==> q ; ::_thesis: Ex (x,p) <==> Ex (x,q) then 'not' p <==> 'not' q by Lm5; then All (x,('not' p)) <==> All (x,('not' q)) by Th58; then A1: 'not' (All (x,('not' p))) <==> 'not' (All (x,('not' q))) by Lm5; Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def_5; hence Ex (x,p) <==> Ex (x,q) by A1, QC_LANG2:def_5; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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))) let k be Element of NAT ; ::_thesis: 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))) let l be QC-variable_list of k,A; ::_thesis: 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))) let a be free_QC-variable of A; ::_thesis: for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x))) let x be bound_QC-variable of A; ::_thesis: still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x))) now__::_thesis:_for_y_being_set_st_y_in_still_not-bound_in_l_holds_ y_in_still_not-bound_in_(Subst_(l,(a_.-->_x))) let y be set ; ::_thesis: ( y in still_not-bound_in l implies y in still_not-bound_in (Subst (l,(a .--> x))) ) A1: still_not-bound_in l = { (l . n) where n is Element of NAT : ( 1 <= n & n <= len l & l . n in bound_QC-variables A ) } by QC_LANG1:def_29; assume A2: y in still_not-bound_in l ; ::_thesis: y in still_not-bound_in (Subst (l,(a .--> x))) then reconsider y9 = y as Element of still_not-bound_in l ; A3: still_not-bound_in (Subst (l,(a .--> x))) = { ((Subst (l,(a .--> x))) . n) where n is Element of NAT : ( 1 <= n & n <= len (Subst (l,(a .--> x))) & (Subst (l,(a .--> x))) . n in bound_QC-variables A ) } by QC_LANG1:def_29; consider n being Element of NAT such that A4: y9 = l . n and A5: 1 <= n and A6: n <= len l and A7: l . n in bound_QC-variables A by A1, A2; l . n <> a by A7, QC_LANG3:34; then A8: l . n = (Subst (l,(a .--> x))) . n by A5, A6, CQC_LANG:3; n <= len (Subst (l,(a .--> x))) by A6, CQC_LANG:def_1; hence y in still_not-bound_in (Subst (l,(a .--> x))) by A3, A4, A5, A7, A8; ::_thesis: verum end; hence still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x))) by TARSKI:def_3; ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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} let k be Element of NAT ; ::_thesis: 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} let l be QC-variable_list of k,A; ::_thesis: 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} let a be free_QC-variable of A; ::_thesis: for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x} let x be bound_QC-variable of A; ::_thesis: still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x} let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in still_not-bound_in (Subst (l,(a .--> x))) or y in (still_not-bound_in l) \/ {x} ) A1: still_not-bound_in l = { (l . n) where n is Element of NAT : ( 1 <= n & n <= len l & l . n in bound_QC-variables A ) } by QC_LANG1:def_29; assume A2: y in still_not-bound_in (Subst (l,(a .--> x))) ; ::_thesis: y in (still_not-bound_in l) \/ {x} then reconsider y9 = y as Element of still_not-bound_in (Subst (l,(a .--> x))) ; still_not-bound_in (Subst (l,(a .--> x))) = { ((Subst (l,(a .--> x))) . n) where n is Element of NAT : ( 1 <= n & n <= len (Subst (l,(a .--> x))) & (Subst (l,(a .--> x))) . n in bound_QC-variables A ) } by QC_LANG1:def_29; then consider n being Element of NAT such that A3: y9 = (Subst (l,(a .--> x))) . n and A4: 1 <= n and A5: n <= len (Subst (l,(a .--> x))) and A6: (Subst (l,(a .--> x))) . n in bound_QC-variables A by A2; A7: n <= len l by A5, CQC_LANG:def_1; percases ( l . n = a or l . n <> a ) ; suppose l . n = a ; ::_thesis: y in (still_not-bound_in l) \/ {x} then y9 = x by A3, A4, A7, CQC_LANG:3; then y9 in {x} by TARSKI:def_1; hence y in (still_not-bound_in l) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum end; suppose l . n <> a ; ::_thesis: y in (still_not-bound_in l) \/ {x} then l . n = (Subst (l,(a .--> x))) . n by A4, A7, CQC_LANG:3; then y9 in still_not-bound_in l by A1, A3, A4, A6, A7; hence y in (still_not-bound_in l) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum end; end; 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 let A be QC-alphabet ; ::_thesis: 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) let x be bound_QC-variable of A; ::_thesis: for h being QC-formula of A holds still_not-bound_in h c= still_not-bound_in (h . x) defpred S1[ QC-formula of A] means still_not-bound_in \$1 c= still_not-bound_in (\$1 . x); A1: for p being Element of QC-WFF A st S1[p] holds S1[ 'not' p] proof let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ 'not' p] ) still_not-bound_in (('not' p) . x) = still_not-bound_in ('not' (p . x)) by CQC_LANG:19 .= still_not-bound_in (p . x) by QC_LANG3:7 ; hence ( S1[p] implies S1[ 'not' p] ) by QC_LANG3:7; ::_thesis: verum end; A2: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds S1[p '&' q] proof let p, q be Element of QC-WFF A; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] ) assume that A3: S1[p] and A4: S1[q] ; ::_thesis: S1[p '&' q] A5: still_not-bound_in ((p '&' q) . x) = still_not-bound_in ((p . x) '&' (q . x)) by CQC_LANG:21 .= (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) by QC_LANG3:10 ; still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:10; hence S1[p '&' q] by A3, A4, A5, XBOOLE_1:13; ::_thesis: verum end; A6: for x being bound_QC-variable of A for p being Element of QC-WFF A st S1[p] holds S1[ All (x,p)] proof let y be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st S1[p] holds S1[ All (y,p)] let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ All (y,p)] ) assume A7: S1[p] ; ::_thesis: S1[ All (y,p)] percases ( y = x or y <> x ) ; suppose y = x ; ::_thesis: S1[ All (y,p)] hence S1[ All (y,p)] by CQC_LANG:24; ::_thesis: verum end; supposeA8: y <> x ; ::_thesis: S1[ All (y,p)] A9: still_not-bound_in (All (y,p)) = (still_not-bound_in p) \ {y} by QC_LANG3:12; still_not-bound_in ((All (y,p)) . x) = still_not-bound_in (All (y,(p . x))) by A8, CQC_LANG:25 .= (still_not-bound_in (p . x)) \ {y} by QC_LANG3:12 ; hence S1[ All (y,p)] by A7, A9, XBOOLE_1:33; ::_thesis: verum end; end; end; A10: for k being Element of NAT for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds S1[P ! ll] proof let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds S1[P ! ll] let P be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds S1[P ! ll] let ll be QC-variable_list of k,A; ::_thesis: S1[P ! ll] A11: still_not-bound_in ((P ! ll) . x) = still_not-bound_in (P ! (Subst (ll,((A a. 0) .--> x)))) by CQC_LANG:17 .= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by QC_LANG3:5 ; still_not-bound_in ll c= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by Th60; hence S1[P ! ll] by A11, QC_LANG3:5; ::_thesis: verum end; A12: S1[ VERUM A] by CQC_LANG:15; thus for h being QC-formula of A holds S1[h] from QC_LANG1:sch_1(A10, A12, A1, A2, A6); ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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} let x be bound_QC-variable of A; ::_thesis: for h being QC-formula of A holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x} defpred S1[ QC-formula of A] means still_not-bound_in (\$1 . x) c= (still_not-bound_in \$1) \/ {x}; A1: for p being Element of QC-WFF A st S1[p] holds S1[ 'not' p] proof let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ 'not' p] ) still_not-bound_in (('not' p) . x) = still_not-bound_in ('not' (p . x)) by CQC_LANG:19 .= still_not-bound_in (p . x) by QC_LANG3:7 ; hence ( S1[p] implies S1[ 'not' p] ) by QC_LANG3:7; ::_thesis: verum end; A2: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds S1[p '&' q] proof let p, q be Element of QC-WFF A; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] ) assume that A3: S1[p] and A4: S1[q] ; ::_thesis: S1[p '&' q] A5: still_not-bound_in ((p '&' q) . x) = still_not-bound_in ((p . x) '&' (q . x)) by CQC_LANG:21 .= (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) by QC_LANG3:10 ; A6: ((still_not-bound_in p) \/ {x}) \/ ((still_not-bound_in q) \/ {x}) = ((still_not-bound_in p) \/ ({x} \/ (still_not-bound_in q))) \/ {x} by XBOOLE_1:4 .= (((still_not-bound_in p) \/ (still_not-bound_in q)) \/ {x}) \/ {x} by XBOOLE_1:4 .= ((still_not-bound_in p) \/ (still_not-bound_in q)) \/ ({x} \/ {x}) by XBOOLE_1:4 .= ((still_not-bound_in p) \/ (still_not-bound_in q)) \/ {x} ; (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) c= ((still_not-bound_in p) \/ {x}) \/ ((still_not-bound_in q) \/ {x}) by A3, A4, XBOOLE_1:13; hence S1[p '&' q] by A5, A6, QC_LANG3:10; ::_thesis: verum end; A7: for x being bound_QC-variable of A for p being Element of QC-WFF A st S1[p] holds S1[ All (x,p)] proof let y be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st S1[p] holds S1[ All (y,p)] let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ All (y,p)] ) assume A8: S1[p] ; ::_thesis: S1[ All (y,p)] percases ( y = x or y <> x ) ; supposeA9: y = x ; ::_thesis: S1[ All (y,p)] A10: (still_not-bound_in p) \ {x} c= still_not-bound_in p by XBOOLE_1:36; A11: still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by QC_LANG3:12; still_not-bound_in p c= still_not-bound_in (p . x) by Th62; then still_not-bound_in (All (x,p)) c= still_not-bound_in (p . x) by A11, A10, XBOOLE_1:1; then A12: still_not-bound_in (All (x,p)) c= (still_not-bound_in p) \/ {x} by A8, XBOOLE_1:1; (still_not-bound_in (All (y,p))) \/ {x} = ((still_not-bound_in p) \ {x}) \/ {x} by A9, QC_LANG3:12 .= (still_not-bound_in p) \/ {x} by XBOOLE_1:39 ; hence S1[ All (y,p)] by A9, A12, CQC_LANG:24; ::_thesis: verum end; supposeA13: y <> x ; ::_thesis: S1[ All (y,p)] A14: (still_not-bound_in (All (y,p))) \/ {x} = ((still_not-bound_in p) \ {y}) \/ {x} by QC_LANG3:12 .= ((still_not-bound_in p) \/ {x}) \ {y} by A13, XBOOLE_1:87, ZFMISC_1:11 ; still_not-bound_in ((All (y,p)) . x) = still_not-bound_in (All (y,(p . x))) by A13, CQC_LANG:25 .= (still_not-bound_in (p . x)) \ {y} by QC_LANG3:12 ; hence S1[ All (y,p)] by A8, A14, XBOOLE_1:33; ::_thesis: verum end; end; end; A15: for k being Element of NAT for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds S1[P ! ll] proof let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds S1[P ! ll] let P be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds S1[P ! ll] let ll be QC-variable_list of k,A; ::_thesis: S1[P ! ll] A16: still_not-bound_in ((P ! ll) . x) = still_not-bound_in (P ! (Subst (ll,((A a. 0) .--> x)))) by CQC_LANG:17 .= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by QC_LANG3:5 ; still_not-bound_in (Subst (ll,((A a. 0) .--> x))) c= (still_not-bound_in ll) \/ {x} by Th61; hence S1[P ! ll] by A16, QC_LANG3:5; ::_thesis: verum end; A17: still_not-bound_in (VERUM A) = {} by QC_LANG3:3; (VERUM A) . x = VERUM A by CQC_LANG:15; then still_not-bound_in ((VERUM A) . x) = {} by A17; then A18: still_not-bound_in ((VERUM A) . x) c= (still_not-bound_in (VERUM A)) \/ {x} by XBOOLE_1:2; A19: S1[ VERUM A] by A18; thus for h being QC-formula of A holds S1[h] from QC_LANG1:sch_1(A15, A19, A1, A2, A7); ::_thesis: verum 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 let A be QC-alphabet ; ::_thesis: 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 let p be Element of CQC-WFF A; ::_thesis: 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 let h be QC-formula of A; ::_thesis: 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 let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & x <> y & not y in still_not-bound_in h implies not y in still_not-bound_in p ) assume that A1: p = h . x and A2: x <> y and A3: not y in still_not-bound_in h and A4: y in still_not-bound_in p ; ::_thesis: contradiction A5: still_not-bound_in p c= (still_not-bound_in h) \/ {x} by A1, Th63; percases ( y in still_not-bound_in h or y in {x} ) by A4, A5, XBOOLE_0:def_3; suppose y in still_not-bound_in h ; ::_thesis: contradiction hence contradiction by A3; ::_thesis: verum end; suppose y in {x} ; ::_thesis: contradiction hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; end; 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 let A be QC-alphabet ; ::_thesis: 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) let p, q be Element of CQC-WFF A; ::_thesis: 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) let h be QC-formula of A; ::_thesis: 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) let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h implies All (x,p) <==> All (y,q) ) assume that A1: p = h . x and A2: q = h . y and A3: not x in still_not-bound_in h and A4: not y in still_not-bound_in h ; ::_thesis: All (x,p) <==> All (y,q) percases ( x = y or x <> y ) ; suppose x = y ; ::_thesis: All (x,p) <==> All (y,q) hence All (x,p) <==> All (y,q) by A1, A2; ::_thesis: verum end; supposeA5: x <> y ; ::_thesis: All (x,p) <==> All (y,q) then not x in still_not-bound_in q by A2, A3, Th64; then A6: (All (y,q)) => (All (x,p)) is valid by A1, A2, A4, CQC_THE2:27; not y in still_not-bound_in p by A1, A4, A5, Th64; then (All (x,p)) => (All (y,q)) is valid by A1, A2, A3, CQC_THE2:27; hence All (x,p) <==> All (y,q) by A6, Th50; ::_thesis: verum end; end; end;