Frame definability, canonicity and cut elimination in common sense modal predicate logics

2020 ◽  
Author(s):  
Takahiro Sawasaki ◽  
Katsuhiko Sano
Keyword(s):  
Common Sense ◽  
Predicate Logic ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Axiom Schema ◽  
Modal Predicate Logics ◽  
Modal Predicate Logic

Abstract The paper presents semantically complete Hilbert-style systems for some variants of common sense modal predicate logic proposed by van Benthem and further developed by Seligman. The paper also investigates frame definability in the logics and shows what axiom schema is canonical in the logics. In addition to these semantic investigations on the logics, the paper provides the sequent calculi for some of the logics which enjoy cut elimination theorem.

On the degrees of unsolvability of modal predicate logics of provability

1994 ◽  
Vol 59 (1) ◽  
pp. 253-261
Author(s):  
Vann McGee
Keyword(s):  
Predicate Logic ◽  
General Theorem ◽  
Modal Formula ◽  
Sentential Logic ◽  
Starting Point ◽  
Special Cases ◽  
Modal Predicate Logics ◽  
Arithmetical Formula ◽  
Modal Predicate Logic ◽  
Striking Contrast

The modal predicate logic of provability identifies the “□” of modal logic with the “Bew” of proof theory, so that, where “Bew” is a formula representing, in the usual way, provability in a consistent, recursively axiomatized theory Γ extending Peano arithmetic (PA), an interpretation of a language for the modal predicate calculus is a map * which associates with each modal formula an arithmetical formula with the same free variables which commutes with the Boolean connectives and the quantifiers and which sets (□ϕ)* equal to Bew(⌈ϕ*⌉). Where Δ is an extension of PA (all the theories we discuss will be extensions of PA), MPL(Δ) will be the set of modal formulas ϕ such that, for every interpretation *, ϕ* is a theorem of Δ. Most of what is currently known about the modal predicate logic of provability consists in demonstrations that MPL(Δ) must be computationally highly complex. Thus Vardanyan [11] shows that, provided that Δ is 1-consistent and recursively axiomatizable, MPL(Δ) will be complete , and Boolos and McGee [5] show that MPL({true arithmetical sentences}) is complete in {true arithmetical sentences}. All of these results take as their starting point Artemov's demonstration in [1] that {true arithmetical sentences} is 1-reducible to MPL({true arithmetical sentences}).The aim here is to consolidate these results by providing a general theorem which yields all the other results as special cases. These results provide a striking contrast with the situation in modal sentential logic (MSL); according to fundamental results of Solovay [8], provided Γ does not entail any falsehoods, MSL({true arithmetical sentences}) and MSL(PA) (which is the same as MSL(Γ)) are both decidable.

Cut Elimination in the Presence of Axioms

1998 ◽  
Vol 4 (4) ◽  
pp. 418-435 ◽  
Author(s):  
Sara Negri ◽  
Jan von Plato
Keyword(s):  
Structural Analysis ◽  
Wide Class ◽  
Predicate Logic ◽  
Free Variable ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Pure Logic ◽  
Suitable Form

AbstractA way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate logic with equality in which also cuts on the equality axioms are eliminated.

UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS

2014 ◽  
Vol 7 (3) ◽  
pp. 455-483 ◽  
Author(s):  
MAJID ALIZADEH ◽  
FARZANEH DERAKHSHAN ◽  
HIROAKIRA ONO
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Substructural Logics ◽  
Substructural Logic ◽  
Sequent Calculi ◽  
Structural Rule ◽  
Modal Propositional Logic ◽  
Uniform Interpolation ◽  
Classical Predicate

AbstractUniform interpolation property of a given logic is a stronger form of Craig’s interpolation property where both pre-interpolant and post-interpolant always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic S4, which have Craig’s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.

Gentzen sequent calculi for some intuitionistic modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 596-623
Author(s):  
Zhe Lin ◽  
Minghui Ma
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Intuitionistic Propositional Logic ◽  
Propositional Language ◽  
Intuitionistic Modal Logics ◽  
Subformula Property ◽  
Gentzen Sequent Calculus

Abstract Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond ,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond ,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

The complexity of the modal predicate logic of “true in every transitive model of ZF”

1997 ◽  
Vol 62 (4) ◽  
pp. 1371-1378
Author(s):  
Vann McGee
Keyword(s):  
Lower Bound ◽  
Set Theory ◽  
Predicate Logic ◽  
Alternative Conception ◽  
Predicate Calculus ◽  
Modal Formula ◽  
Sentential Calculus ◽  
Transitive Model ◽  
Modal Predicate Logic

Robert Solovay [8] investigated the version of the modal sentential calculus one gets by taking “□ϕ” to mean “ϕ is true in every transitive model of Zermelo-Fraenkel set theory (ZF).” Defining an interpretation to be a function * taking formulas of the modal sentential calculus to sentences of the language of set theory that commutes with the Boolean connectives and sets (□ϕ)* equal to the statement that ϕ* is true in every transitive model of ZF, and stipulating that a modal formula ϕ is valid if and only if, for every interpretation *, ϕ* is true in every transitive model of ZF, Solovay obtained a complete and decidable set of axioms.In this paper, we stifle the hope that we might continue Solovay's program by getting an analogous set of axioms for the modal predicate calculus. The set of valid formulas of the modal predicate calculus is not axiomatizable; indeed, it is complete .We also look at a variant notion of validity according to which a formula ϕ counts as valid if and only if, for every interpretation *, ϕ* is true. For this alternative conception of validity, we shall obtain a lower bound of complexity: every set which is in the set of sentences of the language of set theory true in the constructible universe will be 1-reducible to the set of valid modal formulas.

scholarly journals The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

2020 ◽  
Vol 20 (6) ◽  
pp. 990-1005
Author(s):  
Ekaterina Komendantskaya ◽  
Dmitry Rozplokhas ◽  
Henning Basold
Keyword(s):  
Cut Elimination ◽  
Horn Clause ◽  
Sequent Calculi ◽  
New Normal ◽  
Novel Method

AbstractIn sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen’s classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

Sign in / Sign up

Export Citation Format

Share Document