A modified Young double-slit experiment proposed by Wootters and Zurek is considered in which a system P of parallel plates covered with a photographic emulsion has been set up in the region where we would normally expect the central interference fringes. Because under certain conditions P makes it possible to conclude with much more than50% certainty through which of the two slits each particular photon passed, the relevant interference pattern becomes blurred. It is proved that this implies a retroactive effect (...) because the setup of P and the interaction of photons with P appear to influence the momentum transferred to the photons by the edges of the slits at an earlier stage of the experiment. (shrink)

An introduction to writing proofs, presented through compelling mathematical statements with interesting elementary proofs. This book offers an introduction to the art and craft of proof-writing. The author, a leading research mathematician, presents a series of engaging and compelling mathematical statements with interesting elementary proofs. These proofs capture a wide range of topics, including number theory, combinatorics, graph theory, the theory of games, geometry, infinity, order theory, and real analysis. The goal is to show students and aspiring mathematicians how (...) to write proofs with elegance and precision. (shrink)

Sequent calculi constitute an interesting and important category of proof systems. They are much less known than axiomatic systems or natural deduction systems are, and they are much less known than they should be. Sequent calculi were designed as a theoretical framework for investigations of logical consequence, and they live up to the expectations completely as an abundant source of meta-logical results. The goal of this book is to provide a fairly comprehensive view of sequent calculi -- including a (...) wide range of variations. The focus is on sequent calculi for various non-classical logics, from intuitionistic logic to relevance logic, through linear and modal logics. A particular version of sequent calculi, the so-called consecution calculi, have seen important new developments in the last decade or so. The invention of new consecution calculi for various relevance logics allowed the last major open problem in the area of relevance logic to be solved positively: pure ticket entailment is decidable. An exposition of this result is included in chapter 9 together with further new decidability results (for less famous systems). A series of other results that were obtained by J. M. Dunn and me, or by me in the last decade or so, are also presented in various places in the book. Some of these results are slightly improved in their current presentation. Obviously, many calculi and several important theorems are not new. They are included here to ensure the completeness of the picture; their original formulations may be found in the referenced publications. This book contains very little about semantics, in general, and about the semantics of non-classical logic in particular. (shrink)

'Numbers and Proofs' presents a gentle introduction to the notion of proof to give the reader an understanding of how to decipher others' proofs as well as construct their own. Useful methods of proof are illustrated in the context of studying problems concerning mainly numbers (real, rational, complex and integers). An indispensable guide to all students of mathematics. Each proof is preceded by a discussion which is intended to show the reader the kind of thoughts they might (...) have before any attempt proof is made. Established proofs which the student is in a better position to follow then follow. Presented in the author's entertaining and informal style, and written to reflect the changing profile of students entering universities, this book will prove essential reading for all seeking an introduction to the notion of proof as well as giving a definitive guide to the more common forms. Stressing the importance of backing up "truths" found through experimentation, with logically sound and watertight arguments, it provides an ideal bridge to more complex undergraduate maths. (shrink)

Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed (...) as special cases of the cut-elimination theorems for intuitionistic logic. (shrink)

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)

Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’.This paper presents classical proof forests as a graphical proof formalism and investigates the (...) possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given.Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising. (shrink)

We present a proof for a conjecture previously formulated by Dzhafarov et al.. The conjecture specifies a measure for the degree of contextuality and a criterion for contextuality in a broad class of quantum systems. This class includes Leggett–Garg, EPR/Bell, and Klyachko–Can–Binicioglu–Shumovsky type systems as special cases. In a system of this class certain physical properties \ are measured in pairs \ \); every property enters in precisely two such pairs; and each measurement outcome is a binary random variable. (...) Denoting the measurement outcomes for a property \ in the two pairs it enters by \ and \, the pair of measurement outcomes for \ \) is \ \). Contextuality is defined as follows: one computes the minimal possible value \ for the sum of \ ) that is allowed by the individual distributions of \ and \; one computes the minimal possible value \ for the sum of \ across all possible couplings of the entire set of random variables \ in the system; and the system is considered contextual if \ ). This definition has its justification in the general approach dubbed Contextuality-by-Default, and it allows for measurement errors and signaling among the measured properties. The conjecture proved in this paper specifies the value of \ in terms of the distributions of the measurement outcomes \ \). (shrink)

We present some proof-theoretic results for the normal modal logic whose characteristic axiom is \. We present a sequent system for this logic and a hypersequent system for its first-order form and show that these are equivalent to Hilbert-style axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and first-order logical truth, respectively. We close by proving equivalences with a Fitch-style proof system for revision theory.

The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s manifestation argument (...) does not obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame (...) class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

Though pictures are often used to present mathematical arguments, they are not typically thought to be an acceptable means for presenting mathematical arguments rigorously. With respect to the proofs in the Elements in particular, the received view is that Euclid's reliance on geometric diagrams undermines his efforts to develop a gap-free deductive theory. The central difficulty concerns the generality of the theory. How can inferences made from a particular diagrams license general mathematical results? After surveying the history behind the received (...) view, this essay provides a contrary analysis by introducing a formal account of Euclid's proofs, termed Eu. Eu solves the puzzle of generality surrounding Euclid's arguments. It specifies what diagrams Euclid's diagrams are, in a precise formal sense, and defines generality-preserving proof rules in terms of them. After the central principles behind the formalization are laid out, its implications with respect to the question of what does and does not constitute a genuine picture proof are explored. (shrink)

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in (...) previous work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

The author analyzes proof and argumentation as a form of appeal to a scientific community with deep ethical meaning. He presents proof primarily as an effort to persuade a scientific community rather than a search for true knowledge, as an instrument by which responsibility is taken for the correctness of the thesis being proved, which usually originates in a sudden flash of insight.

The article presents a full proof‐theoretic semantics for natural deduction based on an extended inversion principle: the elimination rule for an operator q may invert the introduction rule for q, but also vice versa, the introduction rule for a connective q may invert the elimination rule for q. Such an inversion—extending Prawitz' concept of inversion—gives the following theorem: Inversion for two rules of operator q (intro rule, elim rule) exists iff a reduction of a maximum formula for q exists. (...) The inversion theorem is specified to two logics, Lambek calculus (LC) and intuitionistic linear logic (ILL), with four propositional connectives: two multiplicatives (implication and conjunction) and two additives (conjunction and disjunction), with two quantifiers and two modals. LC is defined by using elimination rules by composition. ILL is defined by using usual general elimination rules. Elimination rules by composition are an exciting alternative to general elimination rules; in some cases, they do not need permutations. (shrink)

__Language Proof and Logic_ is available as a physical book with the software included on CD and as a downloadable package of software plus the book in PDF format. The all-electronic version is available from Openproof at ggweb.stanford.edu._ The textbook/software package covers first-order language in a method appropriate for first and second courses in logic. An on-line grading services instantly grades solutions to hundred of computer exercises. It is designed to be used by philosophy instructors teaching a logic course (...) to undergraduates in philosophy, computer science, mathematics, and linguistics. Introductory material is presented in a systematic and accessible fashion. Advanced chapters include proofs of soundness and completeness for propositional and predicate logic, as well as an accessible sketch of Godel's first incompleteness theorem. The book is appropriate for a wide range of courses, from first logic courses for undergraduates to a first graduate logic course. The software package includes four programs: Tarski's World 5.0, a new version of the popular program that teaches the basic first-order language and its semantics; Fitch, a natural deduction proof environment for giving and checking first-order proofs; Boole, a program that facilitates the construction and checking of truth tables and related notions ; Submit, a program that allows students to submit exercises done with the above programs to the Grade Grinder, the automatic grading service. Grade reports are returned to the student and, if requested, to the student's instructor, eliminating the need for tedious checking of homework. All programs are available for Windows, Macintosh and Linux systems. Instructors do not need to use the programs themselves in order to be able to take advantage of their pedagogical value. More about the software can be found at lpl.stanford.edu. The price of a new text/software package includes one Registration ID, which must be used each time work is submitted to the grading service. Once activated, the Registration ID is not transferable. (shrink)

Proof complexity is a rich subject drawing on methods from logic, combinatorics, algebra and computer science. This self-contained book presents the basic concepts, classical results, current state of the art and possible future directions in the field. It stresses a view of proof complexity as a whole entity rather than a collection of various topics held together loosely by a few notions, and it favors more generalizable statements. Lower bounds for lengths of proofs, often regarded as the key (...) issue in proof complexity, are of course covered in detail. However, upper bounds are not neglected: this book also explores the relations between bounded arithmetic theories and proof systems and how they can be used to prove upper bounds on lengths of proofs and simulations among proof systems. It goes on to discuss topics that transcend specific proof systems, allowing for deeper understanding of the fundamental problems of the subject. (shrink)

We present a series of proof systems for exact entailment (i.e. relevant truthmaker preservation from premises to conclusion) and prove soundness and completeness. Using the proof systems, we observe that exact entailment is not only hyperintensional in the sense of Cresswell but also in the sense recently proposed by Odintsov and Wansing.

