2

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$"

Community
  • 1
Metta World Peace
  • 6,403

1 Answers1

2

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.

Asaf Karagila
  • 393,674
  • 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
  • 2
    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