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

Jan Popiolek

Warsaw University, Bialystok

Supported by RPBP.III24.C8.

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III24.C1.
Summary.

Continues the analysis of classical
language of first order (see [6], [1],
[3], [4], [2]).
Three connectives: truth, negation and conjuction are primary
(see [6]). The others (alternative, implication and equivalence)
are defined with respect to them (see [1]).
We prove some important tautologies of the calculus of propositions.
Most of them are given as the axioms of classical logical calculus (see
[5]). In the last part of our article we give some basic rules of inference.
The terminology and notation used in this paper have been
introduced in the following articles
[7]
[3]
[4]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
Connectives and subformulae of the first order language.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek, Agata Darmochwal, and Andrzej Trybulec.
Propositional calculus.
Journal of Formalized Mathematics,
2, 1990.
 [3]
Czeslaw Bylinski.
A classical first order language.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Agata Darmochwal.
A firstorder predicate calculus.
Journal of Formalized Mathematics,
2, 1990.
 [5]
Andrzej Grzegorczyk.
\em Zarys logiki matematycznej.
PWN, Warsaw, 1973.
 [6]
Piotr Rudnicki and Andrzej Trybulec.
A first order language.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received October 23, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]