Can anyone explain the FOL inference rules?

Philosophy Forums Philosophy
1

Hey!

I need an example of a FOL proof. I know how to do propositional logic proofs (got an A in the class, and solved a very long proof the professor posed to intimidate the class!), but our class just touched on FOL.

I’m just confused about Universal Introduction, Universal Elimination, Existential Introduction, Existential Elimination, and Substitution.

Thanks,
Lexi

2

I’m a little confused as to what you’re asking. Anything involving merely items in sets or categories is an FOL proof. Soo… exactly what are you looking for?

  1. All of my marbles are in my bag.
  2. The red marble is one of my marbles.
  3. Thus, the red marble is in my bag.

Or are you asking for the AI lingo?

3

I mean first-order predicate logic, you know, the formal system of logic that involves quantification and predicates? The one with the upside-down Es and As?

4

Sorry, I’m not a linguist. Around here, someone would have to go to the trouble of learning their symbolic dialect and translating it for you. Their language would be a lot more common if they bothered to use type-able characters.

“Quantification” merely means measuring something within a range of a property. To “quantify it” is to give it a degree of measure or define its limits. The range is the “set”.

“Predicate” merely means a description of the common property of an item possibly in a set/range of items, a qualifier for belonging in the range/set. And it can be either a function with variables or a simple statement.

5

Hi TSLexi,

We called it Universal Instantiation (Universal Elimination), Universal Generalization (Universal Introduction), Existential Instantiation (Existential Elimination), and Existential Generalization (Existential Introduction) when I took/taught logic.

A generalization is when you have the general rule, for example, of the form (x)(Fx * Gx) “For all x, x is F and x is G.” – a universal – or (∃x)(Px * Hx) “There exists an x, such that x is P and x is H.” – an existential statement. In proofs, to use the valid rules of inference you’ve learned, you can only apply them to specific statements, not general ones with quantifiers attached. The valid inference rules were designed to work on truth functional statements in sentential logic. Generalized Forms are not truth functional. So to use the inference rules in predicate logic proofs you need to remove the quantifier of the statement you want to use an inference rule on.

The first of the four quantifier rules is called Universal Instantiation (UI) (or in your terms, Universal Elimination), because we are eliminating the universal quantifier and we are providing a specific instance of the universal statement, thus instantiation:

  1. (x)(Fx * Gx) premise ---------- /prove Fa
  2. Fa * Ga ------------------------- from 1, Universal Instantiation
  3. Fa ------------------------------ 2 Simplification

When you instantiate, you replace the “quasivariables” (commonly x, y, & z) with “instantial letters” (commonly the earlier letters of the alphabet).

What if we needed to prove (x) Fx ? We would need to use the inference rule of simplification as above, so again we would need to use Universal Instantiation, but then since our conclusion is a universal statement we would need to use Universal Generalization (Universal Introduction), going from an instance of, say, Fb “Bob is a fast runner” to the universal statement (x) Fx, “For any x, x is a fast runner.” :

  1. (x)(Fx * Gx) p ---------- /prove (x) Fx
  2. Fb * Gb ----------------- 1 Universal Instantiation
  3. Fb ----------------------- 2 Simplification
  4. (x) Fx ------------------- 3 Universal Generalization

When you generalize, you replace the instantial letters, like b, with quasivariables, like x.
Very simple examples, but it’s been awhile since I did any of this. I recommend Hurley’s A Concise Introduction to Logic if you can get it from a library, or Logic and Philosophy: A Modern Introduction. The Existential rules are similar.

All ravens are birds.
Shelly is a raven.
Therefore, there is at least one bird.

  1. (x)(Rx > Bx) p
  2. Rs p --------------- / prove (∃x) Bx

The conclusion we need to prove is an existential statement, so it tells us we’re going to need to make an Existential Generalization (to introduce an existential statement):

  1. (x)(Rx > Bx) p
  2. Rs p --------------- / prove (∃x) Bx
  3. Rs > Bs ----------- 1 UI
  4. Bs ----------------- 2, 3 Modus Ponens
  5. (∃x) Bx ----------- 4 Existential Generalization

And Lastly, Existential Instantiation, which allows us to eliminate the existential qualifier and provide a specific instance of the existential statement.

All attorneys are college graduates.
Some attorneys are golfers.
Therefore, some golfers are college graduates.

  1. (x)(Ax > Cx) p
  2. (∃x)(Ax * Gx) p ---------- / prove (∃x)(Gx * Cx)
  3. Ab > Cb ------------------- 1 UI
  4. Ab * Gb ------------------- 2 Existential Instantiation
  5. Ab ------------------------- 4 Simp
  6. Cb ------------------------- 3, 5 Modus Ponens
  7. Gb * Ab ------------------- 4 Commutation
  8. Gb ------------------------- 7 Simp
  9. Gb * Cb ------------------- 6, 8 Conjunction
  10. (∃x)(Gx * Cx) ----------- 9 Existential Generalization
6

So let’s say I’m trying this:

Premise 1. Ax(Px → Qx)
Premise 2. Ex(~Qx)
Prove: Ex(~Px)

  1. Pa → Qa From Premise 1, UI
  2. ~Qa From Premise 2, EI
  3. ~Pa From 1, 2, MT
  4. Ex(~Px) From 4, EG
    QED

So, how do I deal with quantification over predicates in SOL? And how do I get the logic symbols; the alt codes aren’t working…

7

I forgot to explain that whenever you do an Existential Instantiation you need to use a new instantial letter that has not previously occurred before in the proof, otherwise problems of assumption can arise. So in this proof, you need to do Existential Instantiation before Universal Instantiation and then you can use the same instantial letter ‘a’ throughout. It should be fixed in the last example of my previous post, too.
Your proof looks good to me, though.

EDIT: Nevermind, I didn’t read your question correctly the first time. I have never studied beyond first order predicate logic.

Instead of alt. codes you can just paste the ∃ from another webpage or use Microsoft’s character map tool in the “accessories → system tools” folder in the start menu if you have Windows. For the universal quantifier, I’ve always just used a variable in parentheses before the statement.

8

Thanks. Although isn’t it odd using a particular modus tollens to prove a quantified modus tollens? That doesn’t seem right…

9

I edited my last post, btw

I don’t see a quantified modus ponens. Modus ponens is the argument form

A > B
A
Therefore, B.

What you have quantified in the premise is a statement of logical implication in premise 1 and a statement of negation in premise 2.

10

Basically, you’re not quantifying whole argument forms, only statements. The conclusion is a quantified statement of negation. You used modus tollens in the proof as a step of valid inference to arrive at the conclusion. Modus tollens is not line 3 itself, but the reasoning you used to arrive at line 3. Hopefully that makes sense.

11

So, here’s another one:

P1. AxAy: P(x,y) || Q(x,y)
P2. AxAy: Q(x,y) → R(x,y)
P3. ExEy: ~R(x,y)
Prove: ExEy: P(x,y)

  1. ~R(a,b) P3, EI
  2. Q(a,b) → R(a,b) P2, UI
  3. P(a,b) || Q(a,b) P1 UI
  4. ~Q(a,b) 1,2, MT
  5. P(a,b) 3,4 DS
  6. ExEy: P(x,y) 5, EG
    QED

BTW, is FOL semi-decidable? A valid proof will eventually terminate, while an invalid one will go on forever.

12

These are multiply quantified relational predicate statements? I’m used to slightly different notation, e.g. “Some x pulls some y.” would be (∃x)(∃y)Pxy – is that the meaning of ExEy: P(x,y) ?

Yes, FOL is considered to be semi-decidable.

13

I learned ExEy. And thanks, I heard somewhere that it was semi-decidable, but I forgot where.