8
$\begingroup$

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:

$\endgroup$
  • 1
    $\begingroup$ Just to be clear: you're asking specifically for a proof formalism that (a) looks like natural deduction at least for its propositional fragment, and (b) is sound and complete for possibly-empty structures, and (c) does not obviously treat the empty structure as a special case (e.g. such as declaring that a proof consists of a standard proof plus the fact that the sentence evaluates true in the empty structure). Right? $\endgroup$ – Henning Makholm Jun 10 '16 at 19:54
  • 2
    $\begingroup$ @HenningMakholm: Yes, that is right. And this proof formalism should also look like natural deduction for its quantifier fragment. $\endgroup$ – ooooooo Jun 10 '16 at 19:56
  • 1
    $\begingroup$ x @ooo: That would actually be unsound -- with that rule, you could derive $x\ne 0\vdash \exists x(x\ne x)$ from $x\ne 0\vdash x\ne 0$, but $\exists x(x\ne x)$ is definitely false. $\endgroup$ – Henning Makholm Jun 10 '16 at 21:11
  • 1
    $\begingroup$ @StephenA.Meigs: No, a three-valued logic is not what I am searching for. $\endgroup$ – ooooooo Jun 11 '16 at 9:53
  • 1
    $\begingroup$ I am anxious to read your answer. But the demanded calculus has to be precisely defined. In my opinion the calculus you gave here math.stackexchange.com/questions/1681857/… is very intuitive but not precisely defined. $\endgroup$ – ooooooo Jun 11 '16 at 13:05
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I'm a bit confused about the "$x$ most not be used in any previous step" side condition for your $\exists$elim rule. Isn't that just the kind of "action at a distance" conditions that keeping track of a context to the left of the turnstile is supposed to _eliminate_? And if $x$ must not even have been mentioned previously, then how could we possibly have concluded $S;Q\vdash \exists x (A)$? Even stating that judgement seems to violate the condition. $\endgroup$ – Henning Makholm Jun 11 '16 at 15:01
  • $\begingroup$ By the way, do you distinguish between variables that are "used in $S,Q$, etc." and ones that are "free in $S$, $Q$, etc."? $\endgroup$ – Henning Makholm Jun 11 '16 at 15:03
  • $\begingroup$ I don't think this is sound for the empty structure. Let $P$ be an unary predicate and $S$ be $\{\forall x(Px)\}$. Then we can derive $$\begin{array}{ll} S;\vdash \forall x(Px) & \text{axiom} \\ S;\exists y\vdash \forall x(Px) & \exists\text{restate} \\ S;\exists y\vdash Py & \forall\text{elim} \\ S;\exists y\vdash \exists z(Pz) & \exists\text{intro} \\ S;\vdash \exists z(Pz) & \exists\text{unbind} \end{array}$$ But this conclusion is not true in the empty structure! $\endgroup$ – Henning Makholm Jun 11 '16 at 15:21
  • $\begingroup$ @HenningMakholm: Thanks very much! I've fixed the errors. Yes the 'action at a distance' condition for the ∃elim rule that you've pointed out is not simple to wrap up in a context to the left of "$\vdash$" without carrying along the entire preceding proof. You see, I was merely trying to push the Fitch-style calculus into the sequent-shoe, and it doesn't want to fit. The problem is that you can instantiate different existential statements under the same context chain but not use the same variable names unless they are separated instances of the context chain (which is the case in Fitch-style). $\endgroup$ – user21820 Jun 11 '16 at 15:28
  • $\begingroup$ @HenningMakholm: So "not used in any previous step" is now "not used in $Q$ in any previous step", and "used" includes both free and bound variables, and your derivation of contradiction no longer works. $\endgroup$ – user21820 Jun 11 '16 at 15:31
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ With this, you can conclude (with empty $V$ and $\Gamma$) $[\,]\vdash \neg \bot$ by propositional reasoning, and thence by the $\exists$-introduction rule, $[\,]\vdash\exists x(\neg \bot)$ ... $\endgroup$ – Henning Makholm Jun 11 '16 at 16:33
  • $\begingroup$ That particular problem can be fixed with a side condition requiring that all free variables of $t$ are in $V$. But I don't know how to actually make the calculus work -- otherwise I'd have answered by now ... :-) $\endgroup$ – Henning Makholm Jun 11 '16 at 16:35
  • $\begingroup$ @HenningMakholm: What do you mean with "I don't know how to actually make the calculus work". Why does my calculus not work? The bug is now fixed. Is everything correct now? $\endgroup$ – ooooooo Jun 11 '16 at 16:40
  • 1
    $\begingroup$ I mean that I don't have an oracle that tells me whether such calculi work, and just because I (or you) can't immediately come up with an example of something that breaks doesn't mean that there is nothing that breaks. As this and the other comment thread shows, these things are subtle, and in the end I wouldn't trust anything else than an actual detailed soundness and completeness proof. $\endgroup$ – Henning Makholm Jun 11 '16 at 16:46
  • $\begingroup$ @HenningMakholm: But do you think the rough idea involved in this answer (that one equips the sequent with a set of variables) can solve our problem? $\endgroup$ – ooooooo Jun 11 '16 at 16:56
0
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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

$\endgroup$
  • $\begingroup$ As I've already said previously, when one writes down a sequent $[V]\ \Gamma\vdash\phi$, then one implicitly assumes that all free variables in $\Gamma$ and $\phi$ are elements of $V$. Now you are using $[\emptyset]\ \Gamma\vdash\exists x(p(x, y))$ as a sequent, but it isn't a sequent, because $y$ is free in $\exists x(p(x, y)$ and $y\not\in\emptyset$. $\endgroup$ – ooooooo Jun 12 '16 at 11:50
  • $\begingroup$ @ooooooo: Okay I missed that condition. Sorry. But I still don't know whether your system is sound because of the lack of ordering. Do you want me to leave my post here? If not I'll delete it. $\endgroup$ – user21820 Jun 12 '16 at 12:01
  • $\begingroup$ Don't delete it, at least your post logs our work process :-) $\endgroup$ – ooooooo Jun 12 '16 at 12:11
  • $\begingroup$ I plan to prove the soundness of "my" proposed system. $\endgroup$ – ooooooo Jun 12 '16 at 12:11
  • $\begingroup$ @ooooooo: Sure, and all the best! I'm more or less happy with my version since it's close to my Fitch-style system, but I'm too lazy to sit down and prove soundness and completeness rule by rule. =) $\endgroup$ – user21820 Jun 12 '16 at 12:18

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.