This is an introduction to, and survey of, the constructive approaches to pure mathematics. The authors emphasise the viewpoint of Errett Bishop's school, but intuitionism. Russian constructivism and recursive analysis are also treated, with comparisons between the various approaches included where appropriate. Constructive mathematics is now enjoying a revival, with interest from not only logicans but also category theorists, recursive function theorists and theoretical computer scientists. This account for non-specialists in these and other disciplines.

Here is an account of recent investigations into the two main concepts of negation developed in the constructive logic: the negation as reduction to absurdity, and the strong negation. These concepts are studied in the setting of paraconsistent logic.

Manifestationalism holds that science aims only to give us theories that are correct about what has been observed thus far. Several philosophers, including Bas van Fraassen, have argued that manifestationalism cannot make sense of the scientific impetus to make new observations, since such observations only risk turning manifestationally adequate theories into inadequate ones. This paper argues that a strikingly similar objection applies to van Fraassen’s own constructive empiricism, the view that science aims only to find theories that are empirically (...) adequate. Roughly, the objection is that constructive empiricism cannot make sense of the scientific impetus to expand the limits of what can be observed, since such expansions only risk turning empirically adequate theories into inadequate ones. (shrink)

James Ladyman has argued that constructive empiricism entails modal realism, and that this renders constructive empiricism untenable. We maintain that constructive empiricism is compatible with modal nominalism. Although the central term 'observable' has been analyzed in terms of counterfactuals, and in general counterfactuals do not have objective truth conditions, the property of being observable is not a modal property, and hence there are objective, non-modal facts about what is observable. Both modal nominalism and constructive empiricism require (...) clarification in the face of Ladyman's argument. But we also argue that, even if Ladyman were right that constructive empiricism entails modal realism, this would not be a problem for constructive empiricism. (shrink)

Martin Heidegger devotes extensive discussion to medieval philosophers, particularly to their treatment of Truth and Being. On both these topics, Heidegger accuses them of forgetting the question of Being and of being responsible for subjugating truth to the modern crusade for certainty: ‘truth is denied its own mode of being’ and is subordinated ‘to an intellect that judges correctly’. Though there are some studies that discuss Heidegger’s debt to and criticism of medieval thought, particularly that of Thomas Aquinas, there is (...) no constructive reply to his assertions. As a result, Heidegger’s critique had an unprecedented effect on the credibility of medieval philosophy, whereby great portions of the philosophical community dismiss it altogether as an illegitimate Onto‐Theology. It is the aim of this study to offer a constructive reply that will fundamentally grapple with these allegations. By constructive reply we mean not only a reply that avoids the problems Heidegger raises regarding existence, essence and truth, but more importantly, one that uses Heidegger’s criticism in order to present a more insightful account of these notions. The present study is composed of two parts where the second serves as a sort of addendum. The first part, the core of this study, is an attempt to develop an understanding of the distinction between essence and existence that, on the one hand, accords with Heidegger’s criticism while on the other hand advances our understanding of how we think and understand reality. After presenting Heidegger’s depiction of Aquinas’s distinction between essence and existence (esse) as a real distinction, the study will present several views propounded by scholars of Aquinas regarding the status of this distinction. It will be argued that it is not clear whether the distinction is real, formal or conceptual, and that different types of distinction are applied in different places, particularly in regard to the phantasm that Aquinas considers essential to the human act of thinking. The second part diverges from the first part and focuses on Heidegger’s criticism of Aquinas’s conception of truth as adequation, i.e., what it is that grounds the possibility of truth as adequation. This divergence is necessary in order to present a full metaphysical response to Heidegger’s criticism. Since the aim of the present study is to argue that Aquinas’s philosophical system can contend with Heidegger’s criticism, a partial reply would greatly diminish its effectiveness. (shrink)

