Fitch proofs help?

Question

I'm new to logic and can see how to write these out informally, but need some help seeing how they should be translated into formal proofs in Fitch.

Answer 1

|  ~Dodec(a) -> Large(a)
|  Large(d) -> (Large(b) v Large(c)
|  Large(b) -> ~Large(d)
|_ Dodec(a) -> ~Large(c)
:
|  Large(d) -> Large(a)

You seek to derive a conditional. So you should use conditional introduction. Thus assume Large(d) aiming to derive Large(a).

Having made that assumption you may use conditional elimination on the second premise, to derive a disjunction. So you should use disjunction elimination; which is a "proof by cases" structure.

|  ~Dodec(a) -> Large(a)
|  Large(d) -> (Large(b) v Large(c))
|  Large(b) -> ~Large(d)
|_ Dodec(a) -> ~Large(c)
|  |_ Large(d)
|  |  Large(b) v Large(c)              ->E
|  |  |_ Large(b)
|  |  |  :
|  |  |  Large(a)
|  |  +
|  |  |_ Large(c)
|  |  |  :
|  |  |  Large(a)
|  |  Large(a)                          v E
|  Large(d) -> Large(a)                 ->I

And you should continue on in that vein.

---

|  Ax (Dodec(x) -> SameCol(x, a))
|_ SameCol(a, c)
:
|  Ax (Dodec(x) -> SameCol(x, c))

Now you seek to derive a universal statement. So use universal introduction: assume a fresh arbitrary term (let's say b) and derive the predicate in its context.

The predicate is a conditional statement, so use conditional introduction to derive it. Thus assume Dodec(b) aiming to derive SameCol(b, c).

To do this you need to invoke an analytical consequence, that (SameCol(a,c) & SameCol(b, a)) -> SameCol(b, c) may be used as an axiomatic schema.