search

Quelklef / fitch

Interactive proof assistant for Fitch-style natural deduction
https://maynards.site/fitch
3 stars 0 forks source link

∃-intro justification is wrong in vacuous cases #14

Closed Quelklef closed 2 years ago

Quelklef commented 2 years ago

See below:

│ 1. [a]      assumed
│ 2. Pa       assumed
├──────────
│ 3. ∃xPa     ∃I:2[a→x]

The justification given is ∃I:2[a→x], but should be ∃I:2[a→a]

Quelklef commented 2 years ago

Meh, not a bug, just confusing.

Line 3 was indeed concluded from line 2 via a variable replacement a→x, it's just that 0 as were replaced with x

Not a big deal; closing