A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

This book offers a concise introduction to both proof-theory and algebraic methods, the core of the syntactic and semantic study of logic respectively. The importance of combining these two has been increasingly recognized in recent years. It highlights the contrasts between the deep, concrete results using the former and the general, abstract ones using the latter. Covering modal logics, many-valued logics, superintuitionistic and substructural logics, together with their algebraic semantics, the book also provides an introduction to nonclassical logic for (...) undergraduate or graduate level courses.The book is divided into two parts: Proof Theory in Part I and Algebra in Logic in Part II. Part I presents sequent systems and discusses cut elimination and its applications in detail. It also provides simplified proof of cut elimination, making the topic more accessible. The last chapter of Part I is devoted to clarification of the classes of logics that are discussed in the second part. Part II focuses on algebraic semantics for these logics. At the same time, it is a gentle introduction to the basics of algebraic logic and universal algebra with many examples of their applications in logic. Part II can be read independently of Part I, with only minimum knowledge required, and as such is suitable as a textbook for short introductory courses on algebra in logic. (shrink)

Paraconsistent Weak Kleene Logic is the 3-valued propositional logic defined on the weak Kleene tables and with two designated values. Most of the existing proof systems for PWK are characterised by the presence of linguistic restrictions on some of their rules. This feature can be seen as a shortcoming. We provide a cut-free calculus for PWK that is devoid of such provisos. Moreover, we introduce a Priest-style tableaux calculus for PWK.

Fuzzy logics are many-valued logics that are well suited to reasoning in the context of vagueness. They provide the basis for the wider field of Fuzzy Logic, encompassing diverse areas such as fuzzy control, fuzzy databases, and fuzzy mathematics. This book provides an accessible and up-to-date introduction to this fast-growing and increasingly popular area. It focuses in particular on the development and applications of "proof-theoretic" presentations of fuzzy logics; the result of more than ten years of intensive work by (...) researchers in the area, including the authors. In addition to providing alternative elegant presentations of fuzzy logics, proof-theoretic methods are useful for addressing theoretical problems and developing efficient deduction and decision algorithms. Proof-theoretic presentations also place fuzzy logics in the broader landscape of non-classical logics, revealing deep relations with other logics studied in Computer Science, Mathematics, and Philosophy. The book builds methodically from the semantic origins of fuzzy logics to proof-theoretic presentations such as Hilbert and Gentzen systems, introducing both theoretical and practical applications of these presentations. (shrink)

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than (...) in the explanation of the rules. (shrink)

The paper briefly surveys the sentential proof-theoretic semantics for fragment of English. Then, appealing to a version of Frege’s context-principle (specified to fit type-logical grammar), a method is presented for deriving proof-theoretic meanings for sub-sentential phrases, down to lexical units (words). The sentential meaning is decomposed according to the function-argument structure as determined by the type-logical grammar. In doing so, the paper presents a novel proof-theoretic interpretation of simple type, replacing Montague’s model-theoretic type interpretation (in arbitrary Henkin (...) models). The domains of derivations are collections of derivations in the associated “dedicated” natural-deduction proof-system, and functions therein (with no appeal to models, truth-values and elements of a domain). The compositionality of the semantics is analyzed. (shrink)

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a (...) technical point of view. (shrink)

In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction.

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. (...) With minor restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the logics. (shrink)

Progressions of iterated reflection principles can be used as a tool for the ordinal analysis of formal systems. We discuss various notions of proof-theoretic ordinals and compare the information obtained by means of the reflection principles with the results obtained by the more usual proof-theoretic techniques. In some cases we obtain sharper results, e.g., we define proof-theoretic ordinals relevant to logical complexity Π1 0 and, similarly, for any class Π n 0. We provide a more general version (...) of the fine structure relationships for iterated reflection principles (due to U. Schmerl [25]). This allows us, in a uniform manner, to analyze main fragments of arithmetic axiomatized by restricted forms of induction, including IΣ n, IΣ n −, IΠ n − and their combinations. We also obtain new conservation results relating the hierarchies of uniform and local reflection principles. In particular, we show that (for a sufficiently broad class of theories T) the uniform Σ1-reflection principle for T is Σ2-conservative over the corresponding local reflection principle. This bears some corollaries on the hierarchies of restricted induction schemata in arithmetic and provides a key tool for our generalization of Schmerl's theorem. (shrink)

One of the most fundamental questions in the philosophy of mathematics concerns the relation between truth and formal proof. The position according to which the two concepts are the same is called deflationism, and the opposing viewpoint substantialism. In an important result of mathematical logic, Kurt Gödel proved in his first incompleteness theorem that all consistent formal systems containing arithmetic include sentences that can neither be proved nor disproved within that system. However, such undecidable Gödel sentences can be established (...) to be true once we expand the formal system with Alfred Tarski s semantical theory of truth, as shown by Stewart Shapiro and Jeffrey Ketland in their semantical arguments for the substantiality of truth. According to them, in Gödel sentences we have an explicit case of true but unprovable sentences, and hence deflationism is refuted. -/- Against that, Neil Tennant has shown that instead of Tarskian truth we can expand the formal system with a soundness principle, according to which all provable sentences are assertable, and the assertability of Gödel sentences follows. This way, the relevant question is not whether we can establish the truth of Gödel sentences, but whether Tarskian truth is a more plausible expansion than a soundness principle. In this work I will argue that this problem is best approached once we think of mathematics as the full human phenomenon, and not just consisting of formal systems. When pre-formal mathematical thinking is included in our account, we see that Tarskian truth is in fact not an expansion at all. I claim that what proof is to formal mathematics, truth is to pre-formal thinking, and the Tarskian account of semantical truth mirrors this relation accurately. -/- However, the introduction of pre-formal mathematics is vulnerable to the deflationist counterargument that while existing in practice, pre-formal thinking could still be philosophically superfluous if it does not refer to anything objective. Against this, I argue that all truly deflationist philosophical theories lead to arbitrariness of mathematics. In all other philosophical accounts of mathematics there is room for a reference of the pre-formal mathematics, and the expansion of Tarkian truth can be made naturally. Hence, if we reject the arbitrariness of mathematics, I argue in this work, we must accept the substantiality of truth. Related subjects such as neo-Fregeanism will also be covered, and shown not to change the need for Tarskian truth. -/- The only remaining route for the deflationist is to change the underlying logic so that our formal languages can include their own truth predicates, which Tarski showed to be impossible for classical first-order languages. With such logics we would have no need to expand the formal systems, and the above argument would fail. From the alternative approaches, in this work I focus mostly on the Independence Friendly (IF) logic of Jaakko Hintikka and Gabriel Sandu. Hintikka has claimed that an IF language can include its own adequate truth predicate. I argue that while this is indeed the case, we cannot recognize the truth predicate as such within the same IF language, and the need for Tarskian truth remains. In addition to IF logic, also second-order logic and Saul Kripke s approach using Kleenean logic will be shown to fail in a similar fashion. (shrink)

Charles Peirce’s alpha system \ is reformulated into a deep inference system where the rules are given in terms of deep graphical structures and each rule has its symmetrical rule in the system. The proof analysis of \ is given in terms of two embedding theorems: the system \ and Brünnler’s deep inference system for classical propositional logic can be embedded into each other; and the system \ and Gentzen sequent calculus \ can be embedded into each other.

This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od of the system O of ordinal diagrams in Arai 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.

The impossibility results in judgement aggregation show a clash between fair aggregation procedures and rational collective outcomes. In this paper, we are interested in analysing the notion of rational outcome by proposing a proof-theoretical understanding of collective rationality. In particular, we use the analysis of proofs and inferences provided by linear logic in order to define a fine-grained notion of group reasoning that allows for studying collective rationality with respect to a number of logics. We analyse the well-known paradoxes (...) in judgement aggregation and we pinpoint the reasoning steps that trigger the inconsistencies. Moreover, we extend the map of possibility and impossibility results in judgement aggregation by discussing the case of substructural logics. In particular, we show that there exist fragments of linear logic for which general possibility results can be obtained. (shrink)

