:: Calculus of Propositions :: by Jan Popio{\l}ek and Andrzej Trybulec :: :: Received October 23, 1990 :: Copyright (c) 1990-2021 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; begin :: Tautologies reserve A for QC-alphabet; reserve p, q, r, s for Element of CQC-WFF(A); theorem :: PROCAL_1:1 'not' ( p '&' 'not' p ) in TAUT(A); theorem :: PROCAL_1:2 p 'or' 'not' p in TAUT(A); theorem :: PROCAL_1:3 p => ( p 'or' q ) in TAUT(A); theorem :: PROCAL_1:4 q => ( p 'or' q ) in TAUT(A); theorem :: PROCAL_1:5 ( p 'or' q ) => ( 'not' p => q ) in TAUT(A); theorem :: PROCAL_1:6 'not' ( p 'or' q ) => ( 'not' p '&' 'not' q ) in TAUT(A); theorem :: PROCAL_1:7 ( 'not' p '&' 'not' q ) => 'not' ( p 'or' q ) in TAUT(A); theorem :: PROCAL_1:8 ( p 'or' q ) => ( q 'or' p ) in TAUT(A); theorem :: PROCAL_1:9 'not' p 'or' p in TAUT(A); theorem :: PROCAL_1:10 'not' ( p 'or' q ) => 'not' p in TAUT(A); theorem :: PROCAL_1:11 ( p 'or' p ) => p in TAUT(A); theorem :: PROCAL_1:12 p => ( p 'or' p ) in TAUT(A); theorem :: PROCAL_1:13 ( p '&' 'not' p ) => q in TAUT(A); theorem :: PROCAL_1:14 ( p => q ) => ( 'not' p 'or' q ) in TAUT(A); theorem :: PROCAL_1:15 ( p '&' q ) => 'not' ( p => 'not' q ) in TAUT(A); theorem :: PROCAL_1:16 'not' ( p => 'not' q ) => ( p '&' q ) in TAUT(A); theorem :: PROCAL_1:17 'not' ( p '&' q ) => ( 'not' p 'or' 'not' q ) in TAUT(A); theorem :: PROCAL_1:18 ( 'not' p 'or' 'not' q ) => 'not' ( p '&' q ) in TAUT(A); theorem :: PROCAL_1:19 ( p '&' q ) => p in TAUT(A); theorem :: PROCAL_1:20 ( p '&' q ) => ( p 'or' q ) in TAUT(A); theorem :: PROCAL_1:21 ( p '&' q ) => q in TAUT(A); theorem :: PROCAL_1:22 p => p '&' p in TAUT(A); theorem :: PROCAL_1:23 ( p <=> q ) => ( p => q ) in TAUT(A); theorem :: PROCAL_1:24 ( p <=> q ) => ( q => p ) in TAUT(A); theorem :: PROCAL_1:25 (( p 'or' q ) 'or' r ) => ( p 'or' ( q 'or' r )) in TAUT(A); theorem :: PROCAL_1:26 (( p '&' q ) '&' r ) => ( p '&' ( q '&' r )) in TAUT(A); theorem :: PROCAL_1:27 ( p 'or' ( q 'or' r )) => (( p 'or' q ) 'or' r ) in TAUT(A); theorem :: PROCAL_1:28 p => ( q => ( p '&' q )) in TAUT(A); theorem :: PROCAL_1:29 ( p => q ) => (( q => p ) => ( p <=> q )) in TAUT(A); theorem :: PROCAL_1:30 ( p 'or' q ) <=> ( q 'or' p ) in TAUT(A); theorem :: PROCAL_1:31 (( p '&' q ) => r ) => ( p => ( q => r )) in TAUT(A); theorem :: PROCAL_1:32 ( p => ( q => r )) => (( p '&' q ) => r ) in TAUT(A); theorem :: PROCAL_1:33 ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in TAUT(A); theorem :: PROCAL_1:34 (( p 'or' q ) => r ) => (( p => r ) 'or' ( q => r )) in TAUT(A); theorem :: PROCAL_1:35 ( p => r ) => (( q => r ) => (( p 'or' q ) => r)) in TAUT(A); theorem :: PROCAL_1:36 (( p => r ) '&' ( q => r )) => (( p 'or' q ) => r) in TAUT(A); theorem :: PROCAL_1:37 ( p => ( q '&' 'not' q )) => 'not' p in TAUT(A); theorem :: PROCAL_1:38 (( p 'or' q ) '&' ( p 'or' r )) => ( p 'or' ( q '&' r )) in TAUT(A); theorem :: PROCAL_1:39 ( p '&' ( q 'or' r )) => (( p '&' q ) 'or' ( p '&' r )) in TAUT(A); theorem :: PROCAL_1:40 (( p 'or' r ) '&' ( q 'or' r )) => (( p '&' q ) 'or' r ) in TAUT(A); theorem :: PROCAL_1:41 (( p 'or' q ) '&' r ) => (( p '&' r ) 'or' ( q '&' r )) in TAUT(A); :: Deduction Rules theorem :: PROCAL_1:42 p in TAUT(A) implies ( p 'or' q ) in TAUT(A); theorem :: PROCAL_1:43 q in TAUT(A) implies ( p 'or' q ) in TAUT(A); theorem :: PROCAL_1:44 ( p '&' q ) in TAUT(A) implies p in TAUT(A); theorem :: PROCAL_1:45 ( p '&' q ) in TAUT(A) implies q in TAUT(A); theorem :: PROCAL_1:46 ( p '&' q ) in TAUT(A) implies ( p 'or' q ) in TAUT(A); theorem :: PROCAL_1:47 p in TAUT(A) & q in TAUT(A) implies p '&' q in TAUT(A); theorem :: PROCAL_1:48 p => q in TAUT(A) implies ( p 'or' r ) => ( q 'or' r ) in TAUT(A); theorem :: PROCAL_1:49 p => q in TAUT(A) implies ( r 'or' p ) => ( r 'or' q ) in TAUT(A); theorem :: PROCAL_1:50 p => q in TAUT(A) implies ( r '&' p ) => ( r '&' q ) in TAUT(A); theorem :: PROCAL_1:51 p => q in TAUT(A) implies ( p '&' r ) => ( q '&' r ) in TAUT(A); theorem :: PROCAL_1:52 r => p in TAUT(A) & r => q in TAUT(A) implies r => ( p '&' q ) in TAUT(A); theorem :: PROCAL_1:53 p => r in TAUT(A) & q => r in TAUT(A) implies ( p 'or' q ) => r in TAUT(A); theorem :: PROCAL_1:54 ( p 'or' q ) in TAUT(A) & 'not' p in TAUT(A) implies q in TAUT(A); theorem :: PROCAL_1:55 ( p 'or' q ) in TAUT(A) & 'not' q in TAUT(A) implies p in TAUT(A); theorem :: PROCAL_1:56 p => q in TAUT(A) & r => s in TAUT(A) implies ( p '&' r ) => ( q '&' s ) in TAUT(A); theorem :: PROCAL_1:57 p => q in TAUT(A) & r => s in TAUT(A) implies ( p 'or' r ) => ( q 'or' s ) in TAUT(A); theorem :: PROCAL_1:58 ( p '&' 'not' q ) => 'not' p in TAUT(A) implies p => q in TAUT(A);