A new semantics is presented for the logic of proofs (LP), [1, 2], based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results.

The Logic of Proofs realizes the modalities from traditional modal logics with proof polynomials, so an expression □F becomes t:F where t is a proof polynomial representing a proof of or evidence for F. The pioneering work on explicating the modal logic is due to S. Artemov and was extended to several subsystems by V. Brezhnev. In 2000, R. Kuznets presented a algorithm for deducibility in these logics; in the present paper we will show that (...) the deducibility problem is -complete. Both Kuznets’s work and the present results make assumptions on the values of proof constants. (shrink)

We present algebraic semantics for the classical logic of proofs based on Boolean algebras. We also extend the language of the logic of proofs in order to have a Boolean structure on proof terms and equality predicate on terms. Moreover, the completeness theorem and certain generalizations of Stone’s representation theorem are obtained for all proposed algebras.

The logic of proofs is a refinement of modal logic introduced by Artemov in 1995 in which the modality ◻A is revisited as ⟦t⟧A where t is an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness and is capable of reflecting its own proofs . We develop the Hypothetical Logic of Proofs, a reformulation of LP based on judgemental reasoning.

In the recent literature on proof theory, there seems to be a new raising topic which consists in identifying those properties that characterise a good sequent calculus. The property that has received by far the most attention is the analyticity property. In this paper we propose a new argument in support of the analyticity property. We will do it by means of the example of the logic of proofs, a logic recently introduced by Artemov [1]. Indeed a (...) detailed proof analysis of this logic sheds new light on the logic itself and perfectly exemplifies our argument in favour of the analiticity. (shrink)

How the concept of proof has enabled the creation of mathematical knowledge. The Story of Proof investigates the evolution of the concept of proof--one of the most significant and defining features of mathematical thought--through critical episodes in its history. From the Pythagorean theorem to modern times, and across all major mathematical disciplines, John Stillwell demonstrates that proof is a mathematically vital concept, inspiring innovation and playing a critical role in generating knowledge. Stillwell begins with Euclid and (...) his influence on the development of geometry and its methods of proof, followed by algebra, which began as a self-contained discipline but later came to rival geometry in its mathematical impact. In particular, the infinite processes of calculus were at first viewed as "infinitesimal algebra," and calculus became an arena for algebraic, computational proofs rather than axiomatic proofs in the style of Euclid. Stillwell proceeds to the areas of number theory, non-Euclidean geometry, topology, and logic, and peers into the deep chasm between natural number arithmetic and the real numbers. In its depths, Cantor, Gödel, Turing, and others found that the concept of proof is ultimately part of arithmetic. This startling fact imposes fundamental limits on what theorems can be proved and what problems can be solved. Shedding light on the workings of mathematics at its most fundamental levels, The Story of Proof offers a compelling new perspective on the field's power and progress. (shrink)

Proofs and Refutations is essential reading for all those interested in the methodology, the philosophy and the history of mathematics. Much of the book takes the form of a discussion between a teacher and his students. They propose various solutions to some mathematical problems and investigate the strengths and weaknesses of these solutions. Their discussion raises some philosophical problems and some problems about the nature of mathematical discovery or creativity. Imre Lakatos is concerned throughout to combat the classical picture of (...) mathematical development as a steady accumulation of established truths. He shows that mathematics grows instead through a richer, more dramatic process of the successive improvement of creative hypotheses by attempts to 'prove' them and by criticism of these attempts: the logic of proofs and refutations. (shrink)

The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

A sequent calculus methodology for systems of agency based on branching-time frames with agents and choices is proposed, starting with a complete and cut-free system for multi-agent deliberative STIT; the methodology allows a transparent justification of the rules, good structural properties, analyticity, direct completeness and decidability proofs.

