search

wo / tpg

Tree Proof Generator
GNU General Public License v3.0
156 stars 20 forks source link

TPG should not allow nested quantifiers with the same variable. #27

Closed CCHeckman closed 7 months ago

CCHeckman commented 7 months ago

TPG says that ∀x∃x(P(x)→P(x)) is valid, but there are two nested quantifiers with an x in them, making this formula badly-formed.

wo commented 7 months ago

The formula is certainly "badly" formed, but it's controversial whether it should count as well-formed. Some textbooks say yes, some no. I want to err on the liberal side.

CCHeckman commented 7 months ago

The formula is certainly "badly" formed, but it's controversial whether it should count as well-formed. Some textbooks say yes, some no. I want to err on the liberal side.

Actually, it is legal (by convention, the variable belongs to the innermost quantifier), but it's a bad habit to allow it.