Constructions, proofs and the meaning of logical constants (Q793721): Difference between revisions

This and the preceding paper start from the tradition of the socalled theory of meaning, restricted to the general area of constructivity. It is almost diametrically opposite to the ordinary scientific, including the mathematical, tradition. The latter gives priority to the question whether any - intended or contrived - meaning is suitable for purposes firmly rooted in scientific experience. The author's main, more or less novel, point (p. 164) is a distinction between 3 meanings of 'construction', and no doubt impeccable within his tradition. Two of these meanings concern construction processes, when regarded as dynamic or completed; the third refers to end results. The distinction is then applied to meanings of the usual intuitionistic logical operations in the style initiated by Brouwer and Heyting. A typical example of the difference between the two traditions mentioned, occurs on p. 159, l. -8, where a proposal is rejected - completely correctly according to his tradition - because it involves an 'equation' between a proposition and its explanation. This is parallel to the rejection of the topological interpretation when it is presented as 'equating' a proposition A and a certain subset S(A) of a topological space S. For the theory of meaning it was a substantial advance to introduce an additional parameter \(\alpha\) over S into all non-logical constants of A to form the predicate \(A^+\), and then 'equate': \(\alpha\in S(A)\) and \(A^+\). For the mathematical tradition it was the correction of a terminological lapsus. - Reviewer's remark. On p. 167, l. 16 the expression 'formula-as-type', due to Howard, is mentioned, but not the fact that the notion goes back to a lecture by \textit{D. Scott} in 1968 [Lecture Notes Math. 125, 237-275 (1970; Zbl 0206.284)]. A significant difference, not apparent from Howard's terminology, is that he also considers terms together with computation rules, corresponding to derivations with normalization rules. Scott considers of course derivations-as-terms, too.