There exist valuable methods for theorem proving in non classical logics based on translation from these logics into first-order classical logic (abbreviated henceforth FOL). The key notion in these approaches istranslation from aSource Logic (henceforth abbreviated SL) to aTarget Logic (henceforth abbreviated TL). These methods are concerned with the problem offinding a proof in TL by translating a formula in SL, but they do not address the very important problem ofpresenting proofs in SL via a backward (...) translation. We propose a framework for presenting proofs in SL based on a partial backward translation of proofs obtained in a familiar TL: Order-Sorted Predicate Logic. The proposed backward translation transfers some formulasF TL belonging to the proof in TL into formulasF SL , such that the formulasF SL either (a) belong to a corresponding deduction in SL (in the best case) or, (b) are semantically related in some precise way, to formulas in the corresponding deduction in SL (in the worst case). The formulasF TL andF SL can obviously be considered aslemmas of their respective proofs. Therefore the transfer of lemmas of TL gives at least a skeleton of the corresponding proof in SL. Since the formulas of a proof keep trace of the strategy used to obtain the proof, clearly the framework can also help in solving another fundamental and difficult problem:the transfer of strategies from classical to non classical logics. We show how to apply the proposed framework, at least to S5, S4(p), K, T, K4. Two conjectures are stated and we propose sufficient (and in general satisfactory) conditions in order to obtain formulas in the proof in SL. Two particular cases of the conjectures are proved to be theorems. Three examples are treated in full detail. The main lines of future research are given. (shrink)

In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations of it in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the (...) present day. However, it might sound somewhat strange that no proof theory for GLS was ever developed nor even suggested thus far, except for the axiomatic system offered by Solovay. In this paper, we develop a proof theory for GLS based on the sequent calculus method. We provide a sequent calculus for GLS and prove the cut-elimination and some standard consequences of it: the interpolation and definability theorems. As another consequence of cut-elimination, we also prove the equivalence of GL and GLS with respect to a special form of formulas which we call Gödel sentences, using a purely proof-theoretical method. (shrink)

The logic of change formulated by K. Świętorzecka, has its motivation coming from the Aristotelian theory of substantial change which is undrstood as a transformation consisting in the disappearing and becoming of individual substances. The transition: becoming/disapearing (and conversely) is expressed in by the primitive operator C, to be read: it changes that …, and it is mapped by the progressively expanding language. We are interested in attributive changes of individual substances. We consider a formalism with two non-normal and (...) not mutually definable operators of possible and necessary change, inspired by Aristotelian distinction of accidental and essential attributes. From we adopt the idea that temporal concepts are defined via change operators, and the idea of an expanding language. In what follows, We axiomatise our new logic and describe its semantics, giving the proof of its completeness. We compare our formalism with selected modal logics. (shrink)

The question of who has the burden of proof is often important in practice. We must frequently make decisions and act on the basis not of conclusive evidence but of what is reasonable to presume true. Consequently, it happens that a given practical question must be solved by referring to principles that explicitly or implicitly determine, at least partly, where the burden of proof should rest. In this essay, I consider the role of the logic of the (...) burden of proof in a debate on global justice. In particular, I ask how the logic of the burden of proof is seen by those who defend conservative positions in a debate and deny our obligations to reduce poverty beyond borders. I argue that defenders of conservative positions tend to shift the burden of proof in an unjustified way. (shrink)

This paper is a critique of Kenneth Arrow's thesis concerning the logical impossibility of a constitution. I argue that one of the premises of Arrow's proof, that of the transitivity of indifference, is untenable. Several concepts of preference are introduced and counter-instances are offered to the transitivity of indifference defined along the standard lines in terms of these concepts. Alternate analyses of indifference in terms of preference are considered, and it is shown that these do not serve Arrow's purposes (...) either. Finally, it is argued that in the single special case in which indifference could plausibly be held to be transitive, Arrow's thesis is innocuous. (shrink)

The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective. However, what if we go a step further and ask about the meaning of a proof as a whole? In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs. Two questions are central here. First of all, if (...) we have two different derivations, does this always lead to a difference, firstly, in sense, and secondly, in denotation? The other question is about the relation between different kinds of proof systems with respect to this distinction. Do the different forms of representing a proof necessarily correspond to a difference in how the inferential steps are given? In our framework it will be possible to identify denotation as well as sense of proofs not only within one proof system but also between different kinds of proof systems. Thus, we give an account to distinguish a mere syntactic divergence from a divergence in meaning and a divergence in meaning from a divergence of proof objects analogous to Frege’s distinction for singular terms and sentences. (shrink)

