How/where is this technique generalised and proven for other (standard, first order) logical operations (if possible)? A method of natural deduction.

Question

Logic is something I am entirely self-taught in. Due to my resulting ignorance, it is difficult for me to search for the right things. Therefore, please excuse me if this has been asked before.

The Details:

In this YouTube video by Attic Philosophy, an approach to doing natural deduction proofs is demonstrated but neither proven nor rigorously defined. (It is just an introduction.)

---

Essentially, one works backwards. The example given is a proof of

$$p\to (q\to r)\vdash (s\to p)\to(q\to(s\to r)).$$

We start by assuming $p\to (q\to r)$, leaving a big gap, then writing $(s\to p)\to(q\to(s\to r))$, like so:

$$\begin{array}{|lc} p\to (q\to r) & \\ \hline & \\ & \\ & \\ & \\ & \\ & \\ & \\ (s\to p)\to (q\to (s\to r)). & \end{array}$$

Then we assume the first bit of the conclusion and do the same thing as above, like so:

$$\begin{array}{|lc} p\to (q\to r) & \\ \hline \rlap{\begin{array}{|lc} s\to p & \\ \hline & \\ & \\ & \\ & \\ & \\ q\to (s\to r) & \end{array}}&\\ (s\to p)\to (q\to (s\to r)). & \end{array}$$

And again:

$$\begin{array}{|lc} p\to (q\to r) & \\ \hline \rlap{\begin{array}{|lc} s\to p & \\ \hline \rlap{\begin{array}{|lc} q & \\ \hline & \\ & \\ & \\ s\to r & \\ \end{array}}& \\ q\to (s\to r) & \end{array}}&\\ (s\to p)\to (q\to (s\to r)). & \end{array}$$

Once more:

$$\begin{array}{|lc} p\to (q\to r) & \\ \hline \rlap{\begin{array}{|lc} s\to p & \\ \hline \rlap{\begin{array}{|lc} q & \\ \hline \rlap{\begin{array}{|lc} s & \\ \hline & \\ & \\ r \end{array}}& \\ s\to r & \\ \end{array}}& \\ q\to (s\to r) & \end{array}}&\\ (s\to p)\to (q\to (s\to r)). & \end{array}$$

Now we fill in the gap using all the assumptions we like from above it, like so: because there's an $r$ in the first row, we can use modus ponens using $s$ and $s\to p$, which gives $p$, then again with $p$ and $p\to(q\to r)$ to get $q\to r$, from which we get $r$; this looks like:

$$\begin{array}{|lc} p\to (q\to r) & \\ \hline \rlap{\begin{array}{|lc} s\to p & \\ \hline \rlap{\begin{array}{|lc} q & \\ \hline \rlap{\begin{array}{|lc} s & \\ \hline p & \\ q\to r & \\ r \end{array}}& \\ s\to r & \\ \end{array}}& \\ q\to (s\to r) & \end{array}}&\\ (s\to p)\to (q\to (s\to r)). & \end{array}$$

The Question:

How/where is this technique generalised and proven for other (standard, first order) logical operations (if possible)?

Context:

I am familiar with the method of analytic tableaux.

To get an idea of my capabilities, see this question of mine:

An alternative, formal proof that $(\lnot\forall xPx)\to(\exists y(\lnot Py)).$

Answer 1

Your strategy of proving a conditional by assuming the antecedent and trying to get to the consequent (i.e. doping a conditional proof) is an excellent strategy. And there are other strategies:

• If you want to prove $\neg \phi$, try to do a proof by contradiction: assume $\phi$, and see if you can get to a contradiction

• If you want to prove $\phi \land \psi$, try and prove $\phi$ and $\psi$ individually

• If you want to prove $\phi \lor \psi$, try one of the following 3 methods:

1. Maybe there is a fairly easy way to get to $\phi$ or $\psi$ by themselves (unlikely to happen if this is the overall goal of a human-constructed logic problem, but often occurs within a subproof)

2. See if among the statements that you have you have some other disjunction, e.g. $\chi \lor \lambda$, and set up a proof by cases on that one (oftentimes, one of $\chi$ or $\lambda$ will lead to $\phi$, and the other to $\psi$)

3. Try a proof by contradiction: Assuming $\neg (\phi \lor \psi)$, you can go through a set pattern get both $\neg \phi$ and $\neg \psi$ and you may be well on your way to the contradiction you want.

Etc.

In fact, I could lay out a set of rules that, when followed in a certain order as an algorithm, systematically crank out formal proofs for any valid argument, whether in propositional logic or full first-order logic.

However, in order for such an algorithm to be guaranteed to always find a proof there is a cost: the proof it comes up with isn't always the most efficient .. sometimes far from it!

Simple example. Suppose I have two premises, $P$ and $P \to (Q \to (R \to (S \to T)))$, and my goal is $Q \to (R \to (S \to T))$. Strictly following the strategy of proving any conditional using conditional proofs, you'd create a bunch of nested subproofs, but it's obvious that in this case that is not needed at all.

So, in practice, a 'master' of formal proofs will see all of these strategies as heuristics: something that often works nicely, but that isn't always the fastest or most elegant. And it is experience that will tell them what will work well in what situation.