Proving a sequent is valid without a premise

Question

I'm having issues proving that a sequent is valid, without any premises given.

1. Prove $⊢ (p \to q) \lor (q \to r)$ by natural deduction.
2. Prove $⊢ \forall x \forall y P(x, y) \to \exists y \forall x P(x, y)$ by natural deduction.

I don't know where to begin with, as I normally use my premises in the first place. What's the general approach when encountering a sequent like theses ones?

Answer 1

Preliminary: in the derivations below, $[A]^i$ means that the formula $A$ has been discharged, the index $i$ shows where.

Concerning the first question, the formula $(p \to q) \lor (q \to p)$ is valid only in classical logic, not in intuitionistic logic. This means that, as suggested by Bram28, the proof of $(p \to q) \lor (q \to p)$ in natural deduction must use some inference rule (e.g. reductio ad absurdum) or equivalently some axiom (e.g. tertium non datur) valid only in classical logic. The following is a derivation in natural deduction of $(p \to q) \lor (q \to p)$ assuming the classical axiom tertium non datur $p \lor \lnot p$: $$ \dfrac{p \lor \lnot p \qquad \dfrac{\dfrac{[p]^1}{q \to p}\small{\to_{intro}}}{(p \to q) \lor (q \to p)}{\small\lor_{intro}} \qquad \dfrac{\dfrac{\dfrac{\dfrac{[\lnot p]^1 \qquad [p]^2}{\bot}\small{\lnot_{elim}}}{q}\small{\textit{efq}}}{p \to q}\small{\to_{intro} 2}}{(p \to q) \lor (q \to p)}\small{\lor_{intro}}}{(p \to q) \lor (q \to p)}\small{\lor_{elim} \ 1} $$

If you aren't allowed to use the law of tertium non datur as an axiom, then you can derive it using the rule of reductio ad absurdum as below, the derivation you are looking for being the composition of the two (plug the second derivation above $p \lor \lnot p$ in the first derivation). $$ \dfrac{\dfrac{[\lnot(p \lor \lnot p)]^1 \qquad \dfrac{\dfrac{\dfrac{[\lnot(p \lor \lnot p)]^1 \qquad \dfrac{[p]^2}{p \lor \lnot p}\small{\lor_{intro}}}{\bot}\small{\lnot_{elim}}}{\lnot p}\small{\lnot_{intro} \ 2}}{p \lor \lnot p}\small{\lor_{intro}}}{\bot}\small{\lnot_{elim}}}{p \lor \lnot p}\small{{raa} \ 1} $$

Concerning the second question, the idea is that you suppose that everyone is in relation with everyone, then in particular (since the domain in non-empty) there is someone in relation with everyone. The derivation in natural deduction of $\forall x \forall y P(x,y) \to \exists y \forall x P(x,y)$ is the following (valid both in classical and intuitionistic logic): $$ \dfrac{\dfrac{\dfrac{\dfrac{\dfrac{[\forall x\forall y P(x,y)]^1}{\forall y P(x,y)}\small{\forall_{elim}}}{P(x,y)}\small{\forall_{elim}}}{\forall x P(x,y)}\small{\forall_{intro}}}{\exists y \forall x P(x,y)}\small{\exists_{intro}}}{\forall x \forall y P(x,y) \to \exists y \forall x P(x,y)}\small{\to_{intro}1} $$

Answer 2

That depends on what rules you have in your proof system.

Do you have any rule that can infer something from nothing, e.g. $\vdash p \lor \neg p$?

If not, try a proof by contradiction, i.e. Assume the negation, and now you have something to work with ... if you get to a contradiction, you can reject the assumption, and thus obtain the desired statement.

For the second problem, since you need to prove a conditional, do a conditional proof: assume the antecedent (the 'if' part), and try to derive the consequent (the 'then' part) from that. Presumably you have a rule that can point to that, and conclude the conditional as a whole.