Good book for learning and practising axiomatic logic
Are you looking for a book on Hilbert axiomatic systems in particular, or just a book on proof theory more generally? There are many different kinds of proof systems, apart from the axiomatic Hilbert-style systems. In particular, proof theory benefits most from the sequent calculus presentation. If you're only interested in Hilbert systems, then I don't know of any resources that focus exclusively on that. If you're just interested in proof theory, there's an array of books that would suit most of your needs.
The thing about proof theory books is that, most of the time, they focus mostly on two logics: classical and intuitionistic. Those, it seems, have been the most influential in developing the course of proof theory. Still, to understand proof theory for other logics, you need to understand some of the basics for proof theory in classical and intuitionistic logic first. Negri and von Plato's Structural Proof Theory is a good place to start. Takeuti's Proof Theory develops proof theory from a different angle, focusing on arithmetic and consistency proofs. For something a little faster paced, look at Troelstra and Schwichtenberg's Basic Proof Theory. All of these are written post-2000.
If you've got some understanding of sequent calculi, then the book you're looking for is definitely Greg Restall's An Introduction to Substructural Logics. This is a fantastic book (one of my favorites actually), and I keep going back to it again and again. Only the first 7 chapters talk about proof theory, but he talks about proof systems with fewer connectives, nonclassical proof systems, modal proof systems, etc., and gives plenty of good examples. The cool thing about the substructural viewpoint is that it's an amazingly elegant way to characterize a lot of nonclassical and many-valued logics in one fell swoop. Again though, to fully appreciate it, you should be sure you know some sequent calculus before reading this book.
I've started studying L. H. Hackstaff's 1966 book Systems of Formal Logic. It looks useful for this purpose and seems to have fundamentally sound advice. Its systems don't have a rule of simultaneous substitution as a primitive rule of inference or involve axiom schema. If more systems did this it might actually make it possible to teach the axiomatic method in logic at a lower level than presently done.
It has sections on the axiomatic method which says things like:
- Know (the major ones/some of the major ones) the derivable rules of inference of the logical systems by heart.
- Know the axioms of the logical system by heart. Otherwise you'll have to refer to the axioms constantly when trying to construct a proof.
- Know the rules of inference by heart.
- Know the problem.
- Know the evidence.
Unlike many other books I have seen it also has plenty of examples axiomatic proofs (with the abbreviations for wffs adopted by the text).
As an example of how to prove something using just one variable at a time substitution. Suppose our first thesis is that of suffixing or reverse hypothetical syllogism.
Our language here has only has variables {a, b, c, ..., f} and subscripted variables if necessary. Our meta-language will happen with {p, ..., z} so we can talk about rules of inference.
1 C Cab C Cca Ccb
If we used condensed detachment would tell us that the next most general result of this system will be C CdCab C d C Cca Ccb. Can we prove this using only single variable at a time substitution and detachment?
1 has form Cxy, and so does Cab. So, since we only have one thesis, it seems to try to make or find some form of CCabCCcaCcb such that we can detach something. How might we do this? Well the antecedent of 1 is Cab and the antecedent of Cab is a. So, we need to substitute something for a such that a has form Cxy. Would Cab work?
2? C CCabb C CcCab Ccb.
We want to have "b" in one have the form CCcaCcb. But, the rule of uniform substitution happen tells us we have to substitute for all propositional variables. So, now if we used 2 to substitute something, we'd have to substitute the b in the first Cab. But, then we'd have to make even more substitutions. Do we have a simpler path possible here?
Well, maybe we could adopt a procedural technique to vary substitutions such that when substituting for variables, more variables appear than in the original wff. So, let's try substituting a with Cad in 1. Then we obtain 2:
2 C CCadb C CcCad Ccb.
Now we want to have some form of 1 become the antecedent. So we want something like CCbaCbd. Oops, I didn't follow my own technique. I mean 2 b/CCeaCed yields 3
3 C CCadCCeaCed C CcCad CcCCeaCed *
Now we want CCabCCcaCcb to match 3 (this exercise, surprising to me, I find kind of hard, because I know the form CCqrCCpqCpr by heart, but CCabCCcaCcb I don't know by heart). So, 1 b/d yields
4 CCadCCcaCcd
Now 4 c/e yields 5
5 C Cad C Cea Cea
Now we can detach 6 from 3 and 5:
6 C CcCad C c C Cea Ced We want the following:
G C CdCab C d C Cca Ccb
So, 6 c/d yields
7? C CdCad C d C Cea Cdb
No, that won't work since substitutions have to happen uniformly. b does not appear in 6. So, if we substitute d for b first, we can still apply substitutions later. So, 6 d/b yields
7 C CcCab C c C Cea Ceb Now 7 c/d yields
8 C CdCab C d C Cea Ceb Now 8 e/c yields
9 C CdCab C d C Cca Ccb
This proof isn't unique since I might have made other substitutions first. Let's look at 3 again:
3 C CCadCCeaCed C CcCad CcCCeaCed
The Detachment Theorem gives us a tip or hint that this from a wff of the type CCadCCeaCed, another wff of the type CcCad, we may infer CcCeaCed. Do we have a more general rule? Let's back up to 1
1 C Cab C Cca Ccb
But this time let's substitute b with CCeaCed first. We then obtain
10 C CaCCeaCed C Cca CcCCeaCed.
Along with The Detachment Theorem this gives us a clue about more general rules of inference than 3 would. So, we have
CpCCqpCqr => CC s p C s CCqpCqr (s does not appear on the left-side of the statement of the rule)
CpCCqpCqr, Csp => CsCCqpCpr
CpCCqpCqr, Csp, s => CCqpCpr
CpCCqpCqr, Csp, s, Cqp => Cpr and
CpCCqpCqr, Csp, s, Cqp, p => r