Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that (...) restricts its use to cases in which the premiss does not depend on assumptions. This restriction is entirely analogous to the restriction of the rule of universal generalization of first-order logic. A necessitation rule with this restriction permits a proof of the deduction theorem in its usual formulation. Other suggestions presented in the literature to deal with the problem are reviewed, and the present solution is argued to be preferable to the other alternatives. A contraction-and cut-free sequent calculus equivalent to the Hubert system for basic modal logic shows the standard failure argument untenable by proving the underivability of DA from A. (shrink)

Résumé1Le rôle prlvilégié que joue l'implication « si … alors » dans la pensée donne à sa formalisation loglque une importance capitale. Mais la formalisation classique se heurte à certaines difficultés.2On montre, par la méthode L de Gentzen, que c'est la partie positive de la logique intuitionniste qui exprime au plus près l'idée intuitive de l'implication.3L'implication est liée à la négation. On est conduit à distinguer « réfutable », «absurde» et «faux».4L'analyse de ces notions peut se faire aussi par la (...) méthode N de Gentzen. Elle conduit à une certaine symétrie dans les résultats.5Un système S, dû à F. B. Fitch, conduit à une nouvelle sorte de négation.6La négation dans S peut s'interpréter comme «contraire aux faits».Zusammenfassung1Dei der besonderen Rolle der Implikation «wenn … dann »im Denken 1st deren logische Formalisierung von wesentlicher Bedeutung. Die klassische Formalisierung stösst auf gewisse Schwierigkeiten.2Gentzens Méthode L erweist, dass der positive Teil der intuitionistischen Logik der intuitiven Idee der Implikation am nächsten kommt.3Die Implikation ist an die Negation gebunden. Folgende Unterscheidungen ergeben sich: widerlegbar, unmöglich, falsch.4Die Analyse dieser Begriffe kann auch nach Gentzens Méthode N geschehen. Sie führt zu einer gewissen Symmetrie in den Ergebnissen.5Das logische System S, das F. B. Fitch aufgestellt hat, führt zu einer neuen Art der Negation.6Die Negation kann in S als «im Widerspruch zu den Tatsachen» interpretiert werden. (shrink)

We present a proof of the equivalence between two deductive systems for constructive necessity, namely an axiomatic characterisation inspired by Hakli and Negri's system of derivations from assumptions for modal logic , a Hilbert-style formalism designed to ensure the validity of the deduction theorem, and the judgmental reconstruction given by Pfenning and Davies by means of a natural deduction approach that makes a distinction between valid and true formulae, constructively. Both systems and the proof of their equivalence are formally verified (...) using the state-of-the-art proof assistant Coq. The proof approach taken throughout the paper unveils the use of some alternative proof methods that allow for a smooth transition from the high-level mathematical proofs to their mechanised counterparts. (shrink)

There is an obvious difference between what a term designates and what it means. At least it is obvious that there is a difference. In some way, meaning determines designation, but is not synonymous with it. After all, “the morning star” and “the evening star” both designate the planet Venus, but don't have the same meaning. Intensional logic attempts to study both designation and meaning and investigate the relationships between them.

This paper is concerned with counterfactual logic and its implications for the modal status of mathematical claims. It is most directly a response to an ambitious program by Yli-Vakkuri and Hawthorne (2018), who seek to establish that mathematics is committed to its own necessity. I claim that their argument fails to establish this result for two reasons. First, their assumptions force our hand on a controversial debate within counterfactual logic. In particular, they license counterfactual strengthening— the inference from ‘If A (...) were true then C would be true’ to ‘If A and B were true then C would be true’—which many reject. Second, the system they develop is provably equivalent to appending Deduction Theorem to a T modal logic. It is unsurprising that the combination of Deduction Theorem with T results in necessitation; indeed, it is precisely for this reason that many logicians reject Deduction Theorem in modal contexts. If Deduction Theorem is unacceptable for modal logic, it cannot be assumed to derive the necessity of mathematics. (shrink)