Some standard kinds of proof systems include natural deductive systems, sequent systems, axiomatic systems, and so on. There are various approaches to each of these kinds of proof systems. The rules/axioms of these systems can be tailored to the specific needs of those who use/study them. Model theorists like to use semantic tableaux and axiomatic systems; proof theorists like to use sequent systems. Most people argue using some sort of natural deduction. These systems all coalesce into an interplay between the semantics and syntax of a logic $\mathcal L$. Some systems are sound and complete, and there are systems everywhere in-between.
A well-known axiomatization of Classical Logic with Modus Ponens as its inference rules is as follows:
P1. $\varphi \to (\psi \to \varphi)$
P2. $(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$
P3. $(\neg \psi \to \neg \varphi) \to (\varphi \to \psi)$
If one takes only P1 and P2, Positive Implicational Logic is achieved. However, an equivalent axiomatization puts things in a different light:
A1. $\varphi\to \neg\neg \varphi$
A2. $\neg \varphi \to (\varphi \to \psi)$
A3. $(\neg \varphi \to \varphi) \to (\psi \to \varphi)$
A4. $(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$
Here, the validity of adding an assumption (formalized by P1) is a consequence of a kind of “Modus Mirabilis”, which is formalized as A3, as opposed to being assumed. In natural deductive systems, P1 may be proven using the Deduction Theorem/Conditional Introduction.
I suppose my question is akin to “is math invented or discovered?” But, in this case, it is to be seen whether or not a logic is prior to its possible proof systems. Equivalently, I wonder whether or not proof systems/inference patterns are prior to logics.
As an aside, does anyone know whether the second axiomatization would be complete if A4 were replaced with Hypothetical Syllogism as an inference rule?
Best Answer
Both systems that you mention are systems that were meant to formalize classical propositional logic. And I would say that our ideas and concepts regarding this logic (every statements is either true or false ; the truth-value of any complex statement is a function of the truth-values of the smaller statements it comprises, together with the operators working as truth-functional operators as typically spelled out in the familiar truth-tables, etc.) came before we tried to formalize them. Indeed, it took a good bit of playing around with the axioms of these kinds of Hilbert-style axiomatic systems to try and make them complete with just a few axioms, i.e. we clearly knew what our goal was, and tried to make our formalization fit the bill. So at least in this narrow context, I would say the 'logic' came before the 'logic system'.
For your (small) question at the end:
I take this to mean the following system:
A1. $\varphi\to \neg\neg \varphi$
A2. $\neg \varphi \to (\varphi \to \psi)$
A3. $(\neg \varphi \to \varphi) \to (\psi \to \varphi)$
A4. $(\varphi \to \psi) \to ((\psi \to \chi) \to (\varphi \to \chi))$
No, that system is not complete. It cannot prove the original axiom A4, and here is why.
Suppose we are working with a 3-valued system where every variable and statement evaluates to either $0$, $1$, or $2$.
Suppose the $\neg$ operator works as follows:
\begin{array}{c|c} p&\neg p\\ \hline 0&1\\ 1&0\\ 2&2\\ \end{array}
And suppose the $\to$ operator works like this:
\begin{array}{cc|c} p&q&p\to q\\ \hline 0&0&0\\ 0&1&2\\ 0&2&2\\ 1&0&0\\ 1&1&0\\ 1&2&0\\ 2&0&0\\ 2&1&2\\ 2&2&0\\ \end{array}
Now let's evaluate each of the axioms:
\begin{array}{c|cccc} p& p & \to & \neg & \neg & p\\ \hline 0&0&\color{red}0&0&1&0\\ 1&1&\color{red}0&1&0&1\\ 2&2&\color{red}0&2&2&2\\ \end{array}
\begin{array}{cc|ccccc} p&q&\neg & p & \to & (p & \to & q)\\ \hline 0&0&1&0&\color{red}0&0&0&0\\ 0&1&1&0&\color{red}0&0&2&1\\ 0&2&1&0&\color{red}0&0&2&2\\ 1&0&0&1&\color{red}0&1&0&0\\ 1&1&0&1&\color{red}0&1&0&1\\ 1&2&0&1&\color{red}0&1&0&2\\ 2&0&2&2&\color{red}0&2&0&0\\ 2&1&2&2&\color{red}0&2&2&1\\ 2&2&2&2&\color{red}0&2&0&2\\ \end{array}
\begin{array}{cc|ccccccccc} p&q&(\neg & p & \to & \neg & q) & \to & (q & \to & p)\\ \hline 0&0&1&0&0&1&0&\color{red}0&0&0&0\\ 0&1&1&0&0&0&1&\color{red}0&1&0&0\\ 0&2&1&0&0&2&2&\color{red}0&2&0&0\\ 1&0&0&1&2&1&0&\color{red}0&0&2&1\\ 1&1&0&1&0&0&1&\color{red}0&1&0&1\\ 1&2&0&1&2&2&2&\color{red}0&2&2&1\\ 2&0&2&2&2&1&0&\color{red}0&0&2&2\\ 2&1&2&2&0&0&1&\color{red}0&1&0&2\\ 2&2&2&2&0&2&2&\color{red}0&2&0&2\\ \end{array}
OK, I skipped the axiom for $(\varphi \to \psi) \to ((\psi \to \chi) \to (\varphi \to \chi))$ since that table would be 27 lines long, but if you were to work that one out you'll find that, like these first three axioms, it always evaluates to $0$.
We can call such statements (that always evaluate to $0$) '$0$-tautologies'. That is, all axioms turn out to be $0$ -tautologies.
Moreover, notice from the table of $\to$, that the only time that $p\ to q$ has the value of $0$, and $p$ has the value of $0$, is when $q$ has the value of $0$ as well. This means that with Modus Ponens as our only inference rule (which is what is assumed here with all these Hilbert-style systems), you can only infer something that is a $0$-tautology from any other $0$-tautologies. And that means that in any proof in this system, every statement will have to be a $0$-tautology.
OK, but now let's take a look at the original axioms A4, which was $(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$. Is that a $0$-tautology? No, it is not. Consider the case where $p$ has the value of $2$, $q$ has the value of $0$, and $r$ has the value of $1$. Then $(p \to (q \to r)) \to ((p \to q) \to (q \to r))$ works out to $(2 \to (0 \to 1)) \to ((2 \to 0) \to (0 \to 1)) = (2 \to 2) \to (0 \to 2) = 0 \to 2 = 2$
This means that $(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$ is not a $0$-tautology, and hence cannot occur as any line in any proof within this system. But since $(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$ is a tautology in the classical 2-valued system (after all, it was used as an axiom in the original system), this system is incomplete.