PRESERVATION OF STRUCTURAL PROPERTIES IN INTUITIONISTIC EXTENSIONS OF AN INFERENCE RELATION

2018 ◽  
Vol 24 (3) ◽  
pp. 291-305 ◽  
Author(s):  
TOR SANDQVIST
Keyword(s):  
Structural Properties ◽  
Sequent Calculus ◽  
General Nature ◽  
Cut Elimination ◽  
Formal Proofs ◽  
Structural Rules ◽  
Logical Operators ◽  
First Order ◽  
Order Language ◽  
The Given

AbstractThe article approaches cut elimination from a new angle. On the basis of an arbitrary inference relation among logically atomic formulae, an inference relation on a language possessing logical operators is defined by means of inductive clauses similar to the operator-introducing rules of a cut-free intuitionistic sequent calculus. The logical terminology of the richer language is not uniquely specified, but assumed to satisfy certain conditions of a general nature, allowing for, but not requiring, the existence of infinite conjunctions and disjunctions. We investigate to what extent structural properties of the given atomic relation are preserved through the extension to the full language. While closure under the Cut rule narrowly construed is not in general thus preserved, two properties jointly amounting to closure under the ordinary structural rules, including Cut, are.Attention is then narrowed down to the special case of a standard first-order language, where a similar result is obtained also for closure under substitution of terms for individual parameters. Taken together, the three preservation results imply the familiar cut-elimination theorem for pure first-order intuitionistic sequent calculus.In the interest of conceptual economy, all deducibility relations are specified purely inductively, rather than in terms of the existence of formal proofs of any kind.

The consistency of arithmetic

2021 ◽  
pp. 268-311
Author(s):  
Paolo Mancosu ◽  
Sergio Galvan ◽  
Richard Zach
Keyword(s):  
Simple Proof ◽  
Sequent Calculus ◽  
Cut Elimination ◽  
Successor Function ◽  
Cut Rule ◽  
Original Proof ◽  
First Order ◽  
Successive Elimination ◽  
Pure Logic ◽  
Classical Arithmetic

This chapter opens the part of the book that deals with ordinal proof theory. Here the systems of interest are not purely logical ones, but rather formalized versions of mathematical theories, and in particular the first-order version of classical arithmetic built on top of the sequent calculus. Classical arithmetic goes beyond pure logic in that it contains a number of specific axioms for, among other symbols, 0 and the successor function. In particular, it contains the rule of induction, which is the essential rule characterizing the natural numbers. Proving a cut-elimination theorem for this system is hopeless, but something analogous to the cut-elimination theorem can be obtained. Indeed, one can show that every proof of a sequent containing only atomic formulas can be transformed into a proof that only applies the cut rule to atomic formulas. Such proofs, which do not make use of the induction rule and which only concern sequents consisting of atomic formulas, are called simple. It is shown that simple proofs cannot be proofs of the empty sequent, i.e., of a contradiction. The process of transforming the original proof into a simple proof is quite involved and requires the successive elimination, among other things, of “complex” cuts and applications of the rules of induction. The chapter describes in some detail how this transformation works, working through a number of illustrative examples. However, the transformation on its own does not guarantee that the process will eventually terminate in a simple proof.

On the unification of classical, intuitionistic and affine logics

2018 ◽  
Vol 29 (8) ◽  
pp. 1177-1216
Author(s):  
CHUCK LIANG
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Kripke Semantics ◽  
Cut Elimination ◽  
Structural Rules ◽  
Phase Semantics ◽  
Intuitionistic Logics

This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the λμ calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.

scholarly journals Pretopologies and completeness proofs

1995 ◽  
Vol 60 (3) ◽  
pp. 861-878 ◽  
Author(s):  
Giovanni Sambin
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Predicate Logic ◽  
Linear Logic ◽  
Double Negation ◽  
Open Problems ◽  
Completeness Proof ◽  
Structural Rules ◽  
First Order ◽  
Definition Of

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules, ex falso quodlibet or double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward.

Stratification and cut-elimination

1991 ◽  
Vol 56 (1) ◽  
pp. 213-226 ◽  
Author(s):  
Marcel Crabbé
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Cut Elimination ◽  
Simple Type ◽  
First Order ◽  
Similar Reason ◽  
Separation Axioms ◽  
Simple Type Theory ◽  
Order Language ◽  
The Universe

