Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### 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;

```

Back to top