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

### Calculus of Propositions

by
Jan Popiolek, and
Andrzej Trybulec

MML identifier: PROCAL_1
[ Mizar article, MML identifier index ]

```environ

vocabulary CQC_LANG, ZF_LANG, CQC_THE1;
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 for Element of CQC-WFF;

:::::::::::::::::::::::::::::
::   T A U T O L O G I E   ::
:::::::::::::::::::::::::::::

theorem :: PROCAL_1:1
'not' ( p '&' 'not' p ) in TAUT;

theorem :: PROCAL_1:2
p 'or' 'not' p in TAUT;

theorem :: PROCAL_1:3
p => ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:4
q => ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:5
( p 'or' q ) => ( 'not' p => q ) in TAUT;

theorem :: PROCAL_1:6
'not' ( p 'or' q ) => ( 'not' p '&' 'not' q ) in TAUT;

theorem :: PROCAL_1:7
( 'not' p '&' 'not' q ) => 'not' ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:8
( p 'or' q ) => ( q 'or' p ) in TAUT;

theorem :: PROCAL_1:9
'not' p 'or' p in TAUT;

theorem :: PROCAL_1:10
'not' ( p 'or' q ) => 'not' p in TAUT;

theorem :: PROCAL_1:11
( p 'or' p ) => p in TAUT;

theorem :: PROCAL_1:12
p => ( p 'or' p ) in TAUT;

theorem :: PROCAL_1:13
( p '&' 'not' p ) => q in TAUT;

theorem :: PROCAL_1:14
( p => q ) => ( 'not' p 'or' q ) in TAUT;

theorem :: PROCAL_1:15
( p '&' q ) => 'not' ( p => 'not' q ) in TAUT;

theorem :: PROCAL_1:16
'not' ( p => 'not' q ) => ( p '&' q ) in TAUT;

theorem :: PROCAL_1:17
'not' ( p '&' q ) => ( 'not' p 'or' 'not' q ) in TAUT;

theorem :: PROCAL_1:18
( 'not' p 'or' 'not' q ) => 'not' ( p '&' q ) in TAUT;

theorem :: PROCAL_1:19
( p '&' q ) => p in TAUT;

theorem :: PROCAL_1:20
( p '&' q ) => ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:21
( p '&' q ) => q in TAUT;

theorem :: PROCAL_1:22
p => p '&' p in TAUT;

theorem :: PROCAL_1:23
( p <=> q ) => ( p => q ) in TAUT;

theorem :: PROCAL_1:24
( p <=> q ) => ( q => p ) in TAUT;

theorem :: PROCAL_1:25
(( p 'or' q ) 'or' r ) => ( p 'or' ( q 'or' r )) in TAUT;

theorem :: PROCAL_1:26
(( p '&' q ) '&' r ) => ( p '&' ( q '&' r )) in TAUT;

theorem :: PROCAL_1:27
( p 'or' ( q 'or' r )) => (( p 'or' q ) 'or' r ) in TAUT;

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

theorem :: PROCAL_1:29
( p => q ) => (( q => p ) => ( p <=> q )) in TAUT;

theorem :: PROCAL_1:30
( p 'or' q ) <=> ( q 'or' p ) in TAUT;

theorem :: PROCAL_1:31
(( p '&' q ) => r ) => ( p => ( q => r )) in TAUT;

theorem :: PROCAL_1:32
( p => ( q => r )) => (( p '&' q ) => r ) in TAUT;

theorem :: PROCAL_1:33
( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in TAUT;

theorem :: PROCAL_1:34
(( p 'or' q ) => r ) => (( p => r ) 'or' ( q => r )) in TAUT;

theorem :: PROCAL_1:35
( p => r ) => (( q => r ) => (( p 'or' q ) => r)) in TAUT;

theorem :: PROCAL_1:36
(( p => r ) '&' ( q => r )) => (( p 'or' q ) => r) in TAUT;

theorem :: PROCAL_1:37
( p => ( q '&' 'not' q )) => 'not' p in TAUT;

theorem :: PROCAL_1:38
(( p 'or' q ) '&' ( p 'or' r )) => ( p 'or' ( q '&' r )) in TAUT;

theorem :: PROCAL_1:39
( p '&' ( q 'or' r )) => (( p '&' q ) 'or' ( p '&' r )) in TAUT;

theorem :: PROCAL_1:40
(( p 'or' r ) '&' ( q 'or' r )) => (( p '&' q ) 'or' r ) in TAUT;

theorem :: PROCAL_1:41
(( p 'or' q ) '&' r ) => (( p '&' r ) 'or' ( q '&' r )) in TAUT;

::::::::::::::::::::::::::::::::::::::::::::
::   R E G U L Y   D O W O D Z E N I A    ::
::::::::::::::::::::::::::::::::::::::::::::

theorem :: PROCAL_1:42
p in TAUT implies ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:43
q in TAUT implies ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:44
( p '&' q ) in TAUT implies p in TAUT;

theorem :: PROCAL_1:45
( p '&' q ) in TAUT implies q in TAUT;

theorem :: PROCAL_1:46
( p '&' q ) in TAUT implies ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:47
p in TAUT & q in TAUT implies p '&' q in TAUT;

theorem :: PROCAL_1:48
p => q in TAUT implies ( p 'or' r ) => ( q 'or' r ) in TAUT;

theorem :: PROCAL_1:49
p => q in TAUT implies ( r 'or' p ) => ( r 'or' q ) in TAUT;

theorem :: PROCAL_1:50
p => q in TAUT implies ( r '&' p ) => ( r '&' q ) in TAUT;

theorem :: PROCAL_1:51
p => q in TAUT implies ( p '&' r ) => ( q '&' r ) in TAUT;

theorem :: PROCAL_1:52
r => p in TAUT & r => q in TAUT implies r => ( p '&' q ) in TAUT;

theorem :: PROCAL_1:53
p => r in TAUT & q => r in TAUT implies ( p 'or' q ) => r in TAUT;

theorem :: PROCAL_1:54
( p 'or' q ) in TAUT & 'not' p in TAUT implies q in TAUT;

theorem :: PROCAL_1:55
( p 'or' q ) in TAUT & 'not' q in TAUT implies p in TAUT;

theorem :: PROCAL_1:56
p => q in TAUT & r => s in TAUT implies ( p '&' r ) => ( q '&' s ) in TAUT;

theorem :: PROCAL_1:57
p => q in TAUT & r => s in TAUT implies ( p 'or' r ) => ( q 'or' s ) in
TAUT;

theorem :: PROCAL_1:58
( p '&' 'not' q ) => 'not' p in TAUT implies p => q in TAUT;
```