A species-algebraic interpretation of the intuitionistic propositional calculus.
Jekeri Okee · Notre Dame Journal of Formal Logic · 1976
JEKERI OKEEThe topological and lattice-theoretical interpretations of the intuitionistic propositional calculus (see [4] and [5]) differ from the setalgebraic interpretation of the classical two-valued propositional calculus in that, in the former cases, the intuitionistic propositional calculus is interpreted by means of classical theories which are definable in the second order classical predicate calculus, but, in the latter, the classical propositional calculus is interpreted by means of a classical theory which is definable in the monadic classical predicate calculus of the first order.The algebra of species is the intuitionistic analogy to the Boolean algebra of sets (for details, see [1] and [2]).The aim of this article is to give a species-algebraic interpretation of the intuitionistic propositional calculus analogous to the set-algebraic interpretation of the classical propositional calculus.By using the method of logical matrix, it will be shown that the intuitionistic propositional calculus is equivalent to the algebra of species, of all subspecies of any infinite species, in the sense that, if the intuitionistic propositional functors-», v, Λ, ~, are interpreted as the corresponding species-algebraic operators, namely: species-implication =Φ, species-union u, species-intersection Π, and species-complement -, then the formulae of the propositional calculus can be mapped one-to-one onto the formulae of the algebra of species, in such a way that a formula H of the intuitionistic propositional calculus is provable in the intuitionistic propositional calculus if and only if the corresponding formula § of the algebra of species is valid in every algebra of species of all subspecies of any infinite species.1 The intuitionistic propositional calculus In the formulae of the propositional calculus variables of only one kind occur, namely, propositional variables, the letters P l9 P 2 , . ..,PW will be used.In addition to the variables, four constants occur in the propositional calculus: the implication sign -*, the disjunction sign v, the conjunction sign Λ, and the negation sign ~, (a fifth constant, the equivalence sign , may also be used).