Proof analysis in intermediate logics
type: Item
instance of: scholarly article
title: Proof analysis in intermediate logics
zbMATH Open document ID: 1241.03068
author: Roy Dyckhoff
author: Sara Negri
published in: Archive for Mathematical Logic
publication date: 2012-02-10T00:00:00Z
review text: The authors continue the investigation of cut-free systems for superintuitionistic logics inspired by translating a formula \(F\) into a formula saying ``\(F\) is true in all Kripke models'' (of a given logic). The approach works smoothly when the condition on the accessibility relation in Kripke models is expressed by a geometric formula \(\forall\bar{Z}P\rightarrow \exists\bar{x}M\) where \(P\) is a conjunction of atomic formulas and \(M\) is a disjunction of conjunctions of atomic formulas.
reviewed by: G. E. Mints
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B55
Mathematics Subject Classification ID: 03F03
zbMATH DE Number: 6005016
zbMATH Keywords: sequent calculus
zbMATH Keywords: intermediate logic
zbMATH Keywords: modal logic
zbMATH Keywords: labelled deduction
describes a project that uses: Pesca
MaRDI profile type: Publication
full work available at URL: s00153-011-0254-7
OpenAlex ID: W1968581827
cites work: Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics
cites work: On Skolemization in constructive theories
cites work: Q3367318
cites work: Q3128959
cites work: Expanding the Realm of Systematic Proof Theory
cites work: Modal Logics Between S 4 and S 5
cites work: A deterministic terminating sequent calculus for Godel-Dummett logic
cites work: Decision methods for linearly ordered Heyting algebras
cites work: A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding
cites work: Counting the maximal intermediate constructive logics
cites work: Proof methods for modal and intuitionistic logics
cites work: Q4894942
cites work: Tableau methods for modal and temporal logics
cites work: On the rules of intermediate logics
cites work: THE CALCULUS OF THE WEAK "LAW OF EXCLUDED MIDDLE"
cites work: Q3241192
cites work: Q5843956
cites work: Q5688807
cites work: A completeness theorem in modal logic
cites work: Interpolation properties of superintuitionistic logics
cites work: Q5545505
cites work: Some theorems about the sentential calculi of Lewis and Heyting
cites work: Q4495850
cites work: Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
cites work: Proof analysis in modal logic
cites work: Q5457385
cites work: Cut Elimination in the Presence of Axioms
cites work: Structural proof theory. With an appendix by Aarne Ranta
cites work: Proof systems for lattice theory
cites work: Proof-theoretical analysis of order relations
cites work: Proof Analysis
cites work: A sequent calculus and a theorem prover for standard conditional logics
cites work: Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents
cites work: Q3999539
cites work: Proof theory of modal logic. Proceedings of a workshop, Hamburg, Germany, November 19--20, 1993
cites work: Displaying modal logic
DOI: 10.1007/S00153-011-0254-7
Recommended article: Q3787975
Recommended article: Proof analysis in modal logic
Recommended article: Q5457385
Recommended article: A proof-theoretical analysis of semiconstructive intermediate theories
Recommended article: Analytic Methods for the Logic of Proofs
Recommended article: Q3340837
Recommended article: Q3212265
Recommended article: Q3824287
Recommended article: An analytic calculus for the intuitionistic logic of proofs
Recommended article: Q4726226
description: scientific article; zbMATH DE number 6005016