A weak intuitionistic propositional logic with purely constructive implication

DOI10.1007/BF00370647MaRDI QIDQ1102265zbMATH OpenOpenAlexFDO

Authors Mitsuhiro Okada

Publication date 1987

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00370647

zbMATH Keywords

completenessconstructive semanticscut-eliminationintuitionistic logicKripke modelsmodal operatorssequent calculus

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Review text

By weakening the intuitionistic implication, two subsystems WLJ and SI of the sequent calculus LJ for intuitionistic logic are defined. The cut- elimination theorems for WLJ and SI are given and the corresponding constructive semantics is described. An interpretation of the system SI by means of modal operators and classical implication is considered, where a weak modal system WM is obtained. In the end of the paper, the Kripke models for WM are presented and the completeness theorem is proved.

Recommendations

• Weak Logics with Strict Implication
• On a theory of weak implications
• Subintuitionistic logics
• Weak subintuitionistic logics
• scientific article; zbMATH DE number 1953898

Cites work

• scientific article; zbMATH DE number 3557754 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• The consistency of arithmetics
• The foundations of mathematics. A study in the philosophy of science
• Untersuchungen über das logische Schliessen. I

Cited in

(5)

• Implication via spacetime
• scientific article; zbMATH DE number 5316399 (Why is no real title available?)
• Weak Logics with Strict Implication
• scientific article; zbMATH DE number 1354095 (Why is no real title available?)
• On a generalization of Heyting algebras. I

This page was built for publication: A weak intuitionistic propositional logic with purely constructive implication

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1102265)