Lebesgue’s dominated convergence theorem in Bishop’s style

We present a constructive proof in Bishop’s style of Lebesgue’s dominated convergence theorem in the abstract setting of ordered uniform spaces. The proof generalises to this setting a classical proof in the framework of uniform lattices presented by Hans Weber in [Uniform lattices. II: order continuity and exhaustivity, Annali di Matematica pura ed applicata, (IV) CLXV (1993) 133-158].     

Proof and refutation in MALL as a game

We present a setting in which the search for a proof of B or a refutation of B (i.e., a proof of ¬B) can be carried out simultaneously: in contrast, the usual approach in automated deduction views proving B or proving ¬B as two, possibly unrelated, activities. Our approach to proof and refutation is described as a two-player game in which each player follows the same rules. A winning strategy translates to a proof of the formula and a counter-winning strategy translates to a refutation of the formula. The game is described for multiplicative and additive linear logic (MALL). A game theoretic treatment of the multiplicative connectives is intricate and our approach to it involves two important ingredients. First, labeled graph structures are used to represent positions in a game and, second, the game playing must deal with the failure of a given player and with an appropriate resumption of play. This latter ingredient accounts for the fact that neither player might win (that is, neither B nor ¬B might be provable).     

Classical proof forestry

Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’.This paper presents classical proof forests as a graphical proof formalism and investigates the possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given.Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising.     

Some remarks on lengths of propositional proofs

We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly bounded by the number of lines. Depthd Frege proofs ofm lines can be transformed into depthd proofs ofO(m ^d+1) symbols. We show that renaming Frege proof systems are p-equivalent to extended Frege systems. Some open problems in propositional proof length and in logical flow graphs are discussed. Supported in part by NSF grant DMS-9205181     

Proof-theoretic conservations of weak weak intuitionistic constructive set theories

The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional set theories whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms.     

A focused approach to combining logics

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.     

Aglianò-Montagna type decomposition of linear pseudo hoops and its applications

We decompose every linear pseudo hoop as an Aglianò-Montagna type of ordinal sum of linear Wajsberg pseudo hoops which are either negative cones of linear ?-groups or intervals in linear unital ?-groups with strong unit. We apply the decomposition to present a new proof that every linear pseudo BL-algebra and consequently every representable pseudo BL-algebra is good. Moreover, we show that every maximal filter and every value of a linear pseudo hoop is normal, and every σ-complete linear pseudo hoop is commutative.     

Another theorem of Cauchy which ‘admits exceptions’

Several exceptions are provided for a theorem in Cauchy’s Cours d’Analyse in the proof of which the need for uniform convergence has been ignored. A reconstruction of this theorem is offered.     

Erratum to: “The Schrödinger–Maxwell system with Dirac mass” [Ann. Inst. H. Poincaré Anal. Non Linéaire 24 (5) (2007) 773–793]

We correct the proof of [G.M. Coclite, H. Holden, The Schrödinger–Maxwell system with Dirac mass, Ann. Inst. H. Poincaré Anal. Non Linéaire 24 (5) (2007) 773–793, Lemma 4.1].     

Ordinal arithmetic with simultaneously defined theta‐functions

This article provides a detailed comparison between two systems of collapsing functions. These functions play a crucial role in proof theory, in the analysis of patterns of resemblance, and the analysis of maximal order types of well partial orders. The exact correspondence given here serves as a starting point for far reaching extensions of current results on patterns and well partial orders. © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim     

Epsilon substitution method for elementary analysis

We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.     

Axiomatizations of team logics

In a modular approach, we lift Hilbert-style proof systems for propositional, modal and first-order logic to generalized systems for their respective team-based extensions. We obtain sound and complete axiomatizations for the dependence-free fragment FO(～) of Väänänen's first-order team logic TL, for propositional team logic PTL, quantified propositional team logic QPTL, modal team logic MTL, and for the corresponding logics of dependence, independence, inclusion and exclusion.As a crucial step in the completeness proof, we show that the above logics admit, in a particular sense, a semantics-preserving elimination of modalities and quantifiers from formulas.     

Decomposition of BL-chains

A simple and self contained proof of decomposition of BL-chains into ordinal sums of Wajsberg hoops is given.Received October 23, 2003; accepted in final form September 11, 2004.     

On quantitative versions of theorems due to F.E. Browder and R. Wittmann

This paper is another case study in the program of logically analyzing proofs to extract new (typically effective) information (‘proof mining’). We extract explicit uniform rates of metastability (in the sense of T. Tao) from two ineffective proofs of a classical theorem of F.E. Browder on the convergence of approximants to fixed points of nonexpansive mappings as well as from a proof of a theorem of R. Wittmann which can be viewed as a nonlinear extension of the mean ergodic theorem. The first rate is extracted from Browder's original proof that is based on an application of weak sequential compactness (in addition to a projection argument). Wittmann's proof follows a similar line of reasoning and we adapt our analysis of Browder's proof to get a quantitative version of Wittmann's theorem as well. In both cases one also obtains totally elementary proofs (even for the strengthened quantitative forms) of these theorems that neither use weak compactness nor the existence of projections anymore. In this way, the present article also discusses general features of extracting effective information from proofs based on weak compactness. We then extract another rate of metastability (of similar nature) from an alternative proof of Browder's theorem essentially due to Halpern that already avoids any use of weak compactness. The paper is concluded by general remarks concerning the logical analysis of proofs based on weak compactness as well as a quantitative form of the so-called demiclosedness principle. In a subsequent paper these results will be utilized in a quantitative analysis of Baillon's nonlinear ergodic theorem.     

A complete many-valued logic with product-conjunction

A simple complete axiomatic system is presented for the many-valued propositional logic based on the conjunction interpreted as product, the coresponding implication (Goguen's implication) and the corresponding negation (Gödel's negation). Algebraic proof methods are used. The meaning for fuzzy logic (in the narrow sense) is shortly discussed.This article was processed by the author using the LATEX style filepljorlm from Springer-Verlag.     

Corrigendum to “Kripke‐style semantics for many‐valued logics”

This note contains a correct proof of the fact that the set of all first‐order formulas which are valid in all predicate Kripke frames for Hájek's many‐valued logic BL is not arithmetical. The result was claimed in [5], but the proof given there was incorrect. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Order-enriched categorical models of the classical sequent calculus

It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations.     

Erratum to “Normality and countable paracompactness of hyperspaces of ordinals” [Topology Appl. 154 (2007) 358-362]

We correct the proof of Theorem 8 in “Normality and countable paracompactness of hyperspaces of ordinals” [Topology Appl. 154 (2007) 358-362].     

Algebraic proof theory for substructural logics: Cut-elimination and completions

We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.We introduce the substructural hierarchy — a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N₂ in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.