How do we derive new inference rules? I've been toying with a system of inference rules for propositional logic. I can use the system to prove theorems; but my question is, can I use the system to obtain new inference rules?
Here are the details. We begin with 5 inference rules, and 0 axioms.
(1) Proof by contradiction. We can open a proof/subproof by assuming $\neg A$. If we obtain a contradiction, we may close the proof/subproof and deduce $A$.
(2) Double Negation Elimination. $$\neg\neg A \vdash A$$
(3) Conjunction Elimination. $$A \wedge B \vdash A,\quad A \wedge B \vdash B$$
(4) De Morgan's Principles.
$$\neg(A \wedge B) \vdash \neg A \vee \neg B,\quad \neg(A \vee B) \vdash \neg A \wedge \neg B$$
(5) [Don't Know What To Call This]
$$(\neg A \vee \neg B), A \vdash \neg B,\quad (\neg A \vee \neg B), B \vdash \neg A$$
Now it seems to me that I can prove a lot using just these rules; I'm guessing the logic is complete. For a simple example, lets prove $\neg(A \wedge B) \vee (B \wedge A).$ Assume not.
Then by De Morgan, we get $\neg\neg(A \wedge B) \wedge \neg(B \wedge A)$.
Using both versions of rule (3), we obtain


*

*$\neg\neg(A \wedge B)$

*$\neg(B \wedge A)$


which (by 2) becomes


*

*$A \wedge B$

*$\neg(B \wedge A)$


which using both versions of rule (3) again, becomes


*

*$A$

*$B$

*$\neg(B \wedge A)$


which (thank you for the correction, Doug) becomes 


*

*$A$

*$B$

*$\neg B \vee \neg A.$


Finally, using rule (5), from $B$ and $\neg B \vee \neg A$ we deduce $\neg A$.
Since both $A$ and $\neg A$ are written down, we're done!
Okay, so we've proved the theorem $\neg(A \wedge B) \vee (B \wedge A).$ But, I'd like to view this as a new rule of inference rather than a theorem. Am I allowed to deduce that $A \wedge B \vdash B \wedge A$ is an admissible rule of inference? In general, how does one deduce a new rule of inference?
For instance, is it a general principle that if we have a theorem of the general form $\neg \Gamma \vee \Delta$, then it follows that $\Gamma \vdash \Delta$ is an admissible rule of inference?
Is the converse true?
Similarly, suppose we want to demonstrate that a rule of the form $\Gamma, \Gamma' \vdash \Delta$ is admissible. Is it sufficient to begin the game with $\Gamma$ and $\Gamma'$ written down, and deduce $\Delta$? If so, why? I'm having difficulty organizing my thoughts on the issue.
 A: What new rule of inference would this be?  What would such a rule say you could infer from (¬(A∧B)∨(B∧A))?  Yes, you can get rules of inference via writing proofs.  For your case you would show that from (A∧B) you can deduce (B∧A) for your system (but you can't discharge a supposition like you did in your proof... proof-by-contradiction discharges the supposition).  Then you would have (A∧B)⊢(B∧A) as a derived rule of inference.
And yes you can have multiple things on the left.  You already have two such rules here, rules covered by (5).  But, I guess you wanted to see at least three things on the left to convince you of this.  Let's say our only rules of inference are detachment (basically modus ponens) and substitution for variables and our axioms (in Polish notation) are the following theses:
1) CCqrCCpqCCrsCps Sorites
2) CCpCqrCCpqCpr Frege
1 q/CpCqr, r/CCpqCpr * C2-3 
(n x/Czy means x is substituted with Czy in the formula with numeral n, Ca-b indicates that thesis n is the antecedent of the formula after we've made the substitutions in the n formula, it has consequent b, and thus we detach thesis b)
3 CCpCpCqrCCCCpqCprsCps
From thesis 3 and detachment it follows that "CpCpCqr, CCCpqCprs, p⊢s" is a derivable rule of inference.  We can demonstrate that as follows:
1 CpCpCqr assumption
2 CCCpqCprs assumption
3 p assumption

4 CCCCpqCprsCps thesis 3, 1 detachment
5 Cps 4, 2 detachment
6 s 5, 3 detachment
Also, if you look at the justification for "CpCpCqr, CCCpqCprs, p⊢s" as a derivable rule of inference, you can find other derivable rules of inference also.  I'll clarify this if you like.
If you have a Deduction (meta) Theorem for your system, or a rule of conditional introduction, you can get another rule of inference R' from any rule of inference R which has multiple premises by applying the rule of conditional introduction/the theory's Deduction Theorem.  For example, with "CpCpCqr, CCCpqCprs, p⊢s" supposing we had a deduction theorem or a rule of conditional introduction, we might infer "CpCpCqr, CCCpqCprs⊢Cps" as a rule of inference.
Now, I did say "supposing" there.  The system {CCqrCCpqCCrsCps, CCpCqrCCpqCpr} under detachment and substitution doesn't actually have a conditional-in rule or a Deduction Theorem.  But, we can still get that second rule.  One half of what some authors call the Deduction Theorem, or what I'd call The Detachment Theorem says this:
For any propositions $\alpha$, $\beta$ "If C$\alpha$$\beta$ holds, if $\alpha$ also, then $\beta$ holds also." (this isn't quite like detachment which says "from C$\alpha$$\beta$, as well as $\alpha$, we may infer $\beta$ we use detachment to justify The Detachment Theorem, but not conversely.")  The upshot comes as that with a set of premises $\gamma$, from $\gamma$ $\vdash$Cpq we may infer ($\gamma$ U {p}) $\vdash$ q.  Or in other symbolism we might write 
"from $\alpha$, ..., $\omega$ $\vdash$ Cpq, we may infer $\alpha$, ..., $\omega$, p $\vdash$ q."
So, since we derived CCpCpCqrCCCCpqCprsCps we have $\vdash$CCpCpCqrCCCCpqCprsCps.  Thus, as rules of inference we can derive using the Detachment Theorem:
1: CpCpCqr $\vdash$ CCCCpqCprsCps.  From 1 and the Detachment Theorem we can derive
2: CpCpCqr, CCCpqCprs $\vdash$ Cps.  From 2 and the Detachment Theorem we can derive
3: CpCpCqr, CCCpqCprs, p $\vdash$ s.
If we wanted to justify each of those rules without The Detachment Theorem in one proof we might write the following:
1 CCpCpCqrCCCCpqCprsCps  by the derivation above
2 $\alpha$ CpCpCqr  assumption
3 $\alpha$ CCCCpqCprsCps 2, 1 detachment (thus rule 1 above)
4 $\alpha$$\beta$ CCCpqCprs assumption
5 $\alpha$$\beta$ Cps 3, 4 detachment (thus rule 2 above)
6 $\alpha$$\beta$$\gamma$ p assumption
7 $\alpha$$\beta$$\gamma$ s 6, 7 detachment (thus rule 3 above) 
A: You wrote:  "[Don't Know What To Call This] (¬A∨¬B),A⊢¬B,(¬A∨¬B),B⊢¬A "
The answer is not found ONLY using natural deduction rules.  There are in fact more rules of inference than that.  The one in particular you did not know the name of is and has been named "Disjunctive Syllogism".
It goes like this, for example: 1. either you are a republican or a democrat.  (r or d).
                                2. You are not a democrat.                      (not d).
                                Therefore you are republican.               (Therefore r.)
(This of course is provided there are ONLY two alternatives, which the context above is more than 2 alternatives).  The argument form above is valid for all disjunctions. Valid does not mean the statement is true.  Soundness deals with truth!  The example case above is clearly NOT SOUND however. The valid form for disjunctive syllogism is (p v q), deny exactly one disjunct; therefore you conclude the one possibility left over.  This also goes by the name "process of elimination". 
If you think of the example above you will see a fallacy: the fallacy of bifurcation.  The reason it is a fallacy is NOT a formal case; it has to do with content of the proposition.  Bifurcation is a content error because more than two alternatives exist than given; perhaps someone is trying to bully you or trying to persaude you of what they want instead of you choosing from all possible alternatives available.  If you use an absolute case with exactly two alternatives (with no possibility of a third, a fourth, etc.) then all resoning with disjunctive syllogism form is sound; all sound arguments are and MUST be valid.  It is up to the user of the argument to know what he or she is doing than to blindly and literally follow rules.  
