5

In natural deduction, is it correct that an inference rule operates on sequents which have only one formula on their right hand sides?

Why does an inference rule seem to operate on formulas in Hurley's An Concise Introduction to Logic? For example:

modus ponens (MP)

$$\dfrac{\quad p ⊃ q \quad \\ \quad p \quad}{q} $$

Is it correct that an inference rule under natural deduction operates on sequents, but can be shortened by omitting the antecedents of the sequents and therefore seem to operate on formulas (succedent)? (note: a sequent consists of an antecedent of formulas and a succedent (only one formula for natural deduction).)

Thanks.

Taroccoesbrocco
  • 16,143
  • 9
  • 27
  • 63
Tim
  • 45,716
  • 51
  • 220
  • 492
  • 1
    Many different proof system: Hlibert-style, Tableaux, ND, Sequent calculus. All equivalent with respect to a "chosen" semantics, e.g. that of classical logic. Each system, in turn, may have more than one version, differing basically for the presentation-style (Ebbinghaus' one may be defined a system of Natural Deduction in sequent-style). – Mauro ALLEGRANZA Jul 30 '20 at 16:17

1 Answers1

4

Natural deduction can be equivalently expressed in both formulations, either operating on formulas or operating on sequents.

If we restrict to the (intuitionistic) fragment with only implication, the rules for natural deduction operating on sequents are: $$ \dfrac{}{\Gamma, A \vdash A}\text{ax} \qquad \dfrac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}\to_\text{intro} \qquad \dfrac{\Gamma \vdash A \to B \qquad \Gamma \vdash A}{\Gamma \vdash B}\to_\text{elim} $$

Note that the inference rules of natural deduction for sequents change only the formula on the right part of a sequent, except for discharging some hypotheses on the left of a sequent (see $\to_\text{intro}$). For this reason, it is natural to formulate natural deduction as a deductive system operating only on formulas.

The rules for natural deduction operating on formulas are ($[A]$ means that the hypotheses $A$ is discharged):

$$ A \qquad \dfrac{[A]^* \\ \ \vdots \\ B}{A \to B}\to_\text{intro}^* \qquad \dfrac{A \to B \qquad A}{B}\to_\text{elim} $$

and we write $\Gamma \vdash_\text{ND} A$ if there is a derivation in natural deduction for formulas whose conclusion (the bottom of the derivation) is $A$ and whose hypotheses (the formulas on the top of the derivation that are not discharged) are among the formulas in $\Gamma$.

Now it is clear that $\Gamma \vdash_\text{ND} A$ in natural deduction for formulas (i.e. there is a derivation of $A$ where the hypotheses are among the formulas in $\Gamma$) if and only if the sequent $\Gamma \vdash A$ is derivable in natural deduction for sequents.

This approach extends easily to other connectives and quantifications.


As usual, each formulation has its pros and cons. For instance, natural deduction on formulas is handy to express the composition of derivations (the operation that replaces an hypothesis with a derivation of that hypothesis, if any). Natural deduction on sequents manages inference rules that discharge hypotheses (such as $\to_\text{intro}$) in a more natural way.


For the sake of completeness, the inference rules used by Hurley's book for its version of natural deduction for formulas are not exactly the same as the rules I wrote here. His modus ponens is $\to_\text{elim}$ here, but there is not analogue of $\to_\text{intro}$. This is not a problem, because his formulation of natural deduction for formulas is equivalent to the formulation of natural deduction for formulas presented here. Indeed, the rule $\to_\text{intro}$ can be simulated in his system (deduction theorem) and vice-versa, Hurley's inference rules can be simulated in the formulation of natural deduction for formulas presented here.

Taroccoesbrocco
  • 16,143
  • 9
  • 27
  • 63
  • Thanks. (1) Do you call the first rule " / Γ,⊢" on sequents "ax" i.e. an axiom? Natural deduction has no axiom, and an inference rule is not an axiom. (2) In which books can I find →intro and →elim? I have not seen "elimination" and "introduction" concepts. – Tim Jul 30 '20 at 14:48
  • 1
    @Tim - Yes, "ax" stands for axiom, where axiom means inference rule with no premises. It is the starting point for any derivation (without inference rules with no premises, it would be impossible to build any derivation). This is the only kind of axiom required in natural deduction. It means that you can derive $A$ from $A$, i.e. if $A$ holds then $A$ holds. – Taroccoesbrocco Jul 30 '20 at 22:50
  • 1
    @Tim - The main reference for natural deduction as I presented in my answer (for specialists) is D. Prawitz, "Natural Deduction: A Proof-theoretical Study", 1965 (reprinted by [Dover](https://www.amazon.it/Natural-Deduction-Proof-theoretical-Dag-Prawitz/dp/0486446557), 2006). A more accessible introduction to natural deduction on formulas as I presented is in [Van Dalen's textbook](http://www.cin.ufpe.br/~mlogica/livros/Logic%20and%20Structure%20-%20Van%20Dalen.pdf) "Logic and Structure". – Taroccoesbrocco Jul 30 '20 at 22:59
  • Thanks. I am still wondering about: Does an inference rule operate on formulas or on instances of $\vdash$ (e.g. $\Phi \vdash \phi$)? Does that depend on the form in which an inference rule is written, in a Hilbert system or a sequent-style natural system?. See some recent comment and post https://math.stackexchange.com/questions/3819852/what-distinguishes-different-styles-of-proof-systems-hilbert-natural-deduction?noredirect=1&lq=1#comment7877506_3819852 and https://math.stackexchange.com/questions/3819814/do-inference-rules-mean-the-same-in-a-hilbert-system-and-in-a-natural-deductive. – Tim Sep 09 '20 at 16:42
  • @Tim - It depends on the proof system. And even in the same proof system, there could be different presentations, some ones acting on formulas, other ones acting on sequents. For instance, Hilbert calculus is usually presented as acting on formulas. The sequent calculus has only presentations acting on sequents. Natural deduction has many equivalent presentations, as I said in my answer: some of them act on formulas, other ones act on sequent. – Taroccoesbrocco Sep 09 '20 at 17:06