Explicit Provability and Constructive Semantics

2001 ◽  
Vol 7 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Sergei N. Artemov
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Modal Logics ◽  
Combinatory Logic ◽  
Underlying Structure ◽  
Intuitionistic Propositional Logic ◽  
Intuitionistic Modal Logics

AbstractIn 1933 Gödel introduced a calculus of provability (also known as modal logicS4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logicLPof propositions and proofs and show that Gödel's provability calculus is nothing but the forgetful projection ofLP. This also achieves Gödel's objective of defining intuitionistic propositional logicIntvia classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics forIntwhich resisted formalization since the early 1930s.LPmay be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus.

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.

scholarly journals A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Ki Yung Ahn ◽  
Ross Horne ◽  
Alwen Tiu
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
Completeness Proof ◽  
Intuitionistic Modal Logic ◽  
Free Variables ◽  
Open Process ◽  
Intuitionistic Modal Logics

Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.

Deductive Completeness

1996 ◽  
Vol 2 (3) ◽  
pp. 243-283 ◽  
Author(s):  
Kosta Došen
Keyword(s):  
Category Theory ◽  
Propositional Logic ◽  
Completeness Theorem ◽  
Substructural Logics ◽  
Combinatory Logic ◽  
Functional Completeness ◽  
Deduction Theorem ◽  
Intuitionistic Propositional Logic

AbstractThis is an exposition of Lambek's strengthening and generalization of the deduction theorem in categories related to intuitionistic propositional logic. Essential notions of category theory are introduced so as to yield a simple reformulation of Lambek's Functional Completeness Theorem, from which its main consequences can be readily drawn. The connections of the theorem with combinatory logic, and with modal and substructural logics, are briefly considered at the end.

scholarly journals From intuitionism to Brouwer’s modal logic

2020 ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Main Idea ◽  
Intuitionistic Propositional Logic ◽  
Strict Implication

We try to translate the intuitionistic propositional logic INT into Brouwer’s modal logic KTB. Our translation is motivated by intuitions behind Brouwer’s axiom p →☐◊p as discussed in [4]. The main idea is to interpret intuitionistic implication as modal strict implication, whereas variables and other positive sen-tences remain as they are. The proposed translation preserves fragments of the Rieger-Nishimura lattice which is the Lindenbaum algebra of monadic formulas in INT. Unfortunately, INT is not embedded by this mapping into KTB.

A CORRECT POLYNOMIAL TRANSLATION OF S4 INTO INTUITIONISTIC LOGIC

2019 ◽  
Vol 84 (02) ◽  
pp. 439-451
Author(s):  
RAJEEV GORÉ ◽  
JIMMY THOMSON
Keyword(s):  
Modal Logic ◽  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Intuitionistic Propositional Logic ◽  
Normal Modal Logic ◽  
Modal Logic S4 ◽  
Polynomial Translation

AbstractWe show that the polynomial translation of the classical propositional normal modal logic S4 into the intuitionistic propositional logic Int from Fernández is incorrect. We give a modified translation and prove its correctness, and provide implementations of both translations to allow others to test our results.

On formalizing the distinction between logical and factual truth

1966 ◽  
Vol 31 (3) ◽  
pp. 460-477
Author(s):  
William H. Hanson
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Modal Logics ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Feature Section

Semantical systems that distinguish between logically true and factually true formulas are well-known from the work of Carnap. The present paper is concerned with extending the formalization of this distinction in two ways. First, we show how to construct syntactical (i.e., logistic) systems that correspond to semantical systems of the type just mentioned. Such a syntactical system for propositional logic is developed in section 3. Similar systems for first-order logic are sketched in section 5. Second, we show how to extend semantical systems that make the logical-factual distinction to languages containing modal connectives. Carnap's work on modal logic conspicuously lacks this feature. Section 4 contains such semantical systems for four well-known modal logics. It also contains a syntactical equivalent of one of these modal semantical systems.

A Modal Semantics of Negation in Logic Programming

1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani
Keyword(s):  
Modal Logic ◽  
Logic Programming ◽  
Modal Logics ◽  
Kripke Models ◽  
Logic Programs ◽  
Modal Semantics ◽  
Soundness And Completeness ◽  
Modal Completion ◽  
Well Foundedness

The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.

Sign in / Sign up

Export Citation Format

Share Document