Formula of the Day: CδCpqδANpq.

"δ" in opposition to representing a propositional variable indicates a functorial variable of arity one.  In other words, it stands for any of the unary functions presumed.  Given the context of classical logic this means it stands for any of the functions belonging to {F, N, I, V} where F(0)=0, F(1)=0, N(0)=1, N(1)=0, I(0)=0, I(1)=1, V(0)=1, V(1).  Thus we can check that CδCpqδANpq constitutes a tautology by checking that each member of {CFCpqFANpq, CNCpqNANpq, CICpqIANpq, CVCpqVANpq} is a tautology in 2-valued logic.

In notation for substitution for δ, an apostrophe " ' " means that we substitute the argument that follows delta for the apostrophe.  For example, from 1 δp, 1 δ/C'q we substitute δ with C, then the argument that follows δ which is "p" in this case, and then "q" obtaining Cpq.  If we write 2 CsδCpCqr, 2 δ/C'' that means we substitute δ with C, then the argument of δ CpCqr, then the argument of δ CpCqr obtaining CsCCpCqrCpCqr.  If we write 3 CpCCpδqr, 3 δ/CC'r' then we write CC, the argument of δ q, r, and lastly the argument of δ "q" again in place of δq obtaining CpCCpCCqrqr.  δ/' just means we substitute δ with the argument of δ.
CδCpqδANpq can effectively take the place of a definition of the conditional "C" in a logical calculus.  Let's consider CδCpqδANpq in the following system:

axiom                     1 ApNp
axiom                     2 CδCpqδANpq
2 δ/CCδCpqδ'CδANpqδCpq    3 CCCδCpqδCpqCδANpqδCpqCCδCpqδANpqCδANpqδCpq
2 δ/Cδ'δCpq               4 CCδCpqδCpqCδANpqδCpq
D3.4                      5 CCδCpqδANpqCδANpqδCpq
D5.2                      6 CδANpqδCpq
6 δ/'                     7 CANpqCpq
D7.1                      8 CpNNp

Thus, double negation introduction CpNNp follows from these two axioms.  It also follows that in the presence of a definition corresponding to axiom 2, the law of the excluded middle ApNp allows us to derive the law of double negation introduction CpNNp.

Well-Formed Formula of the Day: ApNp

ApNp consists of a symbolic formulation of the law of the excluded middle "either a proposition is true or it is not true."  If we wanted to use at as an axiom, we might want to have as a deduction rule {ANpq, p}->q, but even then we'd probably want to commute ApNp and use ANpp instead.  Let's say we have ANpp as an axiom along with ANpANqp as an axiom.  We might proceed as follows.

axiom  1 ANpp
axiom  2 ANpANqp
D2.2    3 ANpANqANrq
D2.1    4 ANpANqq

ApNp can get proved from the axiom set {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp, CpApq, CpAqp}.  ApNp is unique among classical logic theorems which only have C, A, K, E, and N as connectives in them in that it has exactly 4 symbols.

Formula of the Day: EEEpqrEpEqr

EEEpqrEpEqr comes as a way of saying that logical equivalence associates.  Along with EEpqEqp can serve as one of the axioms of the equivalential calculus.  Equivalential calculus allows us to deduce all tautologies which only have equivalence symbols and variables in them.  The rule of inference for equivalential calculus comes as a modified form of detachment "from Eab, as well as "a", we may infer b" where "a" and "b" consist of meta-variables.  Or more compactly

{Eab, a} -> b

We can condensed such an E-detachment along with uniform substitution just like we can condense C-detachment with uniform substitution.  Taking EEEpqrEpEqr as an axiom, we can develop the system {EEEpqrEpEqr} as follows:

axiom 1 EEEpqrEpEqr
D1.1   2 EEpqErEpEqr
D1.2   3 EpEqErEpEqr
D2.1   4 EsEEEpqrEEpEqrs
D1.3   5 EpEqErEsEEpqErs
D1.4   6 EpEqEEErstEErEstEpq
D2.2   7 EpEEqrEEsEqErsp
D2.3   8 EsEpEEqErEpEqrs

The system with a single axiom which corresponds to each of these theorems has no last theorem under condensed detachment (unlike {Cpp} which has Cpp as its only theorem under condensed detachment).  For {EEpqErEpEqr} each theorem will have some form Eab, which implies that there exists a substitution which enables a detachment from the antecedent of Epq of EEpqErEpEqr with EEpqErEpEqr as the major premise, and any theorem of the system {EEpqErEpEqr}.  For the systems corresponding to theorems 3 through 8, each axiom serving as the major premise and any theorem serving as the minor premise enables a condensed detachment.  Does *every* theorem EEEpqrEpEqr correspond to a system with a sole axiom which has no last theorem under condensed detachment?

EEEpqrEpEqr seems to come as a theorem that requires a fair amount of work to prove in the natural deduction systems I've encountered and in non-equivalential systems of logic which use definitions to get equivalences into the system.

Formula of the Day: The law of commutation CCpCqrCqCpr.

If we look at CCpCqrCqCpr it turns out that we can obtain the consequent implying the antecedent just from substitution.  Let X p/a indicate that variable p gets substituted with a throughout formula X.

axiom  1 CCpCqrCqCpr
1 p/a    2 CCaCqrCqCar
2 q/p    3 CCaCprCpCar
3 a/q    4 CCqCprCpCqr

Or if we allow simultaneous substitution in a formula we can proceed as follows:

axiom       1 CCpCqrCqCpr
1 p/q, q/p  2 CCqCprCpCqr

The law of commutation, unlike the law of identity, can also serve as the sole axiom of a system under detachment, and from it as an axiom we can obtain well-formed formulas (or "formulas") which are not substitution instances of it (unlike Cpp as the sole axiom of a system).

axiom  1 CCpCqrCqCpr
D1.1    2 CpCCqCprCqr
D2.2    3 CCpCCqCCrCqsCrstCpt
D2.1    4 CCpCCCqCrsCrCqstCpt
D1.4    5 CpCCpCCCqCrsCrCqstt
D1.3    6 CpCCpCCqCCrCqsCrstt
D2.3    7 CCuCCCpCCqCCrCqsCrstCptvCuv
D2.7    8 CCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwy
D2.8    9 CCzCCCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwyaCza

The system {CCpCqrCqCpr} has no last most general theorem, as can get understood from theorem 2 CpCCqCprCqr.  D2.x will always yield a theorem, since any variable can get substituted by any theorem, and CCqCprCqr where p is any theorem is a well-formed formula.  Thus, D2.2 yields a theorem.  D2.D2.2 yields a theorem.  D2.D2.D2.2 yields a theorem and so on.  Each theorem has more symbols than the last theorem also, since the antecedent "p" appears in the consequent of CpCCqCprCqr, and since every theorem has more symbols than Cp, the detached theorem having the form CCqCprCqr will have more letters than the theorem that served as the major premise.  Theorems 5, and 6 also indicate that there exist subsystems of CCpCqrCqCpr which like the subsystem {CpCCqCprCqr} have no last most general theorem.

The law of commutation appeared in the first axiom system for propositional calculus ever proposed.  Gottlob Frege's system was {CpCqp, CCpCqrCCpqCpr, CCpCqrCqCpr, CNNpp, CpNNp, CCpqCNqNp}.  Jan Lukasiewicz figured out that the law of commutation could get derived from the first two axioms a few decades later.  Here's a proof:

axiom   1 CpCqp
axiom   2 CCpCqrCCpqCpr
D1.2     3 CpCCqCrsCCqrCqs
D2.3     4 CCpCqCrsCpCCqrCqs
D1.4     5 CpCCqCrCstCqCCrsCrt
D2.5     6 CCpCqCrCstCpCqCCrsCrt
D6.1     7 CCpCqrCsCCpqCpr
D4.7     8 CCpCqrCCsCpqCsCpr
D2.8     9 CCCpCqrCsCpqCCpCqrCsCpr
D1.1   10 CpCqCrq
D9.10 11 CCpCqrCqCpr

The law of commutation also appears as an axiom or theorem in many other systems of logic.  If one has it in a system S, and it does NOT need one of the axioms to get derived, then there may very well exist a way to figure out an alternative system A which has the same theorems as S.  For instance, we'll start by pointing out that CCpCqrCqCpr comes as derivable from {CpCqp, CCpCqrCCpqCpr} above.  Now since CCpqCNqNp and D [CCpCqrCCpqCpr].[CCpqCNqNp] exists it turns out that the theorems of Frege's system have another axiomization than {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5a-CCpqCNqNp}.  Namely, that axiomization is {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5b-CNpCCqpNq}.  To prove this we only need to write out that D[ CCpCqrCqCpr].5a yields 5b and D[CCpCqrCqCpr].5b yields 5a.

Also, let's suppose that we have CCpCqrCqCpr and Cpp as our axioms:

axiom   1  CCpCqrCqCpr
axiom   2  Cpp
D1.2     3  CpCCpqq
D3.2     4  CCCppqq
D1.4     5  CpCCCqqCprr
D1.5     6  CCCppCqrCqr

Notice that 6 is not the same formula as 4, but 6 is a more specialized (or less general) formula than 4 since we can obtain 6 from 4 by substitution only.

Whenever I refer to an axiom set, unless stated otherwise, I presume the rule of detachemnt {|-Cab, |-a} -> b, where "a" and "b" constitute metavariables, and uniform substitution for variables.  The notation Da.b stands for a condensed detachment with "a" as the major premise and "b" as the minor premise.

Logical Formula of the Day: Cpp

Since this consists of a new thing I plan to do I guess I'll start small with one of the shortest tautologies in existence.  Cpp sometimes appears as an axiom in some propositional calculi.  For instance, A. N. Prior's formal logic lists {Cpp, CCCpqrCCrpCsCtp} as a basis for implicational propositional calculus.  It also appeared as an axiom in Peirce's axiom set for C-0 (0 meaning "falsum") classical logic {Cpp, CCpCqrCqCpr, CCpqCCqrCpr, C0p, CCCpqpp}.  In a natural deduction setting you can prove it as follows:

hypothesis 1 | p
Ci 1-1        2   Cpp

where "Ci" stands for conditional introduction.  For positive implicational propositional calculus with the axiom set {CpCqp, CCpCqrCCpqCpr} we can prove it in two condensed detachments.

axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
D2.1   3 CCpqCpp
D3.1   4 Cpp

In classical logic with the basis {CCpqCCqrCCpr, CCNppp, CpCNpq} we can prove it in two steps also.

axiom 1 CCpqCCqrCpr
axiom 2 CCNppp
axiom 3 CpCNpq
D1.3   4 CCCNpqrCpr
D4.2   5 Cpp

Here's another proof from another axiom set:

axiom 1 CCCpqrCqr
axiom 2 CCCpqpp
D 1.2  3 Cpp

Actually, let's say we fix CCCpqrCqr as the first axiom 1.  Now replace the first p in CCCpqpp with CCpqp.  This yields CCCCCpqpqpp.  D1. CCCCCpqpqpp yields Cpp.  In any system sufficient for the conditional of classical logic, the variable "p" can get replaced by "CCpqp" since CCCpqpp is a theorem and CpCCpqp is also a theorem.  Consequently, we can iterate the process of replacing a "p" in any formula obtained in this way with CCCpqpp as the starting point and still obtain a theorem in classical logic, provided that we do NOT replace the last two "p's".  Each theorem obtained in this way serving as the minor premise along with CCCpqrCqr as the major premise will yield Cpp after a condensed detachment.

One can also prove it in Wajsberg-Lukasiewicz three-valued from the following basis as follows:

axiom 1 CpCqp
axiom 2 CCpqCCqrCpr
axiom 3 CCCpNppp
axiom 4 CCNpNqCqp
D2.1   5 CCCqprCpr
D5.3   6 Cpp

Or Lukasiewicz infinite valued-logic:

axiom     1 CpCqp
axiom     2 CCpqCCqrCpr
axiom     3 CCNpNqCqp
axiom     4 CCCpqqCCqpp
D2.1       5 CCCpqrCqr
D2.2       6 CCCCqrCprsCCpqs
D6.6       7 CCpCqrCCsqCpCsr
D5.4       8 CpCCpqq
C8.7       9 CCpCqrCqCpr
D9.1     10 CpCqq
D10.10 11 Cpp

Or from double suffixing CCpqCCqrCpr and the double negation laws CpNNp, CNNpp.

axiom   1 CCpqCCqrCpr
axiom   2 CpNNp
axiom   3 CNNpp
D1.2     4 CCNNpqCpq
D4.3     5 Cpp