By a result of Paris and Friedman, the collection axiom schema for $\Sigma_{n+1}$ formulas, $B\Sigma_{n+1}$, is $\Pi_{n+2}$ conservative over $I\Sigma_n$. We give a new proof-theoretic proof of this theorem, which is based on a reduction of $B\Sigma_n$ to a version of collection rule and a subsequent analysis of this rule via Herbrand's theorem. A generalization of this method allows us to improve known results on reflection principles for $B\Sigma_n$ and to answer some technical questions left open by Sieg (...) [23] and Hájek [9]. We also give a new proof of independence of $B\Sigma_{n+1}$ over $I\Sigma_n$ by a direct recursion-theoretic argument and answer an open problem formulated by Gaifman and Dimitracopoulos [8]. (shrink)

This paper is dedicated to the memory of Mike Dunn. His untimely death is a loss not only to logic, computer science, and philosophy, but to all of us who knew and loved him. The paper gives an argument for closure under γ in standard systems of relevance logic (first proved by Meyer and Dunn 1969). For definiteness, I chose the example of R. The proof also applies to E and to the quantified systems RQ and EQ. The argument (...) uses semantic tableaux (with one exceptional rule not satisfying the subformula property). It avoids the previous arguments’ use of cutting down inconsistent sets of formulas to consistent sets. Like all tableau arguments, it extends partial valuations to total valuations. (shrink)

Quantum theory predicts that, e.g., in a Stern-Gerlach experiment with electrons the measured spin component $S_Z = \pm \frac{1}{2}$ does not come about by an adjustment at the last moment, a forced “flipping” or “tilting” of the spin (vector), which would imply z-angular momentum exchange between particle and instrument, but will afterward appear to have had the value $\frac{1}{2} or - \frac{1}{2}$ already before the measurement. Because an electron spin cannot have components $ \pm \frac{1}{2}$ in all directions at the (...) same time, the measuring direction has a “privileged” status before the measurement, however we choose that direction, which implies a retroactive effect. A second proof of retroactivity is derived from a special case of the paradox of Einstein, Podolsky, and Rosen. It is strongly suggested by our result that, in essential respects, both Bohr and Einstein were right in their famous controversy about determinism and considering microprocesses “as a whole.”. (shrink)

The mathematical practice of proving theorems seems clearly to result in improved mathematical understanding; the aim of proving, and reproving, theorems in mathematics is better understanding. And yet, as is by now well known, fully formalized mathematical proofs are usually unintelligible; they do not advance our mathematical understanding. How, then, should we understand the relationship between proving theorems and advancing our mathematical understanding? I argue that, first, we need a different notion of (formal) proof, one that does not take (...) form to be opposed to con­tent. Eighteenth century algebraic proof provides an example of fully rigorous and fully contentful mathematical proof, and in this case one can see how mathematical proof might provide mathematical understanding. The task is to extrapolate the insights gained from this case to the sort of deductive reasoning from concepts that has been the norm in mathematical practice since the nineteenth century. (shrink)

By the middle of the seventeenth century we that find that algebra is able to offer proofs in its own right. That is, by that time algebraic argument had achieved the status of proof. How did this transformation come about?

In Feferman’s work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin–Löf type theory and constructive Zermelo–Fraenkel set theory. Proof theory has contributed to a deeper grasp of the relationship between different frameworks for constructive mathematics. Some of the reductions are known only through ordinal-theoretic characterizations. The paper also addresses the strength of Voevodsky’s univalence axiom. A further goal is to investigate the strength of (...) intuitionistic theories of generalized inductive definitions in the framework of intuitionistic explicit mathematics that lie beyond the reach of Martin–Löf type theory. (shrink)

