Natural deduction, beginning premises

Question

For natural deduction. how do i go about picking how to start off my proof and is there any rules as to how i have to start off my proof. Do i have to individually prove each premise as that's not what the example below does.

${\color{red}{\text{Given $\color{blue}{\lnot A\lor B}$ and $\color{blue}A$, how do we derive $\color{blue}B$?}}\\\text{Here is a proof:}\\\qquad\dfrac{\lower{1.5ex}{\lnot A\lor B}\quad\dfrac{\dfrac{\dfrac{A\quad[\lnot A]^1}{\bot}{\small\lnot E}}{B}{\small\bot E}}{\lnot A\to B}{\small{\to}I^1}\quad\dfrac{[B]^2}{B\to B}{\small{\to}E^2}}{B}{\small\vee E}}\\~\\\therefore \lnot A\vee B, A\vdash B$

Answer 1

I don't know there's a single mechanic procedure for your general proof search question which is the holy grail of automated theorem proving. Natural deduction was originally outlined by Gentzen in 1935 and it's really close to our natural reasoning. But one of its drawback is the non-local nature of its proofs because usually the premise is far away from its conclusion like in your above tree (you don't need to prove any premise but they may not be immediately above your conclusion especially those discharged premises) or in Fitch style nested subproof branches, and you also need to skillfully introduce and discharge temporary premises like $\lnot A, B$ in your example. As a human we generally search proof from conclusion and sometimes deduce from premises and see if somehow they meet in between, and most times it easily works since most problems are man-made and not that hard by design. However, such heuristics is not guaranteed to always work regardless you're using natural deduction, Hilbert system or sequent calculi with cut elimination, thus prompts further research in category theory and type theory. Currently we're mainly analyzing and searching proof on a case by case basis when proving things manually. Maybe the easiest method for your example proof is turn your premise $\lnot A \lor B$ to a Horn clause $A \to B$ per the definition of material conditional logical connective, then together with another premise $A$ you just need one step of inference (modus ponens, $\to E$) to arrive at your desired conclusion $B$.

In automated proof search industry there're many different algos for different decidable problems such as the notorious SAT problem:

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula... SAT is the first problem that was proven to be NP-complete; see Cook–Levin theorem.

And in practice the most popular and efficient proof search inference rule of first order logic is resolution:

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the (complement of the) Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

For your example problem, if you try to use resolution to prove $(\lnot A \lor B) \land A \to B$, then you only need to prove the unsatisfiability of the CNF formula $(\lnot A \lor B) \land A \land \lnot B$ from truth table of the material conditional connective and clearly the 3 conjunct clauses easily resolved to empty {} and thus proves your original result.

Answer 2

Do i have to individually prove each premise as that's not what the example below does.

You never prove the premises. They are undischarged assumptions.

how do i go about picking how to start off my proof and is there any rules as to how i have to start off my proof.

You start by looking at what you were given: the premises, the desired conclusion, and the rules of inference.

In most Natural Deduction systems, the rules of inference are named by the logical connectives and whether they are being 'introduced' or 'eliminated'. So the first task is to identify what main connectives you have in the premises (with may need elimination) and conclusion (which may need introduction).

So here we have a disjunction and an atom in the premises, and an atom in the conclusion. So should we start with eliminating the disjunction, because ... well, that's all we have to work with.

The second task is to look up the relevant rule to see how it is implemented -- and find what you would need to complete it.   So now we look up the rule of disjunction elimination.   Different systems have their own implementations.   Yours seems to be based on having the disjunction and two conditionals.$$\dfrac{\lnot A\vee B\quad \lnot A\to B\quad B\to B}{B}{\vee E}$$

Well, the disjunction is a premise, and hopefully can derive the conditionals by, ah, what's the rule? Oh, yes that one; requiring deriving the consequent from the assumption of the antecedent.

One case is trivial. $B$ is obviously derivable from assumed $B$, so therefore $B\to B$ by conditional introduction.

The other case requires deriving $B$ from assumed $\lnot A$. We have a rule to eliminate that negation, but it requires also having $A$. Oh, that is the other premise! So we can apply negation introduction, which produces a contradiction; and we may eliminate that with 'contradiction elimination' (sometimes known as 'ex falso quodlibet' or 'explosion') to derive the required $B$. Then we will have deduced $\lnot A\to B$ by conditional introduction.

Putting it all together builds your proof tree.