Alright, so these First Order logic rules are kind of wacky.

Here's some things to remember:

Mickey mentioned on Tuesday that "∀" and "∃" are kind of negations of each other. That's... kind of right.
Let me try to clarify:

If I say, "ALL of Van Gogh's paintings are oils," (painting(x) AND vanGoghPainting(x) => oilPainting(x)), and you know anything about Van Gogh, you'd probably say, "No way!"

How would you go about proving me wrong? Well, you'd say, "I can show you at least one Van Gogh painting that isn't an oil! That is, ∃ a Van Gogh that is NOT an oil!"


In some sense, the negation of the for all is a "there exists NOT". We'll show this, I think, later. For now, have some things that don't exist:


Anyway, that's why the "∀ Introduction" and "∃ Elimination" are kind of similar (they both use the "u can't be a free variable" condition). Likewise, "∀ Elimination" and "∃ Introduction" are kind of related.

So here's the intuition for the four rules:

∃ Introduction:

Γ
D
P[τ/t]
_________
tP


This is probably the easiest. How do you show that an existencial statement is valid? Like, "There exists a number that is even?" Easy: just pick a specific example, and show that the statement is true. So, here, pick a number, say 2, and show that 2 is even. (Duh). Then, the statement is true.

How do you get that 2? That is, how do you get the specific example you need (the tau in the general form of the rule)? Well, you have to use what you know. It's a little tricky, but if the statement is true you should be able to do it.

Also note that tau is a term: it doesn't matter if tau is a variable or the result of a function, all it matters is you show there's some thing that makes the statement true.

∀ Elimination:

Γ
D
∀tP
_________
P[τ/t]


We'll do this one next, because it's super similar.
Getting rid of universal quantifiers is super easy. If you have ∀ x, P is true, you can stick ANY term in for x, and P must be true.


As an example: if I say ALL pumpkins eventually rot, and that statement is provable, then I can get rid of the for all statement by picking a specific pumpkin: let's say... the pumpkin to the right. If ALL pumpkins eventually rot, it's definitely true that the pumpkin to the right is eventually going to rot.

(Note that the statement does not apply to images of pumpkins).


∃ Elimination:

Γ                 Δ,P[u/t]^x
D1                         D2
tP                          C
_______________________________x
tP


This is a little trickier!

Think of it this way: say we know that that ∃ a prime number greater than 5. Maybe we don't know what it actually looks like, but this rule lets us basically pull that prime number out, and we give it a name, "u." Of course, u can't already be used in the proof, (because then things would turn into an Abbott and Costello sketch)

Anyway. If you look at the form of the rule, you'll see that the we get rid of the ∃ and replace it with a unique free variable that stands in for the thing which must exist.

∀ Introduction:

Γ
D
P[u/t]
_________
tP


Can we extend the process in the ∃ elimination to this one? Well, we'd have to work with a LOT of objects, to show ∀. In fact, we'd have to consider everything in the entire universe! That's... not really practical, especially if there are an infinite number of things in the universe.


The trick is that we have to think about what we mean when we say "FOR ALL." If we say, "ALL Trick-or-treaters wear costumes." Which trick or treaters are we talking about? Well, we're actually talking about an arbitrary trick-or-treater.

So if we can pick an arbitrary element, let that element stand for any possible element in the domain, and show that our statement holds for it, that is sufficent to show that ∀ t P.

But what the heck does arbitrary mean? Well, it means we have no control over what is picked. The proof has to hold regardless of the elemnt that is picked. That's the u in the above proof; notice that in the notes the condition along with this rule states that u can't be used anywhere else in the proof; it has to be completely unrestrained.

Now try the proof on page 31 of the slides!

Allons-y! Back to CIS160 Page