The paper proposes a semantic value for the logical constants (connectives and quantifiers) within the framework of proof-theoretic semantics, basic meaning on the introduction rules of a meaning conferring natural deduction proof system. The semantic value is defined based on Fregecontributions” to sentential meanings as determined by the function-argument structure as induced by a type-logical grammar. In doing so, the paper proposes a novel proof-theoretic interpretation of the semantic types, traditionally interpreted in Henkin models. The compositionality of (...) the resulting attribution of semantic values is discussed. Elsewhere, the same method was used for defining proof-theoretic meaning of subsentential phrases in a fragment of natural language. Doing the same for (the simpler and clearer case of) logic sheds more light on the proposal. (shrink)

This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.

Responsible Research and Innovation (RRI) is described as a new way of doing science that brings science closer to society. Based on a qualitatively oriented case study, this article supports previous research indicating that researchers face a variety of ethical problems and dilemmas when implementing RRI for the first time. These include difficulties with anticipating and controlling future impacts, an asymmetry of power between project partners and an elusive understanding of the RRI concept. The researchers’ challenges were rooted in conventional (...) research ethics and could be boiled down to one core dilemma: If RRI had been applied from the very beginning of the project period, the chance of realising proof of concept within the scheduled time may decrease. The researchers’ solution to this dilemma was to prioritize proof of concept and postpone RRI activities to later stages of the project. If RRI is expected to live up to its ambition of representing a new way of doing science, more effort is needed at the political level to facilitate change. (shrink)

A cut-free Gentzen sequent calculus for Ewald’s intuitionistic tense logic \ is established. By the proof-theoretic method, we prove that, for every set of strictly positive implications S, the classical tense logic \ is embedded into its intuitionistic analogue \ via Kolmogorov, Gödel–Genzten and Kuroda translations respectively. A sufficient and necessary condition for Glivenko type theorem in tense logics is established.

This contribution defends two claims. The first is about why thought experiments are so relevant and powerful in mathematics. Heuristics and proof are not strictly and, therefore, the relevance of thought experiments is not contained to heuristics. The main argument is based on a semiotic analysis of how mathematics works with signs. Seen in this way, formal symbols do not eliminate thought experiments (replacing them by something rigorous), but rather provide a new stage for them. The formal world resembles (...) the empirical world in that it calls for exploration and offers surprises. This presents a major reason why thought experiments occur both in empirical sciences and in mathematics. The second claim is about a looming aporia that signals the limitation of thought experiments. This aporia arises when mathematical arguments cease to be fully accessible, thus violating a precondition for experimenting in thought. The contribution focuses on the work of Vladimir Voevodsky (1966–2017, Fields medalist in 2002) who argued that even very pure branches of mathematics cannot avoid inaccessibility of proof. Furthermore, he suggested that computer verification is a feasible path forward, but only if proof is not modeled in terms of formal logic. (shrink)

The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main (...) features of display calculi, a proof-theoretic paradigm that has been successfully employed to give a proof-theoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced proof-theoretic semantic principles. The contributions of the present article include a generalization of Belnap's cut-elimination metatheorem for display calculi, and a revised version of the display-style calculus D.EAK. We verify that the revised version satisfies the previously mentioned proof-theoretic semantic principles, and show that it enjoys cut-elimination as a consequence of the generalized metatheorem. (shrink)

In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn of degree (...) n. Cheney's proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL . The result of our analysis provides the first effective uniform modulus of uniqueness . Moreover, the extracted modulus has the optimal ε-dependency as follows from Kroó 331). The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed fC[0,1] with arbitrary precision. The second author uses this result to give a complexity upper bound on the computation of the best L1-approximation in Oliva 66–77). (shrink)

In procedural-law scholarship as well as in the theoretical analysis of the notion of proof as a result of the joint assessment of all items of evidence introduced in a trial, reference is frequently made to notions such as the conviction, belief, or certainty of a judge or a jury member about what happened. All these notions underscore the mental states involved in the process of determining the facts on the part of a judge or a jury. In this (...) analysis, I look at the links between beliefs and the justification in the findings of fact provided by the judge or jury in her or its verdict. (shrink)

We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.

The completeness of the modal logic S4 for all topological spaces as well as for the real line , the n-dimensional Euclidean space and the segment etc. was proved by McKinsey and Tarski in 1944. Several simplified proofs contain gaps. A new proof presented here combines the ideas published later by G. Mints and M. Aiello, J. van Benthem, G. Bezhanishvili with a further simplification. The proof strategy is to embed a finite rooted Kripke structure for S4 into (...) a subspace of the Cantor space which in turn encodes . This provides an open and continuous map from onto the topological space corresponding to . The completeness follows as S4 is complete with respect to the class of all finite rooted Kripke structures. (shrink)

Constructive mathematics is based on the thesis that the meaning of a mathematical formula is given, not by its truth-conditions, but in terms of what constructions count as a proof of it. However, the meaning of the terms 'construction' and 'proof' has never been adequately explained (although Kreisel, Goodman and Martin-Löf have attempted axiomatisations). This monograph develops precise (though not wholly formal) definitions of construction and proof, and describes the algorithmic substructure underlying intuitionistic logic. Interpretations of Heyting (...) arithmetic and constructive analysis are given. The philosophical basis of constructivism is explored thoroughly in Part I. The author seeks to answer objections from platonists and to reconcile his position with the central insights of Hilbert's formalism and logic. Audience: Philosophers of mathematics and logicians, both academic and graduate students, particularly those interested in Brouwer and Hilbert; theoretical computer scientists interested in the foundations of functional programming languages and program correctness calculi. (shrink)

We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley–Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities such as AB=I→BA=I.

In lieu of an abstract, here is a brief excerpt of the content:Proof and Persuasion in the Philosophical Debate about AbortionChris KaposyPhilosophers involved in debating the abortion issue often assume that the arguments they provide can offer decisive resolution.1 Arguments on the prolife side of the debate, for example, usually imply that it is rationally mandatory to view the fetus as having a right to life, or full moral standing.2 Such an account assumes that philosophical argument can compel the (...) reader to see the fetus in a certain way and that dissent risks irrationality.I wish to question this image of the use of philosophical argument in the abortion debate. I focus on the question of fetal moral standing, which is one of the subproblems in the debate. I am especially concerned with prolife arguments for fetal moral standing, since the prolife side must argue for a position that is compulsory. The prochoice side, in contrast, typically holds that people are entitled to believe what they want about the fetus’s moral standing.My position is that philosophical arguments should be understood as tools for persuasion in the abortion debate rather than as a method for discovering decisive proofs about the morality of abortion. I argue that because any one position on the moral standing of fetuses cannot be established decisively, law and policy should favour the prochoice position. In support of these conclusions, I present two common argumentative strategies used to suggest that the prolife view of the fetus is rationally [End Page 139] mandatory, and I illustrate why arguments involving these strategies do not compel us to view the fetus as having full moral standing.Framing the IssueIn order to show that abortion is wrong (in cases in which it is considered wrong), one must first establish that fetuses have full moral standing.3 It is a serious moral wrong to take the life of someone with full moral standing—this is part of what it means to have this status. The possessor of full moral standing is entitled to have his or her life protected. If abortion is wrong, then the fetus must have full moral standing, because without such standing, killing a fetus could be justified by the pregnant woman’s strong interest in ending an unwanted pregnancy. Those arguing against the moral permissibility of abortion must show that it is mandatory (in some way) to view the fetus as having full moral standing. There are a range of positions one could take with regard to the fetus’s status, from viewing the fetus as an incipient organism with no moral standing to seeing the fetus as gaining moral standing as the pregnancy progresses. But if it is mandatory to view the fetus as having full moral standing, all other positions must then be mistaken, incorrect, or somehow unjustified.This paper analyzes why philosophers opposed to abortion think it is mandatory to attribute full moral standing to fetuses. There are two popular argumentative strategies offering different accounts of the source of this obligation. The first strategy suggests that fetal full moral standing derives from morally relevant facts about the fetus. According to this line of argument, we are rationally obligated to view the fetus as having full moral standing because we cannot deny (without courting irrationality) that there are properties, characteristics, or attributes of the fetus that entitle it to this status.The second strategy is to claim that the fetus has full moral standing because this position is most consistent with our intuitions in cases unrelated to abortion. Philosophers taking this approach are fond of analogies comparing fetuses to comatose adults or to people at the end of life, for example. This strategy of appealing to your interlocutor’s sense of consistency I call the “shared-value” strategy.The two strategies map very well onto the distinction some have made between argumentum ad rem and argumentum ad hominem. The philosopher of rhetoric Henry Johnstone Jr. draws this distinction in very clear terms, and others in the history of philosophy make note of the difference [End Page 140] between these two types of arguments as well.4 The appeal to the facts (or argumentum ad rem) seeks to establish the truth of its... (shrink)

