Stoic Sequent Logic and Proof Theory

This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzen-inspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich contemporary discussion. Much of Stoic logic appears surprisingly modern: a recursively formulated syntax with some truth-functional propositional operators; analogues to cut rules, axiom schemata and Gentzen’s negation-introduction rules; an implicit variable-sharing principle and deliberate rejection of Thinning and avoidance of paradoxes of implication. These latter features mark the system out as a relevance logic, where the absence of duals for its left and right introduction rules puts it in the vicinity of McCall’s connexive logic. Methodologically, the choice of meticulously formulated meta-logical rules in lieu of axiom and inference schemata absorbs some structural rules and results in an economical, precise and elegant system that values decidability over completeness.     

On Structural Features of the Implication Fragment of Frege’s <Emphasis Type="Italic">Grundgesetze</Emphasis>

We set out the implication fragment of Frege’s Grundgesetze, clarifying the implication rules and showing that this system extends Absolute Implication, or the implication fragment of Intuitionist logic. We set out a sequent calculus which naturally captures Frege’s implication proofs, and draw particular attention to the Cut-like features of his Hypothetical Syllogism rule.     

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.

     

Frege's Begriffsschrift is Indeed First-Order Complete

It is widely taken that the first-order part of Frege's Begriffsschrift is complete. However, there does not seem to have been a formal verification of this received claim. The general concern is that Frege's system is one axiom short in the first-order predicate calculus comparing to, by now, standard first-order theory. Yet Frege has one extra inference rule in his system. Then the question is whether Frege's first-order calculus is still deductively sufficient as far as the first-order completeness is concerned. In this short note we confirm that the missing axiom is derivable from his stated axioms and inference rules, and hence the logic system in the Begriffsschrift is indeed first-order complete.     

Substructural Implicational Logics Including the Relevant Logic E

We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic logic. This revised version was published online in June 2006 with corrections to the Cover Date.     

Analytic Rules for Mereology

We present a sequent calculus for extensional mereology. It extends the classical first-order sequent calculus with identity by rules of inference corresponding to well-known mereological axioms. Structural rules, including cut, are admissible.     

Cut Elimination inside a Deep Inference System for Classical Predicate Logic

Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations.     

Aspects of analytic deduction

Let ? be the ordinary deduction relation of classical first-order logic. We provide an “analytic” subrelation ?³ of ? which for propositional logic is defined by the usual “containment” criterion $$\Gamma \vdash ^a \varphi iff \Gamma \vdash \varphi and Atom(\varphi ) \subseteq Atom(\Gamma ),$$ whereas for predicate logic, ?^a is defined by the extended criterion $$\Gamma \vdash ^a \varphi iff \Gamma \vdash \varphi and Atom(\varphi ) \subseteq ' Atom(\Gamma ),$$ where Atom(?) $ \subseteq '$ Atom(Γ) means that every atomic formula occurring in ? “essentially occurs” also in Γ. If Γ, ? are quantifier-free, then the notions “occurs” and “essentially occurs” for atoms between Γ and ? coincide. If ? is formalized by Gentzen's calculus of sequents, then we show that ?^a is axiomatizable by a proper fragment of analytic inference rules. This is mainly due to cut elimination. By “analytic inference rule” we understand here a rule r such that, if the sequent over the line is analytic, then so is the sequent under the line. We also discuss the notion of semantic relevance as contrasted to the previous syntactic one. We show that when introducing semantic sequents as axioms, i.e. when extending the pure logical axioms and rules by mathematical ones, the property of syntactic relevance is lost, since cut elimination no longer holds. We conclude that no purely syntactic notion of analytic deduction can ever replace successfully the complex semantico-syntactic deduction we already possess.     

Sequent Calculi and Decision Procedures for Weak Modal Systems

We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of Löb rules are given.     

Speak your mind and I will make it right: the case of “selection task”

ABSTRACT

The “Wason selection task” is still one of the most studied tasks in cognitive psychology. We argue that the low performance originally obtained seems to be caused by how the information of the task is presented. By systematically manipulating the task instructions, making explicit the information that participants are required to infer in accordance with the logical interpretation of the material implication “if, then”, we found an improvement in performance. In Experiment 1, the conditional rule has been formulated within a relevant context and in accordance with the conversational rules of communication, hence transmitting the actual meaning of the material implication. In Experiment 2, a similar improvement has been obtained even without the realistic scenario, only by making explicit the unidirectionality of the material implication. We conclude that task instructions are often formulate neglecting the conversational rules of communication, and this greatly reduces the possibility to succeed in the task.     

On a property of BCK-identities

A BCK-algebra is an algebra in which the terms are generated by a set of variables, 1, and an arrow. We mean by aBCK-identity an equation valid in all BCK-algebras. In this paper using a syntactic method we show that for two termss andt, if neithers=1 nort=1 is a BCK-identity, ands=t is a BCK-identity, then the rightmost variables of the two terms are identical.This theorem was conjectured firstly in [5], and then in [3]. As a corollary of this theorem, we derive that the BCK-algebras do not form a variety, which was originally proved algebraically by Wroski ([4]).To prove the main theorem, we use a Gentzen-type logical system for the BCK-algebras, introduced by Komori, which consists of the identity axiom, the right and the left introduction rules of the implication, the exchange rule, the weakening rule and the cut. As noted in [2], the cut-elimination theorem holds for this system.Presented byJan Zygmunt     

Sequent Calculi for $${\mathsf {}}$$

In this paper we are applying certain strategy described by Negri and Von Plato (Bull Symb Log 4(04):418–435, 1998), allowing construction of sequent calculi for axiomatic theories, to Suszko’s Sentential calculus with identity. We describe two calculi obtained in this way, prove that the cut rule, as well as the other structural rules, are admissible in one of them, and we also present an example which suggests that the cut rule is not admissible in the other.     

On the inferential epistemics of trait centrality in impression formation

We provide a novel, inferential, account of the trait centrality phenomenon. We suggest that a trait possesses the property of “centrality” to the extent that it is subjectively deemed to imply other traits. Five studies explore four central elements of this view. First, trait relations can be stored as unidirectional rules (“if X then Y” but not necessarily “if Y then X”). Second, the strength of individuals' lay inference rules determines the effect of traits on impressions. Third, situationally manipulating the strength of lay inference rules influences the impact of traits on impressions. Fourth, the impact of an inference rule is reduced when it is difficult to discern the inference rule and when processing resources are limited. Copyright © 2009 John Wiley & Sons, Ltd.     

Protoalgebraic Gentzen Systems and the Cut Rule

In this paper we show that, in Gentzen systems, there is a close relation between two of the main characters in algebraic logic and proof theory respectively: protoalgebraicity and the cut rule. We give certain conditions under which a Gentzen system is protoalgebraic if and only if it possesses the cut rule. To obtain this equivalence, we limit our discussion to what we call regular sequent calculi, which are those comprising some of the structural rules and some logical rules, in a sense we make precise. We note that this restricted set of rules includes all the usual rules in the literature. We also stress the difference between the case of two-sided sequents and the case of many-sided sequents, in which more conditions are needed.     

Limiting logical pluralism

In this paper I argue that pluralism at the level of logical systems requires a certain monism at the meta-logical level, and so, in a sense, there cannot be pluralism all the way down. The adequate alternative logical systems bottom out in a shared basic meta-logic, and as such, logical pluralism is limited. I argue that the content of this basic meta-logic must include the analogue of logical rules Modus Ponens (MP) and Universal Instantiation (UI). I show this through a detailed analysis of the ‘adoption problem’, which manifests something special about MP and UI. It appears that MP and UI underwrite the very nature of a logical rule of inference, due to all rules of inference being conditional and universal in their structure. As such, all logical rules presuppose MP and UI, making MP and UI self-governing, basic, unadoptable, and (most relevantly to logical pluralism) required in the meta-logic for the adequacy of any logical system.

     

Expressive Power and Incompleteness of Propositional Logics

Natural deduction systems were motivated by the desire to define the meaning of each connective by specifying how it is introduced and eliminated from inference. In one sense, this attempt fails, for it is well known that propositional logic rules (however formulated) underdetermine the classical truth tables. Natural deduction rules are too weak to enforce the intended readings of the connectives; they allow non-standard models. Two reactions to this phenomenon appear in the literature. One is to try to restore the standard readings, for example by adopting sequent rules with multiple conclusions. Another is to explore what readings the natural deduction rules do enforce. When the notion of a model of a rule is generalized, it is found that natural deduction rules express “intuitionistic” readings of their connectives. A third approach is presented here. The intuitionistic readings emerge when models of rules are defined globally, but the notion of a local model of a rule is also natural. Using this benchmark, natural deduction rules enforce exactly the classical readings of the connectives, while this is not true of axiomatic systems. This vindicates the historical motivation for natural deduction rules. One odd consequence of using the local model benchmark is that some systems of propositional logic are not complete for the semantics that their rules express. Parallels are drawn with incompleteness results in modal logic to help make sense of this.     

Refining the Inferential Model of Scientific Understanding

In this article, I use a mental models computational account of representation to illustrate some details of my previously presented inferential model of scientific understanding. The hope is to shed some light on possible mechanisms behind the notion of scientific understanding. I argue that if mental models are a plausible approach to modelling cognition, then understanding can best be seen as the coupling of specific rules. I present our beliefs as ‘ordinary’ conditional rules, and the coupling process as one where the consequent of one ordinary rule (OR) matches and activates the antecedent of the rule to which it is coupled in virtue of the activation of an intermediate ‘inference’ rule. I argue that on this approach knowledge of an explanation is the activation of ORs in a cognitive hierarchy, while understanding is achieved when those activated ORs are also coupled via correct inference rules. I do not directly address issues regarding the plausibility of mental models themselves. This article should therefore be seen as an exercise in refining the inferential model within an already presupposed computational setting, not one of arguing for the psychological adequacy of computational approaches.     

Implications-as-Rules vs. Implications-as-Links: An Alternative Implication-Left Schema for the Sequent Calculus

The interpretation of implications as rules motivates a different left-introduction schema for implication in the sequent calculus, which is conceptually more basic than the implication-left schema proposed by Gentzen. Corresponding to results obtained for systems with higher-level rules, it enjoys the subformula property and cut elimination in a weak form.