We present a complete and cut-free proof-system for a fragment of MTL, where modal operators are only labelled by bounded intervals with rational endpoints.

This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition.

An engaging and accessible introduction to mathematical proof incorporating ideas from real analysis A mathematical proof is an inferential argument for a mathematical statement. Since the time of the ancient Greek mathematicians, the proof has been a cornerstone of the science of mathematics. The goal of this book is to help students learn to follow and understand the function and structure of mathematical proof and to produce proofs of their own. An Introduction to Proof through (...) Real Analysis is based on course material developed and refined over thirty years by Professor Daniel J. Madden and was designed to function as a complete text for both first proofs and first analysis courses. Written in an engaging and accessible narrative style, this book systematically covers the basic techniques of proof writing, beginning with real numbers and progressing to logic, set theory, topology, and continuity. The book proceeds from natural numbers to rational numbers in a familiar way, and justifies the need for a rigorous definition of real numbers. The mathematical climax of the story it tells is the Intermediate Value Theorem, which justifies the notion that the real numbers are sufficient for solving all geometric problems. • Concentrates solely on designing proofs by placing instruction on proof writing on top of discussions of specific mathematical subjects • Departs from traditional guides to proofs by incorporating elements of both real analysis and algebraic representation • Written in an engaging narrative style to tell the story of proof and its meaning, function, and construction • Uses a particular mathematical idea as the focus of each type of proof presented • Developed from material that has been class-tested and fine-tuned over thirty years in university introductory courses An Introduction to Proof through Real Analysis is the ideal introductory text to proofs for second and third-year undergraduate mathematics students, especially those who have completed a calculus sequence, students learning real analysis for the first time, and those learning proofs for the first time. Daniel J. Madden, PhD, is an Associate Professor of Mathematics at The University of Arizona, Tucson, Arizona, USA. He has taught a junior level course introducing students to the idea of a rigorous proof based on real analysis almost every semester since 1990. Dr. Madden is the winner of the 2015 Southwest Section of the Mathematical Association of America Distinguished Teacher Award. Jason A. Aubrey, PhD, is Assistant Professor of Mathematics and Director, Mathematics Center of the University of Arizona. (shrink)

Mathematicians do not claim to know a proposition unless they think they possess a proof of it. For all their confidence in the truth of a proposition with weighty non-deductive support, they maintain that, strictly speaking, the proposition remains unknown until such time as someone has proved it. This article challenges this conception of knowledge, which is quasi-universal within mathematics. We present four arguments to the effect that non-deductive evidence can yield knowledge of a mathematical proposition. We also show (...) that some of what mathematicians take to be deductive knowledge is in fact non-deductive. 1 Introduction2 Why It Might Matter3 Two Further Examples and Preliminaries4 An Exclusive Epistemic Virtue of Proof?5 Analyses of Knowledge6 The Inductive Basis of Deduction7 Physical to Mathematical Linkages8 Conclusion. (shrink)

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.

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.

In this paper I shall present a method for proving determinacy from large cardinals which, in many cases, seems to yield optimal results. One of the main applications extends theorems of Martin, Steel and Woodin about determinacy within the projective hierarchy. The method can also be used to give a new proof of Woodin's theorem about determinacy in L.The reason we look for optimal determinacy proofs is not only vanity. Such proofs serve to tighten the connection between large cardinals (...) and descriptive set theory, letting us bring our knowledge of one subject to bear on the other, and thus increasing our understanding of both. A classic example of this is the Harrington-Martin proof that -determinacy implies -determinacy. This is an example of a transfer theorem, which assumes a certain determinacy hypothesis and proves a stronger one. While the statement of the theorem makes no mention of large cardinals, its proof goes through 0#, first proving that-determinacy ⇒ 0# exists,and then that0# exists ⇒ -determinacyMore recent examples of the connection between large cardinals and descriptive set theory include Steel's proof thatADL ⇒ HODL ⊨ GCH,see [9], and several results of Woodin about models of AD+, a strengthening of the axiom of determinacy AD which Woodin has introduced. These proofs not only use large cardinals, but also reveal a deep, structural connection between descriptive set theoretic notions and notions related to large cardinals. (shrink)

A self contained proof of Shelah's theorem is presented: If μ is a strong limit singular cardinal of uncountable cofinality and 2μ > μ+ then $\left( {\begin{array}{*{20}c} {\mu ^ + } \\ \mu \\ \end{array} } \right) \to \left( {\begin{array}{*{20}c} {\mu ^ + } \\ {\mu + 1} \\ \end{array} } \right)_{< cf\mu } $.