The (dis)continuism debate—the debate over whether remembering is a form of imagining—is a prominent one in contemporary philosophy of memory. In recent work, Langland-Hassan (2021) has argued that this debate is best understood as a dispute over whether remembering is a form of constructive imagining. In this paper, I argue that remembering is not a form of constructive imagining because constructive processes in remembering and imagining are constrained, and hence controlled, in different ways at the level of (...) consciousness. More specifically, I argue that remembering and imagining differ in terms of the interventions we can make on the constructive processes as they unfold. If this is correct, then a form of discontinuism is vindicated: remembering and imagining are, on this view, processes of different kinds. (shrink)

Starting from difference as the sole ontological origin, this paper establishes a self-consistent and complete constructive theory of space in which relations, rather than entities or a pre-existing container, serve as the fundamental basis. Difference is isomorphic and synonymous with this-that; space is generated directly by the unfolding of this-that as a relational act, not merely described by relations within a ready-made arena. Three secondary spatial relations: up-down, left-right, inside-outside-are further derived within space. All physical phenomena, including quantum superposition, (...) entanglement, wavefunction collapse, and parity non-conservation, are superficial manifestations determined by these underlying spatial relations. This theory unifies the explanation of space and quantum phenomena and proposes four falsifiable, experimentally testable predictions. (shrink)

This article explores some open questions related to the problem of verification of theories in the context of empirical sciences by contrasting three epistemological frameworks. Each of these epistemological frameworks is based on a corresponding central metaphor, namely: (a) Neo-empiricism and the gambling metaphor; (b) Popperian falsificationism and the scientific tribunal metaphor; (c) Cognitive constructivism and the object as eigen-solution metaphor. Each of one of these epistemological frameworks has also historically co-evolved with a certain statistical theory and method for testing (...) scientific hypotheses, respectively: (a) Decision theoretic Bayesian statistics and Bayes factors; (b) Frequentist statistics and p-values; (c) Constructive Bayesian statistics and e-values. This article examines with special care the Zero Probability Paradox (ZPP), related to the verification of sharp or precise hypotheses. Finally, this article makes some remarks on Lakatos’ view of mathematics as a quasi-empirical science. (shrink)

We propose a non-standard interpretation of Alternating-time Temporal Logic with imperfect information, for which no commonly accepted semantics has been proposed yet. Rather than changing the semantic structures, we generalize the usual interpretation of formulae in single states to sets of states. We also propose a new epistemic operator for ?practical? or ?constructive? knowledge, and we show that the new logic (which we call Constructive Strategic Logic) is strictly more expressive than most existing solutions, while it retains the (...) same model checking complexity. Finally, we study properties of constructive knowledge and other operators in this non-standard semantics. (shrink)

Summary Logics with strong negation are a class of sentential calculi that originally arose from concerns about the non-constructive nature of negation in intuitionistic logic. Nelson’s paraconsistent constructive logic with strong negation N4 (Almukdad and Nelson, 1984; Odintsov, 2003, 2004, 2008), the most important member of this class, is an axiomatic expansion of the negation-free fragment of the intuitionistic propositional calculus (Rasiowa, 1974, Chapter X) by a unary logical connective ~ of strong negation. It is well known that (...) strong negation plays an important role as ‘explicit negation’ in logic programming (Akama, 1997; Eiter et al., 1999; Gelfond, 2002; Kamide and Wansing, 2012; Pearce, 1999; Wansing, 1993). (shrink)

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL ew of the substructural logic FL ew . In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL ew (namely, a certain variety of FL ew -algebras) are term equivalent. This answers a longstanding question of Nelson (...) [30]. Extensive use is made of the automated theorem-prover Prover9 in order to establish the result. The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL ew are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL ew. (shrink)