In this paper, we show the normalization of proofs of NF (Quine's New Foundations; see [15]) minus extensionality. This system, called SF (Stratified Foundations) differs in many respects from the associated system of simple type theory. It is written in a first order language and not in a multi-sorted one, and the formulas need not be stratifiable, except in the instances of the comprehension scheme. There is a universal set, but, for a similar reason as in type theory, the paradoxical sets cannot be formed.It is not immediately apparent, however, that SF is essentially richer than type theory. But it follows from Specker's celebrated result (see [16] and [4]) that the stratifiable formula (extensionality → the universe is not well-orderable) is a theorem of SF.It is known (see [11]) that this set theory is consistent, though the consistency of NF is still an open problem.The connections between consistency and cut-elimination are rather loose. Cut-elimination generally implies consistency. But the converse is not true. In the case of set theory, for example, ZF-like systems, though consistent, cannot be freed of cuts because the separation axioms allow the formation of sets from unstratifiable formulas. There are nevertheless interesting partial results obtained when restrictions are imposed on the removable cuts (see [1] and [9]). The systems with stratifiable comprehension are the only known set-theoretic systems that enjoy full cut-elimination.

scholarly journals Generalized quantification as substructural logic

1996 ◽  
Vol 61 (3) ◽  
pp. 1006-1044 ◽  
Author(s):  
Natasha Alechina ◽  
Michiel Van Lambalgen
Keyword(s):  
Proof Theory ◽  
Sequent Calculus ◽  
Substructural Logic ◽  
Generalized Quantifiers ◽  
Accessibility Relation ◽  
Dependence Relation ◽  
Structural Rules ◽  
First Order ◽  
Proof Systems ◽  
Structured Objects

AbstractWe show how sequent calculi for some generalized quantifiers can be obtained by generalizing the Herbrand approach to ordinary first order proof theory. Typical of the Herbrand approach, as compared to plain sequent calculus, is increased control over relations of dependence between variables. In the case of generalized quantifiers, explicit attention to relations of dependence becomes indispensible for setting up proof systems. It is shown that this can be done by turning variables into structured objects, governed by various types of structural rules. These structured variables are interpreted semantically by means of a dependence relation. This relation is an analogue of the accessibility relation in modal logic. We then isolate a class of axioms for generalized quantifiers which correspond to first-order conditions on the dependence relation.

A focused linear logical framework and its application to metatheory of object logics

2021 ◽  
pp. 1-29
Author(s):  
Amy Felty ◽  
Carlos Olarte ◽  
Bruno Xavier
Keyword(s):  
Programming Languages ◽  
Sequent Calculus ◽  
Necessary Conditions ◽  
Linear Logic ◽  
Cut Elimination ◽  
Logical Framework ◽  
Minimal Logic ◽  
First Order ◽  
Fundamental Properties ◽  
Logical Frameworks

Abstract Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL’s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories.

scholarly journals On the correspondence between nested calculi and semantic systems for intuitionistic logics

2020 ◽  
Author(s):  
Tim Lyon
Keyword(s):  
Intuitionistic Logic ◽  
Structural Rules ◽  
First Order ◽  
Constant Domains ◽  
The Relationship ◽  
Intuitionistic Logics

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

Weakly atomic-compact relational structures

1971 ◽  
Vol 36 (1) ◽  
pp. 129-140 ◽  
Author(s):  
G. Fuhrken ◽  
W. Taylor
Keyword(s):  
Abelian Group ◽  
Model Theory ◽  
Compact Abelian Group ◽  
Finite Subset ◽  
Relational Structure ◽  
Similarity Type ◽  
First Order ◽  
Relational Structures ◽  
Order Language ◽  
Weakly Atomic

A relational structure is called weakly atomic-compact if and only if every set Σ of atomic formulas (taken from the first-order language of the similarity type of augmented by a possibly uncountable set of additional variables as “unknowns”) is satisfiable in whenever every finite subset of Σ is so satisfiable. This notion (as well as some related ones which will be mentioned in §4) was introduced by J. Mycielski as a generalization to model theory of I. Kaplansky's notion of an algebraically compact Abelian group (cf. [5], [7], [1], [8]).

scholarly journals ON PRODUCTS OF ELEMENTARILY INDIVISIBLE STRUCTURES

2016 ◽  
Vol 81 (3) ◽  
pp. 951-971
Author(s):  
NADAV MEIR
Keyword(s):  
New Products ◽  
Elementary Substructure ◽  
First Order ◽  
Order Language ◽  
Image Position

AbstractWe say a structure ${\cal M}$ in a first-order language ${\cal L}$ is indivisible if for every coloring of its universe in two colors, there is a monochromatic substructure ${\cal M}\prime \subseteq {\cal M}$ such that ${\cal M}\prime \cong {\cal M}$. Additionally, we say that ${\cal M}$ is symmetrically indivisible if ${\cal M}\prime$ can be chosen to be symmetrically embedded in ${\cal M}$ (that is, every automorphism of ${\cal M}\prime$ can be extended to an automorphism of ${\cal M}$). Similarly, we say that ${\cal M}$ is elementarily indivisible if ${\cal M}\prime$ can be chosen to be an elementary substructure. We define new products of structures in a relational language. We use these products to give recipes for construction of elementarily indivisible structures which are not transitive and elementarily indivisible structures which are not symmetrically indivisible, answering two questions presented by A. Hasson, M. Kojman, and A. Onshuus.

Sign in / Sign up

Export Citation Format

Share Document