This picture is from the book "Mathematical Logic, 2nd edition, Christopher C. Leary, Lars Kristensen" :

quantifier rules of inference

I have two questions :

  1. Why are the quantifier rules of inference reasonable as they write in the start of the text ?

  2. Consider these variations :

$$(\{\psi\rightarrow \phi\}, \psi \rightarrow (\exists x \phi)\})$$

$$(\{\phi\rightarrow \psi\}, (\forall x \phi) \rightarrow \psi\})$$

Why is it not reasonable to have these quantifier rules of inference ?

  • 1
    $\begingroup$ I have never been able to make sense of this notation. In the simplest case, I look at it this way: If we begin a proof by assuming $P(x)$ and, without introducing any other assumptions, we derive $Q(x)$ with no free variables other than $x$, then we can infer that $\forall a: [P(a) \to Q(a)]$. $\endgroup$ Apr 19 at 3:51
  • $\begingroup$ The rules are "reasonable" because they are sound: they produce true conclusions from true premises. $\endgroup$ Apr 19 at 5:48
  • $\begingroup$ You have to consider the full system; using the rules and the quantifier axioms (Ch.2.3) you can easily prove your formulas. $\endgroup$ Apr 19 at 6:23
  • $\begingroup$ The intuitive explanation is to prove a formula that contain a fresh variable (eigenvariable) is effectively proving that a formula holds for all elements in the domain. And proving a fromula not involving an eigenvariable from an antecedent that may involve that eigenvraible is effectively proving that that fromula follows from an existential claim. Both are because of the arbitrariness of the eigenvariables. The reason we need an antecedent for the universal generalization (the first rule) is that Hilbert systems do not have a notion of context, unlike natural deduction or sequent calculus. $\endgroup$
    – Poscat
    Apr 22 at 7:40

4 Answers 4


Let us say , we have used matrix/vector/linear algebra with a list of axioms to show (Proof P1) that $0 \cdot x=0$

Now , we must have $0 \cdot 1 = 0$ , $0 \cdot 0 = 0$ , etc
We can not have some $x$ where that fails.
In case there is some $x$ where that fails , then Proof P1 is false : it is not working for that $x$ , whereas we claimed that P1 works & we claimed that P1 is true.
Hence there can be no $x$ where P1 fails.
Hence P1 works for all $x$ :
$[ P1 \implies 0 \cdot x=0 ] \equiv [ P1 \implies \forall x : 0 \cdot x=0 ]$

It is indeed true that we can change $\forall$ to $\exists$ :
$[ P1 \implies 0 \cdot x=0 ] \implies [ P1 \implies \exists x : 0 \cdot x=0 ]$
That is weaker claim. It is not equivalent claim.
That might be a new rule of inference like this :
$[ \forall x P ] \implies [ \exists y P ]$
Example :
"for all rational x , 2x is rational" versus "there exists some rational x , 2x is rational"
"all humans are made of carbon" versus "there is some human made of carbon"

The other rule is similarly justified.

It will roughly go like this :
Without Details on what $x$ is , we can show (Proof P2) that "when $\sin x$ is rational , then we must have that $\pi$ is irrational" : Proof P2 is not the Issue here.
We must then show that $\sin x$ rational does occur. Automatically , we can show $\pi$ is irrational via P2.
In case there is no way to make $\sin x$ rational , then we can make no claim on $\pi$ irrationality.

In other words : (A) When there does not exist a single $x$ where $\sin x$ is rational , then we can not infer the conclusion. (B) When there does exist at least a single $x$ where $\sin x$ is rational , then we can infer the conclusion using P2. (C) When for all $x$ we have $\sin x$ is rational , then we can still infer the conclusion using P2 , though that is unnecessary overwork.

OP variations are valid , though one is weaker & the other is overkill.


For anyone interested, there is a categorical interpretation of this too. So this is an answer of a different flavor.

I posted an answer relating to this not so long ago but for the rules of the equality instead. It's basically the same idea.

Simplifying a bit, in the context of posets, a Galois connection or an adjunction, is a pair of monotone maps $f : X \rightarrow Y$, $g : Y \rightarrow X$ for $X$ and $Y$ posets, such that $f(x) \leq y$ iff $x \leq g(y)$, forall $x:X$ and $y:Y$.

If such is the case, we write that $f\dashv g$.

Now consider that formulas make a poset with $\varphi\leq\psi$ iff $\varphi\vdash\psi$. (They have more structure than that but let's leave it there.)

You actually can construct one poset for each set of formulas that depend on a certain number of variables. Say $\Gamma$ is a list of variables, then $Form(\Gamma)$ is the set of formulas that depend on $\Gamma$.

For instance if $\Gamma=\emptyset$, then $Form(\emptyset)$ is the set of sentences or closed formulas. If $\Gamma = \{x\}$ then some formulas of $Form(\{x\})$ will be "$x=x$", "$\forall y.\ x=y$". And so on.

We may say that $\forall y.\ y=y$ or any closed formula is also a formula of $Form(\{x\})$. The same way that you can define a function and not use one of the variables it depends on; as in $f(x,y) := x+2$.

Then there's a very important monotone map between $Form(\Gamma)$ and $Form(\Gamma\cup\{x\})$ (for $x$ not occurring in $\Gamma$) that sends every formula of $Form(\Gamma)$ to itself, but with an unused variable $x$. Call this map $w_{\Gamma,x}:Form(\Gamma)\rightarrow Form(\Gamma\cup\{x\})$.

With all of this, we can define the quantifiers as:

$$\exists \dashv w \dashv \forall$$

This means that $\forall x$ is a monotone map that picks up a formula that depends on $\Gamma\cup\{x\}$ and gives a formula that depends on $\Gamma$, and also satisfies $w(\varphi) \rightarrow \psi$ iff $\varphi \rightarrow \forall x.\ \psi$.

Something similar can be said of the existential quantifier.


The two variations you proposed are sound (provided you're using the usual definition of structure, which requires the domain to be nonempty). So adding them as rules of inference would do no harm. It would also do no good, because these new rules would be redundant; anything you can deduce using them would have been deducible in the original system without new rules.

But if you were thinking of using the new rules instead of (rather than in addition to) the original quantifier rules, then that would do harm: The new system would be incomplete. (Confession: I haven't checked this incompleteness claim, but I'm convinced it's correct.)


In mathematical proofs, we don't usually talk about arbitrary objects about which nothing is known or assumed (as in your example), but rather we talk about objects in an explicitly specified, possibly empty domain, e.g. $\forall x :[x \in D \implies P(x)]$, or $\forall x: [D(x) \implies P(x)]$. If, for example, we want to prove the former, we could start by assuming $a\in D$ and then deriving $P(a)$. Then we can infer, as required, that $\forall x :[x \in D \implies P(x)]$ if $x$ is not free in $P(a)$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .