2 added 773 characters in body
source | link

The form of 'v elimination' is a Proof by Cases. You raise two subproofs, by assuming the cases of a given disjunction in turn, with the goal in each to derive the same conclusion.

| A v B   Given [Premise, Assumption, or Derived]
|  -
|  |_ A   Assumption
|  |  :
|  |  C   Derived
|  -
|  |_ B   Assumption
|  |  :
|  |  C   Derived
|  -
|  C      v Elimination

So you will have

|_ [f] S(f)                       Assumption
|  (D(f) ^ L(f)) v (C(f) ^ S(f))  Universal Elimination
|  |_ D(f) ^ L(f)                 Assumption
|  |  L(f)                        Conjunction Elimination
|  |  :
|  |  ~~F(f)                      Negation Elimination
|  |  F(f)                        Double Negation Elimination
|  -
|  |_ C(f) ^ S(f)                 Assumption
|  |  C(f)                        Conjunction Elimination
|  |  C(f) -> F(f)                Universal Elimination
|  |  F(f)                        Disjunction Elimination               
|  F(f)                           Disjunction Elimination
Ax (S(x) -> F(x))                 Universal Introduction

The form of 'v elimination' is a Proof by Cases. You raise two subproofs, by assuming the cases of a given disjunction in turn, with the goal in each to derive the same conclusion.

| A v B   Given [Premise, Assumption, or Derived]
|  -
|  |_ A   Assumption
|  |  :
|  |  C   Derived
|  -
|  |_ B   Assumption
|  |  :
|  |  C   Derived
|  -
|  C      v Elimination

The form of 'v elimination' is a Proof by Cases. You raise two subproofs, by assuming the cases of a given disjunction in turn, with the goal in each to derive the same conclusion.

| A v B   Given [Premise, Assumption, or Derived]
|  -
|  |_ A   Assumption
|  |  :
|  |  C   Derived
|  -
|  |_ B   Assumption
|  |  :
|  |  C   Derived
|  -
|  C      v Elimination

So you will have

|_ [f] S(f)                       Assumption
|  (D(f) ^ L(f)) v (C(f) ^ S(f))  Universal Elimination
|  |_ D(f) ^ L(f)                 Assumption
|  |  L(f)                        Conjunction Elimination
|  |  :
|  |  ~~F(f)                      Negation Elimination
|  |  F(f)                        Double Negation Elimination
|  -
|  |_ C(f) ^ S(f)                 Assumption
|  |  C(f)                        Conjunction Elimination
|  |  C(f) -> F(f)                Universal Elimination
|  |  F(f)                        Disjunction Elimination               
|  F(f)                           Disjunction Elimination
Ax (S(x) -> F(x))                 Universal Introduction
1
source | link

The form of 'v elimination' is a Proof by Cases. You raise two subproofs, by assuming the cases of a given disjunction in turn, with the goal in each to derive the same conclusion.

| A v B   Given [Premise, Assumption, or Derived]
|  -
|  |_ A   Assumption
|  |  :
|  |  C   Derived
|  -
|  |_ B   Assumption
|  |  :
|  |  C   Derived
|  -
|  C      v Elimination