Syntactical investigations into BI logic and BB^ I logic
Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic
We will be concerned with four implicational logics. Parentheses will be omitted following the convention that \(\to\) associates to the right. For example \(\alpha_ 1\to \alpha_ 2\to \alpha_ 3\to \alpha_ 4\) denotes \(\alpha_ 1\to (\alpha_ 2\to (\alpha_ 3\to \alpha_ 4))\). The first logic, which we call \(B\), has an axiom scheme \((B)\) \((\beta\to \gamma)\to (\alpha\to \beta)\to \alpha\to \gamma\), and modus ponens as a rule. The second logic, \(BI\), has in addition to the axiom scheme and rule of \(B\) the axiom scheme \((I)\;\alpha\to \alpha\). The third logic, \(BB'\), has in addition to the axiom scheme and rule of \(B\) the axiom scheme \((B')\;(\alpha\to \beta)\to (\beta\to \gamma)\to \alpha\to \gamma\). The fourth logic, \(BB'I\), has in addition to the axiom schemes and rule of \(BB'\) the axiom scheme \(I\). Let \(L\) be any one of logics \(B\), \(BI\), \(BB'\) or \(BB'I\). We write \(L\vdash \alpha\) \((L\not\vdash \alpha)\) to mean that \(\alpha\) is (resp. is not) provable in the logic \(L\). We say that a formula \(\alpha\) is trivial (non-trivial) if \(\alpha\) is (resp. is not) of the form \(\beta\to \beta\). By the syntactical method (Gentzen-type formulation and cut elimination), we have the following three main theorems. Theorem \(B\): For any formula \(\alpha\), \(B\vdash \alpha\) if and only if \(BI\vdash \alpha\) and \(\alpha\) is non-trivial. Theorem \(BB'\): For any formula \(\alpha\), \(BB'\vdash \alpha\) if and only if \(BB'I\vdash \alpha\) and \(\alpha\) is non-trivial. Theorem. The four logics \(B\), \(BI\), \(BB'\) and \(BB'I\) are decidable. \textit{A. R. Anderson} and \textit{N. D. Belnap jun.} asked [Entailment: The logic of relevance and necessity. Vol. I (1975; Zbl 0323.02030), \S 8.11] whether \(\alpha\) and \(\beta\) are the same formula if both formulas \(\alpha\to \beta\) and \(\beta\to \alpha\) are provable in \(BB'I\). This question is known as P-W problem to which \textit{E. P. Martin} and \textit{R. K. Meyer} [J. Symbolic Logic 47, 869-887 (1982; Zbl 0498.03011)] have provided a positive solution by a semantical method. Theorem \(BB'\) gives a syntactical proof of a positive solution for the P-W problem.
- scientific article; zbMATH DE number 47660
- Bi-intuitionistic logics: a new instance of an old problem
- Bisimulation and propositional intuitionistic logic
- Syntax and semantics of the logic \({\mathcal L}_{\omega\omega}^\lambda\)
- Bilattices and the semantics of logic programming
- A proof-theoretic study of bi-intuitionistic propositional sequent calculus
- Bialgebraic semantics for logic programming
- Relating sequent calculi for bi-intuitionistic propositional logic
- Programming Languages and Systems
- Bilattice logics and demi-negation
- scientific article; zbMATH DE number 3504935 (Why is no real title available?)
- scientific article; zbMATH DE number 596497 (Why is no real title available?)
- scientific article; zbMATH DE number 3333259 (Why is no real title available?)
- Logics without the contraction rule
- Predicate logics without the structure rules
- Proof theory
- Solution to the P − W problem
- Untersuchungen über das logische Schliessen. I
- A lambda proof of the P-W theorem
- ASSERTIONALLY EQUIVALENT QUASIVARIETIES
- scientific article; zbMATH DE number 2024615 (Why is no real title available?)
- scientific article; zbMATH DE number 1471988 (Why is no real title available?)
- scientific article; zbMATH DE number 1482997 (Why is no real title available?)
- ON EQUATIONAL COMPLETENESS THEOREMS
- The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
- Progressive logic
- New(ish) foundations for theories of entailment
- The fundamental S-theorem - A corollary
- Self-implications in BCI
This page was built for publication: Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1337604)
