Collecting different rules for Natural Deduction

[honestrosewater]

I'm only interested in the inference rules. I've read that people use different sets of rules, and I'm trying to find all of those different sets. Here's the ones I have so far (read "/" as a line break):
1. Modus Ponens (M.P.)
2. Modus Tollens (M.T.)
3. Hypothetical Syllogism (H.S.): p -> q / q -> r / ∴ p -> r.
4. Disjunctive Syllogism (D.S.): p V q / ~p / ∴ q.
5. Constructive Dilemma (C.D.): (p -> q) & (r -> s) / p V r / ∴ q V s.
6. Absorption (Abs.): p -> q / ∴ p -> (p & q).
7. Simplification (Simp.): p & q / ∴ p.
8. Conjunction (Conj.): p / q / ∴ p & q.
9. Addition (Add.): p / ∴ p V q.
(1-9) is a complete set. I've found a set differing from (1-9) only by replacing (6) with
6b. Destructive Dilemma (D.D.): (p -> q) & (r -> s) / ~q V ~s / ∴ ~p V ~r.
Does anyone know of any more?

 

[Owen Holden]

I'm only interested in the inference rules. I've read that people use different sets of rules, and I'm trying to find all of those different sets. Here's the ones I have so far (read "/" as a line break):
1. Modus Ponens (M.P.)
2. Modus Tollens (M.T.)
3. Hypothetical Syllogism (H.S.): p -> q / q -> r / ∴ p -> r.
4. Disjunctive Syllogism (D.S.): p V q / ~p / ∴ q.
5. Constructive Dilemma (C.D.): (p -> q) & (r -> s) / p V r / ∴ q V s.
6. Absorption (Abs.): p -> q / ∴ p -> (p & q).
7. Simplification (Simp.): p & q / ∴ p.
8. Conjunction (Conj.): p / q / ∴ p & q.
9. Addition (Add.): p / ∴ p V q.
(1-9) is a complete set. I've found a set differing from (1-9) only by replacing (6) with
6b. Destructive Dilemma (D.D.): (p -> q) & (r -> s) / ~q V ~s / ∴ ~p V ~r.
Does anyone know of any more?

imo, rules of inference are implicative tautologies in use.

What does the square mean here?

Russell and Whitehead claim they used Modus Ponens as the only rule of inference in Principia Mathematica.

 

[honestrosewater]

What does the square mean here?

Sorry, it's supposed to be "therefore"- I guess I'll just use ".:". I'm trying to find a code that works for everyone.

Russell and Whitehead claim they used Modus Ponens as the only rule of inference in Principia Mathematica.

Well, that's great but a little too insane for my tastes. Have you seen PM? ;)

 

[Owen Holden]

Sorry, it's supposed to be "therefore"- I guess I'll just use ".:". I'm trying to find a code that works for everyone.
Well, that's great but a little too insane for my tastes. Have you seen PM? ;)

The assertion sign '|-' is often used to say that such and such is deducible,
e.g. |- (p & (p -> q)) -> q, or |-(p) & |-(p -> q) -> |-(q), etc.

Yes, I have a copy of the paperback PM.