Proving dogs exist
If x barks then x is a dog: ∀x(Bx → Dx)
t: Timmy (a dog)


  1. ∀x(Bx → Dx) [Premise]
  2. Bt [Premise]
  3. Bt → Dt [1 UI]
  4. Dt [2, 3 MP]
  5. ∃x(Dx) [4 EG]


Proving ghosts don't exist
If the Hessian rider is imperceptible, then ghosts don't exist: ¬Ph → ¬∃x(Gx)
Ph: The headless Hessian rider (Sleepy Hollow) is perceptible


  1. ¬Ph → ¬∃x(Gx)[Premise]
  2. ¬Ph [Premise]
  3. ¬∃x(Gx) [1, 2 MP]
    ¬∃x(Gx) ⇔ ∀x(¬Gx)


Here I faced considerable difficulty. Observe the categorical logic syllogism below:

  1. All imperceptible thingsare nonexistent things
  2. All ghosts are imperceptible things
  3. All ghosts are nonexistent things

No problem at all, but issues pop up when translating the above syllogism into predicate logic. It's difficult to render premise 1 in predicate logic. How should I end this sentence, ∀x(¬Px → ???)?. Existence is not a predicate in predicate logic and if so, I have nothing to negate, to put where ??? is.
If the conclusion is No A are B (no ghosts are existent things) then, we would have to use a particular affirmative statement, viz. ∃x(Gx), there is at least one ghost (that exists) to negate.
The problem with this "proof" is that the Hessian rider is just one instance of a ghost that's imperceptible. To generalize the imperceptibility and thus nonexistence to all ghosts is fallacious. We need an all statement, I can't for the life of me come up with one. Help! Comments/suggestion/answers welcome.

We could do the following: Imagine there are exactly 2 ghosts claimed to exist, Myrtle (m) and the Hessian (h). Then the following would be a valid/sound argument.


  1. ¬Pm ∧ ¬Ph
  2. (¬Pm ∧ ¬Ph) → ¬∃x(Gx)
  3. ¬∃x(Gx)


Suppressed premise: ∀x∀y∀z((Gx ∧ Gy ∧ Gz) → x = y ∧ x ≠ z). There are exactly 2 ghosts.

Derived from the above technique, these statements ∀x(Gx → ¬Px) → ¬∃x(Gx): If for all x, x a ghost THEN x is imperceptible IMPLIES Ghosts don't exist AND ∀x((Gx → ¬Px) → ¬∃x(Gx)), looked full of promise, but it leads to a contradiction because if you instantiate Gx, which you must, you end up with ∃x(Gx) ∧ ¬∃x(Gx), a contradiction.

Proving earth exists
Pe = Earth is perceptible
There exists a thing and that thing is identical to earth: ∃x(x = e) i.e. earth exists


  1. Pe → ∃x(x = e)[Premise]
  2. Pe [Premise]
  3. ∃x(x = e) [1, 2 MP]


Not sure if ∃x(x = e) is the correct translation for earth exists. We're talking about 1 individual here and so it's easier to prove.

Proving Santa does not exist
Exists a thing that is Santa: ∃x(x = s)
Santa is perceptible: Ps


  1. ¬Ps → ¬∃x(x = s) [Premise]
  2. ¬Ps [Premise]
  3. ¬∃x(x = s) [1, 2 MP]


1 individual person and so again easier (to prove existence). Here too, unsure whether ¬∃x(x = s) is the correct translation for Santa Claus does not exist. It feels right, it means nothing is Santa.

The following were easier to prove:

  1. Some dogs exist (Particular affirmative)
  2. Earth exists (An individual, a constant)
  3. Santa does not exist (An individual, a constant)

The following remain unresolved (for me):

  1. No ghosts exist (Universal negative)

Also, I have the same exact issue with UNIVERSAL AFFIRMATIVE claims about existence. How do I prove/say All humans exist? ∀x(Hx → ???), where Hx: x is human. Do I do the same thing I did with the universal negative?

  • 1
    Yes ∃x(x = e) is the correct translation for "earth exists". In the usual interpretation of classical predicate logic, every constant (name) is assumed to "name" something. Thus, if the language has the constant e, the inference from e=e to ∃x(x = e) is correct. Jan 18 at 6:42
  • @MauroALLEGRANZA, what do we usually mean by Socrates exists? Also, e=e to ∃x(x = e), I don't think this is correct. Jan 18 at 7:16
  • :D i did the same, but for another subject and wrote an article regarding. Sharing as is, maybe interested. Logical deductive reasoning and implications. That remind me about Sherlock Holmes. :D
    – user71091
    Jan 19 at 15:29

4 Answers 4


The usual semantics for classical predicate logic assumes that every interpretation must have a not-empty domain and that individual constants (names) must refer to some member of the domain.

Thus, if our language has a constant e (for earth) we can deduce [from identity axiom ∀x(x=x)] e=e and thus ∃x(x = e) follows by (∃I), which is the correct translation for "earth exists".

The same for Socrates: if we use the constant S for it, we get ∃x(x = S) formalizing the statement "Socrates exists" (in the domain of our interpretation, that cannot be today world, where Socrates is dead).

Things are different for "All humans exist"; in this case the existential quantifier will not do and we need the "existence" predicate.

In classical predicate logic, "No ghosts exist" will be formalized with a predicate "G(x)" ("x is a ghost"): ¬∃x G(x).

But when we say "All humans exist" we are not asserting that every single human exists now, but that "existence" must be predicated of humans. With the “existence” predicate E we may have: ∀x(Hx → Ex).