In the paper the joint Logic of Proofs and Provability is presented that incorporates both the modality □ for provability 287–304) and the proof operator tF representing the proof predicate “t is a proof of F” . The obtained system naturally includes both the modal logic of provability GL and Artemov's Logic of Proofs . The presence of the modality □ requires two new operations on proofs that together with operations of allow to realize (...) all the invariant operations on proofs admitting description in the modal propositional language. Logic is proved to be decidable and complete with the intended provability semantics. (shrink)

I introduce a proof system for the logic of relative fundamentality, as well as a natural semantics with respect to which the system is both sound and complete. I then “modalise” the logic, and finally I discuss the properties of grounding given a suggested account of this notion in terms of necessity and relative fundamentality.

The logic of proofs was introduced by Artemov in order to analize the formalization of the concept of proof rather than the concept of provability. In this context, some operations on proofs play a very important role. In this paper, we investigate some very natural operations, paying attention not only to positive information, but also to negative information (i.e. information saying that something cannot be a proof). We give a formalization for a fragment of such a (...) class='Hi'>logic of proofs, and we prove that our fragment is complete and decidable. (shrink)

We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t: F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem. We state a general Correspondence Theorem showing that behind each epistemic modal (...) logic, there is a robust system of justifications. This renders a new, evidence-based foundation for epistemic logic. As a case study, we offer a resolution of the GoldmanRed Barns in Justification Logic. Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and redundancies in Gettier’s reasoning. (shrink)

In this paper individual proofs are integrated into provability logic. Systems of axioms for a logic with operators “A is provable” and “p is a proof of A” are introduced, provided with Kripke semantics and decision procedure. Completeness theorems with respect to the arithmetical interpretation are proved.

I consider the idea of a propositional logic of location based on the following semantic framework, derived from ideas of Prior. We have a collection L of locations and a collection S of statements such that a statement may be evaluated for truth at each location. Typically one and the same statement may be true at one location and false at another. Given this semantic framework we may proceed in two ways: introducing names for locations, predicates for the relations (...) among them and an “at” preposition to express the value of statements at locations; or introduce statement operators which do not name locations but whose truth-conditional effect depends on the truth or falsity of embedded statements at various locations. The latter is akin to Prior’s approach to tense logic. In any logic of location there will be some basic operators which we can define. By ringing the changes on the topology of locations, different logical systems may be generated, and the challenge for the logician is then in each case to find operators, axioms and rules yielding a proof theory adequate to the semantics. The generality of the approach is illustrated with familiar and not so familiar examples from modal, tense and place logic, mathematics, and even the logic of games. To the memory of Ted Dawson, who introduced me to philosophy and the writings of Arthur Prior. (shrink)

Lance Rips describes a unified theory of natural deductive reasoning and fashions a working model of deduction, with strong experimental support, that is capable of playing a central role in mental life.

This is a purely conceptual paper. It aims at presenting and putting into perspective the idea of a proof-theoretic semantics of the logical operations. The first section briefly surveys various semantic paradigms, and Section 2 focuses on one particular paradigm, namely the proof-theoretic semantics of the logical operations.

The goal of this article is to take a step toward the resolution of the problem of finding an analytic sequent calculus for the logic of proofs. For this, we focus on the system Ilp, the intuitionistic version of the logic of proofs. First we present the sequent calculus Gilp that is sound and complete with respect to the system Ilp; we prove that Gilp is cut-free and contraction-free, but it still does not enjoy the subformula property. Then, (...) we enrich the language of the logic of proofs and we formulate in this language a second Gentzen calculus Gilp∗. We show that Gilp∗ is a conservative extension of Gilp, and that Gilp∗ satisfies the subformula property. (shrink)

