Symbolic Logic, Proof with Conditional

1 reply · 2K views · last reply
jehello
Messages
1
Reaction score
0
Screenshot of the Tarski's World proof checker showing a natural deduction proof with numbered lines, check marks and an X marking step 6, FrontOf(d, e), and a goal line at the bottom.


Any advice on how to make step 6 check out?
 
The problem is you can't conclude
FrontOf(d, e)​
from step 4, isn't it?
Then isn't another quantifier elimination all you need (i.e. prove that Cube(e) and Dodec(d) implies FrontOf(d, e)) ?

Also I'm wondering if you mixed up the order of e and y in step 4.