Does natural deduction require a non-empty set of premises?

Question

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?

Answer 1

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.

Answer 2

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).