Calculus of Natural Deduction That Works for Empty Structures

Question

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents.

Definition. If $\Gamma$ is a set of formulas and $\phi$ a formula, then $\Gamma\vdash\phi$ is called a sequent.

The rules of this calculus of natural deduction are:

• Hypothesis. $$ \begin{array}{c} \hline \Gamma\vdash\phi \end{array}\text{, where $\phi\in\Gamma$} $$
• Rules for $\land$. $$ \text{Introduction: } \begin{array}{c} \Gamma\vdash A\quad\Gamma\vdash B\\ \hline \Gamma\vdash A\land B \end{array}\qquad\qquad\text{Elimination: } \begin{array}{c} \Gamma\vdash A\land B\\ \hline \Gamma\vdash A\quad\Gamma\vdash B \end{array} $$
• Rules for $\lor$. $$ \text{Introduction: } \begin{array}{c} \Gamma\vdash A\\ \hline \Gamma\vdash A\lor B \end{array} \quad \begin{array}{c} \Gamma\vdash B\\ \hline \Gamma\vdash A\lor B \end{array} \qquad\text{Elimination: } \begin{array}{c} \Gamma\vdash A\lor B\quad\Gamma\cup \{A\}\vdash C\quad\Gamma\cup \{B\}\vdash C\\ \hline \Gamma\vdash C \end{array} $$
• Rules for $\rightarrow$.

$$ \text{Introduction: } \begin{array}{c} \Gamma\cup \{A\}\vdash B\\ \hline \Gamma\vdash A\rightarrow B \end{array}\qquad\qquad\text{Elimination: } \begin{array}{c} \Gamma\vdash A\rightarrow B\quad\Gamma\vdash A\\ \hline \Gamma\vdash B \end{array} $$

• Rules for $\neg$.

$$ \text{Introduction: } \begin{array}{c} \Gamma \cup\{A\}\vdash\bot\\ \hline \Gamma\vdash \neg A \end{array}\qquad\qquad\text{$\neg\neg$ Elimination: } \begin{array}{c} \Gamma\vdash \neg\neg A\\ \hline \Gamma\vdash A \end{array} $$

• Rule for $\bot$. $$ \text{Introduction: } \begin{array}{c} \Gamma\vdash A\quad\Gamma\vdash \neg A\\ \hline \Gamma\vdash\bot \end{array} $$

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

• Rules for $\exists$. $$ \text{Introduction: } \begin{array}{c} \Gamma\vdash\phi[t/x]\\ \hline \Gamma\vdash\exists x(\phi) \end{array}\qquad\text{Elimination: } \begin{array}{c} \Gamma\vdash\exists x(A)\quad \Gamma\cup \{A[u/x]\}\vdash B\\ \hline \Gamma\vdash B \end{array} \text{, $u$ not free in $\Gamma$ or $B$.} $$

• Rules for $=$. $$ \text{Introduction: } \begin{array}{c} \hline \Gamma\vdash t = t \end{array} \qquad\text{Elimination: } \begin{array}{c} \Gamma\vdash t_1=t_2\quad\Gamma\vdash A\\ \hline \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$)

My problem with this calculus. The problem with the calculus given above is that it only works for non-empty structures. Thus there are sentences like $\exists x(x=x)$ which are derivable in this calculus but do not hold in empty structures. But I am searching for a calculus that works for empty structures too. When I say "works for empty structures too", I mean: If the demanded calculus proves a sentence, then this sentence should hold in all structures, also in the empty structures.

I am searching for a calculus that works for all structures, and not only for non-empty structures.

That is why my question is:

How can one modify the calculus given above such that this new calculus works for all structures, and not only for non-empty structures?

Related threads:

• natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

• Complete calculus of first-order logic working for empty structures too

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

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

Answer 3

[Edit: This post was due to a misreading of ooooooo's system, which required that all free variables on the right of the sequent are in the set of variables on the left (like mine, so it's embarrassing that I missed it). That prevents my second step from going through. However, my intuition does not tell me whether his system is sound or not, but he will attempt to prove it. This is left just for record.]

The following proof of contradiction in ooooooo's proposed system shows that it has a fundamental problem, which is that it is unable to capture correctly the ordering of the context chain, which is a sequence in my proposed system. (This is aside from the easily fixed problem that if there are constants then it is unable to derive the true sentence "$\exists x\ ( \neg \bot )$".)

  $[]\ Γ \vdash \forall y\ \exists x\ ( P(x,y) )$

  $[]\ Γ \vdash \exists x\ ( P(x,y) )$   [∀elim]

  $[u,v]\ Γ,P(u,y) \vdash P(u,y)$   [hyp]

  $[u]\ Γ,P(u,y) \vdash \forall v\ ( P(u,v) )$   [∀intro]   (*)

  $[u]\ Γ,P(u,y) \vdash \exists x\ \forall v\ ( P(x,v) )$   [∃intro]

  $[]\ Γ \vdash \exists x\ \forall v\ ( P(x,v) )$   [∃elim]

