Search

This work presents a model-theoretic approach to the study of the amalgamation property for varieties of semilinear commutative residuated lattices. It is well-known that if a first-order theory T enjoys quantifier elimination in some language L, the class of models of the set of its universal consequences $${\rm T_\forall}$$ has the amalgamation property. Let $${{\rm Th}(\mathbb{K})}$$ be the theory of an elementary subclass $${\mathbb{K}}$$ of the linearly ordered members of a variety $${\mathbb{V}}$$ of semilinear commutative residuated lattices. We show that whenever $${{\rm Th}(\mathbb{K})}$$ has elimination of quantifiers, and every linearly ordered structure in $${\mathbb{V}}$$ is a model of $${{\rm Th}_\forall(\mathbb{K})}$$, then $${\mathbb{V}}$$ has the amalgamation property. We exploit this fact to provide a purely model-theoretic proof of amalgamation for particular varieties of semilinear commutative residuated lattices. [ABSTRACT FROM AUTHOR]

Abstract: We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic. [Copyright &y& Elsevier]

A new set of conversions for derivations in the system of sequents for intuitionistic predicate logic will be defined. These conversions will be some modifications of Zucker's conversions from the system of sequents [InlineMediaObject not available: see fulltext.] from [11], which will have the following characteristics: (1) these conversions will be sufficient for transforming a derivation into a cut-free one, and (2) in the natural deduction the image of each of these conversions will be either in the set of conversions for normalization procedure, or an identity of derivations. This will be used to give a new proof of the normalization theorem for natural deduction, as a consequence of the cut-elimination theorem for the system of sequents. [ABSTRACT FROM AUTHOR]

The standard rule of necessitation in systems of natural deduction for the modal logic S4 concludes □A from A whenever all assumptions A depends on are modal formulas. This condition prevents the composability and normalization of derivations, and therefore modifications of the rule have been suggested. It is shown that both properties hold if, instead of changing the rule of necessitation, all elimination rules are formulated in the manner of disjunction elimination, i.e. with an arbitrary consequence. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The relationship among first-order monadic omega-logic (MOL), propositional (until-free) linear-time temporal logic (LTL), propositional generalized definitional reflection logic (GDRL) and propositional infinitary logic (IL) is clarified via embedding theorems. A theorem for embedding a Gentzen-type sequent calculus MOω for MOL into a Gentzen-type sequent calculus LTω for LTL is proved. The cut-elimination theorem for MOω is proved using this embedding theorem. MOL is also shown to be decidable through the use of this embedding theorem. Theorems for embedding LTω into MOω and MOω into a Gentzen-type sequent calculus LKω for IL are also proved. Moreover, a theorem for embedding MOω into a Gentzen-type sequent calculus GDω for GDRL and a theorem for embedding LTω into GDω are proved. [ABSTRACT FROM AUTHOR]

Inferentialism claims that the rules for the use of an expression express its meaning without any need to invoke meanings or denotations for them. Logical inferentialism endorses inferentialism specifically for the logical constants. Harmonic inferentialism, as the term is introduced here, usually but not necessarily a subbranch of logical inferentialism, follows Gentzen in proposing that it is the introduction-rules which give expressions their meaning and the elimination-rules should accord harmoniously with the meaning so given. It is proposed here that the logical expressions are those which can be given schematic rules that lie in a specific sort of harmony, general-elimination (ge) harmony, resulting from applying a certain operation, the ge-procedure, to produce ge-rules in accord with the meaning defined by the I-rules. Griffiths (2014) claims that identity cannot be given such rules, concluding that logical inferentialists are committed to ruling identity a nonlogical expression. It is shown that the schematic rules for identity given in Read (2004), slightly amended, are indeed ge-harmonious, so confirming that identity is a logical notion. [ABSTRACT FROM AUTHOR]

Connexive logic contains propositional theses such as NCpNp and CCpqNCpNq that are false in two-valued logic. It derives from remarks made by Sextus Empiricus in the fourth century B.C. The logic of causal and subjunctive conditionals is also connexive, since ‘If X is dropped, it will hit the floor’ contradicts ‘If X is dropped, it will not hit the floor’. In the paper below, a Gentzen Sequenzenkalkul formulation of connexive logic is constructed, and a proof is given of the elimination theorem. [ABSTRACT FROM AUTHOR]

Valentini (1983) has presented a proof of cut-elimination for provability logic GL for a sequent calculus using sequents built from sets as opposed to multisets, thus avoiding an explicit contraction rule. From a formal point of view, it is more syntactic and satisfying to explicitly identify the applications of the contraction rule that are ‘hidden’ in proofs of cut-elimination for such sequent calculi. There is often an underlying assumption that the move to a proof of cut-elimination for sequents built from multisets is straightforward. Recently, however, it has been claimed that Valentini’s arguments to eliminate cut do not terminate when applied to a multiset formulation of the calculus with an explicit rule of contraction. The claim has led to much confusion and various authors have sought new proofs of cut-elimination for GL in a multiset setting.Here we refute this claim by placing Valentini’s arguments in a formal setting and proving cut-elimination for sequents built from multisets. The use of sequents built from multisets enables us to accurately account for the interplay between the weakening and contraction rules. Furthermore, Valentini’s original proof relies on a novel induction parameter called “width” which is computed ‘globally’. It is difficult to verify the correctness of his induction argument based on “width.” In our formulation however, verification of the induction argument is straightforward. Finally, the multiset setting also introduces a new complication in the case of contractions above cut when the cut-formula is boxed. We deal with this using a new transformation based on Valentini’s original arguments.Finally, we discuss the possibility of adapting this cut-elimination procedure to other logics axiomatizable by formulae of a syntactically similar form to the GL axiom. [ABSTRACT FROM AUTHOR]

A normalization procedure is given for classical natural deduction with the standard rule of indirect proof applied to arbitrary formulas. For normal derivability and the subformula property, it is sufficient to permute down instances of indirect proof whenever they have been used for concluding a major premiss of an elimination rule. The result applies even to natural deduction for classical modal logic. [ABSTRACT FROM AUTHOR]

Abstract: This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version of a type theory, in which we show the embedding of the modal operators into standard group knowledge operators. [Copyright &y& Elsevier]

We study a system, called NEL, which is the mixed commutative/noncommutative linear logic BV augmented with linear logic's exponentials. Equivalently, NEL is MELL augmented with the noncommutative self-dual connective seq. In this article, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next article of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs. [ABSTRACT FROM AUTHOR]

The aim of this article is Schröder's treatment of the so called solution problem [Auflösungsproblem]. First, I will introduce Schröder's ideas; then I will discuss them taking into account Peirce's considerations in The Logic of Relatives ([13, pp. 161-217] now republished in [9, pp. 288-345]). [ABSTRACT FROM AUTHOR]

In this paper we show some non-elementary speed-ups in logic calculi: Both a predicative second-order logic and a logic for fixed points of positive formulas are shown to have non-elementary speed-ups over first-order logic. Also it is shown that eliminating second-order cut formulas in second-order logic has to increase sizes of proofs super-exponentially, and the same in eliminating second-order epsilon axioms. These are proved by relying on results due to P. Pudlák. (© 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

There is a simple technique, due to Dragalin, for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative Set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop's ı-translation and perpetual reductions. These tools are of independent interest and have proved useful in a variety of Settings; it is therefore natural to Investigate, as we do here, what they have to offer the field of sequent calculus. [ABSTRACT FROM AUTHOR]

We introduce various sequent systems for propositional logics having strict implication, and prove the completeness theorems and the finite model properties of these systems.The cut-elimination theorems or the (modified) subformula properties are proved semantically. [ABSTRACT FROM PUBLISHER]

A mechanism for combining any two substructural logics (e.g. linear and intuitionistic logics) is studied from a proof-theoretic point of view. The main results presented are cut-elimination and simulation results for these combined logics called synthesized substructural logics. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Abstract: The larger project broached here is to look at the generally sentence “if is well-ordered then is well-ordered”, where is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded -models for a particular theory whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function . To illustrate this theme, we prove in this paper that the statement “if is well-ordered then is well-ordered” is equivalent to . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search (deduction chains) [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a (small) fragment of . [Copyright &y& Elsevier]

Abstract: When investigating the complexity of cut-elimination in first-order logic, a natural subproblem is the elimination of quantifier-free cuts. So far, the problem has only been considered in the context of general cut-elimination, and the upper bounds that have been obtained are essentially double exponential. In this note, we observe that a method due to Dale Miller can be applied to obtain an exponential upper bound. [Copyright &y& Elsevier]

Abstract: For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius (1991) for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge (Brünnler and Studer, 2009) and by Hill and Poggiolesi (2010) for PDL, which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can be pushed in general. To this end, we introduce a nested sequent system with syntactic cut-elimination which is incomplete for the modal mu-calculus, but complete with respect to a restricted language that allows only fixed points of a certain form. This restricted language includes the logic of common knowledge and PDL. There is also a traditional sequent system for the modal mu-calculus by Jäger et al. (2008) , without a syntactic cut-elimination procedure. We embed that system into ours and vice versa, thus establishing cut-elimination also for the shallow system, when only the restricted language is considered. [Copyright &y& Elsevier]

Abstract: Starting from Girard’s seminal paper on light linear logic (LLL), a number of works investigated systems derived from linear logic to capture polynomial time computation within the computation-as-cut-elimination paradigm. The original syntax of LLL is too complicated, mainly because one has to deal with sequents which do not just consist of formulas but also of ‘blocks’ of formulas. We circumvent the complications of ‘blocks’ by introducing a new modality which is exclusively in charge of ‘additive blocks’. One of the most interesting features of this purely multiplicative is the possibility of the second-order encodings of additive connectives. The resulting system (with the traditional syntax), called Easy-LLL, is still powerful to represent any deterministic polynomial time computations in purely logical terms. Unlike the original LLL, Easy-LLL admits polynomial time strong normalization together with the Church–Rosser property, namely, cut elimination terminates in a unique way in polytime by any choice of cut reduction strategies. [Copyright &y& Elsevier]

Abstract: In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality △ to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems. [Copyright &y& Elsevier]

Abstract: Geometry of Interaction is a transcendental syntax developed in the framework of operator algebras. This fifth installment of the program takes place inside a von Neumann algebra, the hyperfinite factor. It provides a built-in interpretation of cut-elimination as well as an explanation for light, i.e., complexity sensitive, logics. [Copyright &y& Elsevier]

Abstract: We give a semantic account of the execution time (i.e. the number of cut elimination steps leading to the normal form) of an untyped net. We first prove that: (1) a net is head-normalizable (i.e. normalizable at depth ) if and only if its interpretation in the multiset based relational semantics is not empty and (2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then give a semantic measure of execution time: we prove that we can compute the number of cut elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut-link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the untyped lambda-calculus. [Copyright &y& Elsevier]