Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

On page 121, A Mathematical Introduction to Logic, Herbert B. Enderton(2ed),

3c. The remaining case is where $ϕ$ is $¬∀x ψ$. (In order to show $\Gamma \vdash ¬∀x ψ$)It would suffice to show that $ \Gamma \vdash¬ψ^x_t$ , where $t$ is some term substitutable for $x$ in $ψ$. (Why?) Unfortunately this is not always possible. There are cases in which $$\Gamma \vdash ¬∀x ψ$$, and yet for every term $t$,$$\Gamma \nvdash ¬ψ^x_t$$ (One such example is $\Gamma= ∅$,$ψ = ¬(Px→∀y Py)$.) Contraposition is handy here; $$\Gamma;α \vdash ¬∀x ψ$$ iff $$\Gamma; ∀ x ψ \vdash ¬α$$

Notations: $\Gamma$ represents a set of axioms; $P$ is a unitary relation: $\Gamma \vdash \phi$ means $\phi$ is deducible from $\Gamma$, or $\phi$ is a theorem of $\Gamma$.

The part from "Contraposition is handy here" to the end eludes me, especially I don't know what $\alpha$ represents.

Here's my attempt to understand it: The example is equivalent to: $$\vdash \exists x (Px→∀y Py)$$ for any term $t$, $$\nvdash Pt→∀y Py$$

The former can be shown to be true by discussing situation $\forall x Px$ and its negation(By contrast, in a previous question, Hurkyl argues that whether the formula is well-formed, is, at best, ambiguous). But I got stuck on how to show the latter "for any term $t$, $\nvdash Pt→∀y Py$"

share|cite|improve this question
up vote 2 down vote accepted

We work in a language which has a binary symbol relation $<$ and a constant symbol $0$. Consider the axioms which say that $<$ is an irreflexive dense linear order without endpoints.

Now $\Gamma$ proves that $\lnot(\forall x.0<x)$. Simply because there are no endpoints so there is someone smaller than $0$.

But there is no term $t$ such that $\Gamma\vdash t<0$. Simply because there are no function symbols so terms are either $0$ itself or free variables.

share|cite|improve this answer
Gratitude. So your point is it's one thing to show the existence, but it's quite another to define it. – Metta World Peace Feb 16 '13 at 13:23
Yes. This is very much my point. You can come up with cool and much more complicated examples too. But this is the essence of non-constructive proofs, any non-constructive proof is exactly something like this. – Asaf Karagila Feb 16 '13 at 13:34
The proof that $(\exists x)[x < 0]$ and $(\forall y)\lnot [0 < y \land y < 0]$ implies $\lnot (\forall x)[0 < x]$ is constructively valid. Even in constructive systems, there may not be a term for every object that can be proven to exist - for example this is the case in CZF set theory. It's often necessary to expand the language to obtain the term existence property for a constructive theory. Separately, in classical logic we can have a (nonconstructive) proof of $\Phi(t_1)\lor\Phi(t_2)$ but no proof of $\Phi(t_1)$ or $\Phi(t_2)$ individually, which is a quite different situation. – Carl Mummert Feb 16 '13 at 14:03
@Carl: Illuminating as always! Thanks! – Asaf Karagila Feb 16 '13 at 14:08

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.