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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .