弱逻辑F的矢列演算

本文建立起弱逻辑F的G3-型矢列演算G3F,并证明弱化规则、收缩规则和切割规则在G3F中是可容许的。此外,本文还运用证明论的方法给出一个通过哥德尔–麦金西–塔斯基翻译将G3F嵌入到G3K的新证明。     

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.     

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.     

A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic

In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.     

Semi-intuitionistic Logic

The purpose of this paper is to define a new logic ${\mathcal {SI}}$ called semi-intuitionistic logic such that the semi-Heyting algebras introduced in [4] by Sankappanavar are the semantics for ${\mathcal {SI}}$ . Besides, the intuitionistic logic will be an axiomatic extension of ${\mathcal {SI}}$ .     

Semi-intuitionistic Logic with Strong Negation

Motivated by the definition of semi-Nelson algebras, a propositional calculus called semi-intuitionistic logic with strong negation is introduced and proved to be complete with respect to that class of algebras. An axiomatic extension is proved to have as algebraic semantics the class of Nelson algebras.     

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.

     

Gentzen-Style Axiomatizations for Some Conservative Extensions of Basic Propositional Logic

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.     

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.     

Falsification-Aware Semantics and Sequent Calculi for Classical Logic

Journal of Philosophical Logic - In this study, falsification-aware semantics and sequent calculi for first-order classical logic are introduced and investigated. These semantics and sequent...     

A Cut-Free Sequent System for the Smallest Interpretability Logic

The idea of interpretability logics arose in Visser [Vis90]. He introduced the logics as extensions of the provability logic GLwith a binary modality . The arithmetic realization of A B in a theory T will be that T plus the realization of B is interpretable in T plus the realization of A (T + A interprets T + B). More precisely, there exists a function f (the relative interpretation) on the formulas of the language of T such that T + B C implies T + A f(C).The interpretability logics were considered in several papers. An arithmetic completeness of the interpretability logic ILM, obtained by adding Montagna's axiom to the smallest interpretability logic IL, was proved in Berarducci [Ber90] and Shavrukov [Sha88] (see also Hájek and Montagna [HM90] and Hájek and Montagna [HM92]). [Vis90] proved that the interpretability logic ILP, an extension of IL, is also complete for another arithmetic interpretation. The completeness with respect to Kripke semantics due to Veltman was, for IL, ILMand ILP, proved in de Jongh and Veltman [JV90]. The fixed point theorem of GLcan be extended to ILand hence ILMand ILP(cf. de Jongh and Visser [JV91]). The unary pendant "T interprets T + A" is much less expressive and was studied in de Rijke [Rij92]. For an overview of interpretability logic, see Visser [Vis97], and Japaridze and de Jongh [JJ98].In this paper, we give a cut-free sequent system for IL. To begin with, we give a cut-free system for the sublogic IL4of IL, whose -free fragment is the modal logic K4. A cut-elimination theorem for ILis proved using the system for IK4and a property of Löb's axiom.     

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.     

Lambda Calculus and Intuitionistic Linear Logic

The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.This paper introduces a typed functional language ! and a categorical model for it.The terms of ! encode a version of natural deduction for Intuitionistic Linear Logic such that linear and non linear assumptions are managed multiplicatively and additively, respectively. Correspondingly, the terms of ! are built out of two disjoint sets of variables. Moreover, the -abstractions of ! bind variables and patterns. The use of two different kinds of variables and the patterns allow a very compact definition of the one-step operational semantics of !, unlike all other extensions of Curry-Howard Isomorphism to Intuitionistic Linear Logic. The language ! is Church-Rosser and enjoys both Strong Normalizability and Subject Reduction.The categorical model induces operational equivalences like, for example, a set of extensional equivalences.The paper presents also an untyped version of ! and a type assignment for it, using formulas of Linear Logic as types. The type assignment inherits from ! all the good computational properties and enjoys also the Principal-Type Property.     

A Sequent Formulation of Conditional Logic Based on Belief Change Operations

Peter Gärdenfors has developed a semantics for conditional logic, based on the operations of expansion and revision applied to states of information. The account amounts to a formalisation of the Ramsey test for conditionals. A conditional A > B is declared accepted in a state of information K if B is accepted in the state of information which is the result of revising K with respect to A. While Gärdenfors's account takes the truth-functional part of the logic as given, the present paper proposes a semantics entirely based on epistemic states and operations on these states. The semantics is accompanied by a syntactic treatment of conditional logic which is formally similar to Gentzen's sequent formulation of natural deduction rules. Three of David Lewis's systems of conditional logic are represented. The formulations are attractive by virtue of their transparency and simplicity.     

An Axiomatic System and a Tableau Calculus for STIT Imagination Logic

We formulate a Hilbert-style axiomatic system and a tableau calculus for the STIT-based logic of imagination recently proposed in Wansing (2015). Completeness of the axiom system is shown by the method of canonical models; completeness of the tableau system is also shown by using standard methods.     

The Lambek Calculus Extended with Intuitionistic Propositional Logic

We present sound and complete semantics and a sequent calculus for the Lambek calculus extended with intuitionistic propositional logic.     

一个多值逻辑的一阶谓词系统

鞠实儿曾提出一个开放类三值命题逻辑系统,这一逻辑也可以推广到任意m值逻辑情形,成为一个联结词函数完全的逻辑。本文将对推广的命题逻辑系统L^＊建立一种一阶谓词系统,并证明其可靠性、完全性。     

Relational Semantics of the Lambek Calculus Extended with Classical Propositional Logic

We show that the relational semantics of the Lambek calculus, both nonassociative and associative, is also sound and complete for its extension with classical propositional logic. Then, using filtrations, we obtain the finite model property for the nonassociative Lambek calculus extended with classical propositional logic.     

Marginalia on Sequent Calculi

The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi.