Symbolic Logic - Quantifier Proof (w/ Conditionals)

Question

I'm not sure if lines 6 - 7 & 8 - 11 are being done correctly. I feel like it's necessary to prove 12 which proves the rest of the problem.

I'm a bit stuck on lines 8 - 11. I initially tried to do it straight up. I couldn't see what I was doing wrong so I tried adding in sub-proofs but that complicated everything.

Anyone have any hints on where to go next with this?

Answer 1

You have to use or-elim on 1) considering two separate cases.

1st case : Dodec(x) and Large(x), from which, with 3) and assuming Small(x), derive a contradiction and then FrontOf(x,c).

2nd case Cube(x) and Small(x), from which, with 2), derive FrontOf(x,c).

Answer 2

The form of 'v elimination' is a Proof by Cases. You raise two subproofs, by assuming the cases of a given disjunction in turn, with the goal in each to derive the same conclusion.

| A v B   Given [Premise, Assumption, or Derived]
|  -
|  |_ A   Assumption
|  |  :
|  |  C   Derived
|  -
|  |_ B   Assumption
|  |  :
|  |  C   Derived
|  -
|  C      v Elimination

So you will have

|_ [f] S(f)                       Assumption
|  (D(f) ^ L(f)) v (C(f) ^ S(f))  Universal Elimination
|  |_ D(f) ^ L(f)                 Assumption
|  |  L(f)                        Conjunction Elimination
|  |  :
|  |  ~~F(f)                      Negation Elimination
|  |  F(f)                        Double Negation Elimination
|  -
|  |_ C(f) ^ S(f)                 Assumption
|  |  C(f)                        Conjunction Elimination
|  |  C(f) -> F(f)                Universal Elimination
|  |  F(f)                        Disjunction Elimination               
|  F(f)                           Disjunction Elimination
Ax (S(x) -> F(x))                 Universal Introduction

Answer 3

Here's roughly how to get from your Small(f) assumption (line 4) to Cube(f).

 4. S(f)
 5. | D(f) & L(f)
 6. | | ~C(f)
 7. | | L(f)&S(f)           [contradicts 3]
 8. | C(f)
 9. (D(f) & L(f)) -> C(f)
10. | C(f) & S(f)
11. | C(f)
12. (C(f) & S(f)) -> C(f)      
13. C(f)                     v-elimination

Answer 4

To make this work in the proof checker I am using I made the following substitutions:

• Dodec(x) is replaced with Dx.
• Large(x) is replaced with Lx.
• Cube(x) is replaced with Cx.
• Small(x) is replaced with Sx.
• FrontOf(xc) is replaced with Fxc.

---

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/