:: Calculus of Propositions
:: by Jan Popio{\l}ek and Andrzej Trybulec
::
:: Received October 23, 1990
:: Copyright (c) 1990-2026 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;