Search

The ϵ-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory ID1 using a variant of the cut-elimination formalism introduced by Mints. [ABSTRACT FROM AUTHOR]

We prove that if T is a complete theory with weak elimination of imaginaries, then there is an explicit bijection between strict independence relations for T and strict independence relations for Teq. We use this observation to show that if T is the theory of the Fraïssé limit of finite metric spaces with integer distances, then Teq has more than one strict independence relation. This answers a question of Adler (J Math Log 9(1):1-20, , Question 1.7). [ABSTRACT FROM AUTHOR]

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]

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]

Abstract. Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers. [ABSTRACT FROM AUTHOR]

Abstract. Gentzen's original proof of the Hauptsatz used a rule of multicut in the case that the right premiss of cut was derived by contraction. Cut elimination is here proved without multicut, by transforming suitably the derivation of the premiss of the contraction. [ABSTRACT FROM AUTHOR]

Generalizing Cooper’s method of quantifier elimination for Presburger arithmetic, we give a new proof that all parametric Presburger families {St:t∈N} [as defined by Woods (Electron J Comb 21:P21, 2014)] are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f(t) for every polynomial f∈Z[t]. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic by multiplication by scalars {α(t):α∈R,t∈X} where R is any ring of functions from X into Z. [ABSTRACT FROM AUTHOR]

The $$\Omega $$ -rule was introduced by W. Buchholz to give an ordinal-free proof of cut-elimination for a subsystem of analysis with $$\Pi ^{1}_{1}$$ -comprehension. W. Buchholz's proof provides cut-free derivations by familiar rules only for arithmetical sequents. When second-order quantifiers are present, they are introduced by the $$\Omega $$ -rule and some residual cuts are not eliminated. In the present paper, we introduce an extension of the $$\Omega $$ -rule and prove the complete cut-elimination by the same method as W. Buchholz: any derivation of arbitrary sequent is transformed into its cut-free derivation by the standard rules (with induction replaced by the $$\omega $$ -rule). In fact we treat the subsystem of $$\Pi ^{1}_{1}$$ -CA (of the same strength as $$ID_{1}$$ ) that W. Buchholz used for his explanation of G. Takeuti's finite reductions. Extension to full $$\Pi ^{1}_{1}$$ -CA is planned for another paper. [ABSTRACT FROM AUTHOR]

We present a construction of a truth class (an interpretation of a compositional truth predicate) in an arbitrary countable recursively saturated model of first-order arithmetic. The construction is fully classical in that it employs nothing more than the classical techniques of formal proof theory. [ABSTRACT FROM AUTHOR]

Schmerl and Beklemishev's work on iterated reflection achieves two aims: it introduces the important notion of Π10-ordinal, characterizing the Π10-theorems of a theory in terms of transfinite iterations of consistency; and it provides an innovative calculus to compute the Π10-ordinals for a range of theories. The present note demonstrates that these achievements are independent: we read off Π10-ordinals from a Schütte-style ordinal analysis via infinite proofs, in a direct and transparent way. [ABSTRACT FROM AUTHOR]

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is $${\Pi^1_1}$$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument. [ABSTRACT FROM AUTHOR]