The converse Buridan formula is shown to be invalid

wo / tpg

Tree Proof Generator

GNU General Public License v3.0

156 stars 20 forks source link

The converse Buridan formula is shown to be invalid #22

Closed MichaelRushton closed 1 year ago

MichaelRushton commented 1 year ago

https://en.wikipedia.org/wiki/Buridan_formula

https://www.umsu.de/trees/#~6x~9Fx~5~9~6xFx (∀x◇Fx→◇∀xFx) https://www.umsu.de/trees/#~8~7xFx~5~7x~8Fx (□∃xFx→∃x□Fx)

wo commented 1 year ago

I don't see why this is an issue. The converse Buridan formula is invalid in standard constant domain semantics, and the prover correctly displays a countermodel.