:: Propositional Calculus :: by Grzegorz Bancerek, Agata Darmochwa\l and Andrzej Trybulec :: :: Received September 26, 1990 :: Copyright (c) 1990-2019 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 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 :: LUKASI_1:1 (p => q) => ((q => r) => (p => r)) in TAUT(A); theorem :: LUKASI_1:2 p => q in TAUT(A) implies (q => r) => (p => r) in TAUT(A); theorem :: LUKASI_1:3 p => q in TAUT(A) & q => r in TAUT(A) implies p => r in TAUT(A); theorem :: LUKASI_1:4 :: Identity law p => p in TAUT(A); theorem :: LUKASI_1:5 q => (p => q) in TAUT(A); theorem :: LUKASI_1:6 ((p => q) => r) => (q => r) in TAUT(A); theorem :: LUKASI_1:7 q => ((q => p) => p) in TAUT(A); theorem :: LUKASI_1:8 (s => (q => p)) => (q => (s => p)) in TAUT(A); theorem :: LUKASI_1:9 (q => r) => ((p => q) => (p => r)) in TAUT(A); theorem :: LUKASI_1:10 (q => (q => r)) => (q => r) in TAUT(A); theorem :: LUKASI_1:11 (p => (q => r)) => ((p => q) => (p => r)) in TAUT(A); theorem :: LUKASI_1:12 'not' VERUM(A) => p in TAUT(A); theorem :: LUKASI_1:13 q in TAUT(A) implies p => q in TAUT(A); theorem :: LUKASI_1:14 p in TAUT(A) implies (p => q) => q in TAUT(A); theorem :: LUKASI_1:15 s => (q => p) in TAUT(A) implies q => (s => p) in TAUT(A); theorem :: LUKASI_1:16 s => (q => p) in TAUT(A) & q in TAUT(A) implies s => p in TAUT(A); theorem :: LUKASI_1:17 s => (q => p) in TAUT(A) & q in TAUT(A) & s in TAUT(A) implies p in TAUT(A); theorem :: LUKASI_1:18 q => (q => r) in TAUT(A) implies q => r in TAUT(A); theorem :: LUKASI_1:19 (p => (q => r)) in TAUT(A) implies (p => q) => (p => r) in TAUT(A); theorem :: LUKASI_1:20 (p => (q => r)) in TAUT(A) & p => q in TAUT(A) implies p => r in TAUT(A); theorem :: LUKASI_1:21 (p => (q => r)) in TAUT(A) & p => q in TAUT(A) & p in TAUT(A) implies r in TAUT(A); theorem :: LUKASI_1:22 p => (q => r) in TAUT(A) & p => (r => s ) in TAUT(A) implies p => (q => s) in TAUT(A); theorem :: LUKASI_1:23 p => VERUM(A) in TAUT(A); theorem :: LUKASI_1:24 ('not' p => 'not' q) => (q => p) in TAUT(A); theorem :: LUKASI_1:25 'not' 'not' p => p in TAUT(A); theorem :: LUKASI_1:26 (p => q) => ('not' q => 'not' p) in TAUT(A); theorem :: LUKASI_1:27 p => 'not' 'not' p in TAUT(A); theorem :: LUKASI_1:28 ('not' 'not' p => q) => (p => q) in TAUT(A) & (p => q) => ('not' 'not' p => q) in TAUT(A); theorem :: LUKASI_1:29 (p => 'not' 'not' q) => (p => q) in TAUT(A) & (p => q) => (p => 'not' 'not' q) in TAUT(A); theorem :: LUKASI_1:30 (p => 'not' q) => (q => 'not' p) in TAUT(A); theorem :: LUKASI_1:31 ('not' p => q) => ('not' q => p) in TAUT(A); theorem :: LUKASI_1:32 (p => 'not' p) => 'not' p in TAUT(A); theorem :: LUKASI_1:33 'not' p => (p => q) in TAUT(A); theorem :: LUKASI_1:34 p => q in TAUT(A) iff 'not' q => 'not' p in TAUT(A); theorem :: LUKASI_1:35 'not' p => 'not' q in TAUT(A) implies q => p in TAUT(A); theorem :: LUKASI_1:36 p in TAUT(A) iff 'not' 'not' p in TAUT(A); theorem :: LUKASI_1:37 (p => q) in TAUT(A) iff (p => 'not' 'not' q) in TAUT(A); theorem :: LUKASI_1:38 (p => q) in TAUT(A) iff ('not' 'not' p => q) in TAUT(A); theorem :: LUKASI_1:39 p => 'not' q in TAUT(A) implies q => 'not' p in TAUT(A); theorem :: LUKASI_1:40 'not' p => q in TAUT(A) implies 'not' q => p in TAUT(A); :: predykat |- i schematy konsekwencji registration let A,p,q,r; cluster (p => q) => ((q => r) => (p => r)) -> valid; end; theorem :: LUKASI_1:41 p => q is valid implies (q => r) => (p => r) is valid; theorem :: LUKASI_1:42 p => q is valid & q => r is valid implies p => r is valid; registration let A,p; cluster p => p -> valid; end; registration let A,p,q; cluster p => (q => p) -> valid; end; theorem :: LUKASI_1:43 p is valid implies q => p is valid; registration let A,p,q,s; cluster (s => (q => p)) => (q => (s => p)) -> valid; end; theorem :: LUKASI_1:44 p => (q => r) is valid implies q => (p => r) is valid; theorem :: LUKASI_1:45 p => (q => r) is valid & q is valid implies p => r is valid; theorem :: LUKASI_1:46 p => VERUM(A) is valid & 'not' VERUM(A) => p is valid; registration let A,p,q; cluster p => ((p => q) => q) -> valid; end; registration let A,q,r; cluster (q => (q => r)) => (q => r) -> valid; end; theorem :: LUKASI_1:47 q => (q => r) is valid implies q => r is valid; registration let A,p,q,r; cluster (p => (q => r)) => ((p => q) => (p => r)) -> valid; end; theorem :: LUKASI_1:48 p => (q => r) is valid implies (p => q) => (p => r) is valid; theorem :: LUKASI_1:49 p => (q => r) is valid & p => q is valid implies p => r is valid; registration let A,p,q,r; cluster ((p => q) => r) => (q => r) -> valid; end; theorem :: LUKASI_1:50 (p => q) => r is valid implies q => r is valid; registration let A,p,q,r; cluster (p => q) => ((r => p) => (r => q)) -> valid; end; theorem :: LUKASI_1:51 p => q is valid implies (r => p) => (r => q) is valid; registration let A,p,q; cluster (p => q) => ('not' q => 'not' p) -> valid; end; registration let A,p,q; cluster ('not' p => 'not' q) => (q => p) -> valid; end; theorem :: LUKASI_1:52 'not' p => 'not' q is valid iff q => p is valid; registration let A,p; cluster p => 'not' 'not' p -> valid; end; registration let A,p; cluster 'not' 'not' p => p -> valid; end; theorem :: LUKASI_1:53 'not' 'not' p is valid iff p is valid; registration let A,p,q; cluster ('not' 'not' p => q) => (p => q) -> valid; end; theorem :: LUKASI_1:54 'not' 'not' p => q is valid iff p => q is valid; registration let A,p,q; cluster (p => 'not' 'not' q) => (p => q) -> valid; end; theorem :: LUKASI_1:55 p => 'not' 'not' q is valid iff p => q is valid; registration let A,p,q; cluster (p => 'not' q) => (q => 'not' p) -> valid; end; theorem :: LUKASI_1:56 p => 'not' q is valid implies q => 'not' p is valid; registration let A,p,q; cluster ('not' p => q) => ('not' q => p) -> valid; end; theorem :: LUKASI_1:57 'not' p => q is valid implies 'not' q => p is valid; theorem :: LUKASI_1:58 X|- p => q implies X|- (q => r) => (p => r); theorem :: LUKASI_1:59 X|- p => q & X|- q => r implies X|- p => r; theorem :: LUKASI_1:60 X|- p => p; theorem :: LUKASI_1:61 X|- p implies X|- q => p; theorem :: LUKASI_1:62 X |- p implies X |- (p => q) => q; theorem :: LUKASI_1:63 X |- p => (q => r) implies X |- q => (p => r); theorem :: LUKASI_1:64 X |- p => (q => r) & X |- q implies X |- p => r; theorem :: LUKASI_1:65 X |- p => (p => q) implies X |- p => q; theorem :: LUKASI_1:66 X |- (p => q) => r implies X |- q => r; theorem :: LUKASI_1:67 X |- p => (q => r) implies X |- (p => q) => (p =>r); theorem :: LUKASI_1:68 X |- p => (q => r) & X|- p => q implies X |- p => r; theorem :: LUKASI_1:69 X|- 'not' p => 'not' q iff X|- q => p; theorem :: LUKASI_1:70 X|- 'not' 'not' p iff X|- p; theorem :: LUKASI_1:71 X|- p => 'not' 'not' q iff X|- p => q; theorem :: LUKASI_1:72 X|- 'not' 'not' p => q iff X|- p => q; theorem :: LUKASI_1:73 X|- p => 'not' q implies X|- q => 'not' p; theorem :: LUKASI_1:74 X|- 'not' p => q implies X|- 'not' q => p; theorem :: LUKASI_1:75 X|- p => 'not' q & X |- q implies X|- 'not' p; theorem :: LUKASI_1:76 X|- 'not' p => q & X |- 'not' q implies X|- p;