Wolfgang Schwarz

Unhelpful Trees

Today I wondered about the connection between

Under certain ideal conditions, something is conceivable iff it is possible

and

Something is possible iff it is conceivable under certain ideal conditions.

So I asked my tree prover whether

1) y(Iyx(PxCxy))x(Pxy(IyCxy))

and

2) x(Pxy(IyCxy))y(Iyx(PxCxy)).

The answer to the first question is "not valid (1764 nodes, 84 open branches)". For the second question I manually stopped the prover at "79623 nodes, 727 unticked, 35844 open branches, 18 constants". Clearly, these results are not very helpful.

Returning to pen and paper, I found out that (1) is false iff nothing is I. (Hence (y(Iyx(PxCxy))yIy)x(Pxy(IyCxy)) is valid -- though my tree prover runs into a problem when painting the 491 node tree, at least on Mozilla-1.5/Linux/PPC. Need to investigate further.) And (2) has a counter-model with 3 individuals: Ia, -Pb, Cba, Ic, -Cbc. I'll have to teach my prover to tell me that.