Alternative Ways to Approach Propositional Calculus

There exist several ways to approach propositional calculus: axiomatically, through natural deduction, sequent calculi, semantic tableaux. An axiomatic presentation sometimes will start with a list of axioms, the rule of substitution, and the rule of conditional elimination (Co for "conditional out"). For example, one could start with the axiom set {CCpqCCqrCpr, CCNppp, CpCNpq} A1 or {CqCpq, CCpCqrCCpqCpr, CCNpNqCqp} A2. But, let's say we start another way.

Suppose we have the rules of conditional proof alon with substitution and conditional elimination. In other words, we have a rule which allows to introduce any propositional form as a hypothesis, so long as we keep track of its scope, and we have a rule of conditional introduction (Ci for "conditional in"). Suppose also, we don't want to use any axioms for propositional calculus. What sorts of rules of inference do we need?

Well, since the above axiom sets work as sufficient for propositional calculus, we could use the deduction metatheorem from CCNppp to obtain the rule of inference CNpp|-p. So, instead of using A1 we could use R3 {(Cpq, Cqr, p |-r), (CNpp|-p), (p, Np|-q)} along with just conditional elimination and substitution for propositional calculus. But, really, given the rules of conditional proof, we don't need all those rules as primitive rules. (Cpq, Cqr, p |-r) can get derived using just conditional proof as follows:

1 Cpq hypothesis
2 Cqr hypothesis
3 p hypothesis
4 q 3, 1 Co
5 r 4, 2 Co

We can also derive CqCpq, and CCpCqrCCpqCpr and using just conditional proof as follows:

1 | q hypothesis
2 || p hypothesis
3 ||| q hypothesis
4 || Cqq 3-3 Ci
5 || q 1, 4 Co
6 | Cpq 2-5 Ci
7 CqCpq 1-6 Ci

1 | CpCqr hypothesis
2 || Cpq hypothesis
3 ||| p hypothesis
4 ||| q 3, 2 Co
5 ||| Cqr 3, 1 Co
6 ||| r 4, 5 Co
7 || Cpr 3-6 Ci
8 | CCpqCpr 2-7 Ci
9 CCpCqrCCpqCpr 1-8 Ci

So, by the first proof instead of considering A1 with substitution and conditional elimination, we can consider {CCNppp, CpCNpq} N1 along with the rules of conditional proof, conditional elimination and substitution. By the second and third proofs instead of considering A2 we can consider N2 {CCNpNqCqp} along with the same rules which go along with N1. Now using the deduction metatheorem instead of considering N1 we can consider R1 {(CNpp|-p) R1a, (p, Np|-q) R1b} and R2 {(CNpNq, q |-p) MT}. A few weeks ago I took an old logic book and tried to prove certain theorems in both R1 and R2.

So, let's compare some proofs of Peirce's law CCCpqpp in R2 and R1 (of course more proofs exist, the following just give examples). In R1 a proof might go:

1 | CCpqp hypothesis
2 || Np hypothesis
3 ||| p hypothesis
4 ||| q 2, 3 R1b
5 || Cpq 3-4 Ci
6 || p 5, 1 Co
7 | CNpp 2-6 Ci
8 | p R1a
9 CCCpqpp 1-8 Ci

In R2 a proof might go:

1 | CCpqp hypothesis
2 || Np hypothesis
3 ||| p hypothesis
4 |||| Nq hypothesis
5 ||||| Np hypothesis
6 |||| CNpNp 5-5 Ci
7 |||| Np 2, 6 Co
8 ||| CNqNp 4-7 Ci
9 ||| q 3, 8 MT
10 || Cpq 2-9 Ci
11 || p 10, 1, Co
12 | CNpp 2-11 Ci
13 || Np hypothsis
14 ||| NNCNpp hypothesis
15 |||| NNNp hypothesis
16 ||||| Np hypothesis
17 |||| CNpNp 16-16 Ci
18 |||| Np 13, 17 Co
19 ||| CNNNpNp 15-18 Ci
20 ||| p 13, 12 Co
21 ||| NNp 20, 19 MT
22 || CNNCNppNNp 14-21 Ci
23 || NCNpp 13, 22 MT
24 | CNpNCNpp 13-23 Ci
25 | p 12, 24 MT
26 CCCpqpp 1-25 Ci

Let's also compare proofs of CNNpp and CpNNp. In R1 a proof for CNNpp might go:

1 | NNp hypothesis
2 || Np hypothesis
3 || p 1, 2 R1b
4 | CNpp 2-3 Ci
5 | p 4, R1a
6 CNNpp 1-5 Ci

In R2 a proof for CNNpp might go:

1 | NNp hypothesis
2 || Np hypothesis
3 ||| NNNNp hypothesis
4 |||| NNp hypothesis
5 ||| CNNpNNp 4-4 Ci
6 ||| NNp 1, 5 Co
7 || CNNNNpNNp 3-6 Ci
8 || NNNp 2, 7 MT
9 | CNpNNNp 2-8 Ci
10 | p 1, 9 MT
11 CNNpp 1-10 Ci.

For CpNNp in R1 we can have:

1 | p hypothesis
2 || Np hyopthesis
3 || NNNp 1, 2 R1b
4 | CNpNNNp 2-3 Ci
5 | NNp 4, R2b
6 CpNNp 1-5 Ci

For CpNNp in R2 we can have:

1 | p hypothesis
2 || NNNp hypothesis
3 ||| NNp hypothesis
4 |||| NNNNNp hypothesis
5 ||||| NNNp hypothesis
6 |||| CNNNpNNNp 5-5 Ci
7 |||| NNNp 2, 6 Co
8 ||| CNNNNNpNNNp 4-7 Ci
9 ||| NNNNp 3, 8 MT
10 || CNNpNNNNp 3-9 Ci
11 || Np 2, 10 MT
12 | CNNNpNp 2-11 Ci
13 | NNp 1, 12 MT
14 CpNNp 1-13 Ci.