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.
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)