:: Propositional Calculus :: by Grzegorz Bancerek, Agata Darmochwa\l and Andrzej Trybulec :: :: Received September 26, 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; definitions CQC_THE1; expansions CQC_THE1; theorems CQC_THE1, QC_LANG2; begin reserve A for QC-alphabet; reserve p, q, r, s, t for Element of CQC-WFF(A); reserve X for Subset of CQC-WFF(A); theorem Th1: (p => q) => ((q => r) => (p => r)) in TAUT(A) proof (p => q) => ('not'(q '&' 'not' r) => 'not'(p '&' 'not' r)) in TAUT(A) by CQC_THE1:44; then (p => q) => ((q => r) => 'not'(p '&' 'not' r)) in TAUT(A) by QC_LANG2:def 2; hence thesis by QC_LANG2:def 2; end; theorem Th2: p => q in TAUT(A) implies (q => r) => (p => r) in TAUT(A) proof assume A1: p => q in TAUT(A); (p => q) => ((q => r) => (p => r)) in TAUT(A) by Th1; hence thesis by A1,CQC_THE1:46; end; theorem Th3: p => q in TAUT(A) & q => r in TAUT(A) implies p => r in TAUT(A) proof assume that A1: p => q in TAUT(A) and A2: q => r in TAUT(A); (p => q) => ((q => r) => (p => r)) in TAUT(A) by Th1; then (q => r) => (p => r) in TAUT(A) by A1,CQC_THE1:46; hence thesis by A2,CQC_THE1:46; end; theorem Th4: :: Identity law p => p in TAUT(A) proof ('not' p => p) => p in TAUT(A) & p => ('not' p => p) in TAUT(A) by CQC_THE1:42,43; hence thesis by Th3; end; Lm1: (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT(A) proof (p => q) => ((q => r) => (p => r)) in TAUT(A) by Th1; hence thesis by Th2; end; Lm2: (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT(A) proof ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) ) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in TAUT(A)& (((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in TAUT(A) by Lm1; hence thesis by CQC_THE1:46; end; Lm3: (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT(A) proof ((q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s)) in TAUT(A) & ((( q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s))) => ((p => q) => ( ((p => r) => s) => ((q => r) => s))) in TAUT(A) by Lm1,Th1; hence thesis by CQC_THE1:46; end; Lm4: (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT(A) proof ((p => q) => (((p => r) => s) => ((q => r) => s))) in TAUT(A) & ((p => q) => (( (p => r) => s) => ((q => r) => s))) => ((t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s)))) in TAUT(A) by Lm2,Lm3; hence thesis by CQC_THE1:46; end; Lm5: (('not' p => q) => r) => (p => r) in TAUT(A) proof p => ('not' p => q) in TAUT(A) by CQC_THE1:43; hence thesis by Th2; end; Lm6: p => ((('not' p => r) => s) => ((q => r) => s)) in TAUT(A) proof ('not' p => q) => ((('not' p => r) => s) => ((q => r) => s)) in TAUT(A) & ( (( 'not' p => q) => ((('not' p => r) => s) => ((q => r) => s)) ) => (p => ((( 'not' p => r) => s) => ((q => r) => s)))) in TAUT(A) by Lm3,Lm5; hence thesis by CQC_THE1:46; end; Lm7: (q => (('not' p => p) => p)) => (('not' p => p) => p) in TAUT(A) proof ('not' p => p) => p in TAUT(A) & (('not' p => p) => p) => ((('not'(('not' p => p) => p) => (('not' p => p) => p)) => (('not' p => p) => p)) => ((q => (( 'not' p => p) => p)) => (('not' p => p) => p))) in TAUT(A) by Lm6,CQC_THE1:42; then ('not'(('not' p => p) => p) => (('not' p => p) => p)) => (('not' p => p) => p ) in TAUT(A) & (('not'(('not' p => p) => p) => (('not' p => p) => p)) => (( 'not' p => p) => p)) => ((q => (('not' p => p) => p)) => (('not' p => p) => p)) in TAUT(A) by CQC_THE1:42,46; hence thesis by CQC_THE1:46; end; Lm8: t => (('not' p => p) => p) in TAUT(A) proof ('not' t => (('not' p => p) => p)) => (('not' p => p) => p) in TAUT(A) & (( 'not' t => (('not' p => p) => p)) => (('not' p => p) => p)) => (t => ( ('not' p => p) => p)) in TAUT(A) by Lm5,Lm7; hence thesis by CQC_THE1:46; end; Lm9: ('not' p => q) => (t => ((q => p) => p)) in TAUT(A) proof t => (('not' p => p) => p) in TAUT(A) & (t => (('not' p => p) => p)) => (( 'not' p => q) => (t => ((q => p) => p) )) in TAUT(A) by Lm4,Lm8; hence thesis by CQC_THE1:46; end; Lm10: ((t => ((q => p) => p)) => r) => (('not' p => q) => r) in TAUT(A) proof ('not' p => q) => (t => ((q => p) => p)) in TAUT(A) & (('not' p => q) => (t => ((q => p) => p))) => (((t => ((q => p) => p)) => r) => (('not' p => q) => r) ) in TAUT(A) by Lm9,Th1; hence thesis by CQC_THE1:46; end; Lm11: ('not' p => q) => ((q => p) => p) in TAUT(A) proof ('not'((q => p) => p) => ((q => p) => p)) => ((q => p) => p) in TAUT(A) & ( ( 'not'((q => p) => p) => ((q => p) => p)) => ((q => p) => p)) => (( 'not' p => q ) => ((q => p) => p)) in TAUT(A) by Lm10,CQC_THE1:42; hence thesis by CQC_THE1:46; end; Lm12: p => ((q => p) => p) in TAUT(A) proof ('not' p => q) => ((q => p) => p) in TAUT(A) & (('not' p => q) => ((q => p) => p)) => (p => ((q => p) => p)) in TAUT(A) by Lm5,Lm11; hence thesis by CQC_THE1:46; end; theorem Th5: q => (p => q) in TAUT(A) proof q => (('not' p => q) => q) in TAUT(A) & (q => (('not' p => q) => q)) => ((p => ('not' p => q)) => (q => (p => q))) in TAUT(A) by Lm2,Lm12; then p => ('not' p => q) in TAUT(A) & (p => ('not' p => q)) => (q => (p => q)) in TAUT(A) by CQC_THE1:43,46; hence thesis by CQC_THE1:46; end; theorem Th6: ((p => q) => r) => (q => r) in TAUT(A) proof q => (p => q) in TAUT(A) & (q => (p => q)) => (((p => q) => r) => (q => r)) in TAUT(A) by Th1,Th5; hence thesis by CQC_THE1:46; end; theorem Th7: q => ((q => p) => p) in TAUT(A) proof ('not' p => q) => ((q => p) => p) in TAUT(A) & (('not' p => q) => ((q => p) => p)) => (q => ((q => p) => p)) in TAUT(A) by Lm11,Th6; hence thesis by CQC_THE1:46; end; theorem Th8: (s => (q => p)) => (q => (s => p)) in TAUT(A) proof q => ((q => p) => p) in TAUT(A) & (q => ((q => p) => p)) => ((s => (q => p) ) => (q => (s => p))) in TAUT(A) by Lm2,Th7; hence thesis by CQC_THE1:46; end; theorem Th9: (q => r) => ((p => q) => (p => r)) in TAUT(A) proof (p => q) => ((q => r) => (p => r)) in TAUT(A) & ((p => q) => ((q => r) => ( p => r))) => ((q => r) => ((p => q) => (p => r))) in TAUT(A) by Th1,Th8; hence thesis by CQC_THE1:46; end; Lm13: ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT(A) proof (s => (q => p)) => (q => (s => p)) in TAUT(A) & ((s => (q => p)) => (q => ( s => p))) => (((q => (s => p)) => r) => ((s => (q => p)) => r)) in TAUT(A) by Th1,Th8; hence thesis by CQC_THE1:46; end; Lm14: ((p => q) => p) => p in TAUT(A) proof ('not' p => (p => q)) => (((p => q) => p) => p) in TAUT(A) & (('not' p => ( p => q)) => (((p => q) => p) => p)) => ((p => ('not' p => q)) => (((p => q) => p) => p)) in TAUT(A) by Lm11,Lm13; then p => ('not' p => q) in TAUT(A) & (p => ('not' p => q)) => (((p => q) => p) => p ) in TAUT(A) by CQC_THE1:43,46; hence thesis by CQC_THE1:46; end; Lm15: ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT(A) proof (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT(A) & ((p => q) => (((p => r) => s) => ((q => r) => s))) => (((p => r) => s) => ((p => q) => ((q => r) => s))) in TAUT(A) by Lm3,Th8; hence thesis by CQC_THE1:46; end; Lm16: ((p => q) => r) => ((r => p) => p) in TAUT(A) proof ((p => q) => p) => p in TAUT(A) & (((p => q) => p) => p) => (((p => q) => r ) => ((r => p) => p)) in TAUT(A) by Lm14,Lm15; hence thesis by CQC_THE1:46; end; Lm17: (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT(A) proof ((p => q) => r) => ((r => p) => p) in TAUT(A) & (((p => q) => r) => ((r => p) => p)) => ((((r => p) => p) => s) => (((p => q) => r) => s)) in TAUT(A) by Lm16,Th1; hence thesis by CQC_THE1:46; end; Lm18: ((q => r) => p) => ((q => p) => p) in TAUT(A) proof ((p => q) => q) => ((q => p) => p) in TAUT(A) & (((p => q) => q) => ((q => p) => p)) => (((q => r) => p) => ((q => p) => p)) in TAUT(A) by Lm16,Lm17; hence thesis by CQC_THE1:46; end; theorem Th10: (q => (q => r)) => (q => r) in TAUT(A) proof (q => r) => (q => r) in TAUT(A) & ((q => r) => (q => r)) => ((q => (q => r) ) => (q => r)) in TAUT(A) by Lm18,Th4; hence thesis by CQC_THE1:46; end; Lm19: (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT(A) proof ((q => r) => p) => ((q => p) => p) in TAUT(A) & (((q => r) => p) => ((q => p) => p)) => ((q => s) => (((q => r) => p) => ((s => p) => p))) in TAUT(A) by Lm4,Lm18; hence thesis by CQC_THE1:46; end; Lm20: ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT(A) proof (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT(A) & ((q => s) => (((q => r) => p) => ((s => p) => p))) => (((q => r) => p) => ((q => s) => ((s => p) => p))) in TAUT(A) by Lm19,Th8; hence thesis by CQC_THE1:46; end; Lm21: (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT(A) proof (q => r) => (p => (q => r)) in TAUT(A) & ((q => r) => (p => (q => r))) => ( (q => s) => ((s => (p => (q => r))) => (p => (q => r)))) in TAUT(A) by Lm20,Th5; hence thesis by CQC_THE1:46; end; Lm22: (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT(A) proof (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT(A) & ((q => s) => ((s => (p => (q => r))) => (p => (q => r)))) => ((s => (p => (q => r))) => ( (q => s) => (p => (q => r)))) in TAUT(A) by Lm21,Th8; hence thesis by CQC_THE1:46; end; theorem Th11: (p => (q => r)) => ((p => q) => (p => r)) in TAUT(A) proof (q => r) => ((p => q) => (p => r)) in TAUT(A) & ((q => r) => ((p => q) => ( p => r))) => ((p => (q => r)) => ((p => q) => (p => r))) in TAUT(A) by Lm22,Th9; hence thesis by CQC_THE1:46; end; theorem Th12: 'not' VERUM(A) => p in TAUT(A) proof VERUM(A) => ('not' VERUM(A) => p) in TAUT(A) by CQC_THE1:43; hence thesis by CQC_THE1:41,46; end; theorem Th13: q in TAUT(A) implies p => q in TAUT(A) proof q => (p => q) in TAUT(A) by Th5; hence thesis by CQC_THE1:46; end; theorem p in TAUT(A) implies (p => q) => q in TAUT(A) proof assume A1: p in TAUT(A); p => ((p => q) => q) in TAUT(A) by Th7; hence thesis by A1,CQC_THE1:46; end; theorem Th15: s => (q => p) in TAUT(A) implies q => (s => p) in TAUT(A) proof assume A1: s => (q => p) in TAUT(A); (s => (q => p)) => (q => (s => p)) in TAUT(A) by Th8; hence thesis by A1,CQC_THE1:46; end; theorem Th16: s => (q => p) in TAUT(A) & q in TAUT(A) implies s => p in TAUT(A) proof assume s => (q => p) in TAUT(A); then q => (s => p) in TAUT(A) by Th15; hence thesis by CQC_THE1:46; end; theorem s => (q => p) in TAUT(A) & q in TAUT(A) & s in TAUT(A) implies p in TAUT(A) proof assume s => (q => p) in TAUT(A) & q in TAUT(A); then s => p in TAUT(A) by Th16; hence thesis by CQC_THE1:46; end; theorem q => (q => r) in TAUT(A) implies q => r in TAUT(A) proof (q => (q => r)) => (q => r) in TAUT(A) by Th10; hence thesis by CQC_THE1:46; end; theorem Th19: (p => (q => r)) in TAUT(A) implies (p => q) => (p => r) in TAUT(A) proof assume A1: p => (q => r) in TAUT(A); (p => (q => r)) => ((p => q) => (p => r)) in TAUT(A) by Th11; hence thesis by A1,CQC_THE1:46; end; theorem Th20: (p => (q => r)) in TAUT(A) & p => q in TAUT(A) implies p => r in TAUT(A) proof assume (p => (q => r)) in TAUT(A); then (p => q) => (p => r) in TAUT(A) by Th19; hence thesis by CQC_THE1:46; end; theorem (p => (q => r)) in TAUT(A) & p => q in TAUT(A) & p in TAUT(A) implies r in TAUT(A) proof assume (p => (q => r)) in TAUT(A) & p => q in TAUT(A); then p => r in TAUT(A) by Th20; hence thesis by CQC_THE1:46; end; theorem Th22: p => (q => r) in TAUT(A) & p => (r => s ) in TAUT(A) implies p => (q => s) in TAUT(A) proof assume that A1: p => (q => r) in TAUT(A) and A2: p => (r => s ) in TAUT(A); p => ((q => r) => ((r => s) => (q => s))) in TAUT(A) by Th1,Th13; then p => ((r => s) => (q => s)) in TAUT(A) by A1,Th20; hence thesis by A2,Th20; end; theorem p => VERUM(A) in TAUT(A) by Th13,CQC_THE1:41; Lm23: 'not' p => (p => 'not' VERUM(A)) in TAUT(A) proof p => ('not' p => 'not' VERUM(A)) in TAUT(A) by CQC_THE1:43; hence thesis by Th15; end; Lm24: ('not' p => 'not' VERUM(A)) => p in TAUT(A) proof 'not' p => ('not' VERUM(A) => p) in TAUT(A) & ('not' p => ('not' VERUM(A) => p)) => ( ('not' p => 'not' VERUM(A)) => ('not' p => p)) in TAUT(A) by Th11,Th12,Th13; then A1: ('not' p => 'not' VERUM(A)) => ('not' p => p) in TAUT(A) by CQC_THE1:46; ('not' p => p) => p in TAUT(A) by CQC_THE1:42; hence thesis by A1,Th3; end; theorem Th24: ('not' p => 'not' q) => (q => p) in TAUT(A) proof q => ('not' q => 'not' VERUM(A)) in TAUT(A) & ('not' q => 'not' VERUM(A)) => (( 'not' p => 'not' q) => ('not' p => 'not' VERUM(A))) in TAUT(A) by Th9,CQC_THE1:43; then A1: q => (('not' p => 'not' q) => ('not' p => 'not' VERUM(A))) in TAUT(A) by Th3; q => (('not' p => 'not' VERUM(A)) => p) in TAUT(A) by Lm24,Th13; then q => (('not' p => 'not' q) => p) in TAUT(A) by A1,Th22; hence thesis by Th15; end; theorem Th25: 'not' 'not' p => p in TAUT(A) proof 'not' 'not' p => ('not' p => 'not' VERUM(A)) in TAUT(A) & ('not' p => 'not' VERUM(A)) => (VERUM(A) => p) in TAUT(A) by Lm23,Th24; then 'not' 'not' p => (VERUM(A) => p) in TAUT(A) by Th3; then VERUM(A) => ('not' 'not' p => p) in TAUT(A) by Th15; hence thesis by CQC_THE1:41,46; end; Lm25: now let A,p; 'not' 'not' p => p in TAUT(A) by Th25; then A1: (p => 'not' VERUM(A)) => ('not' 'not' p => 'not' VERUM(A)) in TAUT(A) by Th2; ('not' 'not' p => 'not' VERUM(A)) => 'not' p in TAUT(A) by Lm24; hence (p => 'not' VERUM(A)) => 'not' p in TAUT(A) by A1,Th3; end; theorem Th26: (p => q) => ('not' q => 'not' p) in TAUT(A) proof 'not' q => (q => 'not' VERUM(A)) in TAUT(A) & (q => 'not' VERUM(A)) => ((p => q) => ( p => 'not' VERUM(A))) in TAUT(A) by Lm23,Th9; then A1: 'not' q => ((p => q) => (p => 'not' VERUM(A))) in TAUT(A) by Th3; 'not' q => ((p => 'not' VERUM(A)) => 'not' p) in TAUT(A) by Lm25,Th13; then 'not' q => ((p => q) => 'not' p) in TAUT(A) by A1,Th22; hence thesis by Th15; end; theorem Th27: p => 'not' 'not' p in TAUT(A) proof (VERUM(A) => p) => ('not' p => 'not' VERUM(A)) in TAUT(A) & ('not' p => 'not' VERUM(A)) => 'not' 'not' p in TAUT(A) by Lm25,Th26; then A1: (VERUM(A) => p) => 'not' 'not' p in TAUT(A) by Th3; p => (VERUM(A) => p) in TAUT(A) by Th5; hence thesis by A1,Th3; end; theorem Th28: ('not' 'not' p => q) => (p => q) in TAUT(A) & (p => q) => ('not' 'not' p => q) in TAUT(A) proof p => 'not' 'not' p in TAUT(A) by Th27; hence ('not' 'not' p => q) => (p => q) in TAUT(A) by Th2; 'not' 'not' p => p in TAUT(A) by Th25; hence thesis by Th2; end; theorem Th29: (p => 'not' 'not' q) => (p => q) in TAUT(A) & (p => q) => (p => 'not' 'not' q) in TAUT(A) proof (p => ('not' 'not' q => q)) => ((p => 'not' 'not' q) => (p => q)) in TAUT(A) & p => ('not' 'not' q => q) in TAUT(A) by Th11,Th13,Th25; hence (p => 'not' 'not' q) => (p => q) in TAUT(A) by CQC_THE1:46; (p => (q => 'not' 'not' q)) => ((p => q) => (p => 'not' 'not' q)) in TAUT(A) & p => (q => 'not' 'not' q) in TAUT(A) by Th11,Th13,Th27; hence thesis by CQC_THE1:46; end; theorem Th30: (p => 'not' q) => (q => 'not' p) in TAUT(A) proof (p => 'not' q) => ('not' 'not' q => 'not' p) in TAUT(A) & ('not' 'not' q => 'not' p) => (q => 'not' p) in TAUT(A) by Th26,Th28; hence thesis by Th3; end; theorem Th31: ('not' p => q) => ('not' q => p) in TAUT(A) proof ('not' p => q) => ('not' q => 'not' 'not' p) in TAUT(A) & ('not' q => 'not' 'not' p) => ('not' q => p) in TAUT(A) by Th26,Th29; hence thesis by Th3; end; theorem (p => 'not' p) => 'not' p in TAUT(A) proof ('not' 'not' p => 'not' p) => 'not' p in TAUT(A) & (p => 'not' p) => ('not' 'not' p => 'not' p) in TAUT(A) by Th28,CQC_THE1:42; hence thesis by Th3; end; theorem 'not' p => (p => q) in TAUT(A) proof 'not' p => ('not' 'not' p => q) in TAUT(A) & ('not' 'not' p => q) => (p => q) in TAUT(A) by Th28,CQC_THE1:43; hence thesis by Th3; end; theorem Th34: p => q in TAUT(A) iff 'not' q => 'not' p in TAUT(A) proof (p => q) => ('not' q => 'not' p) in TAUT(A) by Th26; hence p => q in TAUT(A) implies 'not' q => 'not' p in TAUT(A) by CQC_THE1:46; ('not' q => 'not' p) => (p => q) in TAUT(A) by Th24; hence 'not' q => 'not' p in TAUT(A) implies p => q in TAUT(A) by CQC_THE1:46; end; theorem 'not' p => 'not' q in TAUT(A) implies q => p in TAUT(A) by Th34; theorem p in TAUT(A) iff 'not' 'not' p in TAUT(A) proof thus p in TAUT(A) implies 'not' 'not' p in TAUT(A) proof assume A1: p in TAUT(A); p => 'not' 'not' p in TAUT(A) by Th27; hence thesis by A1,CQC_THE1:46; end; assume A2: 'not' 'not' p in TAUT(A); 'not' 'not' p => p in TAUT(A) by Th25; hence thesis by A2,CQC_THE1:46; end; theorem (p => q) in TAUT(A) iff (p => 'not' 'not' q) in TAUT(A) proof thus (p => q) in TAUT(A) implies (p => 'not' 'not' q) in TAUT(A) proof assume A1: p => q in TAUT(A); (p => q) => (p => 'not' 'not' q) in TAUT(A) by Th29; hence thesis by A1,CQC_THE1:46; end; assume A2: p => 'not' 'not' q in TAUT(A); (p => 'not' 'not' q) => (p => q) in TAUT(A) by Th29; hence thesis by A2,CQC_THE1:46; end; theorem (p => q) in TAUT(A) iff ('not' 'not' p => q) in TAUT(A) proof thus (p => q) in TAUT(A) implies ('not' 'not' p => q) in TAUT(A) proof assume A1: p => q in TAUT(A); (p => q) => ('not' 'not' p => q) in TAUT(A) by Th28; hence thesis by A1,CQC_THE1:46; end; assume A2: 'not' 'not' p => q in TAUT(A); ('not' 'not' p => q) => (p => q) in TAUT(A) by Th28; hence thesis by A2,CQC_THE1:46; end; theorem p => 'not' q in TAUT(A) implies q => 'not' p in TAUT(A) proof assume A1: p => 'not' q in TAUT(A); (p => 'not' q) => (q => 'not' p) in TAUT(A) by Th30; hence thesis by A1,CQC_THE1:46; end; theorem 'not' p => q in TAUT(A) implies 'not' q => p in TAUT(A) proof assume A1: 'not' p => q in TAUT(A); ('not' p => q) => ('not' q => p) in TAUT(A) by Th31; hence thesis by A1,CQC_THE1:46; end; :: predykat |- i schematy konsekwencji registration let A,p,q,r; cluster (p => q) => ((q => r) => (p => r)) -> valid; coherence by Th1; end; theorem p => q is valid implies (q => r) => (p => r) is valid proof assume A1: p => q is valid; (p => q) => ((q => r) => (p => r)) is valid; hence thesis by A1,CQC_THE1:65; end; theorem Th42: p => q is valid & q => r is valid implies p => r is valid by Th3; registration let A,p; cluster p => p -> valid; coherence by Th4; end; registration let A,p,q; cluster p => (q => p) -> valid; coherence by Th5; end; theorem p is valid implies q => p is valid by Th13; registration let A,p,q,s; cluster (s => (q => p)) => (q => (s => p)) -> valid; coherence by Th8; end; theorem Th44: p => (q => r) is valid implies q => (p => r) is valid by Th15; theorem p => (q => r) is valid & q is valid implies p => r is valid proof assume p => (q => r) is valid; then q => (p => r) is valid by Th44; hence thesis by CQC_THE1:65; end; theorem p => VERUM(A) is valid & 'not' VERUM(A) => p is valid by Th13,CQC_THE1:41,Th12; registration let A,p,q; cluster p => ((p => q) => q) -> valid; coherence by Th7; end; registration let A,q,r; cluster (q => (q => r)) => (q => r) -> valid; coherence by Th10; end; theorem q => (q => r) is valid implies q => r is valid proof assume A1: q => (q => r) is valid; (q => (q => r)) => (q => r) is valid; hence thesis by A1,CQC_THE1:65; end; registration let A,p,q,r; cluster (p => (q => r)) => ((p => q) => (p => r)) -> valid; coherence by Th11; end; theorem Th48: p => (q => r) is valid implies (p => q) => (p => r) is valid proof assume A1: p => (q => r) is valid; (p => (q => r)) => ((p => q) => (p => r)) is valid; hence thesis by A1,CQC_THE1:65; end; theorem p => (q => r) is valid & p => q is valid implies p => r is valid proof assume that A1: p => (q => r) is valid and A2: p => q is valid; (p => q) => (p => r) is valid by A1,Th48; hence thesis by A2,CQC_THE1:65; end; registration let A,p,q,r; cluster ((p => q) => r) => (q => r) -> valid; coherence by Th6; end; theorem (p => q) => r is valid implies q => r is valid proof assume A1: (p => q) => r is valid; ((p => q) => r) => (q => r) is valid; hence thesis by A1,CQC_THE1:65; end; registration let A,p,q,r; cluster (p => q) => ((r => p) => (r => q)) -> valid; coherence by Th9; end; theorem p => q is valid implies (r => p) => (r => q) is valid proof assume A1: p => q is valid; (p => q) => ((r => p) => (r => q)) is valid; hence thesis by A1,CQC_THE1:65; end; registration let A,p,q; cluster (p => q) => ('not' q => 'not' p) -> valid; coherence by Th26; end; registration let A,p,q; cluster ('not' p => 'not' q) => (q => p) -> valid; coherence by Th24; end; theorem 'not' p => 'not' q is valid iff q => p is valid proof thus 'not' p => 'not' q is valid implies q => p is valid proof assume A1: 'not' p => 'not' q is valid; ('not' p => 'not' q) => (q => p) is valid; hence thesis by A1,CQC_THE1:65; end; assume A2: q => p is valid; (q => p) => ('not' p => 'not' q) is valid; hence thesis by A2,CQC_THE1:65; end; registration let A,p; cluster p => 'not' 'not' p -> valid; coherence by Th27; end; registration let A,p; cluster 'not' 'not' p => p -> valid; coherence by Th25; end; theorem 'not' 'not' p is valid iff p is valid proof thus 'not' 'not' p is valid implies p is valid proof assume A1: 'not' 'not' p is valid; 'not' 'not' p => p is valid; hence thesis by A1,CQC_THE1:65; end; assume A2: p is valid; p => 'not' 'not' p is valid; hence thesis by A2,CQC_THE1:65; end; registration let A,p,q; cluster ('not' 'not' p => q) => (p => q) -> valid; coherence by Th28; end; theorem 'not' 'not' p => q is valid iff p => q is valid proof thus 'not' 'not' p => q is valid implies p => q is valid proof assume A1: 'not' 'not' p => q is valid; ('not' 'not' p => q) => (p => q) is valid; hence thesis by A1,CQC_THE1:65; end; assume A2: p => q is valid; 'not' 'not' p => p is valid; hence thesis by A2,Th42; end; registration let A,p,q; cluster (p => 'not' 'not' q) => (p => q) -> valid; coherence by Th29; end; theorem p => 'not' 'not' q is valid iff p => q is valid proof thus p => 'not' 'not' q is valid implies p => q is valid proof assume A1: p => 'not' 'not' q is valid; (p => 'not' 'not' q) => (p => q) is valid; hence thesis by A1,CQC_THE1:65; end; assume A2: p => q is valid; q => 'not' 'not' q is valid; hence thesis by A2,Th42; end; registration let A,p,q; cluster (p => 'not' q) => (q => 'not' p) -> valid; coherence by Th30; end; theorem p => 'not' q is valid implies q => 'not' p is valid proof assume A1: p => 'not' q is valid; (p => 'not' q) => (q => 'not' p) is valid; hence thesis by A1,CQC_THE1:65; end; registration let A,p,q; cluster ('not' p => q) => ('not' q => p) -> valid; coherence by Th31; end; theorem 'not' p => q is valid implies 'not' q => p is valid proof assume A1: 'not' p => q is valid; ('not' p => q) => ('not' q => p) is valid; hence thesis by A1,CQC_THE1:65; end; theorem X|- p => q implies X|- (q => r) => (p => r) proof assume A1: X|- p => q; X|- (p => q) => ((q => r) => (p => r)) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem Th59: X|- p => q & X|- q => r implies X|- p => r proof assume that A1: X|- p => q and A2: X|- q => r; X|- (p => q) => ((q => r) => (p => r)) by CQC_THE1:59; then X|- (q => r) => (p => r) by A1,CQC_THE1:55; hence thesis by A2,CQC_THE1:55; end; theorem X|- p => p by CQC_THE1:59; theorem X|- p implies X|- q => p proof assume A1: X|- p; X|- p => (q => p) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem X |- p implies X |- (p => q) => q proof assume A1: X |- p; X |- p => ((p => q) => q) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem Th63: X |- p => (q => r) implies X |- q => (p => r) proof assume A1: X |- p => (q => r); X|- (p => (q => r)) => (q => (p => r)) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem X |- p => (q => r) & X |- q implies X |- p => r proof assume X |- p => (q => r); then X |- q => (p => r) by Th63; hence thesis by CQC_THE1:55; end; theorem X |- p => (p => q) implies X |- p => q proof assume A1: X |- p => (p => q); X|- (p => (p => q)) => (p => q) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem X |- (p => q) => r implies X |- q => r proof assume A1: X |- (p => q) => r; X|- ((p => q) => r) => (q => r) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem Th67: X |- p => (q => r) implies X |- (p => q) => (p =>r) proof assume A1: X|- p => (q => r); X |- (p => (q => r)) => ((p => q) => (p =>r)) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem X |- p => (q => r) & X|- p => q implies X |- p => r proof assume X|- p => (q => r); then X |- (p => q) => (p =>r) by Th67; hence thesis by CQC_THE1:55; end; theorem X|- 'not' p => 'not' q iff X|- q => p proof thus X|- 'not' p => 'not' q implies X|- q => p proof assume A1: X|- 'not' p => 'not' q; X|- ('not' p => 'not' q) => (q => p) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; assume A2: X|- q => p; X|- (q => p) => ('not' p => 'not' q) by CQC_THE1:59; hence thesis by A2,CQC_THE1:55; end; theorem X|- 'not' 'not' p iff X|- p proof thus X|- 'not' 'not' p implies X|- p proof assume A1: X|- 'not' 'not' p; X|- 'not' 'not' p => p by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; assume A2: X|- p; X|- p => 'not' 'not' p by CQC_THE1:59; hence thesis by A2,CQC_THE1:55; end; theorem X|- p => 'not' 'not' q iff X|- p => q proof thus X|- p => 'not' 'not' q implies X|- p => q proof assume A1: X|- p => 'not' 'not' q; X|- (p => 'not' 'not' q) => (p => q) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; assume A2: X|- p => q; X|- q => 'not' 'not' q by CQC_THE1:59; hence thesis by A2,Th59; end; theorem X|- 'not' 'not' p => q iff X|- p => q proof thus X|- 'not' 'not' p => q implies X|- p => q proof assume A1: X|- 'not' 'not' p => q; X|- ('not' 'not' p => q) => (p => q) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; assume A2: X|- p => q; X|- 'not' 'not' p => p by CQC_THE1:59; hence thesis by A2,Th59; end; theorem Th73: X|- p => 'not' q implies X|- q => 'not' p proof assume A1: X|- p => 'not' q; X|- (p => 'not' q) => (q => 'not' p) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem Th74: X|- 'not' p => q implies X|- 'not' q => p proof assume A1: X|- 'not' p => q; X|- ('not' p => q) => ('not' q => p) by CQC_THE1:59; hence thesis by A1,CQC_THE1:55; end; theorem X|- p => 'not' q & X |- q implies X|- 'not' p proof assume X|- p => 'not' q; then X |- q => 'not' p by Th73; hence thesis by CQC_THE1:55; end; theorem X|- 'not' p => q & X |- 'not' q implies X|- p proof assume X|- 'not' p => q; then X |- 'not' q => p by Th74; hence thesis by CQC_THE1:55; end;