Proof of the independence of the primitive symbols of Heyting's calculus of propositions

In this paper I shall show that no one of the four primitive symbols of Heyting's calculus of propositions is definable in terms of the other three. So as to make the paper self-contained, I begin by stating the rules and primitive sentences given by Heyting. The primitive symbols of the calcul...

Full description

Saved in:
Bibliographic Details
Published in:The Journal of symbolic logic 1939-12, Vol.4 (4), p.155-158
Main Author: McKinsey, J. C. C.
Format: Article
Language:English
Subjects:
Direct products
Proof calculi
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper I shall show that no one of the four primitive symbols of Heyting's calculus of propositions is definable in terms of the other three. So as to make the paper self-contained, I begin by stating the rules and primitive sentences given by Heyting. The primitive symbols of the calculus are “⅂”, “∨”, “∧”, and “⊃”, which may be read, respectively, as “not,” “either…or,” “and,” and “if…then.” The symbol “⊃⊂”, which may be read “if and only if,” is defined in terms of these as follows: The rule of substitution is assumed, and the rule that S 2 follows from S 1 and S 1 ⊃ S 2 ; in addition it is assumed that S 1 ∧ S 2 follows from S 1 and S 2 . The primitive sentences are as follows:
ISSN:0022-4812
1943-5886
DOI:10.2307/2268715