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.     

Completeness for flat modal fixpoint logics

This paper exhibits a general and uniform method to prove axiomatic completeness for certain modal fixpoint logics. Given a set Γ of modal formulas of the form γ(x,p₁,…,p_n), where x occurs only positively in γ, we obtain the flat modal fixpoint language L_?(Γ) by adding to the language of polymodal logic a connective ?_γ for each γ∈Γ. The term ?_γ(φ₁,…,φ_n) is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x,φ₁,…,φ_n). We consider the following problem: given Γ, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language L_?(Γ) on Kripke structures. We prove two results that solve this problem.First, let be the logic obtained from the basic polymodal by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective ?_γ. Provided that each indexing formula γ satisfies a certain syntactic criterion, we prove this axiom system to be complete.Second, addressing the general case, we prove the soundness and completeness of an extension of . This extension is obtained via an effective procedure that, given an indexing formula γ as input, returns a finite set of axioms and derivation rules for ?_γ, of size bounded by the length of γ. Thus the axiom system is finite whenever Γ is finite.     

Prefinitely axiomatizable modal and intermediate logics

A logic Λ bounds a property P if all proper extensions of Λ have P while Λ itself does not. We construct logics bounding finite axiomatizability and logics bounding finite model property in the lattice of intermediate logics and in the lattice of normal extensions of K4.3. MSC: 03B45, 03B55.     

The Skolemization of prenex formulas in intermediate logics

The skolem class of a logic consists of the formulas for which the derivability of the formula is equivalent to the derivability of its Skolemization. In contrast to classical logic, the skolem classes of many intermediate logics do not contain all formulas. In this paper it is proven for certain classes of propositional formulas that any instance of them by (independent) predicate sentences in prenex normal form belongs to the skolem class of any intermediate logic complete with respect to a class of well-founded trees. In particular, all prenex sentences belong to the skolem class of these logics, and this result extends to the constant domain versions of these logics.     

Elementary axioms for local maps of toposes

We present a complete elementary axiomatization of local maps of toposes.     

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 finite model property for semilinear substructural logics

In this paper, we show that the finite model property fails for certain non‐integral semilinear substructural logics including Metcalfe and Montagna's uninorm logic and involutive uninorm logic, and a suitable extension of Metcalfe, Olivetti and Gabbay's pseudo‐uninorm logic. Algebraically, the results show that certain classes of bounded residuated lattices that are generated as varieties by their linearly ordered members are not generated as varieties by their finite members.     

Note on witnessed Gödel logics with Delta

Witnessed Gödel logics are based on the interpretation of ∀ (∃) by minimum (maximum) instead of supremum (infimum). Witnessed Gödel logics appear for many practical purposes more suited than usual Gödel logics as the occurrence of proper infima/suprema is practically irrelevant. In this note we characterize witnessed Gödel logics with absoluteness operator △ w.r.t. witnessed Gödel logics using a uniform translation.     

Note on Deduction Theorems in contraction‐free logics

This paper provides a finer analysis of the well‐known form of the Local Deduction Theorem in contraction‐free logics (understood as Tarski‐style finitary structural consequence relations). An infinite hierarchy of its natural strengthenings is introduced and studied. The main results are the separation of its initial four members and the subsequent collapse of the hierarchy.     

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.     

The double negation of the intermediate value theorem

In the context of intuitionistic analysis, we consider the set F consisting of all continuous functions ? from [0,1] to R such that ?(0)=0 and ?(1)=1, and the set I₀ consisting of ?’s in F where there exists x∈[0,1] such that . It is well-known that there are weak counterexamples to the intermediate value theorem, and with Brouwer’s continuity principle we have I₀≠F. However, there exists no satisfying answer to . We try to answer to this question by reducing it to a schema (which we call ) about intuitionistic decidability that asserts “there exists an intuitionistically enumerable set that is not intuitionistically decidable”. We also introduce the notion of strong Specker double sequence, and prove that the existence of such a double sequence is equivalent to the existence of a function ?∈F_mon where .     

First-order t-norm based fuzzy logics with truth-constants: Distinguished semantics and completeness properties

This paper aims at being a systematic investigation of different completeness properties of first-order predicate logics with truth-constants based on a large class of left-continuous t-norms (mainly continuous and weak nilpotent minimum t-norms). We consider standard semantics over the real unit interval but also we explore alternative semantics based on the rational unit interval and on finite chains. We prove that expansions with truth-constants are conservative and we study their real, rational and finite chain completeness properties. Particularly interesting is the case of considering canonical real and rational semantics provided by the algebras where the truth-constants are interpreted as the numbers they actually name. Finally, we study completeness properties restricted to evaluated formulae of the kind , where φ has no additional truth-constants.     

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.     

Automated discovery of single axioms for ortholattices

We present short single axioms for ortholattices, orthomodular lattices, and modular ortholattices, all in terms of the Sheffer stroke. The ortholattice axiom is the shortest possible. We also give multiequation bases in terms of the Sheffer stroke and in terms of join, meet, and complementation. Proofs are omitted but are available in an associated technical report and on the Web. We used computers extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms.Received February 26, 2004; accepted in final form September 14, 2004.     

Craig interpolation for semilinear substructural logics

The Craig interpolation property is investigated for substructural logics whose algebraic semantics are varieties of semilinear (subdirect products of linearly ordered) pointed commutative residuated lattices. It is shown that Craig interpolation fails for certain classes of these logics with weakening if the corresponding algebras are not idempotent. A complete characterization is then given of axiomatic extensions of the “R‐mingle with unit” logic (corresponding to varieties of Sugihara monoids) that have the Craig interpolation property. This latter characterization is obtained using a model‐theoretic quantifier elimination strategy to determine the varieties of Sugihara monoids admitting the amalgamation property.     

Labeled sequent calculus for justification logics

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for $\mathsf{S4LPN}$ based on Artemov–Fitting models.     

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.     

Separability of normalizable superintuitionistic propositional logics

The problem of separability of superintuitionistic propositional logics that are extensions of the intuitionistic propositional logic is studied. A criterion of separability of normal superintuitionistic propositional logics, as well as results concerning the completeness of their subcalculi is obtained. This criterion makes it possible to determine whether a normalizable superintuitionistic propositional logic is separable. By means of these results, the mistakes discovered by the author in the proofs of certain statements by McKay and Hosoi are corrected.Translated fromMatematicheskie Zametki, Vol. 64, No. 4, pp. 606–615, October, 1998.This research was supported by the Russian Foundation for Basic Research under grant No. 94-01-00944.     

On the classification of first order Gödel logics

We characterize the recursively enumerable first order Gödel logics with △ with respect to validity and non-satisfiability. The finitely valued and four infinitely valued Gödel logics with △ are recursively enumerable, not-satisfiability is recursively enumerable if validity is recursively enumerable. This is in contrast to first order Gödel logics without △, where validity is recursively enumerable for finitely valued and two infinitely valued Gödel logics, not-satisfiability is recursively enumerable if validity is recursively enumerable or 0 isolated in the truth value set.     

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.