A famous theorem by van der Waerden states the following: Given any finite coloring of the integers, one color contains arbitrarily long arithmetic progressions. Equivalently, for every q,k, there is an N = N(q,k) such that for every q-coloring of an interval of length N one color contains a progression of length k. An obvious question is what is the growth rate of N = N(q,k). Some proofs, like van der Waerden's combinatorial argument, answer this question directly, while the topological (...) proof by Furstenberg and Weiss does not. We present an analysis of (Girard's variant of) Furstenberg and Weiss's proof based on monotone functional interpretation, both yielding bounds and providing a general illustration of proof mining in topological dynamics. The bounds do not improve previous results by Girard, but only—as is also revealed by the analysis—because the combinatorial proof and the topological dynamics proof in principle are identical. (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)

Proof Theory of Modal Logic is devoted to a thorough study of proof systems for modal logics, that is, logics of necessity, possibility, knowledge, belief, time, computations etc. It contains many new technical results and presentations of novel proof procedures. The volume is of immense importance for the interdisciplinary fields of logic, knowledge representation, and automated deduction.

Now in so far as it is recognized that the constituents of the environment are not present inside the body in the same way as they are present outside it, to that extent they are bound, the moment they are inside it, to become something essentially different from the environment.

We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the West (...) or the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic. (shrink)

A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.

This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{ the exact proof-theoretic ordinals of these systems are presented.

It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; (...) we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof. (shrink)

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)

This paper presents an analysis of the concept of burden of proof in argument. Relationship of burden of proof to three traditional informal fallacies is considered: (i) argumentum ad hominem, (ii) petitio principii, and (iii) argumentum ad ignorantiam. Other topics discussed include persuasive dialoque, pragmatic reasoning, legal burden of proof, plausible reasoning in regulated disputes, rules of dialogue, and the value of reasoned dialogue.

"Proof" has been and remains one of the concepts which characterises mathematics. Covering basic propositional and predicate logic as well as discussing axiom systems and formal proofs, the book seeks to explain what mathematicians understand by proofs and how they are communicated. The authors explore the principle techniques of direct and indirect proof including induction, existence and uniqueness proofs, proof by contradiction, constructive and non-constructive proofs, etc. Many examples from analysis and modern algebra are included. The exceptionally (...) clear style and presentation ensures that the book will be useful and enjoyable to those studying and interested in the notion of mathematical "proof.". (shrink)

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible to check (...) the correctness of a net in polynomial time, every correct net should be obtainable from a sequent calculus proof, and there should be a cut-elimination procedure which preserves correctness.Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley [22], the author presented a calculus of proof nets satisfying and ; the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of . That sequent calculus, called LK⁎LK⁎ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper [22]), we give a full proof of for expansion nets with respect to LK⁎LK⁎, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria. (shrink)

