Give a proof of $\forall x Fx \lor \forall x Gx \vdash \forall x (Fx \lor Gx)$

Question

Give a proof of: $$\forall x Fx \lor \forall x Gx \vdash \forall x (Fx \lor Gx)$$

I don't know how to proof, but here is my attempt.

1 1) $\forall x Fx \lor \forall xGx \quad$ P

2 2) $\forall xFx \quad$ P

2 3) $Fa \quad$ 2,UI

4 4) $\forall xGx \quad$ P

4 5) $Ga \quad$ 4,UI

1 6) $Fa \lor Ga \quad$ 1,3,5 SL

1 7) $\forall x(Fx \lor Gx) \quad$ 6,UG

The rules used can be found in the following links:

• Predicate logic rules
• Chellas Rules

Answer 1

You want to use a disjunctive premiss $A \lor B$ to prove a conclusion $C$. The trick is temporarily to assume $A$ and derive $C$, then to start over, temporarily to assume $B$ and derive $C$; then we can say, either way we have $C$. This informal reasoning is captured by the propositional calculus rule of disjunction elimination, which has the following schematic pattern:

$A \lor B\\ \quad | \quad A\\ \quad | \quad \ldots\\ \quad | \quad C\\ \quad /\\ \quad | \quad B\\ \quad | \quad \ldots\\ \quad | \quad C\\ C $

Filling in that template in the present case, a canonical natural deduction proof would go:

$(\forall xFx \lor \forall xGx) \quad\quad\quad\textrm{Premiss}\\ \quad | \quad \forall xFx \quad\quad\quad\quad\ \ \textrm{Temporary assumption}\\ \quad | \quad Fa\quad\quad\quad\quad\quad\ \ \textrm{Instantiate universal quantifier}\\ \quad | \quad (Fa \lor Ga) \quad\quad\ \ \textrm{Propositional calc}\\ \quad | \quad \forall x(Fx \lor Gx)\quad\ \ \textrm{Universal quantifier introduction}\\ \quad /\\ \quad | \quad \forall xGx\quad\quad\quad\quad\ \ \textrm{New temporary assumption}\\ \quad | \quad Ga\quad\quad\quad\quad\quad\ \ \textrm{Instantiate universal quantifier}\\ \quad | \quad (Fa \lor Ga) \quad\quad\ \ \textrm{Propositional calc}\\ \quad | \quad \forall x(Fx \lor Gx)\quad\ \ \textrm{Universal quantifier introduction}\\ \forall x(Fx \lor Gx) \quad \quad\quad\ \ \textrm{Using initial premiss, and discharging the two temp. assumptions} $

NB, both subproofs have to end with the target conclusion -- compare your attempted proof which goes wrong in that respect.

Answer 2

Use a tableau. They're often suggestive of where to go in these proofs. You start with the negation of your original formula and apply a series of simple rules which hunt for a contradiction. Look:

Can you see how your proof is related? Work backward from the $\otimes$s. I know this is very indirect but tableaux are useful tools for many problems in predicate calculus.

I hope that helps.

Answer 3

For an informal proof, yours is quite fine. Essentially, you've just left out a number of steps. Judging from the links given, you do this by appealing to $\rm SL$, which is probably short for "Sentential Logic". This abbreviates a bunch of lines which would use $\rm ADD$, $\rm DIL$ and $\rm PC$ from the "Chellas" file.

Depending on how much experience you have with propositional (= sentential) logic, this may or may not be a good idea.

In any case, there is absolutely nothing wrong with the logic of your proof (contrary to what others have said). If the use of the $\rm SL$ shorthand is admissible, I'd even go as far as saying that your derivation is the canonical, intended solution to the problem. Cheers!

---

Added: The objection you received from some of the other users indicates that you should be careful with your use of $\rm SL$. It is probably a good idea to briefly note what each invocation of it amounts to. But then, this is all up to personal taste. Some people dislike abbreviating anything. Others, like me, appreciate the efficiency of using $\rm SL$ in a broad fashion, so as to save time -- particularly when you have access to the completeness result for truth tables and natural deduction.