Admissible rules in the implication-negation fragment of intuitionistic logic

Uniform infinite bases are defined for the single-conclusion and multiple-conclusion admissible rules of the implication-negation fragments of intuitionistic logic and its consistent axiomatic extensions (intermediate logics). A Kripke semantics characterization is given for the (hereditarily) structurally complete implication-negation fragments of intermediate logics, and it is shown that the admissible rules of this fragment of form a PSPACE-complete set and have no finite basis.     

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.     

On the rules of intermediate logics

If the Visser rules are admissible for an intermediate logic, they form a basis for the admissible rules of the logic. How to characterize the admissible rules of intermediate logics for which not all of the Visser rules are admissible is not known. In this paper we give a brief overview of results on admissible rules in the context of intermediate logics. We apply these results to some well-known intermediate logics. We provide natural examples of logics for which the Visser rule are derivable, admissible but nonderivable, or not admissible. Supported by the Austrian Science Fund FWF under projects P16264 and P16539.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

The Σ1-provability logic of HA

In this paper we introduce a modal theory ${\mathsf{iH}}_{\sigma }$ which is sound and complete for arithmetical ${\mathrm{\Sigma }}_1$-interpretations in $\mathsf{HA}$, in other words, we will show that ${\mathsf{iH}}_{\sigma }$ is the ${\mathrm{\Sigma }}_1$-provability logic of $\mathsf{HA}$. Moreover we will show that ${\mathsf{iH}}_{\sigma }$ is decidable. As a by-product of these results, we show that $\mathsf{HA}+\square \perp$ has de Jongh property.     

Reasoning about proof and knowledge

In previous work [15], we presented a hierarchy of classical modal systems, along with algebraic semantics, for the reasoning about intuitionistic truth, belief and knowledge. Deviating from Gödel's interpretation of IPC in S4, our modal systems contain IPC in the way established in [13]. The modal operator can be viewed as a predicate for intuitionistic truth, i.e. proof. Epistemic principles are partially adopted from Intuitionistic Epistemic Logic IEL [4]. In the present paper, we show that the S5-style systems of our hierarchy correspond to an extended Brouwer–Heyting–Kolmogorov interpretation and are complete w.r.t. a relational semantics based on intuitionistic general frames. In this sense, our S5-style logics are adequate and complete systems for the reasoning about proof combined with belief or knowledge. The proposed relational semantics is a uniform framework in which also IEL can be modeled. Verification-based intuitionistic knowledge formalized in IEL turns out to be a special case of the kind of knowledge described by our S5-style systems.     

The complexity of the Pigeonhole Principle

The Pigeonhole Principle forn is the statement that there is no one-to-one function between a set of sizen and a set of sizen–1. This statement can be formulated as an unlimited fan-in constant depth polynomial size Boolean formulaPHP _n inn(n–1) variables. We may think that the truth-value of the variablex _i,j will be true iff the function maps thei-th element of the first set to thej-th element of the second (see Cook and Rechkow [5]).PHP _n can be proved in the propositional calculus. That is, a sequence of Boolean formulae can be given so that each one is either an axiom of the propositional calculus or a consequence of some of the previous ones according to an inference rule of the propositional calculus, and the last one isPHP _n . Our main result is that the Pigeonhole Principle cannot be proved this way, if the size of the proof (the total number or symbols of the formulae in the sequence) is polynomial inn and each formula is constant depth (unlimited fan-in), polynomial size and contains only the variables ofPHP _n .     

Tarski's theorem on intuitionistic logic,for polyhedra