Recent debates in metaphysics have highlighted the significance of type theories, such as Simple Type Theory (STT), for our philosophical analysis. In this chapter, I present the salient features of a constructive type theory in the style of Martin-Löf, termed CTT. My principal aim is to convey the flavour of this rich, flexible and sophisticated theory and compare it with STT. I especially focus on the forms of quantification which are available in CTT. A further aim is to argue (...) that a comparison between a plurality of theories is beneficial to the philosophical analysis. We may, for example, discover helpful features of one theory that we may want to import into another context, thus enriching our repertoire of formal tools. Or, through comparison with a less well-known theory, we may gain a better understanding of the characteristics of the theories we are familiar with. As argued in this chapter, CTT has much to offer in all of these respects. (shrink)

The incorporation of post-event testimonial information into an agent’s memory representation of the event via constructive memory processes gives rise to the misinformation effect, in which the incorporation of inaccurate testimonial information results in the formation of a false memory belief. While psychological research has focussed primarily on the incorporation of inaccurate information, the incorporation of accurate information raises a particularly interesting epistemological question: do the resulting memory beliefs qualify as knowledge? It is intuitively plausible that they do not, (...) for they appear to be only luckily true. I argue, however, that, despite its intuitive plausibility, this view is mistaken: once we adopt an adequate (modal) conception of epistemic luck and an adequate (adaptive) general approach to memory, it becomes clear that memory beliefs resulting from the incorporation of accurate testimonial information are not in general luckily true. I conclude by sketching some implications of this argument for the psychology of memory, suggesting that the misinformation effect would better be investigated in the context of a broader “information effect”. (shrink)

Over the last decade, scholars across the wide spectrum of the discipline of sociology have started to reengage with questions on morality and moral phenomena. The continued wave of research in this field, which has come to be known as the new sociology of morality, is a lively research program that has several common grounds with scholarship in the field of business ethics. The aim of this thematic symposium is to open constructive dialogues between these two areas of study. (...) In this introductory essay, we briefly present the project of the new sociology of morality and discuss its relevance for business ethics. We also review the contributions to this thematic symposium and identify four specific domains where future research can contribute to fruitful dialogues between the two fields. (shrink)

In this paper, I argue that, contrary to the constructive empiricist’s position, observability is not an adequate criterion as a guide to ontological commitment in science. My argument has two parts. First, I argue that the constructive empiricist’s choice of observability as a criterion for ontological commitment is based on the assumption that belief in the existence of unobservable entities is unreasonable because belief in the existence of an entity can only be vindicated by its observation. Second, I (...) argue that the kind of ontological commitment that is under consideration when accepting a scientific theory is commitment to what I call theoretical kinds and that observation can vindicate commitment to kinds only in exceptional cases. (shrink)

Sufficient syntactic conditions for canonicity in intermediate and intuitionistic modal logics are given. We present a new technique which does not require semantic first-order reduction and which is constructive in the sense that it works in an intuitionistic metatheory through a model without points which is classically isomorphic to the usual canonical model.

Existing literature indicates that abusive supervision yields adverse effects for both individuals and organizations. Nevertheless, empirical evidence suggests that people react differently to abusive supervision. In particular, there is insufficient knowledge regarding constructive responses to abusive supervision. Drawing from attribution and cognitive appraisal theories, the current study examines how individuals may behave both constructively and destructively under abusive supervision. Employing two multi-wave, multi-source studies, the current study findings highlight that guilt acts as a mediator between abusive supervision and supervisor-directed (...) constructive deviance, while shame serves as a mediator between abusive supervision and supervisor-directed destructive deviance. Furthermore, the degree of conscientiousness exhibited by subordinates under abusive supervision influences their emotional reactions. This study elucidates the complex psychological mechanisms through which abusive supervision can stimulate both constructive and destructive behaviors toward the supervisor at the same time. Hence, it underpins the impact of abusive supervision on the outcomes of individual subordinates. (shrink)

