2
$\begingroup$

Suppose $\Gamma\vdash A\vee \Delta$, where as usual $\Gamma$ and $\Delta$ are thought of as sets of propositions and the turnstyle is for logical consequence, or entailment.

Given the assumption, may one consider the relation between what is above the line and what is below the line of the sequent $\frac{\Gamma\vdash A, \Delta}{\Gamma\vdash A\vee B, \Delta}$ to be an entailment on a par with - as in, having the same nature as - the relation between the left and the right side of the turnstyle in $\Gamma\vdash A\vee \Delta$, or is there something which prohibits such a point of view?

Improve this question
$\endgroup$
19
  • 2
    $\begingroup$ I know at least one case when it can be devastating:$$\frac A{\Box A}$$ $\endgroup$
    – მამუკა ჯიბლაძე
    Commented May 9, 2021 at 21:59
  • $\begingroup$ The horizontal lines I relate to are those of Gentzen's sequents. $\endgroup$
    – Frode Alfson Bjørdal
    Commented May 9, 2021 at 22:19
  • 1
    $\begingroup$ How is this different from the axiom vs rule issue? A lot of rules are sound but axioms are much more powerful. $\endgroup$
    – François G. Dorais
    Commented May 10, 2021 at 1:26
  • 3
    $\begingroup$ The issue with the necessitation rule is that we don't actually want it as a rule when undertaking conditional modal reasoning, since perhaps we are in a situation where A is true, but not necessary. We use the necessitation rule, rather, as a convenient tool to define modal theories, such as S4, S4.2, S4.3, etc. It is a convenient proof-theoretic way of defining the particular modal theories, not a sound rule of modal reasoning. $\endgroup$
    – Joel David Hamkins
    Commented May 10, 2021 at 7:45
  • 1
    $\begingroup$ @JoelDavidHamkins In fact in my head I always translate it to the language of algebras-with-operators. Under this translation, the necessitation rule corresponds to requiring $\Box(\top)=\top$, which one frequently wants to hold in the algebra. $\endgroup$
    – მამუკა ჯიბლაძე
    Commented May 10, 2021 at 11:26

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .