Ax(Fx -> Ay(Gy -> Hxy)) |- AxAy(Fx -> (Gy ->
Hxy))
1. Ax(Fx -> Ay(Gy -> Hxy))
Ass
2.
Fa
Hyp
3.
Fa -> Ay(Gy -> Hay) 1 UQ elim
4.
Ay(Gy -> Hay)
2,3 -> elim
5.
Gb -> Hab
4 UQ elim
6. Fa -> (Gb -> Hab)
2-5 hyp elim
7. Ay(Fa -> (Gy -> Hay))
6 UQ int
this is a legitimate move once we have
brought our original assumed "a" into a conditional by eliminating the
hypothesis
8. AxAy(Fx -> (Gy -> Hxy))
7 UQ int
One of the most common mistakes students make in working with these proofs is to forget that any inference rule (all those rules to introduce or eliminate a quantifier, for instance) must work with the main connective (what you saw in PLN by looking just at the last letter). In eliminating quantifiers, we work systematically inwards from the left, but in introducing them we can work from anywhere inside building out to the left.
The other common mistake is to ignore the new name rule.
In symbolizing, a good rule is to avoid starting with a prenex form unless there is no choice. Here are two examples.
All students like good teachers.
Ax(Sx -> Ay((Gy & Ty) -> Lxy))
think of this as saying that for anyone
at all (x), if that individual is a student then for anyone at all (y),
if that other individual is a good teacher then individual x will like
individual y
Only good students like hard classes.
AxAy((Hy & Cy & Lxy) -> (Gx & Sx))
Review the page on symbolization with my suggested templates before going on to the assignment.