Calculus of Natural Deduction That Works for Empty Structures

Solution 1:

The easiest (and in my opinion cleanest) way to do this is to augment the context. In the sequent calculus you presented, you have the left-hand of the sequent being a set $Γ$ of formulae. Instead of that, you need to have set of sentences $S$ for axioms and a context chain $Q$. $Q$ is an ordered list, each item being either a conditional context or a universally or existentially quantified variable. The idea is that all free variables in the right-hand of the sequent must be quantified in $Q$. So we should be able to derive "$S;\forall x \vdash x=x$" but not just "$S \vdash x=x$". I give the rules precisely below.

Connective rules

The rules for the boolean connectives are essentially the same as before, but instead of modifying the left-hand set $Γ$ of formulae, we modify the context chain. So here are the changed rules: $\def\imp{\rightarrow}$

[$S$ is any sentence set, and $Q$ is any context chain, and $A,B,C$ are any formulae.]

∨elim   $\dfrac{S;Q \vdash A \lor B \quad S;Q \vdash A \imp C \quad S;Q \vdash B \imp C}{S;Q \vdash C}$

→sub   $\dfrac{}{S;Q,A \vdash A}$   [All free variables in $A$ must be quantified in $Q$.]

→restate   $\dfrac{S;Q \vdash B}{S;Q,A \vdash B}$   [All free variables in $A$ must be quantified in $Q$.]

→intro   $\dfrac{S;Q,A \vdash B}{S;Q \vdash A \imp B}$

→elim   $\dfrac{S;Q \vdash A \quad S;Q \vdash A \imp B}{S;Q \vdash B}$

⊥elim   $\dfrac{S;Q,A \vdash \bot}{S;Q \vdash \neg A}$

Quantifier rules

The quantifier rules are built the same way, to capture the logical structure in the same way as a Fitch-style calculus. Note that this system will forbid the derivation of any sentence with variable shadowing (nested quantifiers that quantify over the same variable). I chose this approach as it is 'more natural' and to avoid the issue of substitutability (or collision freeness) that many textbooks describing Hilbert-style systems have to deal with.

[$x,y$ are any variables, and $t$ is any term whose free variables are all quantified in $Q$.]

∀restate   $\dfrac{S;Q \vdash A}{S;Q,\forall x \vdash A}$   [$x$ must not be quantified in $Q$ or used (free or bound) in $A$.]

∀intro   $\dfrac{S;Q,\forall x \vdash A}{S;Q \vdash \forall x\ ( A )}$

∀elim   $\dfrac{S;Q \vdash \forall x\ ( A )}{S;Q \vdash A[t/x]}$   [Note that $t$ must exist (see above for what $t$ must be).]

∃intro   $\dfrac{S;Q \vdash A[t/x]}{S;Q \vdash \exists x\ ( A )}$   [$x$ must not be quantified in $Q$, and note that $t$ must exist.]

∃elim   $\dfrac{S;Q \vdash \exists x\ ( A ) \quad S;Q,\forall y,A[y/x] \vdash B}{S;Q \vdash B}$   [$y$ must not be used in $B$]

Axiom and equality rules

Finally we slightly modify the rules for axioms and equality so that they do not mess with the context chain.

axiom   $\dfrac{}{S \cup \{A\};{} \vdash A}$

=intro   $\dfrac{}{S;Q \vdash t=t}$   [All free variables in $t$ must be quantified in $Q$.]

Footnote

In this section I give the original existential rules that I had in place of the ∃elim rule above. They are not preferable because the involve a global restriction and so the rules do not define a relation on sequents but rather a relation on entire sequent-style proofs, which is undesirable since the point of a sequent calculus was to capture all necessary information about provability of a sentence in a single sequent.

∃elim   $\dfrac{S;Q \vdash \exists x\ ( A )}{S;Q,\exists y \vdash A[y/x]}$   [$y$ must not occur in $Q$ in all previous steps! (*)]

∃unbind   $\dfrac{S;Q,\exists x \vdash A}{S;Q \vdash A}$   [$x$ must not be used in $A$.]

∃restate   $\dfrac{S;Q \vdash A \quad S;Q,\exists x \vdash B}{S;Q,\exists x \vdash A}$   [$x$ must not be used in $A$.]

(*) This considers a proof as a sequence of rule applications, and only when no previous rule application has $x$ occurring as a quantified variable can we use the ∃elim rule to obtain $\exists x$ as part of the context chain. I thought the 'global' nature of this rule was unavoidable without something equivalent to tagging along the entire sequence of previous steps in the proof on the left of the "$\vdash$", but as shown above it can be avoided.

Solution 2:

Does the following proposal work? Please tell me what you think about the following modification of the calculus given in the question. If you find some mistakes, please tell me.

The solution is a sound dealing with free variables.

Definition. A sequent is an expression of the form $[V]\ \Gamma\vdash\phi$ where

• $V$ is a finite set of variables,
• $\Gamma$ is a set of formulas each of whose free variables are elements of $V$,
• $\phi$ is a formula whose free variables are elements of $V$.

Now we can formulate the rules for $\forall, \exists$ and $=$ as follows:

• Rules for $\forall$. $$ \text{Introduction: } \begin{array}{c} [V\cup\{u\}]\ \Gamma\vdash\phi[u/x]\\ \hline [V]\ \Gamma\vdash\forall x(\phi) \end{array}\text{ ($u\not\in V$)}\qquad\text{Elimination: } \begin{array}{c} [V]\ \Gamma\vdash\forall x(\phi)\\ \hline [V]\ \Gamma\vdash\phi[t/x] \end{array} $$

• Rules for $\exists$. $$ \text{Introduction: } \begin{array}{c} [V]\ \Gamma\vdash\phi[t/x]\\ \hline [V]\ \Gamma\vdash\exists x(\phi) \end{array}\text{ (where every free variable occuring in $t$ is an element of $V$)}\qquad\text{Elimination: } \begin{array}{c} [V]\ \Gamma\vdash\exists x(A)\quad [V\cup\{u\}]\ \Gamma\cup \{A[u/x]\}\vdash B\\ \hline [V]\ \Gamma\vdash B \end{array} \text{ ($u\not\in V$, $u$ not free in $B$)} $$

• Rules for $=$. $$ \text{Introduction: } \begin{array}{c} \hline [V]\ \Gamma\vdash t = t \end{array} \qquad\text{Elimination: } \begin{array}{c} [V]\ \Gamma\vdash t_1=t_2\quad[V]\ \Gamma\vdash A\\ \hline [V]\ \Gamma\vdash A[t_1//t_2] \end{array} $$

(where $A[t_1//t_2]$ is a formula which resulted form $A$ by replacing all or some free occurrences of $t_1$ in $A$ by $t_2$)

The propositional fragment can be formalized as above, one just has to write $[V]$ in front of each sequent.

Solution 3:

Let me present such a system which is based on the notion of de Bruijn indices, which eliminates the need for all those confusing and fragile free variable restrictions because variable shadowing becomes impossible. The basic idea here is that instead of symbolic names, we use variables of the form $[i]$ where $i$ is a natural number (possibly 0), which refers to the bound variable at $i$ levels up. Thus, for example, if we take the extensionality axiom of ZFC

$$ \forall x ~ \forall y ~ [(\forall a ~ (a \in x \leftrightarrow a \in y)) \rightarrow x = y]$$

this would be encoded as

$$\forall{\cdot} \, \forall{\cdot} \, [(\forall{\cdot} \, ([0] \in [2] \leftrightarrow [0] \in [1])) \rightarrow [1] = [0] \,].$$

The basic objects of this presentation will be:

• For each $n \in \mathbb{N}$, $term_n$ represents the terms in up to $n$ free variables.
• For each $n \in \mathbb{N}$, $prop_n$ represents the propositions in up to $n$ free variables.
• For each $n \in \mathbb{N}$, $context_n$ represents the contexts of propositions in up to $n$ free variables; this can either be the power set of $prop_n$, or the set of finite subsets of $prop_n$, or the set of finite ordered lists of $prop_n$, as appropriate.
• In $\Gamma \vdash \phi$, we require $\Gamma \in context_n$ and $\phi \in prop_n$ for the same $n$.

Thus, for example, whenever we have $0 \le i < n$, then $[i] \in term_n$. (In particular, for a language with no nullary function symbols, we would have $term_0$ is empty.) As for $prop_n$, most operations keep the same $n$, with the exceptions being that if $\phi \in term_{n+1}$, then $\forall{\cdot} \, \phi$ and $\exists{\cdot} \, \phi$ are in $term_n$.

Now, for most of the rules of a natural deduction system, $n$ will remain invariant. The exceptions are for $\forall$ and $\exists$; for these rules, it will be convenient to define for $\phi \in prop_n$, $\phi {\uparrow} \in prop_{n+1}$ is defined by $\phi {\uparrow} := \phi[ [0] / [1], [1] / [2], \ldots, [n-1] / [n] ]$. Similarly, for $\Gamma \in context_n$, we define $\Gamma {\uparrow} \in context_{n+1}$ by $\Gamma {\uparrow} := \{ \phi {\uparrow} \mid \phi \in \Gamma \}$.

• ${\forall} I$: For $\Gamma \in context_n$, $\phi \in prop_{n+1}$, if $\Gamma {\uparrow} \vdash \phi$, then $\Gamma \vdash \forall{\cdot} \, \phi$.
• ${\forall} E$: For $\Gamma \in context_n$, $\phi \in prop_{n+1}$, $\tau \in term_n$, if $\Gamma \vdash \forall{\cdot} \, \phi$, then $\Gamma \vdash \phi[[0] / \tau, [1] / [0], [2] / [1], \ldots, [n] / [n-1]]$.
• ${\exists} I$: For $\Gamma \in context_n$, $\phi \in prop_{n+1}$, $\tau \in term_n$, if $\Gamma \vdash \phi[[0] / \tau, [1] / [0], [2] / [1], \ldots, [n] / [n-1]]$, then $\Gamma \vdash \exists{\cdot} \, \phi$.
• ${\exists} E$: For $\Gamma \in context_n$, $\phi \in prop_{n+1}$, $\psi \in prop_n$, if $\Gamma \vdash \exists{\cdot} \, \phi$ and $\Gamma{\uparrow}, \phi \vdash \psi$, then $\Gamma \vdash \psi$.

Now, for example, if we tried to prove $\vdash_{n=0} \exists{\cdot} \, \top$ in a language with no nullary function symbols (which therefore admits an empty model), we would be unable to apply ${\exists} I$ because there is no possible $\tau \in term_0$.