I propose an account of intuition for Bishop's brand of constructive mathematics, where constructions are person programs determined by their computational meaning. Past attempts to elucidate intuition by Parsons and Tieszen drawing on views put forward by Hilbert and Husserl, respectively, have failed to accommodate Bishop's ideas. I argue that, starting from premises building on the works of Brouwer and Heyting on the intuition of units and pairs and their causal sequences, we can explain how we intuit constructions by (...) how their computational meaning is captured by causal relations we project on units and pairs. My exposition of these premises builds on Heyting's reinterpretation of Brouwer's thought and further develops a diagrammatic interpretation proposed recently with the introduction of computations through protentions. (shrink)

The Zhuangzi text deploys two epistemic themes to accomplish its ends of combatting human pretensions to know the world and to prompting us to rediscover the world through fresh eyes. To get us to shed our arrogant dispositions it applies a constructive skepticism to whatever it is that human beings claim to know. To point towards a more constructive relationship with Nature, it articulates the stance of being a mirror to nature. This essay will explain how the text (...) does this and relates its conceptions of skepticism and being as mirror to relevant contemporary science. (shrink)

We often have to draw conclusions about states of machines in computer science and about states of knowledge and belief in artificial intelligence based on partial information. Nerode suggested using constructive logic as the language to express such deductions and also suggested designing appropriate intuitionistic Kripke frames to express the partial information. Following this program, Nerode and Wijesekera developed syntax, semantics and completeness for a system of intuitionistic dynamic logic for proving properties of concurrent programs. Like all dynamics logics, (...) this was a logic of many modalities, each expressing a program, but in intuitionistic rather than in classical logic. In that logic, both box and diamond are needed, but these two are not intuitionistically interdefinable and, worse, diamond does not distribute over ‘or’, except for sequential programs. This also happens in other contemplated computer science and AI applications, and leads outside the class of constructive logics investigated in the literature. The present paper fills this gap. We provide intuitionistic logics with independent box and diamond without assuming distribution of diamond over ‘or’. The completeness theorem is based on intuitionistic Kripke frames , but equipped with an additional, quite separate accessibility relation between worlds. In the interpretation of Nerode and Wijesekera , worlds under the partial order represent states of partial knowledge, the accessibility represents change in state of partial knowledge resulting from executing a specific program. But there are many other computer science interpretations. This formalism covers all computer science applications of which we are aware. We also give a cut elimination theorem and algebraic and topological formulations, since these present some new difficulties. Finally, these results were obtained prior to those in Nerode and Wijesekera. (shrink)

James Ladyman ([2000]) argues that constructive empiricism is untenable because it cannot adequately account for modal statements about observability. In this paper, I attempt to resist Ladyman's conclusion, arguing that the constructive empiricist can grant his modal discourse objective, theory-independent truth-conditions, yet without compromising his empiricism.

Thanks to the work of Kendall Walton, appeals to the notion of pretence (or make-believe) have become popular in philosophy. Now the notion has begun to appear in accounts of truth. My aim here is to assess one of these accounts, namely the ‘constructive methodological deflationism’ put forward by Jc Beall. After introducing the view, I argue that Beall does not manage to overcome the problem of psychological implausibility. Although Beall claims that constructive methodological deflationism supports dialetheism, I (...) argue that it does not, and I show that it in fact provides a classical response to the Liar paradox. (shrink)

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL ew of the substructural logic FL ew. The main result of Part I of this series [41] shows that the equivalent variety semantics of N and the equivalent variety semantics of NFL ew are term equivalent. In this paper, the term equivalence result of Part I [41] is lifted to the setting of (...) deductive systems to establish the definitional equivalence of the logics N and NFL ew. It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural logic. (shrink)

A synthesis of neo-Schumpeterian evolutionary, sociological, and historical coevolution ary models could be used for constructive technology assessment, aimed at the active management of the process of technological change. This article proposes a synthetic quasi-evolutionary model, in which variation and selection are neither independent nor coincidental processes. Variation and selection are linked by actors, resulting in the actor role labeled technological nexus. On the basis of the quasi-evolutionary approach, three constructive technology assessment strategies are proposed: stimulating alternative variations, (...) changing the selection environment, and creating or utilizing technological nexus. The usefulness of these concepts is demonstrated for the case of clean technolo gies. Ultimately, a conscious application of these strategies could result in a new actor role for government as a creative social regulator of technological change. (shrink)