We show that the existence of a weakly compact cardinal over the Zermelo–Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.

This paper explores the interface between principles of self-applicable truth and classical logic. To this end, the proof-theoretic strength of a number of axiomatic theories of truth over intuitionistic logic is determined. The theories considered correspond to the maximal consistent collections of fifteen truth-theoretic principles as isolated in Leigh and Rathjen.

This paper investigates an important aspect of mathematical practice: that proof is required for a finished piece of mathematics. If follows that non-deductive arguments — however convincing — are never sufficient. I explore four aspects of mathematical research that have facilitated the impressive success of the discipline. These I call the Practical Virtues: Permanence, Reliability, Autonomy, and Consensus. I then argue that permitting results to become established on the basis of non-deductive evidence alone would lead to their deterioration. This (...) furnishes us with a partial rational justification for mathematicians strict insistence on proof. (shrink)

We show that the consistency of the first order arithmetic $PA$ follows from the pointwise induction up to the Howard ordinal. Our proof differs from U. Schmerl [Sc]: We do not need Girard's Hierarchy Comparison Theorem. A modification on the ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down $\alpha\mapsto\alpha [1]$ in ordinals. Also a generalization to theories $ID_q$ of finitely iterated inductive definitions is (...) proved. (shrink)

We obtain an equivalent implicit characterization of Lp Banach spaces that is amenable to a logical treatment. Using that, we obtain an axiomatization for such spaces into a higher order logical system, the kind of which is used in proof mining, a research program that aims to obtain the hidden computational content of mathematical proofs using tools from mathematical logic. As an aside, we obtain a concrete way of formalizing Lp spaces in positive-bounded logic. The axiomatization is followed by (...) a corresponding metatheorem in the style of proof mining. We illustrate its use with the derivation for this class of spaces of the standard modulus of uniform convexity. (shrink)

We present a setting in which the search for a proof of B or a refutation of B can be carried out simultaneously: in contrast, the usual approach in automated deduction views proving B or proving ¬B as two, possibly unrelated, activities. Our approach to proof and refutation is described as a two-player game in which each player follows the same rules. A winning strategy translates to a proof of the formula and a counter-winning strategy translates to (...) a refutation of the formula. The game is described for multiplicative and additive linear logic. A game theoretic treatment of the multiplicative connectives is intricate and our approach to it involves two important ingredients. First, labeled graph structures are used to represent positions in a game and, second, the game playing must deal with the failure of a given player and with an appropriate resumption of play. This latter ingredient accounts for the fact that neither player might win. (shrink)

In this paper it is exactly proved that the standard transformations of the three-dimensional (3D) vectors of the electric and magnetic fields E and B are not relativistically correct transformations. Thence the 3D vectors E and B are not well-defined quantities in the 4D space-time and, contrary to the general belief, the usual Maxwell equations with the 3D E and B are not in agreement with the special relativity. The 4-vectors E a and B a , as well-defined 4D quantities, (...) are introduced instead of ill-defined 3D E and B. The proof is given in the tensor and the Clifford algebra formalisms. (shrink)

