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.
> 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 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.
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.
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.
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!
Notice that the conclusion is a conjunction, not an existential.
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.
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.
Hint: this problem does not require any subproofs at all.
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.
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.