Dag Prawitz (1971) put forward the idea that an admissible reduction process does not affect the identity of proofs represented by derivations in natural deduction. The idea relies on his conjecture that two derivations represent the same proof if and only if they are equivalent in the sense that they are reflexive, transitive and symmetric closure of the immediate reducibility relation. Schroeder-Heister and Tranchini (2017) accept Prawitz’s conjecture and propose the triviality test as the criterion for admissible reductions. In (...) the present paper, we will consider two main troubles of the triviality test. The first is the obscurity of a method of evaluating admissible reductions. The second is the circularity problem that the triviality test already assumes the set of admissible reduction procedures. For the solution of the problems, we will propose the spoiler test which immunes the problems of the triviality test and has the role of the criterion for admissible reductions. At last, we shall cover a plausible problem of the spoiler test that can be caused by Crabbé’s case. (shrink)

Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by (...) many researchers to try to put some order in the present logical jungle. Thus Cl91], Ep90] and Wo88] are three recent books in which an attempt is made to develop a general theoretical framework for the study of logics. On the more pragmatic side, several systems have been developed with the goal of providing a computerized logical framework in which many di erent logical systems can be implemented in a uniform way. An example is the Edinburgh LF( HHP91]). (shrink)

This influential book discusses the nature of mathematical discovery, development, methodology and practice, forming Imre Lakatos's theory of 'proofs and refutations'.

This book, written by one of the most distinguished of contemporary philosophers of mathematics, is a fully rewritten and updated successor to the author's earlier The Unprovability of Consistency. Its subject is the relation between provability and modal logic, a branch of logic invented by Aristotle but much disparaged by philosophers and virtually ignored by mathematicians. Here it receives its first scientific application since its invention. Modal logic is concerned with the notions of necessity and possibility. What (...) George Boolos does is to show how the concepts, techniques, and methods of modal logic shed brilliant light on the most important logical discovery of the twentieth century: the incompleteness theorems of Kurt Godel and the 'self-referential' sentences constructed in their proof. The book explores the effects of reinterpreting the notions of necessity and possibility to mean provability and consistency. (shrink)

The papers collected in this volume exemplify some of the trends in current approaches to logic, language and computation. Written by authors with varied academic backgrounds, the contributions are intended for an interdisciplinary audience. The first part of this volume addresses issues relevant for multi-agent systems: reasoning with incomplete information, reasoning about knowledge and beliefs, and reasoning about games. Proofs as formal objects form the subject of Part II. Topics covered include: contributions on logical frameworks, linear logic, and (...) different approaches to formalized reasoning. Part III focuses on representations and formal methods in linguistic theory, addressing the areas of comparative and temporal expressions, modal subordination, and compositionality. (shrink)

This book, one of the handful of truly pathbreaking works in twentieth-century philosophical theology, presents Hartshorne's persuasive rehabilitation of Anselm's Ontological Argument, recast in neoclassical form as "the Modal Proof.".

In a recent paper Berto introduces a semantic system for a logic of imagination, intended as positive conceivability, and aboutness of imaginative acts. This system crucially adopts elements of both the semantics of conditionals and the semantics of analytical implications in order to account for the central logical traits of the notion of truth in an act of imagination based on an explicit input. The main problem left unsolved is to put forward a complete set of axioms for the (...) proposed system. In the present paper I offer a solution to this problem by providing a complete axiomatization of a generalization of the original semantics. The difficulty in proving completeness lies in the fact that the modalities that capture the notion of truth in an act of imagination are neither standard nor minimal, so that the construction of the canonical model and the proof of the truth lemma are to be substantially modified. (shrink)

We introduce the logic LRC, designed to describe and reason about agents’ abilities and capabilities in using resources. The proposed framework bridges two—up to now—mutually independent strands of literature: the one on logics of abilities and capabilities, developed within the theory of agency, and the one on logics of resources, motivated by program semantics. The logic LRC is suitable to describe and reason about key aspects of social behaviour in organizations. We prove a number of properties enjoyed by (...) LRC and its associated analytic calculus. These results lay at the intersection of the algebraic theory of unified correspondence and the theory of multitype calculi in structural proof theory. Case studies are discussed which showcase several ways in which this framework can be extended and enriched while retaining its basic properties, so as to model an array of issues, both practically and theoretically relevant, spanning from planning problems to the logical foundations of the theory of organizations. (shrink)

