search

wo / tpg

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

Validity of some weak syllogisms? #1

Closed shi-rudo closed 4 years ago

shi-rudo commented 4 years ago

First of all I want to say that this is a really great project! Thumbs up! I have tried out a few formulas and came across the following oddity. Shouldn't the following (weak) syllogism also be checked as valid?

Modus Felapton: No flowers are animals. All flowers are plants. Some plants are not animals.

Input: ∀x(Flowers → ¬ Animals) → ∀x(Flowers → Plants) → ∃x(Plants ∧ ¬ Animals)

Output: (∀x(Flowers→¬Animals)→(∀x(Flowers→Plants)→∃x(Plants∧¬Animals))) is invalid.

mackwai commented 4 years ago

Thank you! I'm glad you like it.

The reason that the argument checks as invalid even though Felapton is valid is because Felapton is one of those syllogisms whose premises have existential import. By that, I mean it implicitly assumes that at least one flower exists. If you add the premise "(3x,Sx)" ( ∃x(Flower(x) ) to the argument, it should check out as valid.

If you're interested in syllogisms, the software does allow you to enter them in the 3-letter form, for example,

MeP //     No flowers are animals.
MaS //       All flowers are plants.
.'.  //    ∴ 
SoP // Some plants are not animals.

I might add some text about existential import to the "information" page; I see now that I didn't explain what the software does with it.

wo commented 4 years ago

I assume this issue belongs to mackwai/UnaryPredicateLogic, not to my tree prover. Closing.