When reasoning about proofs, it's tempting to construct them as simply as possible:
- A sequence of lines where every line is an axiom or a deduction
Deductions should be very precise: "If a previous line looks like $[A] \implies [B]$ and a previous line looks like $[A]$, then conclude $[B]$". Ideally deductions should look like "if entire previous lines look like $x_1,\ldots, x_n$, then conclude $y$ where the $x_i$, $y$, have blanks as in the modus ponens example that can be filled in with any well-formed formula. Even more ideally, there would be only modus ponens as a deduction rule, and any other deduction rules just turned into axiom schemas.
There are a number of more practical approaches to formal proofs, such as Fitch-style, Gentzen-style, or presenting proofs in the form of trees. An axiomatization would have to work harder to compensate, for instance, for the lack of Fitch-style assumption-based implication introduction.
But are there texts or other sources that take some time to present this concept of a proof fully, with example proofs? Ideally including proofs in various first-order logics, with a complete presentation of the purely logical axioms necessary to add onto an axiomatization for the first order logic itself to be able to prove everything.
I'd like to be able to say, for instance, "here's everything you need to reason about the first-order logic of linear orderings", and it's just reflexivity, transitivity, anti-symmetry and trichotomy and a full list of first-order logic rules to actually make proofs.