Constructions, proofs and the meaning of logical constants (Q793721): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 12:05, 30 January 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Constructions, proofs and the meaning of logical constants |
scientific article |
Statements
Constructions, proofs and the meaning of logical constants (English)
0 references
1983
0 references
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.
0 references
foundations of intuitionism
0 references
theory of meaning
0 references
constructivity
0 references
construction
0 references
intuitionistic logical operations
0 references