2
$\begingroup$

Normally in a Hilbert system, writing a proof $\Delta \vdash \varphi_n$ with lines $\varphi_1, \varphi_2, ..., \varphi_n$ is done such that each $\varphi_k$ is either a proposition contained in $\Delta$, an axiom of the Hilbert system, or the result of modus ponens on two earlier lines.

In natural deduction, how does this work when we now have no axioms to work with, but rather only rules of inference? Each line could either be the result of a rule, or an element contained in $\Delta$... is that all? Does natural deduction ultimately require a non-empty $\Delta$ in order for us to even write proofs?

$\endgroup$
3
$\begingroup$

Natural deduction systems generally have a notion of assumption introduction and discharge. The easiest-to-understand rule that needs this is $\to$-introduction. This says that if we can assume $A$ and then prove $B,$ then we can infer $A\to B$ and discharge the assumption $A,$ leaving us with an unconditional proof of $A\to B$ (i.e. a proof from the empty set).

The exact nature of how the rules work and the proofs are laid out varies from system to system. For instance, see the hypothetical derivations section of the wikipedia page.

A couple more things

  1. In natural deduction, proofs aren't simply lists of statements like in Hilbert style. Often, they are trees. In one common type of system (which I have typically seen referred to as 'Fitch-style'), they are lists of statements, but have indentations to indicate when you have assumptions (i.e. when there's a 'change of context').
  2. Notice that the $\to$-introduction rule is functionally the exact same thing as the deduction theorem from a Hilbert style system. In natural deduction, it comes 'for free' as an inference rule, at the cost of a somewhat more complicated structure of formal proofs.
  3. Also, only the logical portion of a natural deduction system has no axioms. If we are working in a mathematical system, like PA or ZFC, those axioms are there, and look the same no matter what underlying implementation of first-order logic you are using. Of course, those axioms can just be thought of as assumptions to the left of the turnstile.
$\endgroup$
  • 1
    $\begingroup$ @user525966 No, we start with the empty set (assuming we're even using a system where the proofs are lists of statements, e.g. Fitch-style). Then we introduce assumptions. Then we discharge them. $\endgroup$ – spaceisdarkgreen Sep 25 '18 at 23:54
  • 1
    $\begingroup$ @user525966 Conditional proof. $\endgroup$ – spaceisdarkgreen Sep 26 '18 at 0:03
  • 1
    $\begingroup$ @user525966 The implementation details vary from system to system. But on a high level, yes. The idea is that we can add $A$ to our context, and then prove $B,$ and then discharge and move back to the original context and have $A\to B$ proven in that context. Of course the lines in between the assumption and discharge are 'off limits' afterward since they only held in the context where $A$ was assumed. These ideas need to be made precise in a given system. $\endgroup$ – spaceisdarkgreen Sep 26 '18 at 0:29
  • 1
    $\begingroup$ @user525966 In practice, there are many context changes within a given proof, but yes, at the end you will have returned to the original context and you can't stop when there are still assumptions outright. $\endgroup$ – spaceisdarkgreen Sep 26 '18 at 0:33
  • 1
    $\begingroup$ @user525966 Re 'Fitch-style', I'm not super sharp on the distinctions. In one sense it's a family of natural deduction systems where the proofs take the shape of a sequential list of formulas at different indentation levels. In another sense, tree-style and indented-list-style proofs are inter-convertable, so Fitch is just a choice of layout. $\endgroup$ – spaceisdarkgreen Sep 26 '18 at 0:36
3
$\begingroup$

Natural deduction certainly can prove theorems $\vdash \phi$ with no assumptions to the left of $\vdash$, because rules like $\Rightarrow$-introduction let you discharge (i.e., get rid of) assumptions. For examples, let's prove $\vdash A \Rightarrow A$:

  1. Assume $A$.
  2. Apply $\Rightarrow$-introduction discharging the assumption made in step 1 to conclude $A \Rightarrow A$.

In sequent notation, I have gone from the axiom $A \vdash A$ in step 1 to the theorem $\vdash A \Rightarrow A$ in step 2. So the sequent proof would look like:

  1. $A \vdash A$ (Axiom)
  2. $\vdash A \Rightarrow A$ (from 1 using $\Rightarrow$-introduction).
$\endgroup$
  • $\begingroup$ Isn't "assuming $A$" the same as pulling $A$ out of the assumption set $\Delta$ on the lefthand side? $\endgroup$ – user525966 Sep 25 '18 at 23:43
  • $\begingroup$ No. In sequent notation, "assuming $A$" means using the axiom $A \vdash A$. In the proof tree notation it just means forming a leaf node labelled with $A$. I've updated my answer to show what the sequent notation deduction looks like. $\endgroup$ – Rob Arthan Sep 25 '18 at 23:48
  • $\begingroup$ That seems to be using an assumption on the lefthand side though. And to my knowledge, ND doesn't use axioms $\endgroup$ – user525966 Sep 25 '18 at 23:50
  • $\begingroup$ Does my updated answer help? You seem to be mixing up the sequent notation for natural deduction which does need axioms like $A \vdash A$ and the tree notation which doesn't need (non-logical) axioms. (I say you seem to be mixing things up because you are talking about the lefthand side of something, a notion that only makes sense in the sequent notation, which does need axioms). $\endgroup$ – Rob Arthan Sep 25 '18 at 23:52
  • $\begingroup$ I don't understand the difference. What do you mean by treating $A \vdash A$ as an axiom vs. tree notation that doesn't need non-logical axioms? $\endgroup$ – user525966 Sep 25 '18 at 23:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.