Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic (Q1337604): Difference between revisions

From MaRDI portal
Import240304020342 (talk | contribs)
Set profile property.
ReferenceBot (talk | contribs)
Changed an Item
 
Property / cites work
 
Property / cites work: Q4085699 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4297115 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Untersuchungen über das logische Schliessen. I / rank
 
Normal rank
Property / cites work
 
Property / cites work: Predicate logics without the structure rules / rank
 
Normal rank
Property / cites work
 
Property / cites work: Solution to the <i>P</i> − <i>W</i> problem / rank
 
Normal rank
Property / cites work
 
Property / cites work: Logics without the contraction rule / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5610986 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof theory / rank
 
Normal rank

Latest revision as of 09:19, 23 May 2024

scientific article
Language Label Description Also known as
English
Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic
scientific article

    Statements

    Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic (English)
    0 references
    10 November 1994
    0 references
    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.
    0 references
    relevant logic
    0 references
    substructural logic
    0 references
    implicational logics
    0 references
    cut elimination
    0 references
    syntactical proof of a positive solution for the P-W problem
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references