In conclusion, if we want to salvage the distinction between what is (i.e. what the variables range over; see Quine's criterion of ontological commitment) and what exists, we have to supplement classical logic with some sort of "existence" predicate.

In modern philosophy, the discussion about the "logical" treatment of existence dates since Meinong and Russell. But the issues involved with the use of an "existence" predicate to manage e.g. statements of nonexistence are not easy: we may easily agree that numbers, the Homeric gods, round squares do not exist in the current sense of the term, that regarding everyday objects.

But numbers (i.e. abstract objects) are nonexistent in a different sense wrt Aphrodite [the same for ghosts and Santa]: in the context of Homeric poems the name "Aphrodite" does refer to a particular object (and it is meaningful to assert that "Aphrodite is not Athena").

And both, in turn, are nonexistent in a different sense wrt Napoleon and Socrates, that are today nonexistent, but existed in the past.

And finally, all the previous cases are different from round squares: about the concept "round square", the only normal case when we use it is probably with sentences like “There is no such thing as the round square.”

Relevant: Christian Wolff quoted from Yourgrau's book below:

“Being is what can exist. . . . In other words, what is possible is a being . . . [Indeed,] possibility is the very root of existence, and this is why the possibles are commonly called beings . . . [W]e commonly speak of beings past and future, that is of beings that no longer exist or do not yet exist. . . . Their being has nothing to do with actual existence [emphasis added].”

See e.g. Francesco Berto, Existence as a Real Property (Springer, 2012) as well as Palle Yourgrau, Death and nonexistence (Oxford University Press, 2019)

  • Re: “Being is what can exist. . . . In other words, what is possible is a being . . ." I find this relatable in the sense of looking out for rapidly approaching possible beings when attempting to cross a road. They needn't exist but you still look out for them. Jan 18 at 14:35
  • Arigato. What I have issue with is, where s = Santa, s = s → ∃x(x = s). We can prove anything exists. That won't do now, will it? Jan 19 at 1:50
  • Existence is a presupposition in predicate logic in that we can't refer to a class of existent things (existence is NOT a predicate). However, we may say of certain classes whether they exist/not e.g. ∃x(Gx) which is God exists. I was not aware that there is an existence predicate "∀x(Hx → Ex)" Jan 19 at 2:02

Universals are typically proven by contradiction, e.g. assuming some premise (x exists, or x without some property exists), some contradiction would occur, so the premise is wrong.

But real world reasoning typically is flawed with predicate logic due to unknowns, unclear identity, temporal changes, ...

So logic cannot prove there are no ghosts on far away planets, or far in the future/ far in the past. It can only reason about sets where all elements are known, distinguishable and constant.

  • Good points raised. Gracias. Jan 18 at 12:48

I write on a new page because the OP is already too long.

First off, the OP's issues.

  1. I proved dogs exist via a predicate which makes existential generalization possible. The conclusion is that the class of dogs is nonempty i.e. dogs exist.

  2. I tried proving ghosts don't exist using universal statements. This should've been possible because the fact that universal statements lack existential import doesn't get in the way. However, because nonexistence is the negation of existence, and because existence is not a predicate, this couldn't be achieved, except in a very narrow sense.

  3. Proving earth exists was simpler. All we had to do was find some predicate that applied to earth and infer existence from that. I was expecting some kind of rule like EI, UI, EG, etc. to help me make that inference, but an implication is what I had to use.

  4. Proving Santa does not exist is equivalent to nothing is Santa, a universal statement, and per rules of categorical logic, this is only allowed if the premises are universals themselves. I was basically saying all imperceptible things are nonexistent things (premise 1). However this critical statement had to be fragmented (as you can see there's no universal quantifier, ∀, in the statement) to ¬Ps → ¬∃x(x = s).


The most powerful statements in logic are universal statements. To prove something conclusively, a universal statement is a sine qua non.
To prove ghosts don't exist, the universal statement, imperceptible things don't exist, is problematic as existence is not a predicate.
A different approach is required (vide infra)

  1. ∀x(Px) [Premise]
  2. ∀x(Px → ¬Gx) [Premise]
  3. Pa [1 UI]
  4. Pa → ¬Ga [2 UI]
  5. ¬Ga [3, 4 MP]
  6. ∀x(¬Gx) [5 UG]
  7. ¬∃x(Gx) [equivalent to 6]

∀x(Px): All things are perceptible
∀x(Px → ¬Gx): If something is perceptible then it is not a ghost
Lines 6 and 7 are basically what I want, ghosts don't exist.

With Santa, we do the same thing

  1. ∀x(Px) [Premise]
  2. ∀x(Px → ¬x = s) [Premise]
  3. Pa [1 UI]
  4. Pa → ¬a = s [2 UI]
  5. ¬a = s [3, 4 MP]
  6. ∀x(¬x = s) [5 UG]
  7. ¬∃x(x = s) [equivalent to 6]

∀x(Px → ¬x = s): If something is perceptible it is not Santa

Lines 6 and 7 are saying nothing is Santa

Another question:

How to state/prove some dogs don't exist in predicate logic?

  • Mauro already addressed this in his answer. If you want to say of things that they exist or do not exist, then you cannot use standard logic, since this assumes that every thing is a member of the domain of quantification and every name has an existing referent. Instead you can use one of the free logics which have predicates for indicating that a thing exists.
    – Bumble
    Jan 19 at 5:24

The main point here is that existence is not a predicate, which indeed makes it impossible to translate statements such as "all imperceptible things are nonexistent". But here is also a central deal, which is the notion of existence denoted by the quantifier ∃. That notion is, in actuality, not the concrete notion of "real existence". Real existence is more restricted than this, and if it were applied, equivalences such as "¬∃xFx = ∀x¬Fx" wouldnt follow, given that claiming that there is no existent x who is F is not equivalent to claiming that there is no x who is F, as there could be a nonexistent x who is F. "There exists no being who is a unicorn" doesnt translate to "all beings are not unicorns". The usage of the "real existence" predicate (and in opposition to the broader existential quantifier) is not dead, and it can be seen in Leach's formalization of Anselm's ontological argument, in which the notion of real existence is expressed by the predicate "E", whilst the existential quantifier is used merely to account for property-bearing.

You must log in to answer this question.

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