B. Göran Sundholm

In the present paper I wish to regard constructivelogic as a self-contained system for the treatment ofepistemological issues; the explanations of theconstructivist logical notions are cast in anepistemological mold already from the outset. Thediscussion offered here intends to make explicit thisimplicit epistemic character of constructivism.Particular attention will be given to the intendedinterpretation laid down by Heyting. This interpretation, especially as refined in the type-theoretical work of Per Martin-Löf, puts thesystem on par with the early efforts of Frege andWhitehead-Russell. This quite recent work, however,has proved valuable not only in the philosophy andfoundations of mathematics, but has also foundpractical application in computer science, where thelanguage of constructivism serves as an implementableprogramming language, and within the philosophy oflanguage.\footnote{Nordstr\"{o}m et al. give an overview of the work in computerscience, whereas Ranta provides an impressiveconstructivist alternative to Montague Grammar usingthe richer type structure of Martin-L\"{o}f in placeof the simple classical type theory of Church.} Mypresentation will be carried out through a contrastwith standard metamathematical work.\footnote{Troelstra and van Dalen give an encyclopedictreatment of the metamathematics of constructivism.}In the course of the development I have occasion tooffer some novel considerations on thenature of proof and inference

Truth-maker analyses construe truth as existence of proof, a well-known example being that offered by Wittgenstein in theTractatus. The paper subsumes the intuitionistic view of truth as existence of proof under the general truth-maker scheme. Two generic constraints on truth-maker analysis are noted and positioned with respect to the writings of Michael Dummett and theTractatus. Examination of the writings of Brouwer, Heyting and Weyl indicates the specific notions of truth-maker and existence that are at issue in the intuitionistic truth-maker analysis, namely that of proof in the sense of proof-object (Brouwer, Heyting) and existence in the nonpropositional sense of a judgement abstract (Weyl). Furthermore, possible anticipations in the writings of Schlick and Pfänder are noted.

Tradition is classical. Surely, nothing could be more pleonastic than that? The logical tradition, certainly, was squarely classical from Bolzano to Carnap, with, say, Frege, Moore, Russell and the Wittgenstein of the Tractatus as intermediaries. Propositions are construed as being in themselves true-or-false. Indeed, in this tradition, a declarative sentence S expresses a proposition by being true-or-false. So the meaningfulness of a sentence consists in its being true-or-false. But S is true-orfalse, or so they say, only when S is true, or when S is false. On the classical account the presumption of bivalence is built into the very notion of meaningfulness: there is no difference between asserting that A is a proposition and asserting that A is true-or-false. The matter came to the fore in the foundations of set theory. In his first attempt at giving an application criterion for sets Cantor noted:Eine Mannigfaltigkeit von Elementen, die irgendwelcher Begriffssphäre angehören, nenne ich wohldefiniert, wenn auf Grund ihrer Definition und infolge des logischen Prinzips vom ausgeschlossenen Dritten es als intern bestimmt angesehen werden muss, sowohl ob irgendein derselben Begriffssphäre angehöriges Objekt zu der gedachten Mannigfaltigkeit gehört oder nicht, wie auch, ob zwei zur Mannigfaltigkeit gehörige Objekte trotz formaler Unterschiede in der Art des Gegebenseins einander gleich sind oder nicht.

An implication is a proposition, a consequence is a relation between propositions, and an inference is act of passage from certain premise-judgements to another conclusion-judgement: a proposition is true, a consequence holds, whereas an inference is valid. The paper examines interrelations, differences, refinements and linguistic renderings of these notions, as well as their history. The truth of propositions, respectively the holding of consequences, are treated constructively in terms of verification-objects. The validity of an inference is elucidated in terms of the existence of a chain of immediately evident steps linking premises and conclusion.

An implication is a proposition, a consequence is a relation between propositions, and an inference is act of passage from certain premise-judgements to another conclusion-judgement: a proposition is true, a consequence holds, whereas an inference is valid. The paper examines interrelations, differences, refinements and linguistic renderings of these notions, as well as their history. The truth of propositions, respectively the holding of consequences, are treated constructively in terms of verification-objects. The validity of an inference is elucidated in terms of the existence of a chain of immediately evident steps linking premises and conclusion