We construct an extension P of the standard language of classical propositional logic by adjoining to the alphabet of a new category of logical-pragmatic signs. The well formed formulas of are calledradical formulas (rfs) of P;rfs preceded by theassertion sign constituteelementary assertive formulas of P, which can be connected together by means of thepragmatic connectives N, K, A, C, E, so as to obtain the set of all theassertive formulas (afs). Everyrf of P is endowed with atruth value defined classically, (...) and everyaf is endowed with ajustification value, defined in terms of the intuitive notion of proof and depending on the truth values of its radical subformulas. In this framework, we define the notion ofpragmatic validity in P and yield a list of criteria of pragmatic validity which hold under the assumption that only classical metalinguistic procedures of proof be accepted. We translate the classical propositional calculus (CPC) and the intuitionistic propositional calculus (IPC) into the assertive part of P and show that this translation allows us to interpret Intuitionistic Logic as an axiomatic theory of the constructive proof concept rather than an alternative to Classical Logic. Finally, we show that our framework provides a suitable background for discussing classical problems in the philosophy of logic. (shrink)

In this paper we present a philosophical motivation for the logics of formal inconsistency, a family of paraconsistent logics whose distinctive feature is that of having resources for expressing the notion of consistency within the object language in such a way that consistency may be logically independent of non-contradiction. We defend the view according to which logics of formal inconsistency may be interpreted as theories of logical consequence of an epistemological character. We also argue that in order to philosophically justify (...) paraconsistency there is no need to endorse dialetheism, the thesis that there are true contradictions. Furthermore, we show that mbC, a logic of formal inconsistency based on classical logic, may be enhanced in order to express the basic ideas of an intuitive interpretation of contradictions as conflicting evidence. (shrink)

It is argued that the tensed theory of the creative subject provides a natural formulation of the logic underlying Brouwer's notion of unextendable order and explains the link between that notion and virtual order. The tensed theory of the creative subject is also shown to be a useful tool for interpreting recent evidence about the stages of Brouwer's thinking concerning these two notions of order.

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.

The small, the tiny, and the infinitesimal have been the object of both fascination and vilification for millenia. One of the most vitriolic reviews in mathematics was that written by Errett Bishop about Keisler’s book Elementary Calculus: an Infinitesimal Approach. In this skit we investigate both the argument itself, and some of its roots in Bishop George Berkeley’s criticism of Leibnizian and Newtonian Calculus. We also explore some of the consequences to students for whom the infinitesimal approach is congenial. The (...) casual mathematical reader may be satisfied to read the text of the five act play, whereas the others may wish to delve into the 130 footnotes, some of which contain elucidation of the mathematics or comments on the history. (shrink)

This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)

A nucleus is an operation on the collection of truth values which, like double negation in intuitionistic logic, is monotone, inflationary, idempotent and commutes with conjunction. Any nucleus determines a proof-theoretic translation of intuitionistic logic into itself by applying it to atomic formulas, disjunctions and existentially quantified subformulas, as in the Gödel–Gentzen negative translation. Here we show that there exists a similar translation of intuitionistic logic into itself which is more in the spirit of Kuroda’s negative translation. The key is (...) to apply the nucleus not only to the entire formula and universally quantified subformulas, but to conclusions of implications as well. (shrink)

This paper studies, by way of an example, the intuitionistic propositional connective * defined in the language of second order propositional logic by. In full topological models * is not generally definable, but over Cantor-space and the reals it can be classically shown that; on the other hand, this is false constructively, i.e. a contradiction with Church's thesis is obtained. This is comparable with some well-known results on the completeness of intuitionistic first-order predicate logic.Over [0, 1], the operator * is (...) (constructively and classically) undefinable. We show how to recast this argument in terms of intuitive intuitionistic validity in some parameter. The undefinability argument essentially uses the connectedness of [0, 1]; most of the work of recasting consists in the choice of a suitable intuitionistically meaningful parameter, so as to imitate the effect of connectedness. (shrink)

This paper studies, by way of an example, the intuitionistic propositional connective * defined in the language of second order propositional logic by * ≡ ∃Q. In full topological models * is not generally definable but over Cantor-space and the reals it can be classically shown that *↔ ⅂⅂P; on the other hand, this is false constructively, i.e. a contradiction with Church's thesis is obtained. This is comparable with some well-known results on the completeness of intuitionistic first-order predicate logic. Over (...) [0, 1], the operator * is undefinable. We show how to recast this argument in terms of intuitive intuitionistic validity in some parameter. The undefinability argument essentially uses the connectedness of [0, 1]; most of the work of recasting consists in the choice of a suitable intuitionistically meaningful parameter, so as to imitate the effect of connectedness. Parameters of the required kind can be obtained as so-called projections of lawless sequences. (shrink)

This paper studies an economy whose agents perceive their consumption possibilities subjectively, and whose preferences are defined on what they subjectively experience, rather than on those alternatives that are objectively present. The model of agents' perceptions is based on intuitionistic logic. Roughly, this means that agents reason constructively: a solution to a problem exists only if there is a construction by which the problem can be solved. The theorems that can be proved determine how an agent perceives a set of (...) alternatives. A dual model relates perceived alternatives to a shared language, which the agents use in trading. So perceptions relate objective alternatives to an agent's subjective view of them, and reporting dually relates an agent's subjective world to a shared language. It turns out that an appropriately modified notion of competitive equilibrium always exists. However, in contrast with standard results in economic theory, competitive equilibrium need not be efficient. (shrink)

Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected.Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact (...) set is Bishop compact iff it is located. We translate this result to formal topology. ‘Bishop compact’ is translated as compact and overt. We propose a definition of locatedness on subspaces of a formal topology, and prove that a closed subspace of a compact regular formal space is located iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact — that is, totally bounded and complete — iff its localic completion is compact overt.Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales.We work constructively, predicatively and avoid the use of the axiom of countable choice. (shrink)