This book continues from where the authors' previous book, Structural Proof Theory, ended. It presents an extension of the methods of analysis of proofs in pure logic to elementary axiomatic systems and to what is known as philosophical logic. A self-contained brief introduction to the proof theory of pure logic is included that serves both the mathematically and philosophically oriented reader. The method is built up gradually, with examples drawn from theories of order, lattice theory and elementary geometry. (...) The aim is, in each of the examples, to help the reader grasp the combinatorial behaviour of an axiom system, which typically leads to decidability results. The last part presents, as an application and extension of all that precedes it, a proof-theoretical approach to the Kripke semantics of modal and related logics, with a great number of new results, providing essential reading for mathematical and philosophical logicians. (shrink)

Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four-valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro’s tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in a (...) previous work we presented a sequent system for TML with the cut-elimination property. Besides, in this same work, it was also presented a sound and complete natural deduction system for this logic. In the present article we continue with the study of TML under a proof-theoretic perspective. In the first place, we show that the natural deduction system that we introduced before admits a normalization theorem. In the second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced by A. V. Figallo and P. Landini, we define a decidable tableau system adequate to check validity in the logic TML. Finally, we provide a sound and complete tableau system for TML in the original language. These two tableau systems constitute new (proof-theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras. (shrink)

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.

The Four-Colour Theorem (4CT) proof, presented to the mathematical community in a pair of papers by Appel and Haken in the late 1970's, provoked a series of philosophical debates. Many conceptual points of these disputes still require some elucidation. After a brief presentation of the main ideas of Appel and Haken’s procedure for the proof and a reconstruction of Thomas Tymoczko’s argument for the novelty of 4CT’s proof, we shall formulate some questions regarding the connections between (...) the points raised by Tymoczko and some Wittgensteinian topics in the philosophy of mathematics such as the importance of the surveyability as a criterion for distinguishing mathematical proofs from empirical experiments. Our aim is to show that the “characteristic Wittgensteinian invention” (Mühlhölzer 2006) – the strong distinction between proofs and experiments – can shed some light in the conceptual confusions surrounding the Four-Colour Theorem. (shrink)

Modern insolubility proofs of the measurement problem in quantum mechanics not only differ in their complexity and degree of generality, but also reveal a lack of agreement concerning the fundamental question of what constitutes such a proof. A systematic reworking of the (incomplete) 1970 Fine theorem is presented, which is intended to go some way toward clarifying the issue.

In this paper we describe a novel approach to defining an ontologically fundamental notion of co-presentness that does not go against the tenets of relativity theory. We survey the possible reactions to the problem of the present in relativity theory, introducing a terminological distinction between a static role of the present, which is served by the relation of simultaneity, and a dynamic role of the present, with the corresponding relation of co-presentness. We argue that both of these relations need to (...) be equivalence relations, but they need not coincide. Simultaneity, the sharing of a temporal coordinate, need not have fundamental ontological import, so that a relativizing strategy with respect to simultaneity seems promising. The notion of co-presentness, on the other hand, does have ontological import, and can therefore not be relativized to an observer or to an arbitrarily chosen frame. We argue that a formal representation of indeterminism can provide the structure needed to anchor the relation of co-presentness, and that this addition is in fact congenial to the notion of dynamic time as requiring real change. The resulting picture is one of an extended dynamic present, implying a formal distinction between static simultaneity and dynamic co-presentness. After working out the basics of our approach in the simpler framework of branching time, we provide our full analysis in the framework of branching space-times, which allows for a formal definition of modal correlations. The spatial extension of the dynamic present can reach as far as the modal correlations do. In the limit, the dynamic present could extend across a maximal space-like hypersurface. (shrink)

The Hegel Lectures Series Series Editor: Peter C. Hodgson Hegel's lectures have had as great a historical impact as the works he himself published. Important elements of his system are elaborated only in the lectures, especially those given in Berlin during the last decade of his life. The original editors conflated materials from different sources and dates, obscuring the development and logic of Hegel's thought. The Hegel Lectures series is based on a selection of extant and recently discovered transcripts and (...) manuscripts. Lectures from specific years are reconstructed so that the structure of Hegel's argument can be followed. Each volume presents an accurate new translation accompanied by an editorial introduction and annotations on the text, which make possible the identification of Hegel's many allusions and sources. Lectures on the Proofs of the Existence of God Hegel lectured on the proofs of the existence of God as a separate topic in 1829. He also discussed the proofs in the context of his lectures on the philosophy of religion (1821-31), where the different types of proofs were considered mostly in relation to specific religions. The text that he prepared for his lectures in 1829 was a fully formulated manuscript and appears to have been the first draft of a work that he intended to publish and for which he signed a contract shortly before his death in 1831. The 16 lectures include an introduction to the problem of the proofs and a detailed discussion of the cosmological proof. Philipp Marheineke published these lectures in 1832 as an appendix to the lectures on the philosophy of religion, together with an earlier manuscript fragment on the cosmological proof and the treatment of the teleological and ontological proofs as found in the 1831 philosophy of religion lectures. Hegel's 1829 lectures on the proofs are of particular importance because they represent what he actually wrote as distinct from auditors' transcriptions of oral lectures. Moreover, they come late in his career and offer his final and most seasoned thinking on a topic of obvious significance to him, that of the reality status of God and ways of knowing God. These materials show how Hegel conceived the connection between the cosmological, teleological, and ontological proofs. All of this material has been newly translated by Peter C. Hodgson from the German critical editions by Walter Jaeschke. This edition includes an editorial introduction, annotations on the text, and a glossary and bibliography. (shrink)

Contact relations have been studied in the context of qualitative geometry and physics since the early 1920s, and have recently received attention in qualitative spatial reasoning. In this paper, we present a sound and complete proof system in the style of Rasiowa and Sikorski (1963) for relation algebras generated by a contact relation.

This article investigates the proof theory of the Quantified Argument Calculus as developed and systematically studied by Hanoch Ben-Yami [3, 4]. Ben-Yami makes use of natural deduction, we, however, have chosen a sequent calculus presentation, which allows for the proofs of a multitude of significant meta-theoretic results with minor modifications to the Gentzen’s original framework, i.e., LK. As will be made clear in course of the article LK-Quarc will enjoy cut elimination and its corollaries.

We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version (...) à la Tarski and à la Russell are shown to be the same. (shrink)

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory (...) of finite-valued first order logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)