I have got the following statement: ∀aP(a),∀a(¬P(a)∨S(a)) ⊢∀a S(a)∨¬P(a)
My proof looks like this:
- ∀aP(a) (premise)
- ∀a(¬P(a)∨S(a)) (premise)
Start scope of x as substitution of a
- P(x) (forall elimination 1)
- ¬P(x) ∨ S(x) (forall elimination 2)
- P(x) (¬P(x) ∧ S(x)) (∧-introduction 3, 4)
- (P(a)∧¬P(a))∨(P(a)∧S(a)) (distributive law 5)
- (⊥)∨(P(a)∧S(a)) (¬-elimination 6)
- P(a)∧S(a) (⊥-elimination 7)
- S(x) (∧-elimination 8)
End Scope of x
- ∀a S(a) (∀a-introduction 9)
- ∀aS(a)∨¬P(a) (∨-introduction 10)
Is it possible to simply eliminate the bottom in the disjunction with given a more formal disjunction elimination?
Rules of Inference apply only to whole statements, not parts of statements, so neither the $\neg$-elimination (line 7) nor the $\bot$-elimination (line 8) attempts are valid inferences.
Rather, I suggest applying $\vee$-elimination, to assess the disjuncts of line $6$ individually. (Though to save work, I would do so on line $4$ instead.)
Additionally, that is not what $\bot$-elimination means. The rule, also known as ex falso quodlibet, or the Rule of Explosion, is the rule that $\bot$ allows the inference of any statement ; anything may be inferred from a contradiction.
Finally, the $\vee$ introduction should take place before the $\forall$-introduction. $\forall a~S(a)\vee\neg P(a)$ should be read as $\forall a~(S(a)\vee\neg P(a))$ .