In 1938, Tarski proved that a formula is not intuitionistically valid if, and only if, it has a counter-model in the Heyting algebra of open sets of some topological space. In fact, Tarski showed that any Euclidean space ${\mathbb{R}}^n$ with $n?1$ suffices, as does e.g. the Cantor space. In particular, intuitionistic logic cannot detect topological dimension in the Heyting algebra of all open sets of a Euclidean space. By contrast, we consider the lattice of open subpolyhedra of a given compact polyhedron $P?{\mathbb{R}}^n$, prove that it is a locally finite Heyting subalgebra of the (non-locally-finite) algebra of all open sets of P, and show that intuitionistic logic is able to capture the topological dimension of P through the bounded-depth axiom schemata. Further, we show that intuitionistic logic is precisely the logic of formulæ valid in all Heyting algebras arising from polyhedra in this manner. Thus, our main theorem reconciles through polyhedral geometry two classical results: topological completeness in the style of Tarski, and Ja?kowski's theorem that intuitionistic logic enjoys the finite model property. Several questions of interest remain open. E.g., what is the intermediate logic of all closed triangulable manifolds?     

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).     

Proof internalization in generalized Frege systems for classical logic

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.     

Proofs with monotone cuts

Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK (or equivalently, in Frege systems). We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut‐formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.     

Short propositional refutations for dense random 3CNF formulas

Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notable are the exponential-size resolution refutation lower bounds for random 3CNF formulas with Ω(n^1.5−ε)$\mathrm{\Omega }(n^{1.5-\epsilon })$ clauses (Chvátal and Szemerédi [14], Ben-Sasson and Wigderson [10]). On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutations in a non-abstract propositional proof system is for resolution with Ω(n²/log?n)$\mathrm{\Omega }(n^2/\log ?n)$ clauses, shown by Beame et al. [6]. In this paper we show that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomial-size propositional refutations whose lines are TC⁰${\mathit{T}\mathit{C}}^0$ formulas (i.e., TC⁰${\mathit{T}\mathit{C}}^0$-Frege proofs) for random 3CNF formulas with n   variables and Ω(n^1.4)$\mathrm{\Omega }(n^{1.4})$ clauses.     

A constructive investigation of satisfiability

We present a constructive analysis of the logical notions of satisfiability and consistency for first-order intuitionistic formulae. In particular, we use formal topology theory to provide a positive semantics for satisfiability. Then we propose a “co-inductive” logical calculus, which captures the positive content of consistency.     

Equivalence of bar induction and bar recursion for continuous functions with continuous moduli

We compare Brouwer's bar theorem and Spector's bar recursion for the lowest type in the context of constructive reverse mathematics. To this end, we reformulate bar recursion as a logical principle stating the existence of a bar recursor for every function which serves as the stopping condition of bar recursion. We then show that the decidable bar induction is equivalent to the existence of a bar recursor for every continuous function from ${\mathbb{N}}^{\mathbb{N}}$ to $\mathbb{N}$ with a continuous modulus. We also introduce fan recursion, the bar recursion for binary trees, and show that the decidable fan theorem is equivalent to the existence of a fan recursor for every continuous function from ${\{0,1\}}^{\mathbb{N}}$ to $\mathbb{N}$ with a continuous modulus. The equivalence for bar induction holds over the extensional version of intuitionistic arithmetic in all finite types augmented with the characteristic principles of Gödel's Dialectica interpretation. On the other hand, we show the equivalence for fan theorem without using such extra principles.     

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.     

Arithmetical complexity of fuzzy predicate logics — A survey II

Results on arithmetical complexity of important sets of formulas of several fuzzy predicate logics (tautologies, satisfiable formulas, …) are surveyed and some new results are proven.     

The axiomatic power of Kolmogorov complexity

The famous Gödel incompleteness theorem states that for every consistent, recursive, and sufficiently rich formal theory T there exist true statements that are unprovable in T. Such statements would be natural candidates for being added as axioms, but how can we obtain them? One classical (and well studied) approach is to add to some theory T an axiom that claims the consistency of T  . In this paper we discuss another approach motivated by Chaitin's version of Gödel's theorem where axioms claiming the randomness (or incompressibility) of some strings are probabilistically added, and show that it is not really useful, in the sense that this does not help us prove new interesting theorems. This result answers a question recently asked by Lipton. The situation changes if we take into account the size of the proofs: randomly chosen axioms may help making proofs much shorter (unless NP=PSPACE$\mathrm{NP}=\mathrm{PSPACE}$).