Finding Missing Proofs with Automated Reasoning

This article features long-sought proofs with intriguing properties (such as the absence of double negation and the avoidance of lemmas that appeared to be indispensable), and it features the automated methods for finding them. The theorems of concern are taken from various areas of logic that include two-valued sentential (or propositional) calculus and infinite-valued sentential calculus. Many of the proofs (in effect) answer questions that had remained open for decades, questions focusing on axiomatic proofs. The approaches we take are of added interest in that all rely heavily on the use of a single program that offers logical reasoning, William McCune's automated reasoning program OTTER. The nature of the successes and approaches suggests that this program offers researchers a valuable automated assistant. This article has three main components. First, in view of the interdisciplinary nature of the audience, we discuss the means for using the program in question (OTTER), which flags, parameters, and lists have which effects, and how the proofs it finds are easily read. Second, because of the variety of proofs that we have found and their significance, we discuss them in a manner that permits comparison with the literature. Among those proofs, we offer a proof shorter than that given by Meredith and Prior in their treatment of ukasiewicz's shortest single axiom for the implicational fragment of two-valued sentential calculus, and we offer a proof for the ukasiewicz 23-letter single axiom for the full calculus. Third, with the intent of producing a fruitful dialogue, we pose questions concerning the properties of proofs and, even more pressing, invite questions similar to those this article answers.     

A simple and general method of solving the finite axiomatizability problems for Lambek's syntactic calculi

In [4], I proved that the product-free fragment L of Lambek's syntactic calculus (cf. Lambek [2]) is not finitely axiomatizable if the only rule of inference admitted is Lambek's cut-rule. The proof (which is rather complicated and roundabout) was subsequently adapted by Kandulski [1] to the non-associative variant NL of L (cf. Lambek [3]). It turns out, however, that there exists an extremely simple method of non-finite-axiomatizability proofs which works uniformly for different subsystems of L (in particular, for NL). We present it below to the use of those who refer to the results of [1] and [4].     

On the Proof Theory of the Modal mu-Calculus

We study the proof-theoretic relationship between two deductive systems for the modal mu-calculus. First we recall an infinitary system which contains an omega rule allowing to derive the truth of a greatest fixed point from the truth of each of its (infinitely many) approximations. Then we recall a second infinitary calculus which is based on non-well-founded trees. In this system proofs are finitely branching but may contain infinite branches as long as some greatest fixed point is unfolded infinitely often along every branch. The main contribution of our paper is a translation from proofs in the first system to proofs in the second system. Completeness of the second system then follows from completeness of the first, and a new proof of the finite model property also follows as a corollary. Presented by Heinrich Wansing     

Manifest Invalidity: Neil Tennant's New Argument for Intuitionism

In Chapter 7 of The Taming of the True, Neil Tennant provides a new argument from Michael Dummett's ``manifestation requirement' to the incorrectness of classical logic and the correctness of intuitionistic logic. I show that Tennant's new argument is only valid if one interprets crucial existence claims occurring in the proof in the manner of intuitionists. If one interprets the existence claims as a classical logician would, then one can accept Tennant's premises while rejecting his conclusion of logical revision. Thus, Tennant has provided no evidence that should convince anyone who is not already an intuitionist. Since his proof is a proof for the correctness of intuitionism, it begs the question.     

Syntactic features and synonymy relations: a unified treatment of some proofs of the compactness and interpolation theorems

This paper introduces the notion of syntactic feature to provide a unified treatment of earlier model theoretic proofs of both the compactness and interpolation theorems for a variety of two valued logics including sentential logic, first order logic, and a family of modal sentential logic includingM,B,S ₄ andS ₅. The compactness papers focused on providing a proof of the consequence formulation which exhibited the appropriate finite subset. A unified presentation of these proofs is given by isolating their essential feature and presenting it as an abstract principle about syntactic features. The interpolation papers focused on exhibiting the interpolant. A unified presentation of these proofs is given by isolating their essential feature and presenting it as a second abstract principle about syntactic features. This second principle reduces the problem of exhibiting the interpolant to that of establishing the existence of a family of syntactic features satisfying certain conditions. The existence of such features is established for a variety of logics (including those mentioned above) by purely combinatorial arguments.Presented byMelvin Fitting     

