I'm currently learning Ebbinghaus et. al.'s propositional calculus in their book Mathematical Logic, and I'm trying to derive the very basic rules of inference such as $\land$ introduction, the law of excluded middle, and others. But these proofs are to me at the moment excessively contrived and unintuitive, and I was wondering if anyone has tips on how one is supposed to know the general direction in which to orient proofs when dealing with very few inference rules, or if there is any method to the madness. The current set of rules available to me are in the appendix of this post, but I can very well imagine that in a different text, a different set of initial rules would be available, so I'm wondering if there is usually a method for deriving the very first derivable rules when encountering a new system. For example, I spent a whole lot of time on getting $\land$ introduction and basically stumbled upon the correct proof by luck through trial and error: (and note, contraposition is itself a derived rule)
For $\land$ introduction:
$Γ\vdash A$ (premise)
$Γ\vdash B$ (premise)
$Γ \ \neg C \vdash A$ (assumption rule, we're free to assume anything we want)
$Γ \ \neg C \vdash B$ (again)
$Γ \ \neg A \vdash C$ (contraposition)
$Γ \ \neg B \vdash C$ (contraposition)
$Γ \ (\neg A\lor \neg B) \vdash C$ ($\lor$ introduction in the antecedent)
$Γ \ \neg C \vdash \neg(\neg A\lor\neg B)$ (contraposition)
Then, we redo the whole thing assuming $C$ instead of $\neg C$:
$Γ\vdash A$
$Γ\vdash B$
$Γ \ C \vdash A$
$Γ \ C \vdash B$
$Γ \ \neg A \vdash \neg C$
$Γ \ \neg B \vdash \neg C$
$Γ \ (\neg A\lor \neg B) \vdash \neg C$
$Γ \ C \vdash \neg(\neg A\lor\neg B)$
This establishes the proposition $A, B \vdash A \land B$ using proof by cases, but to me as a beginner, this was excessively difficult and blind luck. The proofs the authors themselves give for other basic derivable rules (excluded middle, contraposition, explosion, chain syllogism, disjunctive syllogism, substitution, transitivity) are similarly completely magical to me, but once these are established, I'm fine. Is there some sort of more general method to know how to progress forward in these types of proofs with very few available inference rules? I imagine logicians often encounter different sets of basic inference rules from which they have to derive the usual ones, but how do they know how to orient proofs towards the goal in each new system, specifically when very few rules are available? Any tips, advice or readings are very appreciated!
Appendix
The set of basic rules currently available to me
Credits to user S.C. for helping me finish the $\land$ introduction proof here: Undo a weakened statement in sequent calculus later in the inferences
Best Answer
In proof theory, a proof system as the one presented in Ebbinghaus at al.'s book must find a balance between at least two features:
It should be handy to use to derive valid formulas; let us call this feature object manageability.
It should be handy to use to derive properties of the proof system itself and its derivations; let us call this feature meta-manageability.
Unfortunately, the two features may be in conflict with each other. The following is a schematic and slightly superficial representation of the issue, but it is helpful to give you an idea.
On the one side, object manageability would tend to add as many inference rules as possible. Indeed, if we can choose among many inference rules, such as $\land$ introduction, excluded middle, contraposition, explosion, chain syllogism, disjunctive syllogism, substitution, transitivity, etc., we have many tools to find a formal derivation of a valid formula $A$, and likely this derivation would be a natural formalization of our intuitive way to prove $A$. The more rules the proof system has, the handier the proof system is to find a derivation of a valid formula.
On the other side, meta-manageability would tend to add as few inference rules as possible. Indeed, when you want to prove a property of the proof system, if the proof system is made of few rules then it is easier to check such a property. For instance, a typical desired property of a proof system is soundness: the proof system can derive only valid formulas (tautologies, in propositional logic). To prove soundness, you essentially have to show that validity is preserved by each inference rule of the proof system: for each inference rule, if its premises are valid formulas, then its conclusion is also a valid formula too. Of course, the proof of soundness is easier if there are few inference rules to check.
How can we find a synthesis between object manageability and meta-manageability? A possible balance is given by the approach somehow followed by Ebbinghaus too.
First, let us fix our proof system as small as possible, in the sense that it contains as few inference rules as possible (anyway, the proof system cannot be minimized too much because it has to be complete, i.e. strong enough to be able to derive all valid formulas). These rules may seem clumsy to use, never mind, the important thing is that they are few in number. This way, meta-manageability is assured. Let us call these inference rules the core rules. In Ebbanghaus's proof system, the core rules are Ass, Ant, PC, Ctr, $\lor$A, $\lor$S.
Second, to ensure object manageability, let us prove that many other inference rules are derivable in the proof system. An inference rule with premises $P_1, \dots, P_n$ and conclusion $C$ is derivable if there is a derivation with hypotheses $P_1, \dots, P_n$ and conclusion $C$ that only uses the core rules of the proof system. These derivable rules such as $\land$ introduction, excluded middle, contraposition, explosion, chain syllogism, disjunctive syllogism, substitution, transitivity, etc., make the task of finding a derivation for a valid formula much easier, in the sense they are closer to our intuitive reasoning. But each of them is just a "macro" for a chain of core rules. You can freely use the derivable rules to derive a valid formula, but the properties of the proof system are "encapsulated" in the core rules.
For practical purposes, there is not a definitive answer to the question "How to approach the proof that an inference rule is derivable?", given a set of core inference rules. In particular, this is true for the core rules of Ebbinghaus' proof system, which are really clumsy (in the "First digression" section here you can find a brief discussion). Being able to use the given inference rules in a smart way, is a matter of practice. In general, the absence of a definitive answer to your question is the reason why proving something is a difficult task!
Since Ebbinghaus' core rules are really clumsy, my suggestion is the following: as soon as you want to use an inference scheme that seems to be natural and general enough, check if it derivable. In this way, in your next derivations you can use this derivable inference rule instead of a clumsy chain of core rules. For instance, are you able to prove that the following (and very handy) inference rule is derivable in Ebbinghaus' system?
\begin{align} \Gamma \vdash A \\ \Gamma, \, A \vdash B \\ \hline \Gamma \vdash B \end{align}