With Conditional Proof You Never Need a Rule of Repetition

Suppose we have the rule of hypothesis introduction, conditional introduction, and conditional elimination. From just these rules of inference, in classical propositional calculus, we never need a rule of repetition, nor need CqCpq as an axiom. In other words, if those rules hold, then "q, p|-q" comes as a valid schema and CqCpq is a theorem.

1 | q hypothesis introduction
2 || p hypothesis introduction
3 ||| q hypothesis introduction
4 || Cqq 3-3 conditional introduction
5 || q 1, 4 conditional elimination
6 | Cpq 2-5 conditional introduction
7 CqCpq 1-6 conditional introduction.

Define a propositional form as follows:

1) Lower case letters, along with lower case letters subscripted with numbers a₁, b₂, c₁₃ are propositional forms.

2) If x and y are both propositional forms, then Cxy is a propositional form.

Let Cab denote the material conditional with 'a' and 'b' taking truth values in {T, F}. Let "C₁ ...C_n" denote a concatenation of n conditionals, and "a₁...a_(n+1)" a concatenation of (n+1) logical variables. E. G. C₁...C₃a₁...a₄ denotes CCCa₁a₂a₃a₄. Let a/b denote a substitution of variable "a" with "b", let a/Cab denote that we substitute variable "a" with Cab.

Axiom 1: CCpqCCqrCpr

Axiom 2: CqCpq

Theorem 1: CCCpqC₁...C_(10^100)a₁...a_((10^100)+1)CqC₁...C_(10^100)a₁...a_((10^100)+1)

Demonstration:

1 CCqCpqCCCpqC₁...C_(10^100)a₁...a_((10^100)+1)CqC₁...C_(10^100)
a₁...a_((10^100)+1) Axiom 1, p/q, q/Cpq, r/C₁...C_(10^100)a₁...a_((10^100)+1)

2 CCCpqC₁...C_(10^100)a₁...a_((10^100)+1)CqC₁...C_(10^100)a₁...a_((10^100)+1) Axiom 2, 1 detachment.

Is ApNp a Conjunctive Normal Form?

The notion of a conjunctive normal form first appears in Paul Bernays's second Habilitationsschrift [1] (doctoral thesis). In that text, Bernays established the completeness of propositional calculus [2]. On p. 38-39 of Formal Logic [3] Arthur Prior writes in the context of a completeness proof for propositional calculus:

"What they show [Hilbert and Ackermann] is that any formula of the propositional calculus is equivalent either (i) to a single propositional variable or the negation of one, or (ii) to an alternation of which all the members are either propositional variables or their negations, or alternations (or alternations of alternations, etc.) of such or (iii) to a conjunction of which all members are of the form listed under (i) and (ii), or conjunctions (or conjunctions of conjunctions, etc.) of such. We may describe all these forms as 'conjunctions of alternations of propositional-variables-or-their-negations', if (a) we call a form like 'KKpqr' a 'conjunction of p, q, and r' instead of calling it a 'conjunction of the-conjunction-of-p-and-q and r', and similarly with alternations, and (b) we regard a single propositional variable (or negation of one) as an alternation with a single alternant (it is as it were a limiting case of alternation; in any case such a variable is equivalent to the alternation of itself with itself-EpApp), and (c) we also regard a single propositional variable (or negation of one) as a conjunction with a single conjunct, and a single alternation as a conjunction-of-alternations with a single conjunct. The forms which would be 'conjunctions of alternations of propositional variables or their negations' would include such examples as

(i) p and Np (conjunctions-with-one-member of alternations-with-one-member).

(ii) ApNq (a conjunction-with-one-member of an alternation with two membes).

(iii) AApNqNp (a conjunction-with-one-member of an alternation with three members).

(iv) KpApq (a conjunction of an alternation-with-one-member and an alternation with two members).

(v) KApqApNq (a conjunction of two alternations-with-two-members).

(vi) KApAqrKApqApAst (a conjunction-with-three-members of an alternation-with-three-members, and an alternation-with-two-members, and another alternation-with-three-members.)

That every truth-functional formula can be 'put into normal form', i.e. shown to be equivalent to (i. e. to imply and be implied by) a formula of the above sort..."

So, for Prior, conditions (i), (ii), and (iii) in the first paragraph almost surely would define a "conjunctive normal form". This suggests that in the context of a (correct) proof of the completeness of propositional logic, that is, where the notion of a conjunctive normal form first got defined, ApNp is indeed a conjunctive normal form.

1 This information I retrieved http://books.google.com/books?id=1xEVkzuX5e0C&pg=PA501&lpg=PA501&dq=conjunctive+normal+form+bernays+Habilitationsschrift&source=bl&ots=DfCwTAO-wL&sig=rMok5p3XCMoGxQY8j-YEWLKCkes&hl=en&ei=GlZ2TpjNMoS6tgfu_6DSDA&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBsQ6AEwAA#v=onepage&q=conjunctive%20normal%20form%20bernays%20Habilitationsschrift&f=false on September 18, 2011.

2 This information I retrieved from http://www.encyclopedia.com/doc/1G2-2830905020.html on September 18, 2011.

3 Prior, Arthur. Formal Logic Oxford University Press 1962.