A weak intuitionistic propositional logic with purely constructive implication (Q1102265)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A weak intuitionistic propositional logic with purely constructive implication |
scientific article; zbMATH DE number 4049612
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A weak intuitionistic propositional logic with purely constructive implication |
scientific article; zbMATH DE number 4049612 |
Statements
A weak intuitionistic propositional logic with purely constructive implication (English)
0 references
1987
0 references
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.
0 references
sequent calculus
0 references
intuitionistic logic
0 references
cut-elimination
0 references
constructive semantics
0 references
modal operators
0 references
Kripke models
0 references
completeness
0 references
