Just as in BOOL and PROP, we need to know how to handle each type of main connective in FOL proofs.

In FOL, when we tell you to look at the * main connective*, we mean “connective or quantifier.”

Technically, quantifiers are not “connectives.” There is a general term, * operator*, for quantifiers and connectives.

But we have been telling you all along that the key strategy for formal proofs is to* look at the main connective*. To keep things simple we’ll keep repeating that idea, but what we mean is “main connective or quantifier”.

In this section, we cover cases where a universal quantifier is wide scope, either as a premise or a conclusion.

Universal premise: use AElim.

Universal conclusion: set up AIntro.

We know that a universal premise calls for the AElim rule, and a universal conclusion calls for AIntro rule.

Let’s look at each case in more detail.

Universal premise: pick a name and use AElim.

A universal premise is one of the most straightforward situations in FOL. You just * use AElim to instantiate the universal claim for a specific name*.

The critical question is always: which name to choose?

The critical question is always: which name to choose?

To answer that question, you look around in the proof for any names. Oftentimes, those other names will tell you how to use AElim.

For example, let’s look at the classic syllogism that assumes that all humans are mortal and Socrates is human. From those premises we can prove that Socrates is mortal.

To figure out that proof, we just needed to notice that instantiating the universal quantifier for the name “s” was the right plan.

If there are multiple names, you need to look for patterns and think about which instantiations would be useful.

Sometimes there are multiple names in a proof. You don’t want to just start instantiating the quantifiers. Instead, you need to think about what patterns there are and which instantiations would be useful.

Here’s an example.

Sometimes you will have a universal premise and there aren’t any other names in the proof.

If there are no other names, then (1) you might need to use the name “a”, or (2) you might need to do something else first, like start a AIntro subproof.

When that happens, there are two different situations you might be in.

First, you might just need to instantiate the quantifier for some name, any name at all, and it doesn’t matter which.

In that case, we will always use the name “a”.

Here is the simplest kind of example.

That situation is not that common, however. Much more likely, if you don’t have another name in the proof that tells you what to instantiate a universal quantifier with, **what you need to do is look around at the main connectives of the other premises and conclusion**.

**Important!** Usually, what you need to do is start with the main connective of some other premise or the conclusion.

Later on you’ll know what name to use for AElim. Typically it will be “n”.

For example, if your conclusion is a wide-scope universal quantifier, then you need to plan out a AIntro proof first, before doing AElim.

Let’s talk about that now.

We’ve been talking about using a universal * premise* with AElim.

If your * conclusion* is a universal quantifier, you need to start a AIntro subproof. That means you must start a new subproof and assume an arbitrary name @n.

Rule: when your conclusion is a wide-scope universal, the best plan is to start a AIntro subproof.

This is such an important idea, we will give you this general rule: * when your conclusion is a wide-scope universal, the best plan is to start a AIntro subproof*.

Let’s try it. We recommend you work this proof out on paper before continuing!

In that proof, since we are proving Ax(P(x)v~P(x)) from no premises, the universal conclusion is all we have to guide us.

If your first reaction was to do a reductio, then we are happy that you mastered one of the key ideas of BOOL: when all else fails, try reductio.

But that rule is preempted here. All else isn’t failing!

Universal conclusion: always start a AIntro subproof!

You need to also master the key rule of this chapter: a universal conclusion always tells you what to do. Start a AIntro subproof.

That is why we assume an arbitrary “n” on line 1.

This rule for a universal conclusion is so important, it supersedes pretty much every other rule about formal proofs.

For example, let’s say you have universal premises and conclusions.

If you initially notice the premises, you might want to start instantiating them. **But it is always a good idea to first start the AIntro proof.**

Often, the arbitrary “n” that you assume will be the name you need to use in AIntro.

Here’s an example.

Login

Accessing this textbook requires a login. Please enter your credentials below!