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
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
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.
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 {
Theorem: {D
(proof hint: D
There exist plenty of corollary theorems also where the alternative axiom set gets obtained by the commuted variant of
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 q/p, r/p * C2-5
1 p/Cpq, q/CCqrCpr, r/s * C1-6
1 p/CNpp, q/p, r/q *C2-7
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
2' q/p * 4-2
3' r/CNpq * 4 p/CNpq-3
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 {
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