In the present paper we introduce a constructive theory of nonstandard arithmetic in higher types. The theory is intended as a framework for developing elementary nonstandard analysis constructively. More specifically, the theory introduced is a conservative extension of HAω + AC. A predicate for distinguishing standard objects is added as in Nelson's internal set theory. Weak transfer and idealisation principles are proved from the axioms. Finally, the use of the theory is illustrated by extending Bishop's constructive analysis with (...) infinitesimals. (shrink)

Alchourrón, Gärdenfors and Makinson have developed and investigated a set of rationality postulates which appear to capture much of what is required of any rational system of theory revision. This set of postulates describes a class of revision functions, however it does not provide a constructive way of defining such a function. There are two principal constructions of revision functions, namely an epistemic entrenchment and a system of spheres. We refer to their approach as the AGM paradigm. We provide (...) a new constructive modeling for a revision function based on a nice preorder on models, and furthermore we give explicit conditions under which a nice preorder on models, an epistemic entrenchment, and a system of spheres yield the same revision function. Moreover, we provide an identity which captures the relationship between revision functions and update operators (as defined by Katsuno and Mendelzon). (shrink)

This paper concerns Ronald Dworkin’s notion of a ‘protestant attitude’ in interpreting constitutional provisions and offers an additional interpretation of Dworkin’s work, finding it useful for a constructive interpretation of the constitution and a partnership conception of democracy.

The notions of permutable and weak-permutable convergence of a series|$\sum _{n=1}^{\infty }a_{n}$|of real numbers are introduced. Classically, these two notions are equivalent, and, by Riemann’s two main theorems on the convergence of series, a convergent series is permutably convergent if and only if it is absolutely convergent. Working within Bishop-style constructive mathematics, we prove that Ishihara’s principle BD-|$\mathbb {N}$|implies that every permutably convergent series is absolutely convergent. Since there are models of constructive mathematics in which the Riemann permutation (...) theorem for series holds but BD-|$\mathbb{N}$|does not, the best we can hope for as a partial converse to our first theorem is that the absolute convergence of series with a permutability property classically equivalent to that of Riemann implies BD-|$\mathbb {N}$|. We show that this is the case when the property is weak-permutable convergence. (shrink)

In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo–Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF+RDC+LPO has indeed the same strength (...) as CZF, where RDC stands for relativized dependent choice. In particular, these theories prove the same Π02 theorems of arithmetic. (shrink)

Over the past years, in books and journals (this journal included), N. Maxwell launched a ferocious attack on B. C. van Fraassen’s view of science called Constructive Empiricism (CE). This attack has been totally ignored. Must we conclude from this silence that no defence is possible and that a fortiori Maxwell has buried CE once and for all? Or is the attack too obviously flawed as not to merit exposure? A careful dissection of Maxwell’s reasoning will make it clear (...) that neither is the case. This dissection includes an analysis of Maxwell’s ‘aberrance–argument’ (omnipresent in his many writings) for the claim that science implicitly and permanently accepts a substantial, metaphysical thesis about the universe, which then paves the way for his own metaphysical-realist hierarchy-view of science. This aberrance-claim, which Maxwell directs against a widely shared and harmful ideology of science called ‘Standard Empiricism’, generally has been ignored too, for more than a quarter of a century. Our conclusions will be that (i) Maxwell’s attacks on CE can be beaten off, and (ii) his ‘aberrance–arguments’ do not establish what Maxwell believes they establish, but (iii) we can draw a number of valuable lessons from these attacks about the nature of science and of the libertarian nature of CE. (shrink)

