A calculus, or its formalization, is m-valued when its truth-functions are allowed to take truth-values ranging from 1 through m. It is customary to divide the m truth-values that are possible into those that are “designated” and those that are “undesignated.” Furthermore, it is usually desired of a formalization that provable formulas and only provable formulas take designated truth-values exclusively. For our present purposes, we shall suppose that the truth-values 1, …, 8 are designated and the truth-values 8+1, …, m are undesignated. When calculi differ in respect to the number of their designated truth-values, we shall consider them different calculi, even if they are otherwise similar.

In his very interesting address On the calculus of refations, Professor Tarski discussed alternative bases for that calculus. He was there interested in “…different methods of setting up the foundations of this elementary calculus in a rigorously deductive way…” and so did not discuss the method of developing the calculus of relations with which this paper is concerned. Our purpose here is to show how the use of matrix notation for relations permits an algorithmic rather than a postulational-deductive development of the calculus of relations. One limitation of the present approach is to be admitted at the very outset: to enjoy the full benefits of the matrix approach, we are obliged to confine our investigations to Universes of Discourse which are finite. The reason for this restriction will become apparent presently.

It has been proved by S. C. Kleene and David Nelson that the formula

is intuitionistically non-deducible, i.e., non-deducible within the intuitionistic functional calculus.

The aim of this note is to outline a general method which permits us to establish the intuitionistic non-deducibility of many formulas and in particular of the formula (1).