The intended interpretation of intuitionistic logic (Q793720)

Two of the the author's main concerns are (a) the inadequacy of realizability as an explanation of the intended intuitionistic logical operations and (b) his inability to give a 'coherent account' of the relation: (the construction) c proves (the proposition) A, which is a key concept in the theory of meaning. More specifically, he repeats the familiar questions whether (i) the key relation is decidable, and (ii) for any A there is an a priori bound on c (in the literature: when c is required to be irredundant). Also his discussion is familiar from the 60's, but neglects more recent material. (a) Realizability is regarded as defective because its definition has a logical residue in the fragment (\(\neg,\wedge,\forall)\), apart from the predicate, of recursion equations, of defining a total function. Oversight, at least, for those sects of the intuitionistic persuasion who see the essence of a proposition in its algorithmic content: Propositions in (\(\neg,\wedge,\forall)\) have none. (b) As to (i) the matter of mere coherence is greatly exaggerated in view of the model, not cited in the paper, by use of hereditarily formalizable operations, in note A of \textit{A. S. Troelstra} [Modern logic: a survey (1981; Zbl 0464.03001)]. As to (ii), there is a perfect parallel in early set theory where the axiom of reducibility for ramified hierarchies was considered very implausible. Parallel: A's correspond to levels (or types) of ordinal \(\alpha\), and c's to terms defining sets all elements of which are defined below \(\alpha\). Gödel's proof of the GCH for the hierarchies above establishes that every set considered that occurs in the hierarchy at all, also has some definition c below the successor cardinal of \(\alpha\). The early doubts remain understandable inasmuch as some definitions, of the same set, at higher level are more informative; albeit in ways not considered in the theory of meaning. Similarly, there is no plausible limit on the possibilities of the mathematical imagination for proving A in informative ways. But b (ii) is not implausible if - in accordance with the theory of meaning -, for any A, the a priori bound is only required to contain some c: c proves A (when A is provable at all). This observation, on b (ii), is one of the many instances in conflict with the hopes expressed 25 years ago that abstract theories of constructions would lead to ideas outside or, at least, neglected in set theory. Instead, by and large, writings on abstract constructions have rehashed puzzles of early set theory, and experience in the latter has been used to straighten them out.