On Modal <Emphasis Type="Italic">μ</Emphasis>-Calculus and Gödel-Löb Logic

We show that the modal μ-calculus over GL collapses to the modal fragment by showing that the fixpoint formula is reached after two iterations and answer to a question posed by van Benthem in [4]. Further, we introduce the modal μ ^~-calculus by allowing fixpoint constructors for any formula where the fixpoint variable appears guarded but not necessarily positive and show that this calculus over GL collapses to the modal fragment, too. The latter result allows us a new proof of the de Jongh, Sambin Theorem and provides a simple algorithm to construct the fixpoint formula. Presented by Melvin Fitting     

Group Cancellation and Resolution

We establish a connection between the geometric methods developed in the combinatorial theory of small cancellation and the propositional resolution calculus. We define a precise correspondence between resolution proofs in logic and diagrams in small cancellation theory, and as a consequence, we derive that a resolution proof is a 2-dimensional process. The isoperimetric function defined on diagrams corresponds to the length of resolution proofs.     

On Reduction Systems Equivalent to The Lambek Calculus with the Empty String

The paper continues a series of results on cut-rule axiomatizability of the Lambek calculus. It provides a complete solution of a problem which was solved partially in one of the author's earlier papers. It is proved that the product-free Lambek Calculus with the empty string (L ₀) is not finitely axiomatizable if the only rule of inference admitted is Lambek's cut rule. The proof makes use of the (infinitely) cut-rule axiomatized calculus C designed by the author exactly for this purpose.     

THE LOST LEGACY OF ANSELM'S ARGUMENT: RE‐THINKING THE PURPOSE OF PROOFS FOR THE EXISTENCE OF GOD

In his Proslogion, Anselm presents a proof for God's existence which has attracted a tremendous amount of scholarly attention. In spite of all that has been said about this proof and proofs for God's existence more generally, scholarly consensus seems to dissipate when it comes to determining whether theistic proofs are persuasive and sound. In this article, I will argue that there is a way to provide compelling proof for the existence of God. To substantiate this claim, I will not attempt to prove that God exists apart from His revelation in any of the ways that have been advocated by various philosophers of religion. Rather, I will endeavor to explain that Anselm's approach to offering evidence for God's existence is quite different from the approach that modern philosophers tend to attribute to him and to elaborate on what that approach involves by reading Anselm's argument in the context of Augustine's De Trinitate and the whole of the Proslogion.     

A Sequent Calculus for a Negative Free Logic

This article presents a sequent calculus for a negative free logic with identity, called N. The main theorem (in part 1) is the admissibility of the Cut-rule. The second part of this essay is devoted to proofs of soundness, compactness and completeness of N relative to a standard semantics for negative free logic.     

Using logical relevance for question answering

We propose a novel method of determining the appropriateness of an answer to a question through a proof of logical relevance rather than a logical proof of truth. We define logical relevance as the idea that answers should not be considered as absolutely true or false in relation to a question, but should be considered true more flexibly in a sliding scale of aptness. This enables us to reason rigorously about the appropriateness of an answer even in cases where the sources we are getting answers from are incomplete or inconsistent or contain errors. We show how logical relevance can be implemented through the use of measured simplification, a form of constraint relaxation, in order to seek a logical proof than an answer is in fact an answer to a particular question. We then give an example of such an implementation providing a set of specific rules for this purpose.     

Truth as an Epistemic Notion

What is the appropriate notion of truth for sentences whose meanings are understood in epistemic terms such as proof or ground for an assertion? It seems that the truth of such sentences has to be identified with the existence of proofs or grounds, and the main issue is whether this existence is to be understood in a temporal sense as meaning that we have actually found a proof or a ground, or if it could be taken in an abstract, tenseless sense. Would the latter alternative amount to realism with respect to proofs or grounds in a way that would be contrary to the supposedly anti-realistic standpoint underlying the epistemic understanding of linguistic expressions? Before discussing this question, I shall consider reasons for construing linguistic meaning epistemically and relations between such reasons and reasons for taking an anti-realist point of view towards the discourse in question.     

Das Problem der apagogischen Beweise in Bolzanos Beyträgen und seiner Wissenschaftslehre

This paper analyzes and evaluates Bolzano's remarks on the apagogic method of proof with reference to his juvenile booklet ‘Contributions to a better founded presentation of mathematics’ of 1810 and to his ‘Theory of science’ (1837). I shall try to defend the following contentions: (1) Bolzanos’ vain attempt to transform all indirect proofs into direct proofs becomes comprehensible as soon as one recognizes the following facts: (1.1) his attitude towards indirect proofs with an affirmative conclusion differs from his stance to indirect proofs with a negative conclusion; (1.2) by Bolzano's lights arguments via consequentia mirabilis only seem to be indirect. (2) Bolzano does not deny that indirect proofs can be perfect certifications (Gewissmachungen) of their conclusion; what he denies is rather that they can provide grounds for their conclusions. (2.1) They cannot do the latter, since they start from false premises and (2.2) since they make an unnecessary detour. (3) The far-reaching agreement between his early and late assessment of apagogical proofs (in the Beyträge of 1810 and the Wissenschaftslehre of 1837) is partly due to the fact that he develops his own position always against the background of Wolff's and Lambert's views.     

A Cut-Free Sequent Calculus for Defeasible Erotetic Inferences

In recent years, the effort to formalize erotetic inferences—i.e., inferences to and from questions—has become a central concern for those working in erotetic logic. However, few have sought to formulate a proof theory for these inferences. To fill this lacuna, we construct a calculus for (classes of) sequents that are sound and complete for two species of erotetic inferences studied by Inferential Erotetic Logic (IEL): erotetic evocation and erotetic implication. While an effort has been made to axiomatize the former in a sequent system, there is currently no proof theory for the latter. Moreover, the extant axiomatization of erotetic evocation fails to capture its defeasible character and provides no rules for introducing or eliminating question-forming operators. In contrast, our calculus encodes defeasibility conditions on sequents and provides rules governing the introduction and elimination of erotetic formulas. We demonstrate that an elimination theorem holds for a version of the cut rule that applies to both declarative and erotetic formulas and that the rules for the axiomatic account of question evocation in IEL are admissible in our system.

     

Reasons and Entailment

What is the relation between entailment and reasons for belief? In this paper, I discuss several answers to this question, and I argue that these answers all face problems. I then propose the following answer: for all propositions p ₁,…,p _n and q, if the conjunction of p ₁,…, and p _n entails q, then there is a reason against a person’s both believing that p ₁,…, and that p _n and believing the negation of q. I argue that this answer avoids the problems that the other answers to this question face, and that it does not face any other problems either. I end by showing what the relation between deductive logic, reasons for belief and reasoning is if this answer is correct.     

The Craig interpolation theorem for prepositional logics with strong negation

This paper deals with, prepositional calculi with strong negation (N-logics) in which the Craig interpolation theorem holds. N-logics are defined to be axiomatic strengthenings of the intuitionistic calculus enriched with a unary connective called strong negation. There exists continuum of N-logics, but the Craig interpolation theorem holds only in 14 of them.     

Why Care about Being an Agent?

The question ‘Why care about being an agent?’ asks for reasons to be something that appears to be non-optional. But perhaps it is closer to the question ‘Why be moral?’; or so I shall argue. Here the constitutivist answer—that we cannot help but have this aim—seems to be the best answer available. I suggest that, regardless of whether constitutivism is true, it is an incomplete answer. I argue that we should instead answer the question by looking at our evaluative commitments to the exercise of our other capacities for which being a full-blown agent is a necessary condition. Thus, the only kind of reason available is hypothetical rather than categorical. The status of this reason may seem to undermine the importance of this answer. I show, however, that it both achieves much of what we want when we cite categorical reasons and highlights why agency is valuable.