Symbolic Logic

Notice that both the premise and the conclusion are negations, not quantifier sentences. So you can't use the quantifier rules to start with.

You can think about this in terms of our usual strategy. The premise is a negation, so think about ~Elim (but you can't use it, because you don't have a double negation).

So we turn to our current goal, which is also a negation. That suggests that we should try using the ~Intro rule.

13.6

> In 13.6, I am very close, but as you can probably see

> I need a Tet(a) which I had a hard time proving within one of

> the subproofs.

That's because you can't prove it inside that subproof! At least not directly. The idea of doing disjunction elimination is not a bad one. In one of the subproofs you can prove Tet(a) and use it to get BackOf(a,c) which is what you really want. In the other subproof, you can derive a contradiction and then use contradiction elimination to get what you want.

13.8

> 13.8 I'm not sure how I can use the rules to turn a

> conditional statement into a conjunction, so that's a big

> sticking point.

This is not quite the right way to think about it -- you can't really turn a conditional into a conjunction (P -> Q doesn't imply P & Q).

But you don't actually need to prove a conjunction. What you need to prove is a conditional with a conjunction as its antecedent.

13.9

I don't assign this one any more, because it's evil. Keep in mind that an
argument is FO valid only if it's not possible for the premises to be true and
the conclusion false, *even if* you substitute different predicates.

13.13

Notice that the rules to think about right off the bat are ∀Elim, ∃Elim, and ∃Intro. Remember that you want to set up ∃Elim before using ∀Elim.

13.23

Same as 13.13! Since you've already done 13.13 for an earlier assignment, you shouldn't have any trouble re-doing it for this problem!

13.24

Notice that the conclusion is a conjunction, not an existential.

13.28

The conclusion is a universal, so you're going to want to use ∀Intro. Remember how to set up the subproof for this. You want the simple version of AIntro, not Generalized Conditional Introduction, so you don't want anything except the boxed constant on the first line. The last line of the subproof must be an instance of the universal you want to prove.

Remember how to construct an instance of a universal: drop the initial quantifier, and leave everything else the same (including the existential quantifier!) except that all of the occurrences of the variable that matches the initial quantifier get replaced by the boxed constant.

13.29

Important: notice that premise 2 is not an existential! It's a conditional. So you can't use ∃Elim on it.

This is actually quite a tricky problem. Hint: it's easiest if you use Taut Con to write down an instance of Excluded Middle. Depending on what instance of Excluded Middle you choose, it can either be very straightforward, or still a bit tricky.

13.30

Hint: this problem does not require any subproofs at all.

13.31

Remember that if all the premises and the conclusion are quantifier
sentences, you will want to do things in the following order:

1. set up
∃Elim and
∀Intro, if needed

2. do
∀Elim

3. propositional stuff

4.
∃Intro

5. finish the
∃Elim and
∀Intro subproofs, if any

In this proof, you are trying to prove a universal, so you *will* need
∀Intro. Also, you have an existential premise, so you will also need
EElim. So you need to set up the subproofs for those two rules first.
After that you can use
∀Elim.

The universal intro subproof is to prove
∀x∃y Likes(x, y). So you need
to start a subproof with a boxed constant (a, let's say). Nothing else
should appear on the line with the constant. The last line of the
subproof will be the result of dropping the universal quantifier and
replacing all the occurrences of its variable with 'a'. That means the last line of that
subproof will be
∃y Likes(a, y).

The
∃Elim subproof is based on line 2, which says
∃x∀y Likes(x, y). So
you need to start a subproof in which the first line is a boxed constant
(b, say) followed by the result of taking that sentence, dropping the
∃x, and replacing the x's with b's. That gives you
∀y Likes(b, y). The
last line of that subproof will be whatever you're trying to prove at
the next level out, which is
∃y Likes(a, y).

By the time you've got all that set up, you're getting pretty close.
(The whole thing took me 10 steps, including the two premises.) After
setting up the
∀Intro and
∃Elim subproofs, it's time to do
∀Elim (twice,
being careful about which constants you use for which variables), then
one propositional step, then one
∃Intro step, and then finish off the
subproofs you set up at the beginning.

13.40

Note that the premise is not an existential, it's a conjunction. So you can't use existential elimination on it -- you need to do conjunction elimination to get the existential separately, then do ∃Elim on that.

13.45

This is *very* close, but you're trying to close off two subproofs at the same time -- can't do that, because each subproof works differently. You have an ∃Elim subproof inside a negation introduction subproof -- need to conclude the existential elimination subproof first (still inside the negation introduction one), then conclude the negation introduction subproof.

Curtis Brown | Symbolic Logic | Philosophy Department | Trinity University

cbrown@trinity.edu