search

gauravmm / Navelgazer

Linter for first-order logic
http://navelgazer.gauravmanek.com/
MIT License
0 stars 1 forks source link

Existential Instantiation Rules #14

Open beachtrees opened 4 years ago

beachtrees commented 4 years ago

I could be mistaken but the code currently flags the following existential instantiation as incorrect:

   [1] (1) (∃x)(∀y)(Fx ≡ Fy)     P
[1][2] (2) (∀y)(Fc ≡ Fy)     (1)cEII

In the error window it says that (2) should read "(∃y)(Fc ≡ Fy)" which I don't think is correct.

gauravmm commented 4 years ago

I think you're right. I'll take a look at it in the next few weeks.

If you figure out the problem, feel free to submit a pull request!