The purpose of this paper is to apply Crispin Wright’s criteria and various axes of objectivity to mathematics. I test the criteria and the objectivity of mathematics against each other. Along the way, various issues concerning general logic and epistemology are encountered.

Michael Dummett presents a modus tollens argument against a Wittgensteinian conception of meaning. In a series of papers, Dummett claims that Wittgensteinian considerations entail strict finitism. However, by a “sorites argument”, Dummett argues that strict finitism is incoherent and therefore questions these Wittgensteinian considerations.In this paper, I will argue that Dummett’s sorites argument fails to undermine strict finitism. I will claim that the argument is based on two questionable assumptions regarding some strict finitist sets of natural numbers. It will be (...) shown that strict finitism entails none of these assumptions. Hence, the argument does not prove that the view is internally incoherent, and consequently, Dummett fails to undermine the Wittgensteinian conception of meaning. (shrink)

ABSTRACTIn reply to Linnebo, I defend my analysis of Tait's argument against the use of classical logic in set theory, and make some preliminary comments on Linnebo's new argument for the same conclusion. I then turn to Shapiro's discussion of intuitionistic analysis and of Smooth Infinitesimal Analysis. I contend that we can make sense of intuitionistic analysis, but only by attaching deviant meanings to the connectives. Whether anyone can make sense of SIA is open to doubt: doing so would involve (...) making sense of mathematical quantities whose relationship to zero and to one another is inherently indeterminate. (shrink)

Michael Dummett has interpreted and expounded upon intuitionism under the influence of Wittgensteinian views on language, meaning and cognition. I argue against the application of some of these views to intuitionism and point to shortcomings in Dummett's approach. The alternative I propose makes use of recent, post-Wittgensteinian views in the philosophy of mind, meaning and language. These views are associated with the claim that human cognition exhibits intentionality and with related ideas in philosophical psychology. Intuitionism holds that mathematical constructions are (...) mental processes or objects. Constructions are, in the first instance, forms of consciousness or possible experience of a particular type. As such, they must be understood in terms of the concept of intentionality. This view has a historical basis in the literature on intuitionism. In a famous 1931 lecture Heyting in fact identifies constructions with fulfilled or fulfillable mathematical intentions. I consider some of the consequences of this identification and contrast them with Dummett's views on intuitionism. (shrink)

I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, an idealisation of more fundamental logical features in the proof theory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of logical consequence.

Epistemic Logic is our basic universal science, the method of our cognitive confrontation in reality to prove the truth of our basic cognitions and theories. Hence, by proving their true representation of reality we can self-control ourselves in it, and thus refuting the Berkeleyian solipsism and Kantian a priorism. The conception of epistemic logic is that only by proving our true representation of reality we achieve our knowledge of it, and thus we can prove our cognitions to be either true (...) or rather false, and otherwise they are doubtful. Therefore, truth cannot be separated from being proved and we cannot hold anymore the principle of excluded middle, as it is with formal semantics of metaphysical realism. In distinction, the intuitionistic logic is based on subjective intellectual feeling of correctness in constructing proofs, and thus it is epistemologically encapsulated in the metaphysical subject. However, epistemic logic is our basic science which enable us to prove the truth of our cognitions, including the epistemic logic itself. (shrink)

In applied problems mathematics is used as language or as a metalanguage on which metatheories are built, E.G., Mathematical theory of experiment. The structure of pure mathematics is grammar of the language. As opposed to pure mathematics, In applied problems we must keep in mind what underlies the sign system. Optimality criteria-Axioms of applied mathematics-Prove mutually incompatible, They form a mosaic and not mathematical structures which, According to bourbaki, Make mathematics a unified science. One of the peculiarities of applied mathematical (...) language is a variety of dialects: a problem can be presented in terms of various mathematical notions. Another peculiarity is polysemy: a problem can be presented in the framework of one dialect by a set of various models with equal right to exist. The pragmatic sense of distinction between applied and pure mathematics must lead to specific training in each case. (shrink)

After the 1930s, the research into the foundations of mathematics changed.None of its main directions (logicism, formalism and intuitionism) had any longer the pretension to be the only true mathematics.Usually, the determining factor in the change is considered to be Gödel?s work, while Heyting?s role is neglected.In contrast, in this paper I first describe how Heyting directly suggested the abandonment of the big foundational questions and the putting forward of a new kind of foundational research consisting in the isolation of (...) formal, intuitive, logical and platonistic elements within classical mathematics.Furthermore, I describe how Heyting indirectly influenced the abandon?ment of the old directions of foundational research by making out some lists of degrees of evidence that exist within intuitionism. (shrink)

The present paper deals with natural intuitionistic semantics for intuitionistic logic within an intuitionistic metamathematics. We show how strong completeness of full first order logic fails. We then consider a negationless semantics à la Henkin for second order intuitionistic logic. By using the theory of lawless sequences we prove that, for such semantics, strong completeness is restorable. We argue that lawless negationless semantics is a suitable framework for a constructive structuralist interpretation of any second order formalizable theory (classical or intuitionistic, (...) contradictory or not). (shrink)