Chapter 7, Tutorial 6

PD: Derivations in PL

[Gold]

Derivations in this chapter all come from the older Logic Cafe text, the text meant to give a treatment of (almost all of) mathematical logic. You may want to read 8.2 and (especially) 8.3 of that text. But
the derivations in this text only include one derived rule we need to add...

... a rule for %E. But let's see how it could be useful and then see why it's a derived rule.

For example, with our current set of rules, think about what you could do with this derivation:

Right now (with our four rules from PD) we
only do this derivations in the following indirect and long-winded way!...

But we can do this more intuitively if we add a derived rule...

...here's the idea:

Just ASSUME that we have a name for the "something" described on line 1. Call it 't'.

This name 't' is used to illustrate or exemplify the object whose name we are not given. We'll use 't' temporarily to refer to any such object that has the property P (as described in line 1).

Once we make this assumption, using our temporary name, we can do this:

But this just shows we can "subderive" the goal...we can derive the goal given an extra assumption.

Still, because the extra assumption only added a name to (one of) the object(s) described in premise 1, we can do this
with a new rule:

But does this rule at line 7 make sense?

The intuition is that once the temporary name is dispensed with, the assumption is no longer essential to what we've derived. So, we can step out of the subderivation as in 7.

But let's make sure this thinking is *justified* by showing *the step in line 7 is a derived rule*.

*Without* our new rule, all we can do with our subderivation is this: