3

In standard FOL, can we prove $\forall x: P(x) \implies \exists x:P(x)$ without introducing a new free variable by universal instantiation, i.e without using $\forall x: P(x) \vdash P(y)$ where $y$ is not does not occur in $P(x)$?

I have tried direct proof, proof by contradiction, and proof by contrapositive. It looks impossible to me, but can't prove it.

Dan Christensen
  • 14,529
  • 1
    I am not quite sure what your concern is. Universal instantiation has no side-conditions, so you could use $x$ rather than $y$. I can't say for certain, because I don't know exactly what formulation of FOL you are using, but I would be very surprised if (a) you have a rule of universal instantiation and (b) you can prove this formula without using it. (If you can, then there is some redundancy in your set of rules.) – Rob Arthan Mar 02 '16 at 15:55
  • 1
    Not everyone agrees that $\exists x:\top$ is a theorem of first-order logic (i.e., that we only consider inhabited structures). IIRC, Poizat's book on model theory has a rant about this (he takes the point of view that the empty structure should not be excluded). In this case, $\forall x:\top$ does not imply $\exists x:\top$ because the former is tautological but the latter need not be true. – Gro-Tsen Mar 02 '16 at 16:20
  • PS: When I said "universal instantiation has no side-condition" that 's because I adopt the convention that $P[t/x]$ means $P$ with $t$ substituted for $x$ and with bound variables renamed as necessary to avoid variable capture problems". Other don't adopt this convention and have a side-condition on this rule. Like I said, you need to say exactly how you are formulating FOL in this kind of question. – Rob Arthan Mar 02 '16 at 16:28
  • @Gro-Tsen Do you have a reference for an at least first-order-logic that doesn't assume a nonempty universe? I'd be very interested in reading an exhibition that doesn't require such an annoying assumption. – DanielV Mar 02 '16 at 17:48
  • @DanielV Have a look at my proof-checking freeware available at my website http://www.dcproof.com The system of logic that it is based on does not assume a non-empty universe. In this and other ways, it is less philosophical and more mathematical and practical than standard FOL, if that makes sense. – Dan Christensen Mar 03 '16 at 05:13
  • @DanChristensen I actually have downloaded your software and visited your website, but haven't found any documentation for your logic. Maybe I'll look again, but any chance I could get some help with that? – DanielV Mar 03 '16 at 11:18
  • @DanChristensen A two or three page document that says "this is the grammar, these are the axioms, these are the rules of inferences" would be really helpful. – DanielV Mar 03 '16 at 11:25
  • @DanielV Click the Help** button in upper-right corner of the main screen. Then click on User Reference Guide. Then you will see the headings for Notation and Rules of Inference. The Notation section will spell out the syntax and grammar under various headings. – Dan Christensen Mar 03 '16 at 13:20
  • @DanielV As I mentioned, Poizat's Course in Model Theory does not make the nonemptiness assumption (see his comment on "almost equivalent" formulæ at the end of §2.1, p. 22), but it's true he doesn't consider proof theory much, so the slight annoyance of making proofs work over the empty universe doesn't bother him. (contd.) – Gro-Tsen Mar 03 '16 at 15:10
  • (contd.) The annoyance is naturally resolved when working in higher-order logic, where a variably of any type being introduced counts as an assumption (essentially, "the type is inhabited"). This is how proof-checkers generally work. If you really want first-order logic, the simplest way to do things is probably to introduce a special atomic formula "U" meaning "the universe is inhabited", which can be deduced from any existential formula or from any (formula involving a) closed term, and is required as a hypothesis for existential introduction. – Gro-Tsen Mar 03 '16 at 15:19

1 Answers1

2

If you use the following system from A Primer for Logic and Proof, Holly P. Hirst and Jeffry L. Hirst,

Axioms
Axiom 1: $A \implies (B \implies A)$
Axiom 2: $(A \implies (B \implies C)) \implies ((A \implies B) \implies (A \implies C))$
Axiom 3: $(\lnot B \implies \lnot A) \implies ((\lnot B \implies A) \implies B)$
Axiom 4: $(\forall x ~:~ A(x)) \implies A(t)$, provided that $t$ is free for $x$ in $A(x)$.
Axiom 5: $\forall x ~:~ (A \implies B) \implies (A \implies \forall x ~:~ B)$, provided that $x$ does not occur free in $A$.

Rules of inference
Modus Ponens (MP): From $A$ and $A \implies B$, deduce $B$.
Generalization (GEN): From $A$, deduce $\forall x ~:~ A$.

Notice that axiom 4 is the only axiom that doesn't hold in an empty universe (substitute false for A). Also notice the theorem to prove doesn't hold in an empty universe. So this axiom must be used somewhere in the proof. So a new variable must be introduced if you use these axioms.

DanielV
  • 23,556
  • 1
    Ah, I was under the impression that he didn't want any new free variable, whether it was named $x$ or not. Is Enderton public domain? – DanielV Mar 02 '16 at 20:07
  • @MauroALLEGRANZA $x$ is not free variable in Axiom 4. It is a bound variable. The $t$ would be a free variable. – Dan Christensen Mar 03 '16 at 04:47