In this paper, consistency is understood as the absence of the negation of a theorem, and not, in general, as the absence of any contradiction. We define the basic constructive logic BKc1 adequate to this sense of consistency in the ternary relational semantics without a set of designated points. Then we show how to define a series of logics extending BKc1 within the spectrum delimited by contractionless minimal intuitionistic logic. All logics defined in the paper are paraconsistent logics.

Euclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. This involves finding “uniform” constructions where normally a case distinction is used. For example, in finding a perpendicular to line L through point p, one usually uses two different constructions, “erecting” a perpendicular when p is on L, and “dropping” a perpendicular when p is not on L, but in (...) constructive geometry, it must be done without a case distinction. Classically, the models of Euclidean geometry are planes over Euclidean fields. We prove a similar theorem for constructive Euclidean geometry, by showing how to define addition and multiplication without a case distinction about the sign of the arguments. With intuitionistic logic, there are two possible definitions of Euclidean fields, which turn out to correspond to different versions of the parallel postulate.We consider three versions of Euclid’s parallel postulate. The two most important are Euclid’s own formulation in his Postulate 5, which says that under certain conditions two lines meet, and Playfair’s axiom, which says there cannot be two distinct parallels to line L through the same point p. These differ in that Euclid 5 makes an existence assertion, while Playfair’s axiom does not. The third variant, which we call the strong parallel postulate, isolates the existence assertion from the geometry: it amounts to Playfair’s axiom plus the principle that two distinct lines that are not parallel do intersect. The first main result of this paper is that Euclid 5 suffices to define coordinates, addition, multiplication, and square roots geometrically.We completely settle the questions about implications between the three versions of the parallel postulate. The strong parallel postulate easily implies Euclid 5, and Euclid 5 also implies the strong parallel postulate, as a corollary of coordinatization and definability of arithmetic. We show that Playfair does not imply Euclid 5, and we also give some other independence results. Our independence proofs are given without discussing the exact choice of the other axioms of geometry; all we need is that one can interpret the geometric axioms in Euclidean field theory. The independence proofs use Kripke models of Euclidean field theories based on carefully constructed rings of real-valued functions. “Field elements” in these models are real-valued functions. (shrink)

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics. 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.

Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories.

Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s myriad aspects. Major themes include: constructive algebra and (...) geometry, constructive analysis, constructive topology, constructive logic and foundations of mathematics, and computational aspects of constructive mathematics. A series of introductory chapters provides graduate students and other newcomers to the subject with foundations for the surveys that follow. Edited by four of the most eminent experts in the field, this is an indispensable reference for constructive mathematicians and a fascinating vista of modern constructivism for the increasing number of researchers interested in constructive approaches. (shrink)

Since molecules are inaccessible to immediate observation, our conception of the molecule is brought about by transdiction which entails invention of various transcendental ideas. In organic chemistry we think that molecules consist of atoms, bonds, functional groups, etc. This is, however, not the unique description of the molecule as is shown by quantum mechanical calculations, for example. Then, what description represents the real molecule? Before asking this question, we have to consider what the real molecule is in the first place. (...) Constructive realism distinguishes our cognitive world and the world just given, and claims that we should accept the former as reality. Understanding our cognitive world is possible only through construction of micro-worlds. Atoms, bonds, functional groups, etc., are micro-worlds which make sense in a theoretical framework of organic chemistry. In this study we translate a micro-world to an affordance and paraphrase it as a context-relative dispositional attribute of an {agent-world} complex. Then, we can understand that it is what we take as molecular structure, not what might be out there to be found, that we should accept as reality. Excluding metaphysical fictions from scientific arguments, constructive realism makes science a meaningful activity. Constructive realism claims that, for getting knowledge of the world, we have to integrate information into our own linguistic frame, i.e., to translate it. Strangification is a technique of intentionally taking an accepted proposition out of one scientific system and putting it into a completely different context. As is the case with translation, strangification brings about deeper understanding of philosophical as well as scientific grounds on which the proposition system holds. We apply this method to molecular structure and reveal that it is an ingenious model to describe molecular behavior in multi-molecular systems with strong interactions between molecules. Information provided by strangification is essential to claim the legitimacy of a proposition system. As far as strangification is properly applied, relativism is irrelevant to constructive realism. (shrink)

Jaskowski's discursive logic (or discussive logic) is the first formal paraconsistent logic which is classified as a non-adjunctive system. It is now recognized that discursive logic is not generally appropriate for paraconsistent reasoning. To improve it in a constructive setting, we propose a constructive discursive logic with strong negation CDLSN based on Nelson's constructive logic N-. In CDLSN, discursive negation is defined similar to intuitionistic negation and discursive implication is defined as material implication using discursive negation. We (...) give an axiomatic system and Kripke semantics with a completeness proof. We also discuss some advantages of the proposed system over other paraconsistent systems. © 2011 Elsevier B.V., All rights reserved. (shrink)

The logic Ciore was introduced with the aim of providing new logical systems that axiomatize formal representations of inconsistency (here, equivalent to contradictoriness) in classical logic. The idea was to present a general formal system apt to handle contradictions in informatics, in particular, in the management of databases. A first order version of Ciore, QCiore, was presented and studied by Coniglio, Gomez-Pereira, and M. Figallo. These authors provided a partial structures semantics for QCiore, which generalizes the semantic notion of quasi-truth (...) considered by Mikeberg, da Costa, and Chuaqui. Besides, some important results of classical Model Theory were obtained for this logic. Recently, a sequent system for QCiore, GQCiore, was presented and proved that this system enjoys the cut-elimination property. In this paper, following Maehara’s method, we provide a constructive proof of the Craig’s interpolation theorem for QCiore as an application of the cut-elimination property of GQCiore. (shrink)

RésuméNous introduisons la notion de structure algébrique dynamique, inspirée de l'évaluation dynamique et de la théorie des modèles. Nous montrons comment cette notion constructive permet une relecture de la théorie d'Artin-Schreier, avec la modification capitale que le résultat final est alors établi de manière constructive. Nous pensons que ce que nous avons réalisé ici sur un cas d'école peut être généralisé à des parties significatives de l'algèbre classique, et est donc une contribution à la réalisation du programme de (...) Hilbert pour l'algèbre classique.We introduce the notion of “Dynamic Algebraic Structure” inspired by Dynamic Evaluation and Model Theory. We show that this constructive notion allows a rereading of the Artin-Schreier-Robinson solution for the 17th Hilbert Problem. So, once we know how to reread the proofs, this kind of abstract theory contains an algorithm which computes the concrete result . Our method gives a constructive semantic for certain parts of abstract classical mathematics.The idea is the following: replace the classical algebraic structures “constructed” by Choice and Principle of Third Excluded Middle , by DAS and dynamic evaluations of these DAS. Then TEM is replaced by construction of branching in the trees of dynamic evaluation of the DAS. If Choice is used in the form of Godel completeness theorem, it is not really necessary to use it for obtaining concrete results: in DAS, Choice is simply replaced by … nothing!. This is because the classical proof is by contradiction: “if there were not a sum of squares then some formal theory would admit a pathological model”. The constructive reasoning is more direct: since the pathological theory proves 0 = 1 we know how to construct the sum of squares … and classical models have disappeared in the proof. They are replaced by dynamic evaluations of DAS. We think that we have given, for an academic example, a new method, realizing a kind of Hilbert Program for significant parts of classical algebra. (shrink)

We study the connection between factors of the Medvedev lattice and constructive logic. The algebraic properties of these factors determine logics lying in between intuitionistic propositional logic and the logic of the weak law of the excluded middle (also known as De Morgan, or Jankov, logic). We discuss the relation between the weak law of the excluded middle and the algebraic notion of join-reducibility. Finally we discuss autoreducible degrees.