Basically, it seems that the intended interpretation of the extra set of variables is that they are universally quantified, so (*) is the point at which an unsound quantifier switch takes place, with "$\forall v$" jumping over "$P(u,y) \rightarrow$".

However, now that I think more about it, the idea of capturing existential elimination via universal subcontexts (which was implicitly present in the original system in the question) should provide a way to remove the global nature of the ∃elim rule in my system, which I'm going to add to my answer in a minute.

Answer 4

In an empty universe, every $\forall$ becomes true and every $\exists$ become false. So you can just split any theorem into two cases, one case assumes the universe is empty and one case does not. In the case where the universe is empty, everything is reducible to propositional logic. In the case where the universe is not empty, you are back to your original logic. Introduce a universe constant $U$ to represent whether the universe is inhabited.

So you axioms become:

$$\frac{ U , \forall x ~ \phi }{\phi[u / x]} \quad \forall\text{Elim}$$

$$\frac{ U , \phi[u / x] }{ \exists x ~ \phi} \quad \exists\text{Intro}$$

$$\frac{\lnot \forall x ~ \phi}{U} \quad \forall\text{Inhabited}$$ $$\frac{\exists x ~ \phi}{U} \quad \exists\text{Inhabited}$$ $$\frac{\forall x ~ \bot}{\lnot U} \quad \forall\text{Uninhabited}_1$$ $$\frac{\lnot \exists x ~ \top}{\lnot U} \quad \exists\text{Uninhabited}_1$$

$$\frac{\lnot U}{\forall x ~ \phi} \quad \forall\text{Uninhabited}_2$$ $$\frac{\lnot U}{\lnot \exists x ~ \phi} \quad \exists\text{Uninhabited}_2$$

There may be some reduncancy in those inferences due to whether you can infer $\forall x ~ \lnot P = \lnot \exists x ~ P$. The structure of the proof of theorem T is:

$$\begin{array} {ll} U \lor \lnot U & \text{Provable with Propositional logic} \\ U \vdash T & \text{Regular proof of T} \\ \lnot U \vdash T & \text{By applying the Uninhabited}_2\text{ inferences and propositional logic} \\ T & \lor\text{ Elim} \end{array}$$

Note that the $\lnot U \vdash T$ can be solved algorithmically, as propostional logic is trivially solvable.

Presumably you want a logic that does not introduce a universal inhabitation constant $U$, and doesn't procede along 2 cases. The "variable chains" in the other answers are effectively just this $U$ constant, where $U$ iff the variable chain isn't empty, as far as I can tell anyway. One approach to restructuring the logic is to see where the inhabited universe assumption comes in from the underlying $\lambda$-calculus. One can define universal quantification as

$$\forall M = (M = \lambda x . \top)$$ or equivalently $$\forall (\lambda x . \phi) = ((\lambda x . \phi) = (\lambda x . \top))$$

(Ignoring type considerations for brevity, and not factoring out the M as you would for an axiom, and using infix for readability). This definition does not assume an inhabited universe. Also $\forall\text{Elim}$ and $\forall\text{Intro}$ can be translated

$$(\forall (\lambda x . \phi) = \top) \iff ((\lambda x . \phi)~u = \top)$$

The $\implies$ side of the above violates the empty universe claim by assuming such a $u$ exists at all. The problem seems to come from the following inference

$$(\lambda x . A) = (\lambda x. B) \vdash A = B$$

which need not be true in an empty universe. Ex, $f(x) = x$ and $g(x) = x + 1$, assuming $x \ne x + 1$, it can still be the case that $f = g$ if their domain is empty. So the challenge seems to be translating $\forall (\lambda x . \phi) \implies ((\lambda x . \phi) = (\lambda x . \top))$ into first order logic without assuming $(\lambda x . A) = (\lambda x. B) \vdash A = B$.

This leads me to suspect (I have no completeness proof for this) that $\forall\text{Elim}$ can be replaced by 2 axioms:

$$\forall x ~ \forall y P \vdash \forall x P[t / y] \quad \forall\text{Elim}_\forall$$ $$\exists x ~ \forall y P \vdash \exists x P[t / y] \quad \forall\text{Elim}_\exists$$

Both statements are sound (the second has been asked a few times on math.stackexchange, interestingly) under the original logic as well as in an empty universe, and they effectively say that the universal quantifier cannot be eliminated unless there really is a context in which the variable may be instantiated.

I have only focued on $\forall$ instead of $\exists$ because $\exists$ can be defined as $\lnot \forall \lnot$ in some logics.