# Symbolic Logic - Quantifier Proof (w/ Conditionals) 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?

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).

• Sorry I'm still a bit confused. Why do I have to drive FrontOf(x) in this case for the sub-sub-proofs (6 - 7 & 8 - 11)? -- In which case how can I fix 8 - 11? I read through your "1st case" and I'm still lost. I've tried to derive a contradiction but the quantifier gets in the way so should I make another subproof for it? – user35766 Nov 23 '18 at 22:32
• @J.Martinez - from 6) derive Cube(x) and from 2) use forall-elim and then to-elim to derive FrontOf(x,c). – Mauro ALLEGRANZA Nov 24 '18 at 8:51
• @J.Martinez - that is 6,7,12,14 of your proof. – Mauro ALLEGRANZA Nov 24 '18 at 11:33
• 8-11 is simply wrong; you have to assume Small(x) and with the second case of or-elim : Dodec(x) and Large(x) derive Small(x) and Large(x), This contradicts 3 and it is (quite) done. – Mauro ALLEGRANZA Nov 24 '18 at 11:35
• This ended up being a lot more complicated than I thought but I managed to figure it out. Thank you so much for your patience and assistance! – user35766 Nov 24 '18 at 19:28

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
``````
• In that case what should be done for Step 8 - 11? – user35766 Nov 24 '18 at 7:47
• As Eliran advised, use Reduction to Absurdity to derive what you need. You should be able to see what contradictions you can use. – Graham Kemp Nov 24 '18 at 8:18

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
``````
• Line 7 doesn't work because of the quantifier. Also why is 9 needed? – user35766 Nov 23 '18 at 22:33
• @J.Martinez Different proof systems use different versions of the rules. Eliran is using that R is infered from P v Q, P -> R, and Q -> R . Since these conditionals are usually derived by subproofs, your proof checker allows a shortcut of directly using those subproofs. – Graham Kemp Nov 24 '18 at 7:37

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/

• This looks a lot more complicated than I initially thought it would be. Is there possibly another way? -- Also for step 6 using DeMorgan's intro rule (~) doesn't work. – user35766 Nov 24 '18 at 7:18
• @J.Martinez Are you saying about step 6 that DeMorgan's rule is not permitted in your proof checker? This is a derived rule. Page 141-2 of forallx give 10-line derivations of both forms. – Frank Hubeny Nov 24 '18 at 12:00