A difficult tableau proof

By the way, here's another problem my prover can't solve (in reasonable time):

Show: ∀y∃z∀x(Fxz ↔ x=y) → ¬∃w∀x(Fxw ↔ ∀u(Fxu → ∃y(Fyu ∧ ¬∃z(Fzu ∧ Fzy))))

This is problem 54 in Pelletier 1986. It is a pure first-order adaptation of a little theorem proved in Montague 1955. Montague gives a fairly simple proof. His proof uses the Cut rule, which the tableau method doesn't have. I've tried to construct a tableau proof by hand, but failed.

This might be a nice example of a relatively straightforward fact that can be proved easily with Cut, but not without.

Comments

No comments yet.

Add a comment

Please leave these fields blank (spam trap):

No HTML please.
You can edit this comment until 30 minutes after posting.