The Mizar abstract of LUKASI

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Propositional Calculus
by
Grzegorz Bancerek,
Agata Darmochwal, and
Andrzej Trybulec
Received September 26, 1990
MML identifier: LUKASI_1
[ Mizar article, MML identifier index ]
environ

 vocabulary CQC_LANG, ZF_LANG, CQC_THE1, QC_LANG1, QMAX_1;
 notation SUBSET_1, CQC_LANG, CQC_THE1;
 constructors CQC_THE1, XBOOLE_0;
 clusters CQC_LANG, ZFMISC_1, XBOOLE_0;


begin

reserve p, q, r, s, t for Element of CQC-WFF;
reserve X for Subset of CQC-WFF;

theorem :: LUKASI_1:1   :: Hypothetical syllogism
 (p => q) => ((q => r) => (p => r)) in TAUT;

theorem :: LUKASI_1:2
p => q in TAUT implies (q => r) => (p => r) in TAUT;

theorem :: LUKASI_1:3
 p => q in TAUT & q => r in TAUT implies p => r in TAUT;

theorem :: LUKASI_1:4  :: Identity law
 p => p in TAUT;

theorem :: LUKASI_1:5  :: Simplification

 q => (p => q) in TAUT;

theorem :: LUKASI_1:6

 ((p => q) => r) => (q => r) in TAUT;

theorem :: LUKASI_1:7  :: Modus ponendo ponens

 q => ((q => p) => p) in TAUT;

theorem :: LUKASI_1:8  :: Contraposition

 (s => (q => p)) => (q => (s => p)) in TAUT;

theorem :: LUKASI_1:9

 (q => r) => ((p => q) => (p => r)) in TAUT;

theorem :: LUKASI_1:10  :: A Hilbert axiom

 (q => (q => r)) => (q => r) in TAUT;

theorem :: LUKASI_1:11  :: Frege's law

 (p => (q => r)) => ((p => q) => (p => r)) in TAUT;

theorem :: LUKASI_1:12
 'not' VERUM => p in TAUT;

theorem :: LUKASI_1:13
  q in TAUT implies p => q in TAUT;

theorem :: LUKASI_1:14
   p in TAUT implies (p => q) => q in TAUT;

theorem :: LUKASI_1:15
 s => (q => p) in TAUT implies q => (s => p) in TAUT;

theorem :: LUKASI_1:16
  s => (q => p) in TAUT & q in TAUT implies s => p in TAUT;

theorem :: LUKASI_1:17
   s => (q => p) in TAUT & q in TAUT & s in TAUT implies p in TAUT;

theorem :: LUKASI_1:18
   q => (q => r) in TAUT implies q => r in TAUT;

theorem :: LUKASI_1:19
 (p => (q => r)) in TAUT implies (p => q) => (p => r) in TAUT;

theorem :: LUKASI_1:20
  (p => (q => r)) in TAUT & p => q in TAUT implies p => r in TAUT;

theorem :: LUKASI_1:21
   (p => (q => r)) in TAUT & p => q in TAUT & p in TAUT implies r in TAUT;

theorem :: LUKASI_1:22
 p => (q => r) in TAUT & p => (r => s ) in TAUT implies p => (q => s) in TAUT;

theorem :: LUKASI_1:23
  p => VERUM in TAUT;

theorem :: LUKASI_1:24
  ('not' p => 'not' q) => (q => p) in TAUT;

theorem :: LUKASI_1:25
  'not' 'not' p => p in TAUT;

theorem :: LUKASI_1:26
  (p => q) => ('not' q => 'not' p) in TAUT;

theorem :: LUKASI_1:27
 p => 'not' 'not' p in TAUT;

theorem :: LUKASI_1:28
 ('not' 'not' p => q) => (p => q) in TAUT & (p => q) => ('not' 'not'
p => q) in TAUT;

theorem :: LUKASI_1:29
 (p => 'not' 'not' q) => (p => q) in TAUT & (p => q) => (p => 'not' 'not'
q) in TAUT;

theorem :: LUKASI_1:30
 (p => 'not' q) => (q => 'not' p) in TAUT;

theorem :: LUKASI_1:31
 ('not' p => q) => ('not' q => p) in TAUT;

theorem :: LUKASI_1:32
(p => 'not' p) => 'not' p in TAUT;

theorem :: LUKASI_1:33
   'not' p => (p => q) in TAUT;

theorem :: LUKASI_1:34
 p => q in TAUT iff 'not' q => 'not' p in TAUT;

theorem :: LUKASI_1:35
   'not' p => 'not' q in TAUT implies q => p in TAUT;

theorem :: LUKASI_1:36
   p in TAUT iff 'not' 'not' p in TAUT;

theorem :: LUKASI_1:37
(p => q) in TAUT iff (p => 'not' 'not' q) in TAUT;

theorem :: LUKASI_1:38
(p => q) in TAUT iff ('not' 'not' p => q) in TAUT;

theorem :: LUKASI_1:39
   p => 'not' q in TAUT implies q => 'not' p in TAUT;

theorem :: LUKASI_1:40
   'not' p => q in TAUT implies 'not' q => p in TAUT;

:: predykat |- i schematy konsekwencji

theorem :: LUKASI_1:41
|- (p => q) => ((q => r) => (p => r));

theorem :: LUKASI_1:42
|- p => q implies |- (q => r) => (p => r);

theorem :: LUKASI_1:43
 |- p => q & |- q => r implies |- p => r;

theorem :: LUKASI_1:44
 |- p => p;

theorem :: LUKASI_1:45
 |- p => (q => p);

theorem :: LUKASI_1:46
   |- p implies |- q => p;

theorem :: LUKASI_1:47
  |- (s => (q => p)) => (q => (s => p));

theorem :: LUKASI_1:48
 |- p => (q => r) implies |- q => (p => r);

theorem :: LUKASI_1:49
   |- p => (q => r) & |- q implies |- p => r;

theorem :: LUKASI_1:50
   |- p => VERUM & |- 'not' VERUM => p;

theorem :: LUKASI_1:51
 |- p => ((p => q) => q);

theorem :: LUKASI_1:52
 |- (q => (q => r)) => (q => r);

theorem :: LUKASI_1:53
   |- q => (q => r) implies |- q => r;

theorem :: LUKASI_1:54
 |- (p => (q => r)) => ((p => q) => (p => r));

theorem :: LUKASI_1:55
 |- p => (q => r) implies |- (p => q) => (p => r);

theorem :: LUKASI_1:56
   |- p => (q => r) & |- p => q implies |- p => r;

theorem :: LUKASI_1:57
 |- ((p => q) => r) => (q => r);

theorem :: LUKASI_1:58
   |- (p => q) => r implies |- q => r;

theorem :: LUKASI_1:59
|- (p => q) => ((r => p) => (r => q));

theorem :: LUKASI_1:60
   |- p => q implies |- (r => p) => (r => q);

theorem :: LUKASI_1:61
 |- (p => q) => ('not' q => 'not' p);

theorem :: LUKASI_1:62
 |- ('not' p => 'not' q) => (q => p);

theorem :: LUKASI_1:63
   |- 'not' p => 'not' q iff |- q => p;

theorem :: LUKASI_1:64
 |- p => 'not' 'not' p;

theorem :: LUKASI_1:65
 |- 'not' 'not' p => p;

theorem :: LUKASI_1:66
    |- 'not' 'not' p iff |- p;


theorem :: LUKASI_1:67
|- ('not' 'not' p => q) => (p => q);

theorem :: LUKASI_1:68
|- 'not' 'not' p => q iff |- p => q;

theorem :: LUKASI_1:69
|- (p => 'not' 'not' q) => (p => q);

theorem :: LUKASI_1:70
|- p => 'not' 'not' q iff |- p => q;

theorem :: LUKASI_1:71
 |- (p => 'not' q) => (q => 'not' p);

theorem :: LUKASI_1:72
   |- p => 'not' q implies |- q => 'not' p;

theorem :: LUKASI_1:73
 |- ('not' p => q) => ('not' q => p);

theorem :: LUKASI_1:74
   |- 'not' p => q implies |- 'not' q => p;

theorem :: LUKASI_1:75
X|- p => q implies X|- (q => r) => (p => r);

theorem :: LUKASI_1:76
X|- p => q & X|- q => r implies X|- p => r;

theorem :: LUKASI_1:77
X|- p => p;

theorem :: LUKASI_1:78
   X|- p implies X|- q => p;

theorem :: LUKASI_1:79
   X |- p implies X |- (p => q) => q;

theorem :: LUKASI_1:80
  X |- p => (q => r) implies X |- q => (p => r);

theorem :: LUKASI_1:81
    X |- p => (q => r) & X |- q implies X |- p => r;

theorem :: LUKASI_1:82
   X |- p => (p => q) implies X |- p => q;

theorem :: LUKASI_1:83
   X |- (p => q) => r implies X |- q => r;

theorem :: LUKASI_1:84
 X |- p => (q => r) implies X |- (p => q) => (p =>r);

theorem :: LUKASI_1:85
   X |- p => (q => r) & X|- p => q implies X |- p => r;

theorem :: LUKASI_1:86
   X|- 'not' p => 'not' q iff X|- q => p;

theorem :: LUKASI_1:87
    X|- 'not' 'not' p iff X|- p;

theorem :: LUKASI_1:88
X|- p => 'not' 'not' q iff X|- p => q;

theorem :: LUKASI_1:89
X|- 'not' 'not' p => q iff X|- p => q;

theorem :: LUKASI_1:90
 X|- p => 'not' q implies X|- q => 'not' p;

theorem :: LUKASI_1:91
 X|- 'not' p => q implies X|- 'not' q => p;

theorem :: LUKASI_1:92
   X|- p => 'not' q & X |- q implies X|- 'not' p;

theorem :: LUKASI_1:93
   X|- 'not' p => q & X |- 'not' q implies X|- p;
The abstract of the Mizar article:

Propositional Calculus
