1

I was recently using https://proofs.openlogicproject.org/ and realized that their version disjunction elimination is fairly restrictive.

I had a proof set up something like this:

  1. p∨q (Premise)

  2. p∨r (Premise)

  3. |p (Assumption)

  4. |.

  5. |.

  6. |.

  7. |s

  8. |q (Assumption)

  9. ||r (Assumption)

  10. ||.

  11. ||.

  12. ||.

  13. ||s

  14. |s (2, 3-7, 9-13, ∨E)

  15. s (1, 3-7, 8-14, ∨E)

I am used to using A→B,C→B,A∨C⊢B as ∨ elim, but I recently became aware of the fact that Fitch-style ∨ elim is important for Gentzen’s original system to have a certain sub-formula property that helps prove consistency.

Are there any similar technical reasons for disallowing the way I used P∨R for ∨ Elim on line 14, or is it just by convention?

Edit my original question was erroneously titled “Question about existential elimination in Fitch”.

3
  • What exactly is the difference between typical disjunction elimination and Fitch style elimination? As for your software not accepting the proof, its likely because you stil have the open assumption of r, you would need to duplicate the proof of p->s inside the scope of q.
    – emesupap
    Aug 13, 2023 at 5:54
  • Is there a reason to this? If you translate the proof into a version using the other rule I mentioned, you can format it basically the same way. By the way, I was doing the deduction ((PvQ)&(PvR))⊢(Pv(Q&R)).
    – PW_246
    Aug 13, 2023 at 6:21
  • if you contrast fitch style with, say, tree style, then fitch "reuses" subproofs. But translating back into tree format directly requires that one "paste" the "reused" subproofs back into proper scope. But since I'm unfamiliar with your software I can't say this is the reason
    – emesupap
    Aug 13, 2023 at 7:11

1 Answer 1

2

It is important not to confuse the object language with the metalanguage. The material conditional → is a connective within the object language, while the deducibility relation ⊢ is a symbol in the metalanguage.

By convention it is usual when setting out the natural deduction rules for a logical constant to make them 'pure', i.e. not depending on any other constants in the object language. So your version of the disjunction elimination rule:

A → B; C → B; A ∨ C ⊢ B 

runs against this convention by making the rule for disjunction depend on the material conditional. The openlogic project and many other sources prefer to express disjunction elimination as a metarule, e.g.

P ∨ Q;  P ⊢ R;  Q ⊢ R  ⇒  R

or sometimes you may see something like:

Γ, P ⊢ R;  Γ, Q ⊢ R  ⇒  Γ, P ∨ Q ⊢ R

That said, the versions of the rules I've presented here are not more restrictive than your version. In fact, by application of the deduction theorem they entail your version.

2
  • Why are we limited to the version of disjunction elim you presented, namely Γ, P ⊢ R; Γ, Q ⊢ R ⇒ Γ, P ∨ Q ⊢ R. The rule I tried to implement can be defined as Γ, P ⊢ R; Γ, Σ, Q ⊢ R ⇒ Γ, Σ, P ∨ Q ⊢ R. Since on line 14 we have s on assumption r, and we have s on line 7 on assumption p, and both assumptions were open before implementing the rule to get line 14, it really seems like nothing is gained from the stricter rule, given that disjunction doesn’t have to depend on implication the way I implemented it.
    – PW_246
    Aug 13, 2023 at 8:08
  • 1
    That version would work too. It just boils down to what your program chooses to accept. The main point is that you must exhibit the move from P to R and from Q to R as a deduction, not a conditional.
    – Bumble
    Aug 13, 2023 at 10:26

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .