search

Quelklef / fitch

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

Semantics around shadowed variables are broken #10

Open Quelklef opened 3 years ago

Quelklef commented 3 years ago

Consider

│ 1. [x]      assumed
│ 2. Px       assumed
├──────────
││ 3. [x]     assumed
│├──────────
││ 4. Px      RI:2
│ 5. ∀xPx     ∀I:3¬4[x→x]

Steps 4 and 5 are both invalid, but are wrongly given a justification.

Currently, the checker rejects step 3 on the grounds that variable shadowing is not allowed. This works, but it's not really an elegant solution.

Quelklef commented 2 years ago

Better example: this lets you prove that existance implies forall

│ 1.                   assumed
├──────────
││ 2. ∃xPx             assumed
│├──────────
│││ 3. [x]             assumed
│││ 4. Px              assumed
││├──────────
││││ 5. [x]            'x' is shadowed
│││├──────────
││││ 6. Px             RI:4
│││ 7. ∀xPx            ∀I:5-6[x→x]
││ 8. ∀xPx             ∃E:2,3-7
│ 9. (∃xPx)→(∀xPx)     →I:2-8