Possible world semantics for first-order logic of proofs

In the tech report Artemov and Yavorskaya (Sidon) (2011) [4] an elegant formulation of the first-order logic of proofs was given, FOLP. This logic plays a fundamental role in providing an arithmetic semantics for first-order intuitionistic logic, as was shown. In particular, the tech report proved an arithmetic completeness theorem, and a realization theorem for FOLP. In this paper we provide a possible-world semantics for FOLP, based on the propositional semantics of Fitting (2005) [5]. We also give an Mkrtychev semantics. Motivation and intuition for FOLP can be found in Artemov and Yavorskaya (Sidon) (2011) [4], and are not fully discussed here.     

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     

Prefixed tableaus and nested sequents

Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants of each other, roughly in the same way that Gentzen sequent calculi and tableaus are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators.     

Elimination of Skolem functions for monotone formulas in analysis

In this paper a new method, elimination of Skolem functions for monotone formulas, is developed which makes it possible to determine precisely the arithmetical strength of instances of various non-constructive function existence principles. This is achieved by reducing the use of such instances in a given proof to instances of certain arithmetical principles. Our framework are systems -qf , where (GA is a hierarchy of (weak) subsystems of arithmetic in all finite types (introduced in [14]), AC-qf is the schema of quantifier-free choice in all types and is a set of certain analytical principles which e.g. includes the binary K?nig's lemma. We apply this method to show that the arithmetical closures of single instances of -comprehension and -choice contribute to the growth of extractable bounds from proofs relative to only by a primitive recursive functional in the sense of Kleene. In subsequent papers these results are widely generalized and the method is used to determine the arithmetical content of single sequences of instances of the Bolzano-Weierstra? principle for bounded sequences in , the Ascoli-lemma and others. February 14, 1996     

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.     

Consistency proof via pointwise induction

We show that the consistency of the first order arithmetic follows from the pointwise induction up to the Howard ordinal. Our proof differs from U. Schmerl [Sc]: We do not need Girard's Hierarchy Comparison Theorem. A modification on the ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down in ordinals. Also a generalization to theories of finitely iterated inductive definitions is proved. Received May 30, 1996     

Kripke semantics for provability logic GLP

A well-known polymodal provability logic due to Japaridze is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic. This system plays an important role in some recent applications of provability algebras in proof theory. However, an obstacle in the study of is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for . First, we isolate a certain subsystem of that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for are defined as the limits of chains of finite expansions of models for . The techniques involves unions of n-elementary chains and inverse limits of Kripke models. All the results are obtained by purely modal-logical methods formalizable in elementary arithmetic.     

Cutting planes,connectivity, and threshold logic

Originating from work in operations research the cutting plane refutation systemCP is an extension of resolution, where unsatisfiable propositional logic formulas in conjunctive normal form are recognized by showing the non-existence of boolean solutions to associated families of linear inequalities. Polynomial sizeCP proofs are given for the undirecteds-t connectivity principle. The subsystemsCP _q ofCP, forq2, are shown to be polynomially equivalent toCP, thus answering problem 19 from the list of open problems of [8]. We present a normal form theorem forCP ₂-proofs and thereby for arbitraryCP-proofs. As a corollary, we show that the coefficients and constant terms in arbitrary cutting plane proofs may be exponentially bounded by the number of steps in the proof, at the cost of an at most polynomial increase in the number of steps in the proof. The extensionCPLE ⁺, introduced in [9] and there shown top-simulate Frege systems, is proved to be polynomially equivalent to Frege systems. Lastly, since linear inequalities are related to threshold gates, we introduce a new threshold logic and prove a completeness theorem.Supported in part by NSF grant DMS-9205181 and by US-Czech Science and Technology Grant 93-205Partially supported by NSF grant CCR-9102896 and by US-Czech Science and Technology Grant 93-205     

Interpolation property for bicartesian closed categories

Summary We show that proofs in the intuitionistic propositional logic factor through interpolants-in this way we prove a stronger interpolation property than the usual one which gives only the existence of interpolants.Translating that to categorical terms, we show that Pushouts (bipushouts) of bicartesian closed categories have the interpolation property (Theorem 3.2).     

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.     

Proof complexity of intuitionistic implicational formulas

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions.In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrube? (2007), generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Je?ábek (2009), can be realized by implicational tautologies.     

Around provability logic

We present some results on algebraic and modal analysis of polynomial (intrinsically definable) distortions of the standard provability predicate in Peano Arithmetic PA, and investigate three provability-like modal systems related to the Gödel-Löb modal system GL. We also present a short review of relational and topological semantics for these systems, and describe the dual category of algebraic models of our main modal system.     

Generalizing realizability and Heyting models for constructive set theory

This article presents a common generalization of the two main methods for obtaining class models of constructive set theory. Heyting models are a generalization of the Boolean models for classical set theory which are a variant of forcing, while realizability is a decidedly constructive method that has first been developed for number theory by Kleene and was later very fruitfully adapted to constructive set theory. In order to achieve the generalization, a new kind of structure (applicative topologies) is introduced, which contains both elements of formal topology and applicative structures. This approach not only deepens the understanding of class models and leads to more efficiency in proofs about these kinds of models, but also makes it possible to prove new results about the two special cases that were not known before and to construct new models.     

Wellfoundedness proofs by means of non-monotonic inductive definitions II: First order operators

In this paper, we give two proofs of the wellfoundedness of a recursive notation system for Π_N-reflecting ordinals. One is based on distinguished classes, and the other is based on -inductive definitions.     

Proof-functional connectives and realizability

The meaning of a formula built out of proof-functional connectives depends in an essential way upon the intensional aspect of the proofs of the component subformulas. We study three such connectives, strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), strong conjunction (where the two components of the conjunction are established by the same proof) and relevant implication (where the implication is established by an identity map). For each of these connectives we give a type assignment system, a realizability semantics, and a completeness theorem. This form of completeness implies the semantic completeness of the type assignment system.     

Positive provability logic for uniform reflection principles

We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ω   corresponds to the full uniform reflection schema, whereas n<ω$n<\omega$ corresponds to its restriction to arithmetical _Πn+1${\Pi }_{n+1}$-formulas. This calculus is shown to be complete w.r.t. a suitable class of finite Kripke models and to be decidable in polynomial time.     

Extended Curry‐Howard terms for second‐order logic

In order to allow the use of axioms in a second‐order system of extracting programs from proofs, we define constant terms, a form of Curry‐Howard terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended Curry‐Howard terms are strongly normalizable.     

On the computational complexity of cut-reduction

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.     

Homology of proof-nets

This work defines homology groups for proof-structures in multiplicative linear logic (see [Gir1], [Gir2], [Dan]). We will show that these groups characterize proof-nets among arbitrary proof-structures, thus obtaining a new correctness criterion and of course a new polynomial algorithm for testing correctness. This homology also bears information on sequentialization. An unexpected geometrical interpretation of the linear connectives is given in the last section. This paper exclusively focuses onabstract proof-structures, i.e. paired-graphs. The relation with actual proofs is investigated in [Gir1], [Gir2], [Dan], [Ret] and [Tro].