The concept of burden of proof is used in a wide range of discourses, from philosophy to law, science, skepticism, and even in everyday reasoning. This paper provides an analysis of the proper deployment of burden of proof, focusing in particular on skeptical discussions of pseudoscience and the paranormal, where burden of proof assignments are most poignant and relatively clear-cut. We argue that burden of proof is often misapplied or used as a mere rhetorical gambit, with (...) little appreciation of the underlying principles. The paper elaborates on an important distinction between evidential and prudential varieties of burdens of proof, which is cashed out in terms of Bayesian probabilities and error management theory. Finally, we explore the relationship between burden of proof and several (alleged) informal logical fallacies. This allows us to get a firmer grip on the concept and its applications in different domains, and also to clear up some confusions with regard to when exactly some fallacies (ad hominem, ad ignorantiam, and petitio principii) may or may not occur. (shrink)

The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept — more precisely, the associated concept of reducibility — is a generalization of Turing reducibility from the traditional, input/output sorts of problems to computational tasks of arbitrary degrees of interactivity.

Conditional statements are ubiquitous, from promises and threats to reasoning and decision making. By now, logicians have studied them from many different angles, both semantic and proof-theoretic. This paper suggests two more perspectives on the meaning of conditionals, one dynamic and one geometric, that may throw yet more light on a familiar and yet in some ways surprisingly elusive and many-faceted notion.1.

I will analyse some properties of abduction that are essential from a logical standpoint. When dealing with the so-called ‘inferential problem’, I will opt for the more general concepts of input and output instead of those of premisses and conclusions, and show that in this framework two consequences can be derived that help clarify basic logical aspects of abductive reasoning: (i) it is more natural to accept the ‘multimodal’ and ‘context-dependent’ character of the inferences involved, (ii) inferences are not merely (...) conceived of in the terms of the process leading to the ‘generation of an output’ or to the proof of it, as in the traditional and standard view of deductive proofs, but rather, from this perspective abductive inferences can be seen as related to logical processes in which input and output fail to hold each other in an expected relation, with the solution involving the modification of inputs, not that of outputs. I will also describe that if we wish to naturalize the logic of the abductive processes and its special consequence relation, we should refer to the following main aspects: ‘optimization of situatedness’, ‘maximization of changeability’ of both input and output, and high ‘information-sensitiveness’. (shrink)

The cut-free Gentzen-type sequent calculus LLK for the logic of likelihood is introduced in the paper. It is proved that the calculus is sound and complete for LL. Using the introduced calculus LLK, a decision procedure for LL is presented.

In this paper, we explore the possibility of applying traditional and modern aesthetical theories to logical and mathematical proofs, with the goal of better understanding the intuitive concept of mathematical beauty. This informal concept takes a central role in the work of logicians and mathematicians and can be thought of as their main motivation. In the present paper, we try to define concepts connected to mathematical beauty or beauty in mathematical proofs, so that we may lay the foundations for a (...) more precise definition of mathematical beauty which would be obtained through a detailed survey among logicians and mathematicians, presented in a future paper. The present paper brings crucial results to be used for constructing the survey. (shrink)

Here are some things that are widely believed about free will and determinism. Free will is prima facie incompatible with determinism. The incompatibility is logical or at least conceptual or a priori. A compatibilist needs to explain how free will can co-exist with determinism, paradigmatically by offering an analysis of ‘free’ action that is demonstrably compatible with determinism. Free will is not impugned by quantum indeterminism, at least not in the same decisive way that it is impugned by determinism. To (...) reconcile free will with quantum indeterminism takes work, but the work comes under the heading of metaphysical business-as-usual; to reconcile free will with determinism requires a conceptual breakthrough.And listen to Laura Waddell Ekstrom on the burden of proof. (shrink)

We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell (...) states) and various linear operators. As an example we sketch an analysis of the teleportation protocol. (shrink)