The present paper aims to show that the reconstruction of the formal framework of the proofs in Pr. An. 1.15, as proposed by Malink and Rosen 2013 (‘Proof by Assumption of the Possible in Prior Analytics 1.15’, Mind, 122, 953-85) is due to affront a double impasse. Malink and Rosen argue convincingly that Aristotle operates with two different modal frameworks, one as found in the system of modal logic presented in Prior Analytics 1.3 and 8-22, and one occurring in (...) many of Aristotle’s works, such as the Physics, De Caelo and the Metaphysics. However, they misconstrue the latter framework. More precisely, they misconstrue the domain of significance of what they call the ‘Principle of Necessitation’. As a consequence, bringing the two frameworks into one results into a contradictory modal logic. On the other hand, if the Principle of Necessitation is rectified, the proofs put forward by Malink and Rosen in the same paper are no longer available. (shrink)

Complex frameworks for defining programming languages aim to generate various tools (e.g. interpreters, symbolic execution engines, deductive verifiers, etc.) using only the formal definition of a language. When used at an industrial scale, these tools are constantly updated, and at the same time, it is required to be trustworthy. Ensuring the correctness of such a framework is practically impossible. A solution is to generate proof objects as correctness artefacts that can be checked by an external trusted checker. A logic (...) suitable for developing such frameworks is matching logic. K framework is a canonical example having matching logic-based foundation. Since the (symbolic) configurations of the programs are represented by matching logic patterns, the algorithms computing the dynamics of these configurations can be seen as pattern transformers and a proof object should be generated for the relationship between these patterns. In this paper, we show that conjunctions and disjunctions of patterns, produced by semantics or analysis rules, can be safely normalized using unification and antiunification algorithms. We also provide a prototype implementation of our proof object generation technique and a checker for certifying the generated objects. (shrink)

The present article proceeds from the mainstream view that the conceptual framework underpinning adversarial systems of criminal adjudication, i.e. a mixture of common-sense philosophy and probabilistic analysis, is unsustainable. In order to provide fact-finders with an operable structure of justification, we need to turn to epistemology once again. The article proceeds in three parts. First, I examine the structural features of justification and how various theories have attempted to overcome Agrippa’s trilemma. Second, I put Inferential Contextualism to the test and (...) show that a defeasible structure of justification allocating epistemic rights and duties to all participants of an inquiry manages to dissolve the problem of scepticism. Third, I show that our epistemic practice already embodies a contextualist mechanism. Our problem was not that our Standard of Proof is inoperable but that it was not adequately conceptualized. Contextualism provides the framework to articulate the abovementioned practice and to treat ‘reasonable doubts’ as a mechanism which we can now describe in detail. The seemingly insurmountable problem with our efforts to define the concept “reasonable doubts” was the fact that we have been conflating the surface features of this mechanism and its internal structure, i.e. the rules for its use. (shrink)

This chapter contains section titled: Matter in the World Extension as a Property of Matter “Body” in the Meditations Body as Non‐Mind Basic Concepts A Proof of the Existence of Bodies Cartesian Limitations.

Among his other contributions to advancing our understanding of classical American pragmatism and, in particular, Charles S. Peirce, none is more worthy of our attention than Richard S. Robin's characteristically painstaking attempt to address the puzzle of Peirce's "Proof" of pragmaticism.1 In this as in so many other respects,2 he shows himself to be, in effect, the student of Max H. Fisch (see especially 1986, chapter 19).3 There are hermeneutical traditions as well as philosophical ones and often the former (...) are integral parts of the latter. This is certainly the case regarding pragmatism. A deeper or better understanding of the inaugural figures in this philosophical movement is taken, by the interpreters of.. (shrink)

We give a reading of binary necessity statements of the form “ϕ is necessary for ψ” in terms of proofs. This reading is based on the idea of interpreting such statements as “Every proof of ψ uses ϕ”.

