I was wondering if anyone could help me on a proof I've been working on: enter image description here

I was able to check that it is valid with a proof tree generator (prooftools): enter image description here

However, I still haven't figured out the proof. This is how far I've gotten: enter image description here

I'm having trouble getting to (Oa --> Ca) using predicate and propositional rules. Can anyone figure out how to do this/if this is actually possible. Once I have a contradiction here the rest of the proof should work out.


  • 1
    I'm not familiar with using trees, but I am puzzled by the bottom of the tree. Where did Oa > Ca come from? I thought we had ~(Oa > Ca) right above that. I found prooftools, but I haven't tried it yet. Welcome. Jun 8, 2019 at 8:20
  • This issue is fixed in ProofTools version 0.6.1. See my answer for a correct tree generated from the product. Jun 14, 2019 at 1:37

1 Answer 1


The ProofTools product has been fixed in version 0.6.1. Here is the output:

enter image description here

The branch on the left is no longer closed.

There is also a feature comparison page for various tree proof tools.


((Td\leftrightarrow (Oj\land Cj))\land (Te\leftrightarrow \forall x(Ox\to Cx)))\to (Td\to Te)

into Tree Proof Generator, a different tool, I get the following result:

enter image description here

Laird Shaw. ProofTools. https://creativeandcritical.net/prooftools Tree generated from Version 0.6.1. on June 19, 2019

Retrieved from Tree Proof Generator on June 8, 2019, at https://www.umsu.de/logik/trees/

  • Yeah that makes sense. Proof-wise it seemed like I would have to make an "illegal" universal introduction or existential elimination. I guess I did something wrong in the translation of the problem (the whole problem is a translation and proof of the Gettier case #1). Jun 8, 2019 at 16:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.