:: Calculus of Propositions :: by Jan Popio{\l}ek and Andrzej Trybulec :: :: Received October 23, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies SUBSET_1, CQC_LANG, XBOOLEAN, CQC_THE1, QC_LANG1; notations SUBSET_1, QC_LANG1, CQC_LANG, CQC_THE1; constructors CQC_THE1; registrations CQC_LANG; theorems CQC_THE1, QC_LANG2, LUKASI_1; begin :: Tautologies reserve A for QC-alphabet; reserve p, q, r, s for Element of CQC-WFF(A); theorem Th1: 'not' ( p '&' 'not' p ) in TAUT(A) proof p => p in TAUT(A) by LUKASI_1:4; hence thesis by QC_LANG2:def 2; end; Lm1: p 'or' q = ( 'not' p => q ) proof 'not' p => q = 'not' ( 'not' p '&' 'not' q ) by QC_LANG2:def 2; hence thesis by QC_LANG2:def 3; end; theorem Th2: p 'or' 'not' p in TAUT(A) proof 'not' p => 'not' p in TAUT(A) by LUKASI_1:4; hence thesis by Lm1; end; theorem Th3: p => ( p 'or' q ) in TAUT(A) proof p => ( 'not' p => q ) in TAUT(A) by CQC_THE1:43; hence thesis by Lm1; end; theorem Th4: q => ( p 'or' q ) in TAUT(A) proof q => ( 'not' p => q ) in TAUT(A) by LUKASI_1:5; hence thesis by Lm1; end; theorem Th5: ( p 'or' q ) => ( 'not' p => q ) in TAUT(A) proof ( 'not' p => q ) => ( 'not' p => q ) in TAUT(A) by LUKASI_1:4; hence thesis by Lm1; end; theorem Th6: 'not' ( p 'or' q ) => ( 'not' p '&' 'not' q ) in TAUT(A) proof 'not' ( p 'or' q ) = 'not' 'not' ( 'not' p '&' 'not' q ) by QC_LANG2:def 3; hence thesis by LUKASI_1:25; end; theorem Th7: ( 'not' p '&' 'not' q ) => 'not' ( p 'or' q ) in TAUT(A) proof 'not' ( p 'or' q ) = 'not' 'not' ( 'not' p '&' 'not' q ) by QC_LANG2:def 3; hence thesis by LUKASI_1:27; end; theorem Th8: ( p 'or' q ) => ( q 'or' p ) in TAUT(A) proof ( 'not' p => q ) => ( 'not' q => p ) in TAUT(A) by LUKASI_1:31; then ( p 'or' q ) => ( 'not' q => p ) in TAUT(A) by Lm1; hence thesis by Lm1; end; theorem 'not' p 'or' p in TAUT(A) proof ( p 'or' 'not' p ) => ( 'not' p 'or' p ) in TAUT(A) by Th8; hence thesis by Th2,CQC_THE1:46; end; theorem 'not' ( p 'or' q ) => 'not' p in TAUT(A) proof ( p => ( p 'or' q )) => ( 'not' ( p 'or' q ) => 'not' p ) in TAUT(A) & ( p => ( p 'or' q )) in TAUT(A) by Th3,LUKASI_1:26; hence thesis by CQC_THE1:46; end; theorem Th11: ( p 'or' p ) => p in TAUT(A) proof ( p 'or' p ) => ( 'not' p => p ) in TAUT(A) & ( 'not' p => p ) => p in TAUT(A) by Th5,CQC_THE1:42; hence thesis by LUKASI_1:3; end; theorem p => ( p 'or' p ) in TAUT(A) by Th3; theorem ( p '&' 'not' p ) => q in TAUT(A) proof 'not' q => 'not' ( p '&' 'not' p ) in TAUT(A) by Th1,LUKASI_1:13; hence thesis by LUKASI_1:35; end; theorem ( p => q ) => ( 'not' p 'or' q ) in TAUT(A) proof A1: ( 'not' 'not' p => p ) => (( p => q ) => ( 'not' 'not' p => q )) in TAUT(A) by LUKASI_1:1; ( 'not' 'not' p => q ) = ( 'not' p 'or' q ) & 'not' 'not' p => p in TAUT(A) by Lm1,LUKASI_1:25; hence thesis by A1,CQC_THE1:46; end; Lm2: ( p '&' q ) => ( 'not' 'not' p '&' q ) in TAUT(A) proof ( p => 'not' 'not' p ) => ('not' ( 'not' 'not' p '&' q ) => 'not' ( p '&' q ) ) in TAUT(A) & p => 'not' 'not' p in TAUT(A) by CQC_THE1:44,LUKASI_1:27; then 'not' ( 'not' 'not' p '&' q ) => 'not' ( p '&' q ) in TAUT(A) by CQC_THE1:46; hence thesis by LUKASI_1:35; end; Lm3: ( 'not' 'not' p '&' q ) => ( p '&' q ) in TAUT(A) proof ( 'not' 'not' p => p ) => ('not' ( p '&' q ) => 'not' ( 'not' 'not' p '&' q ) ) in TAUT(A) & 'not' 'not' p => p in TAUT(A) by CQC_THE1:44,LUKASI_1:25; then 'not' ( p '&' q ) => 'not' ( 'not' 'not' p '&' q ) in TAUT(A) by CQC_THE1:46; hence thesis by LUKASI_1:35; end; theorem Th15: ( p '&' q ) => 'not' ( p => 'not' q ) in TAUT(A) proof A1: ( p '&' 'not' 'not' q ) => 'not' 'not' ( p '&' 'not' 'not' q ) in TAUT(A) by LUKASI_1:27; q '&' p => 'not' 'not' q '&' p in TAUT(A) & p '&' q => q '&' p in TAUT(A) by Lm2,CQC_THE1:45; then A2: p '&' q => 'not' 'not' q '&' p in TAUT(A) by LUKASI_1:3; 'not' 'not' q '&' p => p '&' 'not' 'not' q in TAUT(A) by CQC_THE1:45; then ( p '&' q ) => ( p '&' 'not' 'not' q ) in TAUT(A) by A2,LUKASI_1:3; then ( p '&' q ) => 'not' 'not' ( p '&' 'not' 'not' q ) in TAUT(A) by A1, LUKASI_1:3; hence thesis by QC_LANG2:def 2; end; theorem Th16: 'not' ( p => 'not' q ) => ( p '&' q ) in TAUT(A) proof A1: 'not' 'not' ( p '&' 'not' 'not' q ) => ( p '&' 'not' 'not' q ) in TAUT(A) by LUKASI_1:25; p '&' 'not' 'not' q => 'not' 'not' q '&' p in TAUT(A) & 'not' 'not' q '&' p => q '&' p in TAUT(A) by Lm3,CQC_THE1:45; then A2: p '&' 'not' 'not' q => q '&' p in TAUT(A) by LUKASI_1:3; q '&' p => p '&' q in TAUT(A) by CQC_THE1:45; then ( p '&' 'not' 'not' q ) => ( p '&' q ) in TAUT(A) by A2,LUKASI_1:3; then 'not' 'not' ( p '&' 'not' 'not' q ) => ( p '&' q ) in TAUT(A) by A1, LUKASI_1:3; hence thesis by QC_LANG2:def 2; end; theorem Th17: 'not' ( p '&' q ) => ( 'not' p 'or' 'not' q ) in TAUT(A) proof 'not' 'not' p => p in TAUT(A) & ( 'not' 'not' p => p ) => (( p => 'not' q ) => ( 'not' 'not' p => 'not' q )) in TAUT(A) by LUKASI_1:1,25; then A1: ( p => 'not' q ) => ( 'not' 'not' p => 'not' q ) in TAUT(A) by CQC_THE1:46; 'not' ( p => 'not' q ) => p '&' q in TAUT(A) by Th16; then A2: 'not' ( p '&' q ) => 'not' 'not' ( p => 'not' q ) in TAUT(A) by LUKASI_1:34; 'not' 'not' ( p => 'not' q ) => ( p => 'not' q ) in TAUT(A) by LUKASI_1:25; then 'not' ( p '&' q ) => ( p => 'not' q ) in TAUT(A) by A2,LUKASI_1:3; then 'not' ( p '&' q ) => ( 'not' 'not' p => 'not' q ) in TAUT(A) by A1, LUKASI_1:3; hence thesis by Lm1; end; theorem Th18: ( 'not' p 'or' 'not' q ) => 'not' ( p '&' q ) in TAUT(A) proof A1: ( p => 'not' 'not' p ) => (( 'not' 'not' p => 'not' q ) => ( p => 'not' q )) in TAUT(A) by LUKASI_1:1; p '&' q => 'not' ( p => 'not' q ) in TAUT(A) by Th15; then A2: 'not' 'not' ( p => 'not' q ) => 'not' ( p '&' q ) in TAUT(A) by LUKASI_1:34; ( p => 'not' q ) => 'not' 'not' ( p => 'not' q ) in TAUT(A) by LUKASI_1:27; then A3: ( p => 'not' q ) => 'not' ( p '&' q ) in TAUT(A) by A2,LUKASI_1:3; ( 'not' p 'or' 'not' q ) = ( 'not' 'not' p => 'not' q ) & p => 'not' 'not' p in TAUT(A) by Lm1,LUKASI_1:27; then ( 'not' p 'or' 'not' q ) => ( p => 'not' q ) in TAUT(A) by A1,CQC_THE1:46; hence thesis by A3,LUKASI_1:3; end; theorem Th19: ( p '&' q ) => p in TAUT(A) proof 'not' p => ( 'not' p 'or' 'not' q ) in TAUT(A) by Th3; then A1: 'not' ( 'not' p 'or' 'not' q ) => 'not' 'not' p in TAUT(A) by LUKASI_1:34; ( 'not' p 'or' 'not' q ) => 'not' ( p '&' q ) in TAUT(A) by Th18; then A2: 'not' 'not' ( p '&' q ) => 'not' ( 'not' p 'or' 'not' q ) in TAUT(A) by LUKASI_1:34; ( p '&' q ) => 'not' 'not' ( p '&' q ) in TAUT(A) by LUKASI_1:27; then A3: ( p '&' q ) => 'not' ( 'not' p 'or' 'not' q ) in TAUT(A) by A2,LUKASI_1:3; 'not' 'not' p => p in TAUT(A) by LUKASI_1:25; then 'not' ( 'not' p 'or' 'not' q ) => p in TAUT(A) by A1,LUKASI_1:3; hence thesis by A3,LUKASI_1:3; end; theorem Th20: ( p '&' q ) => ( p 'or' q ) in TAUT(A) proof p => ( p 'or' q ) in TAUT(A) & ( p '&' q ) => p in TAUT(A) by Th3,Th19; hence thesis by LUKASI_1:3; end; theorem Th21: ( p '&' q ) => q in TAUT(A) proof ( q '&' p ) => q in TAUT(A) & ( p '&' q ) => ( q '&' p ) in TAUT(A) by Th19, CQC_THE1:45; hence thesis by LUKASI_1:3; end; theorem p => p '&' p in TAUT(A) proof 'not' ( p '&' p ) => ( 'not' p 'or' 'not' p ) in TAUT(A) & ( 'not' p 'or' 'not' p ) => 'not' p in TAUT(A) by Th11,Th17; then 'not' ( p '&' p ) => 'not' p in TAUT(A) by LUKASI_1:3; hence thesis by LUKASI_1:35; end; theorem ( p <=> q ) => ( p => q ) in TAUT(A) proof ( p <=> q ) = ( p => q ) '&' ( q => p ) by QC_LANG2:def 4; hence thesis by Th19; end; theorem ( p <=> q ) => ( q => p ) in TAUT(A) proof ( p <=> q ) = ( p => q ) '&' ( q => p ) by QC_LANG2:def 4; hence thesis by Th21; end; theorem Th25: (( p 'or' q ) 'or' r ) => ( p 'or' ( q 'or' r )) in TAUT(A) proof 'not' p => (( 'not' r => q ) => ( 'not' q => r )) in TAUT(A) & ( 'not' p => (( 'not' r => q ) => ( 'not' q => r ))) => (( 'not' p => ( 'not' r => q )) => ( 'not' p => ( 'not' q => r ))) in TAUT(A) by LUKASI_1:11,13,31; then A1: ( 'not' p => ( 'not' r => q )) => ( 'not' p => ( 'not' q => r )) in TAUT(A) by CQC_THE1:46; (( p 'or' q ) 'or' r ) => ( r 'or' ( p 'or' q )) in TAUT(A) & ( r 'or' ( p 'or' q )) => ( 'not' r => ( p 'or' q )) in TAUT(A) by Th5,Th8; then (( p 'or' q ) 'or' r ) => ( 'not' r => ( p 'or' q )) in TAUT(A) by LUKASI_1:3; then A2: (( p 'or' q ) 'or' r ) => ( 'not' r => ( 'not' p => q )) in TAUT(A) by Lm1; ( 'not' r => ( 'not' p => q )) => ( 'not' p => ( 'not' r => q )) in TAUT(A) by LUKASI_1:8; then (( p 'or' q ) 'or' r ) => ( 'not' p => ( 'not' r => q )) in TAUT(A) by A2, LUKASI_1:3; then (( p 'or' q ) 'or' r ) => ( 'not' p => ( 'not' q => r )) in TAUT(A) by A1,LUKASI_1:3; then (( p 'or' q ) 'or' r ) => ( 'not' p => ( q 'or' r )) in TAUT(A) by Lm1; hence thesis by Lm1; end; theorem (( p '&' q ) '&' r ) => ( p '&' ( q '&' r )) in TAUT(A) proof A1: ( 'not' p 'or' ( 'not' r 'or' 'not' q )) => (( 'not' r 'or' 'not' q ) 'or' 'not' p ) in TAUT(A) by Th8; 'not' ( q '&' r ) => ( 'not' q 'or' 'not' r ) in TAUT(A) & ( 'not' q 'or' 'not' r ) => ( 'not' r 'or' 'not' q ) in TAUT(A) by Th8,Th17; then 'not' ( q '&' r ) => ( 'not' r 'or' 'not' q ) in TAUT(A) by LUKASI_1:3; then A2: 'not' 'not' p => ( 'not' ( q '&' r ) => ( 'not' r 'or' 'not' q )) in TAUT(A) by LUKASI_1:13; ( 'not' 'not' p => ( 'not' ( q '&' r ) => ( 'not' r 'or' 'not' q ))) => (( 'not' 'not' p => 'not' ( q '&' r )) => ( 'not' 'not' p => ( 'not' r 'or' 'not' q ))) in TAUT(A) by LUKASI_1:11; then ( 'not' 'not' p => 'not' ( q '&' r )) => ( 'not' 'not' p => ( 'not' r 'or' 'not' q )) in TAUT(A) by A2,CQC_THE1:46; then ( 'not' p 'or' 'not' ( q '&' r )) => ( 'not' 'not' p => ( 'not' r 'or' 'not' q )) in TAUT(A) by Lm1; then A3: ( 'not' p 'or' 'not' ( q '&' r )) => ( 'not' p 'or' ( 'not' r 'or' 'not' q )) in TAUT(A) by Lm1; 'not' ( p '&' ( q '&' r )) => ( 'not' p 'or' 'not' ( q '&' r ))in TAUT(A) by Th17; then 'not' ( p '&' ( q '&' r )) => ( 'not' p 'or' ( 'not' r 'or' 'not' q )) in TAUT(A) by A3,LUKASI_1:3; then A4: 'not' ( p '&' ( q '&' r )) => (( 'not' r 'or' 'not' q ) 'or' 'not' p ) in TAUT(A) by A1,LUKASI_1:3; A5: ( 'not' ( p '&' q ) 'or' 'not' r) => 'not' (( p '&' q ) '&' r ) in TAUT(A) by Th18; ( 'not' q 'or' 'not' p ) => ( 'not' p 'or' 'not' q ) in TAUT(A) & ( 'not' p 'or' 'not' q ) => 'not' ( p '&' q ) in TAUT(A) by Th8,Th18; then ( 'not' q 'or' 'not' p ) => 'not' ( p '&' q ) in TAUT(A) by LUKASI_1:3; then A6: 'not' 'not' r => (( 'not' q 'or' 'not' p ) => 'not' ( p '&' q )) in TAUT(A) by LUKASI_1:13; ( 'not' 'not' r => (( 'not' q 'or' 'not' p ) => 'not' ( p '&' q ))) => (( 'not' 'not' r => ( 'not' q 'or' 'not' p )) => ( 'not' 'not' r => 'not' ( p '&' q ))) in TAUT(A) by LUKASI_1:11; then ( 'not' 'not' r => ( 'not' q 'or' 'not' p )) => ( 'not' 'not' r => 'not' ( p '&' q )) in TAUT(A) by A6,CQC_THE1:46; then ( 'not' r 'or' ( 'not' q 'or' 'not' p )) => ( 'not' 'not' r => 'not' ( p '&' q )) in TAUT(A) by Lm1; then A7: ( 'not' r 'or' ( 'not' q 'or' 'not' p )) => ( 'not' r 'or' 'not' ( p '&' q )) in TAUT(A) by Lm1; ( 'not' r 'or' 'not' ( p '&' q )) => ( 'not' ( p '&' q ) 'or' 'not' r) in TAUT(A) by Th8; then ( 'not' r 'or' ( 'not' q 'or' 'not' p )) => ( 'not' ( p '&' q ) 'or' 'not' r) in TAUT(A) by A7,LUKASI_1:3; then A8: ( 'not' r 'or' ( 'not' q 'or' 'not' p )) => 'not' (( p '&' q ) '&' r ) in TAUT(A) by A5,LUKASI_1:3; (( 'not' r 'or' 'not' q ) 'or' 'not' p ) => ( 'not' r 'or' ( 'not' q 'or' 'not' p )) in TAUT(A) by Th25; then 'not' ( p '&' ( q '&' r )) => ( 'not' r 'or' ( 'not' q 'or' 'not' p )) in TAUT(A) by A4,LUKASI_1:3; then 'not' ( p '&' ( q '&' r )) => 'not' (( p '&' q ) '&' r ) in TAUT(A) by A8,LUKASI_1:3; hence thesis by LUKASI_1:35; end; theorem Th27: ( p 'or' ( q 'or' r )) => (( p 'or' q ) 'or' r ) in TAUT(A) proof A1: ( 'not' p => ( 'not' r => q )) => ( 'not' r => ( 'not' p => q )) in TAUT(A) by LUKASI_1:8; 'not' p => (( 'not' q => r ) => ( 'not' r => q )) in TAUT(A) & ( 'not' p => (( 'not' q => r ) => ( 'not' r => q ))) => (( 'not' p => ( 'not' q => r )) => ( 'not' p => ( 'not' r => q ))) in TAUT(A) by LUKASI_1:11,13,31; then A2: ( 'not' p => ( 'not' q => r )) => ( 'not' p => ( 'not' r => q )) in TAUT(A) by CQC_THE1:46; ( p 'or' ( q 'or' r )) => ( 'not' p => ( q 'or' r )) in TAUT(A) by Th5; then ( p 'or' ( q 'or' r )) => ( 'not' p => ( 'not' q => r )) in TAUT(A) by Lm1; then ( p 'or' ( q 'or' r )) => ( 'not' p => ( 'not' r => q )) in TAUT(A) by A2,LUKASI_1:3; then ( p 'or' ( q 'or' r )) => ( 'not' r => ( 'not' p => q )) in TAUT(A) by A1,LUKASI_1:3; then A3: ( p 'or' ( q 'or' r )) => ( r 'or' ( 'not' p => q )) in TAUT(A) by Lm1; ( r 'or' ( 'not' p => q )) => (( 'not' p => q ) 'or' r) in TAUT(A) by Th8; then ( p 'or' ( q 'or' r )) => (( 'not' p => q ) 'or' r) in TAUT(A) by A3, LUKASI_1:3; hence thesis by Lm1; end; theorem Th28: p => ( q => ( p '&' q )) in TAUT(A) proof A1: ((( p '&' q ) 'or' 'not' p ) 'or' 'not' q ) => ( 'not' q 'or' (( p '&' q ) 'or' 'not' p )) in TAUT(A) by Th8; 'not' ( p '&' q ) => ( 'not' p 'or' 'not' q ) in TAUT(A) by Th17; then A2: ( p '&' q ) 'or' ( 'not' p 'or' 'not' q ) in TAUT(A) by Lm1; ( p '&' q ) 'or' ( 'not' p 'or' 'not' q ) => ((( p '&' q ) 'or' 'not' p ) 'or' 'not' q ) in TAUT(A) by Th27; then ((( p '&' q ) 'or' 'not' p ) 'or' 'not' q ) in TAUT(A) by A2,CQC_THE1:46; then ( 'not' q 'or' (( p '&' q ) 'or' 'not' p )) in TAUT(A) by A1,CQC_THE1:46; then A3: ( 'not' 'not' q => (( p '&' q ) 'or' 'not' p )) in TAUT(A) by Lm1; q => ((( p '&' q ) 'or' 'not' p ) => ( 'not' p 'or' ( p '&' q ))) in TAUT(A) & (q => ((( p '&' q ) 'or' 'not' p ) => ( 'not' p 'or' ( p '&' q )))) => ( (q => ( p '&' q ) 'or' 'not' p ) => ( q => ( 'not' p 'or' ( p '&' q )))) in TAUT(A) by Th8,LUKASI_1:11,13; then A4: (q => ( p '&' q ) 'or' 'not' p ) => ( q => ( 'not' p 'or' ( p '&' q ))) in TAUT(A) by CQC_THE1:46; q => 'not' 'not' q in TAUT(A) by LUKASI_1:27; then ( q => (( p '&' q ) 'or' 'not' p )) in TAUT(A) by A3,LUKASI_1:3; then ( q => ( 'not' p 'or' ( p '&' q ))) in TAUT(A) by A4,CQC_THE1:46; then ( q => ( 'not' 'not' p => ( p '&' q ))) in TAUT(A) by Lm1; then A5: 'not' 'not' p => ( q => ( p '&' q )) in TAUT(A) by LUKASI_1:15; p => 'not' 'not' p in TAUT(A) by LUKASI_1:27; hence thesis by A5,LUKASI_1:3; end; theorem ( p => q ) => (( q => p ) => ( p <=> q )) in TAUT(A) proof ( p => q ) => (( q => p ) => (( p => q ) '&' ( q => p ))) in TAUT(A) by Th28; hence thesis by QC_LANG2:def 4; end; Lm4: p in TAUT(A) & q in TAUT(A) implies p '&' q in TAUT(A) proof assume that A1: p in TAUT(A) and A2: q in TAUT(A); p => ( q => ( p '&' q )) in TAUT(A) by Th28; then q => ( p '&' q ) in TAUT(A) by A1,CQC_THE1:46; hence thesis by A2,CQC_THE1:46; end; theorem ( p 'or' q ) <=> ( q 'or' p ) in TAUT(A) proof set P = p 'or' q; set Q = q 'or' p; P => Q in TAUT(A) & Q => P in TAUT(A) by Th8; then ( P => Q ) '&' ( Q => P ) in TAUT(A) by Lm4; hence thesis by QC_LANG2:def 4; end; theorem (( p '&' q ) => r ) => ( p => ( q => r )) in TAUT(A) proof p => (( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r ))) in TAUT(A) & p => ( q => ( p '&' q )) in TAUT(A) by Th28,LUKASI_1:1,13; then A1: p => ((( p '&' q ) => r ) => ( q => r )) in TAUT(A) by LUKASI_1:20; (p => ((( p '&' q ) => r ) => ( q => r ))) => ((( p '&' q ) => r ) => ( p => ( q => r ))) in TAUT(A) by LUKASI_1:8; hence thesis by A1,CQC_THE1:46; end; theorem Th32: ( p => ( q => r )) => (( p '&' q ) => r ) in TAUT(A) proof A1: ( p => (( p '&' q ) => r )) => ((p '&' q ) => ( p => r )) in TAUT(A) by LUKASI_1:8; ((p '&' q ) => ( p => r )) => ((( p '&' q ) => p ) => (( p '&' q ) => r )) in TAUT(A) by LUKASI_1:11; then A2: ((p '&' q ) => ( p => r )) => (( p '&' q ) => r ) in TAUT(A) by Th19, LUKASI_1:16; ( p '&' q ) => q in TAUT(A) & (( p '&' q ) => q) => (( q => r ) => (( p '&' q ) => r )) in TAUT(A) by Th21,LUKASI_1:1; then ( q => r ) => (( p '&' q ) => r ) in TAUT(A) by CQC_THE1:46; then A3: p => (( q => r ) => (( p '&' q ) => r )) in TAUT(A) by LUKASI_1:13; p => (( q => r ) => (( p '&' q ) => r )) => ((p => ( q => r )) => ( p => (( p '&' q ) => r ))) in TAUT(A) by LUKASI_1:11; then (p => ( q => r )) => ( p => (( p '&' q ) => r )) in TAUT(A) by A3, CQC_THE1:46; then (p => ( q => r )) => ((p '&' q ) => ( p => r )) in TAUT(A) by A1,LUKASI_1:3; hence thesis by A2,LUKASI_1:3; end; theorem Th33: ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in TAUT(A) proof r => ( p => ( q => ( p '&' q ))) in TAUT(A) & (r => ( p => ( q => ( p '&' q ))) ) => (( r => p ) => ( r => ( q => ( p '&' q )))) in TAUT(A) by Th28, LUKASI_1:11,13; then A1: ( r => p ) => ( r => ( q => ( p '&' q ))) in TAUT(A) by CQC_THE1:46; ( r => ( q => ( p '&' q ))) => (( r => q ) => ( r => ( p '&' q ))) in TAUT(A) by LUKASI_1:11; hence thesis by A1,LUKASI_1:3; end; theorem (( p 'or' q ) => r ) => (( p => r ) 'or' ( q => r )) in TAUT(A) proof q => ( p 'or' q ) in TAUT(A) & ( q => ( p 'or' q )) => ((( p 'or' q ) => r ) => ( q => r )) in TAUT(A) by Th4,LUKASI_1:1; then (( p 'or' q ) => r ) => ( q => r ) in TAUT(A) by CQC_THE1:46; then 'not' ( p => r ) => ((( p 'or' q ) => r ) => ( q => r )) in TAUT(A) by LUKASI_1:13; then (( p 'or' q ) => r ) => ( 'not' ( p => r ) => ( q => r )) in TAUT(A) by LUKASI_1:15; hence thesis by Lm1; end; theorem Th35: ( p => r ) => (( q => r ) => (( p 'or' q ) => r)) in TAUT(A) proof set AA = ( 'not' r => 'not' p ); set B = ( 'not' r => 'not' q ); set C = ( 'not' r => ( 'not' p '&' 'not' q )); set D = (( p 'or' q ) => r ); set E = q => r; A1: AA => ( B => C) in TAUT(A) by Th33; C => ('not' ( 'not' p '&' 'not' q ) => r ) in TAUT(A) by LUKASI_1:31; then C => D in TAUT(A) by QC_LANG2:def 3; then A2: B => ( C => D ) in TAUT(A) by LUKASI_1:13; B => ( C => D ) => (( B => C ) => ( B => D )) in TAUT(A) by LUKASI_1:11; then ( B => C ) => ( B => D ) in TAUT(A) by A2,CQC_THE1:46; then AA => ( B => D ) in TAUT(A) by A1,LUKASI_1:3; then A3: B => ( AA => D ) in TAUT(A) by LUKASI_1:15; E => B in TAUT(A) by LUKASI_1:26; then E => ( AA => D ) in TAUT(A) by A3,LUKASI_1:3; then A4: AA => ( E => D ) in TAUT(A) by LUKASI_1:15; (p => r) => AA in TAUT(A) by LUKASI_1:26; hence thesis by A4,LUKASI_1:3; end; theorem Th36: (( p => r ) '&' ( q => r )) => (( p 'or' q ) => r) in TAUT(A) proof set P = ( p => r ); set Q = ( q => r ); set R = (( p 'or' q ) => r); P => ( Q => R ) in TAUT(A) & (P => ( Q => R )) => (( P '&' Q ) => R ) in TAUT(A) by Th32,Th35; hence thesis by CQC_THE1:46; end; theorem ( p => ( q '&' 'not' q )) => 'not' p in TAUT(A) proof p => 'not' ( q '&' 'not' q ) in TAUT(A) by Th1,LUKASI_1:13; then A1: 'not' 'not' ( q '&' 'not' q ) => 'not' p in TAUT(A) by LUKASI_1:34; ( q '&' 'not' q ) => 'not' 'not' ( q '&' 'not' q ) in TAUT(A) by LUKASI_1:27; then ( q '&' 'not' q ) => 'not' p in TAUT(A) by A1,LUKASI_1:3; then A2: p => (( q '&' 'not' q ) => 'not' p) in TAUT(A) by LUKASI_1:13; 'not' 'not' p => p in TAUT(A) & ( 'not' 'not' p => p ) => (( p => 'not' p ) => ( 'not' 'not' p => 'not' p )) in TAUT(A) by LUKASI_1:1,25; then ( 'not' 'not' p => 'not' p ) => 'not' p in TAUT(A) & ( p => 'not' p ) => ( 'not' 'not' p => 'not' p ) in TAUT(A) by CQC_THE1:42,46; then A3: ( p => 'not' p ) => 'not' p in TAUT(A) by LUKASI_1:3; p => (( q '&' 'not' q ) => 'not' p) => (( p => ( q '&' 'not' q )) => ( p => 'not' p )) in TAUT(A) by LUKASI_1:11; then ( p => ( q '&' 'not' q )) => ( p => 'not' p ) in TAUT(A) by A2,CQC_THE1:46; hence thesis by A3,LUKASI_1:3; end; theorem (( p 'or' q ) '&' ( p 'or' r )) => ( p 'or' ( q '&' r )) in TAUT(A) proof ( 'not' p => q ) => (( 'not' p => r ) => ( 'not' p => ( q '&' r ))) in TAUT(A) by Th33; then ( p 'or' q ) => (( 'not' p => r ) => ( 'not' p => ( q '&' r ))) in TAUT(A) by Lm1; then ( p 'or' q ) => (( p 'or' r ) => ( 'not' p => ( q '&' r ))) in TAUT(A) by Lm1; then A1: ( p 'or' q ) => (( p 'or' r ) => ( p 'or' ( q '&' r ))) in TAUT(A) by Lm1; (( p 'or' q ) => (( p 'or' r ) => ( p 'or' ( q '&' r )))) => ((( p 'or' q ) '&' ( p 'or' r )) => ( p 'or' ( q '&' r ))) in TAUT(A) by Th32; hence thesis by A1,CQC_THE1:46; end; theorem ( p '&' ( q 'or' r )) => (( p '&' q ) 'or' ( p '&' r )) in TAUT(A) proof A1: 'not' (( p '&' q ) 'or' ( p '&' r )) => ( 'not' ( p '&' q ) '&' 'not' ( p '&' r )) in TAUT(A) by Th6; 'not' ( p => 'not' q ) => ( p '&' q ) in TAUT(A) & ('not' ( p => 'not' q ) => ( p '&' q )) => ( 'not' ( p '&' q ) => ( p => 'not' q )) in TAUT(A) by Th16,LUKASI_1:31; then A2: 'not' ( p '&' q ) => ( p => 'not' q ) in TAUT(A) by CQC_THE1:46; 'not' ( p => 'not' r ) => ( p '&' r ) in TAUT(A) & ('not' ( p => 'not' r ) => ( p '&' r )) => ( 'not' ( p '&' r ) => ( p => 'not' r )) in TAUT(A) by Th16,LUKASI_1:31; then A3: 'not' ( p '&' r ) => ( p => 'not' r ) in TAUT(A) by CQC_THE1:46; ( p => 'not' q ) => (( p => 'not' r ) => ( p => ( 'not' q '&' 'not' r )) ) in TAUT(A) & ( p => ( 'not' q '&' 'not' r )) = 'not' ( p '&' 'not' ( 'not' q '&' 'not' r )) by Th33,QC_LANG2:def 2; then ( p => 'not' q ) => (( p => 'not' r ) => 'not' ( p '&' ( q 'or' r ))) in TAUT(A) by QC_LANG2:def 3; then 'not' ( p '&' q ) => (( p => 'not' r ) => 'not' ( p '&' ( q 'or' r ))) in TAUT(A) by A2,LUKASI_1:3; then ( p => 'not' r ) => ( 'not' ( p '&' q ) => 'not' ( p '&' ( q 'or' r ))) in TAUT(A) by LUKASI_1:15; then 'not' ( p '&' r ) => ('not' ( p '&' q ) => 'not' ( p '&' ( q 'or' r ))) in TAUT(A) by A3,LUKASI_1:3; then A4: 'not' ( p '&' q ) => ('not' ( p '&' r ) => 'not' ( p '&' ( q 'or' r ))) in TAUT(A) by LUKASI_1:15; ( 'not' ( p '&' q ) => ('not' ( p '&' r ) => 'not' ( p '&' ( q 'or' r ) ))) => ((( 'not' ( p '&' q ) '&' 'not' ( p '&' r )) => 'not' ( p '&' ( q 'or' r )))) in TAUT(A) by Th32; then ( 'not' ( p '&' q ) '&' 'not' ( p '&' r )) => 'not' ( p '&' ( q 'or' r )) in TAUT(A) by A4,CQC_THE1:46; then 'not' (( p '&' q ) 'or' ( p '&' r )) => 'not' ( p '&' ( q 'or' r )) in TAUT(A) by A1,LUKASI_1:3; hence thesis by LUKASI_1:35; end; theorem Th40: (( p 'or' r ) '&' ( q 'or' r )) => (( p '&' q ) 'or' r ) in TAUT(A) proof (( 'not' p => r ) '&' ( 'not' q => r )) => (( 'not' p 'or' 'not' q ) => r) in TAUT(A) by Th36; then (( p 'or' r ) '&' ( 'not' q => r )) => (( 'not' p 'or' 'not' q ) => r) in TAUT(A) by Lm1; then A1: (( p 'or' r ) '&' ( q 'or' r )) => (( 'not' p 'or' 'not' q ) => r) in TAUT(A) by Lm1; 'not' ( p '&' q ) => ( 'not' p 'or' 'not' q ) in TAUT(A) & ( 'not' ( p '&' q ) => ( 'not' p 'or' 'not' q )) => ((( 'not' p 'or' 'not' q ) => r) => ( 'not' ( p '&' q ) => r )) in TAUT(A) by Th17,LUKASI_1:1; then (( 'not' p 'or' 'not' q ) => r) => ( 'not' ( p '&' q ) => r ) in TAUT(A) by CQC_THE1:46; then (( p 'or' r ) '&' ( q 'or' r )) => ( 'not' ( p '&' q ) => r ) in TAUT(A) by A1,LUKASI_1:3; hence thesis by Lm1; end; Lm5: p => q in TAUT(A) implies ( r '&' p ) => ( r '&' q ) in TAUT(A) proof A1: 'not' ( r => 'not' q ) => ( r '&' q ) in TAUT(A) by Th16; assume p => q in TAUT(A); then 'not' q => 'not' p in TAUT(A) by LUKASI_1:34; then A2: r => ( 'not' q => 'not' p ) in TAUT(A) by LUKASI_1:13; ( r => ( 'not' q => 'not' p )) => (( r => 'not' q ) => ( r => 'not' p )) in TAUT(A) by LUKASI_1:11; then ( r => 'not' q ) => ( r => 'not' p ) in TAUT(A) by A2,CQC_THE1:46; then A3: 'not' ( r => 'not' p ) => 'not' ( r => 'not' q ) in TAUT(A) by LUKASI_1:34; ( r '&' p ) => 'not' ( r => 'not' p ) in TAUT(A) by Th15; then ( r '&' p ) => 'not' ( r => 'not' q ) in TAUT(A) by A3,LUKASI_1:3; hence thesis by A1,LUKASI_1:3; end; Lm6: p => q in TAUT(A) implies ( p 'or' r ) => ( q 'or' r ) in TAUT(A) proof assume p => q in TAUT(A); then A1: 'not' q => 'not' p in TAUT(A) by LUKASI_1:34; ( 'not' q => 'not' p ) => (( 'not' p => r ) => ( 'not' q => r )) in TAUT(A) by LUKASI_1:1; then ( 'not' p => r ) => ( 'not' q => r ) in TAUT(A) by A1,CQC_THE1:46; then ( p 'or' r ) => ( 'not' q => r ) in TAUT(A) by Lm1; hence thesis by Lm1; end; Lm7: p => q in TAUT(A) implies ( r 'or' p ) => ( r 'or' q ) in TAUT(A) proof assume p => q in TAUT(A); then A1: 'not' r => ( p => q ) in TAUT(A) by LUKASI_1:13; 'not' r => ( p => q ) => (( 'not' r => p ) => ( 'not' r => q )) in TAUT(A) by LUKASI_1:11; then ( 'not' r => p ) => ( 'not' r => q ) in TAUT(A) by A1,CQC_THE1:46; then ( r 'or' p ) => ( 'not' r => q ) in TAUT(A) by Lm1; hence thesis by Lm1; end; theorem (( p 'or' q ) '&' r ) => (( p '&' r ) 'or' ( q '&' r )) in TAUT(A) proof A1: 'not' (( 'not' p 'or' 'not' r ) '&' ( 'not' q 'or' 'not' r )) => ('not' ( 'not' p 'or' 'not' r ) 'or' 'not' ( 'not' q 'or' 'not' r )) in TAUT(A) by Th17; (( 'not' p 'or' 'not' r ) '&' ( 'not' q 'or' 'not' r )) => (( 'not' p '&' 'not' q ) 'or' 'not' r ) in TAUT(A) by Th40; then A2: 'not' (( 'not' p '&' 'not' q ) 'or' 'not' r ) => 'not' (( 'not' p 'or' 'not' r ) '&' ( 'not' q 'or' 'not' r )) in TAUT(A) by LUKASI_1:34; ( 'not' ( 'not' p '&' 'not' q ) '&' 'not' 'not' r ) => 'not' (( 'not' p '&' 'not' q ) 'or' 'not' r ) in TAUT(A) by Th7; then ( 'not' ( 'not' p '&' 'not' q ) '&' 'not' 'not' r ) => 'not' (( 'not' p 'or' 'not' r ) '&' ( 'not' q 'or' 'not' r )) in TAUT(A) by A2,LUKASI_1:3; then A3: (( p 'or' q ) '&' 'not' 'not' r ) => 'not' (( 'not' p 'or' 'not' r ) '&' ( 'not' q 'or' 'not' r )) in TAUT(A) by QC_LANG2:def 3; 'not' ( p '&' r ) => ( 'not' p 'or' 'not' r ) in TAUT(A) & ( 'not' ( p '&' r ) => ( 'not' p 'or' 'not' r )) => ( 'not' ( 'not' p 'or' 'not' r ) => ( p '&' r ) ) in TAUT(A) by Th17,LUKASI_1:31; then 'not' ( 'not' p 'or' 'not' r ) => ( p '&' r ) in TAUT(A) by CQC_THE1:46; then A4: ( 'not' ( 'not' p 'or' 'not' r ) 'or' 'not' ( 'not' q 'or' 'not' r ) ) => (( p '&' r ) 'or' 'not' ( 'not' q 'or' 'not' r )) in TAUT(A) by Lm6; 'not' ( q '&' r ) => ( 'not' q 'or' 'not' r ) in TAUT(A) & ( 'not' ( q '&' r ) => ( 'not' q 'or' 'not' r )) => ( 'not' ( 'not' q 'or' 'not' r ) => ( q '&' r ) ) in TAUT(A) by Th17,LUKASI_1:31; then 'not' ( 'not' q 'or' 'not' r ) => ( q '&' r ) in TAUT(A) by CQC_THE1:46; then A5: (( p '&' r ) 'or' 'not' ( 'not' q 'or' 'not' r )) => (( p '&' r ) 'or' ( q '&' r )) in TAUT(A) by Lm7; r => 'not' 'not' r in TAUT(A) by LUKASI_1:27; then (( p 'or' q ) '&' r ) => (( p 'or' q ) '&' 'not' 'not' r ) in TAUT(A) by Lm5; then (( p 'or' q ) '&' r ) => 'not' (( 'not' p 'or' 'not' r ) '&' ( 'not' q 'or' 'not' r )) in TAUT(A) by A3,LUKASI_1:3; then (( p 'or' q ) '&' r ) => ('not' ( 'not' p 'or' 'not' r ) 'or' 'not' ( 'not' q 'or' 'not' r )) in TAUT(A) by A1,LUKASI_1:3; then (( p 'or' q ) '&' r ) => (( p '&' r ) 'or' 'not' ( 'not' q 'or' 'not' r )) in TAUT(A) by A4,LUKASI_1:3; hence thesis by A5,LUKASI_1:3; end; :: Deduction Rules theorem p in TAUT(A) implies ( p 'or' q ) in TAUT(A) proof assume A1: p in TAUT(A); p => ( p 'or' q ) in TAUT(A) by Th3; hence thesis by A1,CQC_THE1:46; end; theorem q in TAUT(A) implies ( p 'or' q ) in TAUT(A) proof assume A1: q in TAUT(A); q => ( p 'or' q ) in TAUT(A) by Th4; hence thesis by A1,CQC_THE1:46; end; theorem ( p '&' q ) in TAUT(A) implies p in TAUT(A) proof assume A1: ( p '&' q ) in TAUT(A); ( p '&' q ) => p in TAUT(A) by Th19; hence thesis by A1,CQC_THE1:46; end; theorem ( p '&' q ) in TAUT(A) implies q in TAUT(A) proof assume A1: ( p '&' q ) in TAUT(A); ( p '&' q ) => q in TAUT(A) by Th21; hence thesis by A1,CQC_THE1:46; end; theorem ( p '&' q ) in TAUT(A) implies ( p 'or' q ) in TAUT(A) proof assume A1: ( p '&' q ) in TAUT(A); ( p '&' q ) => ( p 'or' q ) in TAUT(A) by Th20; hence thesis by A1,CQC_THE1:46; end; theorem p in TAUT(A) & q in TAUT(A) implies p '&' q in TAUT(A) by Lm4; theorem p => q in TAUT(A) implies ( p 'or' r ) => ( q 'or' r ) in TAUT(A) by Lm6; theorem p => q in TAUT(A) implies ( r 'or' p ) => ( r 'or' q ) in TAUT(A) by Lm7; theorem p => q in TAUT(A) implies ( r '&' p ) => ( r '&' q ) in TAUT(A) by Lm5; theorem Th51: p => q in TAUT(A) implies ( p '&' r ) => ( q '&' r ) in TAUT(A) proof A1: ( p => q ) => (( q => 'not' r ) => ( p => 'not' r )) in TAUT(A) by LUKASI_1:1; assume p => q in TAUT(A); then ( q => 'not' r ) => ( p => 'not' r ) in TAUT(A) by A1,CQC_THE1:46; then A2: 'not' ( p => 'not' r ) => 'not' ( q => 'not' r ) in TAUT(A) by LUKASI_1:34; A3: 'not' ( q => 'not' r ) => ( q '&' r ) in TAUT(A) by Th16; ( p '&' r ) => 'not' ( p => 'not' r ) in TAUT(A) by Th15; then ( p '&' r ) => 'not' ( q => 'not' r ) in TAUT(A) by A2,LUKASI_1:3; hence thesis by A3,LUKASI_1:3; end; theorem r => p in TAUT(A) & r => q in TAUT(A) implies r => ( p '&' q ) in TAUT(A) proof assume that A1: r => p in TAUT(A) and A2: r => q in TAUT(A); ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in TAUT(A) by Th33; then ( r => q ) => ( r => ( p '&' q )) in TAUT(A) by A1,CQC_THE1:46; hence thesis by A2,CQC_THE1:46; end; theorem p => r in TAUT(A) & q => r in TAUT(A) implies ( p 'or' q ) => r in TAUT(A) proof assume p => r in TAUT(A) & q => r in TAUT(A); then A1: ( p => r ) '&' ( q => r ) in TAUT(A) by Lm4; (( p => r ) '&' ( q => r )) => (( p 'or' q ) => r) in TAUT(A) by Th36; hence thesis by A1,CQC_THE1:46; end; theorem ( p 'or' q ) in TAUT(A) & 'not' p in TAUT(A) implies q in TAUT(A) proof assume that A1: ( p 'or' q ) in TAUT(A) and A2: 'not' p in TAUT(A); ( p 'or' q ) => ( 'not' p => q ) in TAUT(A) by Th5; then 'not' p => q in TAUT(A) by A1,CQC_THE1:46; hence thesis by A2,CQC_THE1:46; end; theorem ( p 'or' q ) in TAUT(A) & 'not' q in TAUT(A) implies p in TAUT(A) proof assume that A1: ( p 'or' q ) in TAUT(A) and A2: 'not' q in TAUT(A); ( q 'or' p ) => ( 'not' q => p ) in TAUT(A) & ( p 'or' q ) => ( q 'or' p ) in TAUT(A) by Th5,Th8; then ( p 'or' q ) => ( 'not' q => p ) in TAUT(A) by LUKASI_1:3; then 'not' q => p in TAUT(A) by A1,CQC_THE1:46; hence thesis by A2,CQC_THE1:46; end; theorem p => q in TAUT(A) & r => s in TAUT(A) implies ( p '&' r ) => ( q '&' s ) in TAUT(A) proof assume p => q in TAUT(A) & r => s in TAUT(A); then ( p '&' r ) => ( q '&' r ) in TAUT(A) & ( q '&' r ) => ( q '&' s ) in TAUT(A) by Lm5,Th51; hence thesis by LUKASI_1:3; end; theorem p => q in TAUT(A) & r => s in TAUT(A) implies ( p 'or' r ) => ( q 'or' s ) in TAUT(A) proof assume p => q in TAUT(A) & r => s in TAUT(A); then ( p 'or' r ) => ( q 'or' r ) in TAUT(A) & ( q 'or' r ) => ( q 'or' s ) in TAUT(A) by Lm6,Lm7; hence thesis by LUKASI_1:3; end; theorem ( p '&' 'not' q ) => 'not' p in TAUT(A) implies p => q in TAUT(A) proof A1: 'not' ( p '&' 'not' q ) = ( p => q ) by QC_LANG2:def 2; assume ( p '&' 'not' q ) => 'not' p in TAUT(A); then A2: 'not' 'not' p => 'not' ( p '&' 'not' q ) in TAUT(A) by LUKASI_1:34; p => 'not' 'not' p in TAUT(A) by LUKASI_1:27; then p => 'not' ( p '&' 'not' q ) in TAUT(A) by A2,LUKASI_1:3; hence thesis by A1,LUKASI_1:18; end;