Cpp as a major premise will only give you back the minor premise that you used when doing a condensed detachment.  On the other hand, Cpp as a minor premise has some interesting uses.  For instance D[CCpCqrCqCpr.Cpp] yields "modus ponens" CpCCpqq.  D[CCpCqrCCpqCpr.Cpp] yields CCCpqpCCpqq.  Perhaps more interestingly D[CCNpNqCCNpqq.Cpp] yields the law of Clavius CCNppp.  Additionally, if we consider D[CCpqCCqrCpr.a], and D[CCpqCCqrCpr.a] exists (which is equivalent to saying that "a" is a conditional), then D[D[CCpqCCqrCpr.a]].[Cpp] yields "a".

Basic Rule of inference "From any wff of the form "Cab", and any other wff of the form "a", we may infer "b"."

Axioms:

Group 1:

1 CpCqp  Conditional-Simplification abbreviatied C-s
2 CCpCqrCCpqCpr Conditional-Self-Distribution  abbreviated C-d.

Group 2:

3 CCpKqNqNp  Negation-in  abbreviated Ni
4 CCNpKqNqp  Negation-out abbreviated No

Group 3:

5 CKpqp Conjunction-out left abbreviated Kol
6 CKpqq Conjunction-out right abbreviated Kor
7 CpCqKpq  Conjunction-in abbreviated Ki

Group 4:

8   CpApq Alternation-in left abbreviated Ail
9   CpAqp Alternation-in right abbreviated Air
10 CCpqCCrqCAprq Alternation-out abbreviated Ao

Group 5:

11 CEpqCpq Equivlaence-out right abbreviated Eor
12 CEpqCqp Equivalence-out left abbreviated Eol
13 CCpqCCqpEpq Equivalence-in abbreviated Ei

Lemma 0: Epp. It can end up helpful to use this as a minor premise.

1 ! p hypothesis
2 Cpp 1-1 C-in
3 Epp 2, 2 E-in

Lemma 1: {Epq, p} => q. Nickname: E-detach right.

1 Epq assumption
2 p assumption
3 Cpq 1 E-out left
4 q 3, 2 C-out

Lemma 2: {Epq, q} => p. Nickname: E-detach left.

1 Epq assumption
2 q assumption
3 Cqp 1 E-out right
4 p 2, 3 C-out

Lemma 3: |- EEpqEqp. Nickname: E-commutation.

1 !-1 Epq hypothesis
2 !-1 Cqp 1 E-out right
3 !-1 Cpq 1 E-out left
4 !-1 Eqp 2, 3 E-in
5 CEpqEqp 1-4 C-in
6 !-2 Eqp hypothesis
7 !-2 Cpq 6 E-out right
8 !-2 Cqp 6 E-out left
9 !-2 Epq 7, 8 E-in
10 CEqpEpq 6-9 C-in
11 EEpqEqp 6, 10 E-in

Lemma 4: |- ApNp. Nickname: law of the excluded middle.

1 ! NApNp hypothesis
2 @ Np hypothesis
3 @ ApNp 2 A-in
4 @ KApNpNApNp 3, 1 K-in
5 ! p 2-4 N-out
6 ! ApNp 5 A-in
7 ! KApNpNApNp 6, 1 K-in
8 ApNp 1-7 N-out

Lemma 5: {Cpq, Nq} => Np. Nickname: Modus Tollens.

1 Cpq assumption
2 Nq assumption
3 ! p hypothesis
4 ! q 3, 1 C-out
5 ! KqNq 2, 4 K-in
6 Np 3-5 N-out

Lemma 6: {Np, NEpq} => q. Nickname: Lemma 6.

1 Np assumption
2 NEpq assumption
3 !-1 Nq hypothesis
4 @-1 p hypothesis
5 #-1 Nq hypothesis
6 #-1 KpNp 4, 1 K-in
7 @-1 q 5-6 N-out
8 !-1 Cpq 4-7 C-in
9 @-2 q hypothesis
10 #-2 Np hypothesis
11 #-2 KqNq 9, 3 K-in
12 @-2 p 10-11 N-out
13 !-1 Cqp 9-12 C-in
14 !-1 Epq 8, 13 E-in
15 !-1 KEpqNEpq 14, 2 K-in
16 q 3-15 N-out

Lemma 7: {p, q} => Epq. Nickname: Lemma 7.

1 p assumption
2 q assumption
3 !-1 p hypothesis
4 !-1 q 2 Repitition
5 Cpq 3-4 C-in
6 !-2 q hypothesis
7 !-2 p 1 Repitition
8 Cqp 6-7 C-in
9 Epq 5, 8 E-in


Lemma 8: |- EEpEqrEEpqr. Nickname: E-association.

1 !-1 EpEqr hypothesis
2 @-1 Epq hypothesis
3 #-1 p hypothesis
4 #-1 Eqr 3, 1, E-detach right
5 #-1 q 3, 2, E-detach right
6 #-1 r 5, 4, E-detach right
7 @-1 Cpr 3-6 C-in
8 #-2 Np hypothesis
9 #-2 Cqp 2 E-out left
10 #-2 Nq 8, 9, Modus Tollens
11 #-2 CEqrp 1 E-out right
12 #-2 NEqr 8, 11, Modus Tollens
13 #-2 r 10, 12 Lemma 6
14 @-1 CNpr 8-13 C-in
15 @-1 ApNp law of the excluded middle
16 @-1 r 7, 14, 15 A-out
17 !-1 CEpqr 2-16 C-in
18 @-2 r hypothesis
19 #-3 p hypothesis
20 #-3 Eqr 19, 1, E-detach right
21 #-3 q 18, 20, E-detach left
22 @-2 Cpq 19-21 C-in
23 #-4 q hypothesis
24 #-4 CEqrp 1 E-out right
25 #-4 Eqr 23, 18, lemma 7
26 #-4 p 25, 24 C-out
27 @-2 Cqp 23-26 C-in
28 @-2 Epq 22, 27 E-in
29 !-1 CrEpq 18-28 C-in
30 !-1 EEpqr 17, 29 E-in
31 CEpEqrEEpqr 1-30 C-in
32 !-2 EEpqr hypothesis
33 @-3 p hypothesis
34 #-5 q hypothesis
35 #-5 Epq 33, 34 lemma 7
36 #-5 r 35, 32, E-detach right
37 @-3 Cqr 34-36 C-in
38 #-6 r hypothesis
39 #-6 Epq 38, 32, E-detach left
40 #-6 q 39, 33, E-detach right
41 @-3 Crq 38-40 C-in
42 @-3 Eqr 37, 41 E-in
43 !-2 CpEqr 33-42 C-in
44 @-4 Eqr hypothesis
45 #-7 r hypothesis
46 #-7 q 44, 45, E-detach left
47 #-7 Epq 45, 32, E-detach left
48 #-7 p 46, 47, E-detach right
49 @-4 Crp 45-48 C-in
50 #-8 Nr hypothesis
51 #-8 Cqr 44, E-out left
52 #-8 Nq 50, 51, Modus Tollens
53 #-8 CEpqr 32 E-out left
54 #-8 CEqpr 53, E-commutation
55 #-8 NEqp 50, 54, Modus Tollens
56 #-8 p 52, 55, lemma 6
57 @-4 CNrp 50-56 C-in
58 @-4 ArNr law of the excluded middle
59 @-4 p 49, 57, 58 A-out
60 !-2 CEqrp 44-59 C-in
61 !-2 EpEqr 43, 60 E-in
62 CEEpqrEpEqr 32-61 C-in
63 EEpEqrEEpqr 31, 62 E-in

Some Questions on a Class of Derived Axiom Sets

Define Σ as an abbreviation for CCpqCCqrCpr.

Suppose we have a logic L where all theses have the conditional C as their principal connective, the rules of modus ponens (more generally we could consider any rule of detachment... but modus ponens should suffice here) and uniform substitution, axiom set {α, ..., ω}, Σ is a thesis of L, and Cpp is a thesis of L. Since condensed detachment "D" is a derivable rule of a inference, it follows that

Theorem: {DΣ.α, ..., DΣ.ω, Cpp} is also an axiom set for L
(proof hint: DΣ.x exists, where x is any thesis, and D.DΣ.x.(Cpp) gives you...).

There exist plenty of corollary theorems also where the alternative axiom set gets obtained by the commuted variant of Σ; CCpqCCrpCrq (or CCqpCCpqCpr), or one of the simplest generalizations of Σ CCpqCCqrCCrsCps (Sorites), further generalizations of Σ than Sorites (e. g. CCpqCCqrCCrsCCstCpt) as well as commuted variants of Sorites and its generalizations, where a commuted variant V of a thesis T, means that we can obtain thesis V from T with the help of CCpCqrCqCpr and conversely.

Question 1: The theorem stated here clearly bears a relation to BCI logic. Does there exist a name for the theorem I've stated above?

I'll try and explain this as follows:

An example of how things work here to clarify the questions:
{1-CCpqCCqrCpr or Σ, 2-CCNppp, 3-CpCNpq} is a known axiom set for two-valued propositional calculus which satisfies independence. To make things clear, Cpp and the other axioms of {DΣ.α, ..., DΣ.ω} in this case can get derived as follows:

1 CCpqCCqrCpr axiom
2 CCNppp axiom
3 CpCNpq axiom

   1 q/CNpq * C3-4

4 CCCNpqrCpr (this is DΣ.3)

   4 q/p, r/p * C2-5

5 Cpp

   1 p/Cpq, q/CCqrCpr, r/s * C1-6

6 CCCCqrCprsCCpqs (this is DΣ.1)

   1 p/CNpp, q/p, r/q *C2-7

7 CCpqCCNppq (this is DΣ.2)

Now the theorem here tells us that {CCCCqrCprsCCpqs, CCpqCCNppq, CCNpqrCpr, Cpp} is also an axiom set for two-valued propositional calculus.

Proof: In this example case since each thesis got derived from the axioms of {1-CCpqCCqrCpr or Σ, 2-CCNppp, 3-CpCNpq}, we only need show that from {1'-CCCCqrCprsCCpqs, 2'-CCpqCCNppq, 3'-CCNpqrCpr, 4'-Cpp} we can derive each of the axioms of {1-CCpqCCqrCpr or Σ, 2-CCNppp, 3-CpCNpq} as follows.

1' CCCCqrCprsCCpqs axiom
2' CCpqCCNppq axiom
3' CCNpqrCpr axiom
4' Cpp axiom

    1' s/CCqrCpr * 4 p/CCqrCpr-1 

1 CCpqCCqrCpr

     2' q/p * 4-2

2 CCNppp

     3' r/CNpq * 4 p/CNpq-3

3 CpCNpq
Example of question 2: {1-CCpqCCqrCpr or Σ, 2-CCNppp, 3-CpCNpq} satisfies independence. So, does the set {CCCCqrCprsCCpqs, CCpqCCNppq, CCNpqrCpr} also satisfy independence? Added: Mace4 has given me 3 models which taken together indicate that {CCCCqrCprsCCpqs, CCpqCCNppq, CCNpqrCpr} satisfies independence.

Question 2 more generally: If the axioms {α, ..., ω} satisfy independence, will the axioms of {DΣ.α, ..., DΣ.ω} also satisfy independence? Will the theses belonging to the set obtained from {α, ..., ω} using generalizations of Σ, or commutated variants of those generalizations, or the commuted variant of Σ also satisfy independence?

To perhaps aid in comprehensibility, I'll present the following proof of the theorem above. I'll let letters in bold stand for metalinguistic variables:

Proof: First, all members of {DΣ.α, ..., DΣ.ω} will exist, since all members of the original postulate set {α, ..., ω} come as conditionals, and the antecedent of Σ comes as the conditional Cpq. Next, each instance of DΣ.k, where k belongs to {α, ..., ω} will come as the consequent of a substitution instance of Σ. So, we have a class of formulas of the form CC q rC p r where r does not appear as a subformula in q, nor does r appear as a subformula in p, since r did not appear in the antecedent of Σ. Thus, a unifier of Cpp and the antecedent of whatever formula we choose DΣ.k at a particular time will exist. The unifier will have form C q q. Consequently, D.DΣ.k.(Cpp) will have form C p q. This form matches the original form for k. Since k consisted of an arbitrary name for a variable belonging to {α, ..., ω}, it follows that {DΣ.α, ..., DΣ.ω, Cpp} will also qualify as an axiom set for the same logic.

It might come as some interest to note that this proof implies a uniform method to obtain an unending sequence of alternative postulate sets for a logic under certain conditions. The proofs of the corollaries will also give us another method. Using CpCqp in place of how Σ can get used also consists of another method of obtaining alternative axioms.