Tautological implication (Makinson 1.1a)
We say that one formula tautologically implies another iff there is no assignment of truth values to propositional letters upon which the first formula comes out true and the second comes out false.
So writes Makinson in Topics in Modern Logic, p. 2. This definition seems to coincide with our normal idea of model-theoretic consequence: q is a model-theoretic consequence of p iff in all models where p is true, q is true as well. The only difference is that Makinson is dealing with propositional logic at this stage, so he talks about assignments of truth-values instead of models. In other words, his tautological entailment coincides with what we would symbolize as \(\models\).
So far so good. But then he starts talking about axiomatizing this relation with axiom schemata such as \[\alpha \wedge\ \beta \rightarrow \alpha\] \[\neg \neg \alpha \rightarrow \alpha\] where \(\rightarrow\) is not the conditional, but tautological implication. Which just seems to be wildly confused. You can't have axiom schemata of the form \[\neg \neg\ \alpha\ \models \alpha\] because axioms are meant to be purely proof-theoretic, and \(\models\) is a model-theoretic notion.
So there are two questions here: How did this confusion arise in the first place, and how are we meant to interpret these axioms sensibly?
How did this confusion arise in the first place?
This seems very similar to another confusion in Kleene: http://math.stackexchange.com/questions/577072/virtues-of-presentation-of-fo-logic-in-kleenes-mathematical-logic/577175#577175. In this case, Kleene mixes up
a Hilbert-style axiomatic proof system with an overlay of derived rules which look rather natural-deduction-like...the way he presents FOL perhaps reflects a transitional stage in our understanding of the relations between different types of logical theory.
So I think something similar is going on here, except with proof-theoretic and model-theoretic ideas: where Kleene mixes up Hilbert and Gentzen, Makinson mixes up proof theory and model theory.
How are we to interpret this sensibly?
Makinson also gives us a few derivation rules with his axiom system, for example
\[\textrm{From } \alpha \rightarrow \beta \textrm{ and } \beta \rightarrow \gamma \textrm{ to } \alpha \rightarrow \gamma\]
So it seems like we can charitably take Makinson to be presenting a Hilbert-Gentzen mashup like Kleene. So I suggest we take all of the axiom schemas to be of the form \(\Gamma \supset \beta\) whenever he writes \(\Gamma \rightarrow \beta\). And we can take his derivation rules to be of the form \(\frac {\alpha \quad \beta}{\gamma}\), such that the above rule turns out to be \[\frac {\alpha\rightarrow\beta\quad\beta\rightarrow\gamma}{\alpha\rightarrow\gamma}\]
Alternatively, we can take all axioms to be derivation rules as well, but...well, that's on my to do list - take an axiom system, change all schemas to natural deduction inferential rules, and see what happens. I think it should still be sound and complete, but I should see what else changes. (I remember discussing this with my logic lecturer, and he said that it was similar to something Gentzen did, but that he had forgotten the exact details.)