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.

Does Cantorian Set Theory Have Limitations for Evaluating the Size of Sets?      Cantorian set theory would have us believe that all countable infinites are the same size (or at least, that's the conceptual metaphor commonly used.)  I will try and argue that this makes little sense, in at least one significant case.      Let's look at classical propositional logic from the semantic point-of-view.  There exist three classes of well-formed formulas (hereafter formulas): tautologies, contradictions, and contingencies.  The class of tautologies is well known to be countably infinite, given countably many infinite variables, so via negation the class of contradictions is also countably infinite.  Though I don't know how to demonstrate it, the class of contingencies also seems countably infinite.      But, it does not make much sense to believe contingencies as big as tautologies.  Nor does it make much sense to believe contingencies as big as contradictions.  I will say that I do believe that a skilled set theorist could sufficiently describe two bijections: one between contingencies and tautologies, and another between contingencies and contradictions (and negation gives us a bijection between tautologies and contradictions).      However, if we had a machine which gave us propositional formulas at random, I assert that the class of contingencies would have the greatest frequency of occurrence after a sufficiently large amount of time (if needed, we might postulate 10 billion propositional formulas as enough.  My idea here goes that we have enough propositional formulas so that it becomes all too unlikely that the frequency distribution will change much when getting more propositional formulas at random.)  This would seem, at the very least, to imply the class of contingencies as greater than the class of contradictions.  It also would imply the class of contingencies greater than the class of tautologies.  Of course, that does not say that the frequency of contingencies obtained at random would come as greater than the class of tautologies and the class of contradictions combined.  That said, truth tables might seem to suggest this also, since there exist 14 truth functions of two variables which are contingencies, but only 2 which are either tautologies or contradictions, only 2 truth functions of three variables which are tautologies or contradictions and the rest of the truth functions of three variables are contingencies, and in general only 2 truth functions of n-variables and the rest of the truth functions of n-variables are contingencies.