In lieu of an abstract, here is a brief excerpt of the content:Proof and Persuasion in Black Athena:: The Case of K. O. MüllerJosine H. BlokNon tali auxilio.Virgil, Aeneid II, 521When in 1824 the German classical scholar Karl Otfried Müller (1797–1840) set down to write a review of Champollion’s first Letter to M. Dacier (1822), he was profoundly interested. 1 For several years he had been working on Egypt, and as he told his parents in 1820, “I have come (...) to love Egyptian antiquity so much, that, if I were not constricted by the schedule of my classes, I would have set myself to the decipherment of the hieroglyphs, which I would not deem impossible by the clues I have found.” 2 During the same years (1820–25) that he wrote his early books on ancient Greece, he [End Page 705] reviewed sixteen studies on Egypt alone. 3 In his review of the Letter, then, he wanted to draw “the attention of [the] readers to this, certainly not unfounded, discovery,” 4 though he feared the author was inclined to jump to conclusions. But in August 1824 he reviewed Champollion’s more complete publication of his findings of the same year and, recalling his previous anxiety, commented:Now, however, the reading of the present work has totally convinced me, that the usage of hieroglyphs to indicate sounds is as ancient as this writing system itself. [... This discovery should also mean that...] the history of Egyptian religion and state will be reconstructed and expanded. 5From that moment he sided unequivocally with Champollion, politely but clearly reminding German colleagues who still stumbled on with decipherments of their own, that this would not do. 6With these facts in mind, Martin Bernal’s rendering in his Black Athena, volume I, is bound to surprise: “[U]nlike Humboldt, Niebuhr and Bunsen [Müller] disregarded the sensational scholarly developments between 1815 and 1830. There is no indication that he paid any attention to Champollion’s decipherment” (316). The contradiction between Bernal’s statements and the sources on Müller’s life and work turns out not to be an incidental error but part of a larger pattern. To understand this pattern and its objectives, let me first summarize Bernal’s argument and my own.In his challenging book Bernal argues that the ancient Greek world was founded on the colonization of Greece by Phoenicians and Egyptians in the second millennium bc. 7 The material which is to prove his thesis is offered in volume II, though volume I includes a summary. In this first volume Bernal observes that from late antiquity until the eighteenth century, awareness of the Afroasiatic roots of ancient civilization had been retained as the heritage of ancient Greece itself. Hence Bernal labels this perception underlying Western classical scholarship of the early modern period the “Ancient Model.” By or soon after the 1820s, however, it was replaced by the “Aryan Model,” which took Greek civilization to be partly autochthonous and partly [End Page 706] shaped by invasions coming from the North. To reveal that the fall of the Ancient Model was not the result of internal developments in classical scholarship but of externalist influences, notably the belief in progress, the defense of Christianity, Romanticism, and most importantly racism, is the core theme of volume I. Bernal sustains his argument by contending that historical source criticism was not really or entirely an internal development but created to serve the external ends, and by presenting Müller as the embodiment of Romanticist racism, who was responsible for overthrowing the Ancient Model and inaugurating its Aryan successor. Hence, by thus designating Müller as the axis around which the overall turn of classical scholarship revolved, he wants to prove that the fall of the Ancient Model was unjustified in terms of scholarship but only occurred due to dishonorable ideologies.Through a limited number of representative issues I want to argue that Bernal’s rendering of Müller and the context of his work is untenable in the light of the source material and that Bernal’s explanation of the fall of the Ancient Model is untenable as well. My aim is not just to clear Müller’s name... (shrink)

I propose and defend a proof-based account of legal exceptions. The basic thought is that the characteristic behaviour of exceptions is to be explained in terms of the distinction, relative to some given decision-type C in some decision-making context, between two classes of relevant facts: those that may, and those that may not, remain uncertain if a token decision C is to count as correctly made. The former is the class of exceptions. A fact F is an exception relative (...) to some decision-type C, I claim, if (i) the ascertainment of F is sufficient for a token decision C not to count as correctly made, and (ii) the ascertainment of the negation of F is not necessary for a token decision C to count as correctly made. I also recuperate, reconstruct and discuss some of HLA Hart’s early views on defeasible judicial decisions. These two projects are closely connected: the latter is a vehicle for the former. (shrink)