Friday, June 6, 2014

I wrote about a way to generate more bases for classical logic about a year ago, when you have either CCpqCCqrCpr or CpCqp upfront in the basis.  Examples of such systems are {CCpqCCqrCpr, CCNppp, CpCNpq}-Lukasiewicz, {CCpqCCqrCpr, CCpCpqCpq, CpCqp, CCNpNqCqp}-Tarski, {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp}-I don't think think I've seen this before, but it's basically implied by a system of Mendelsohn since if any system has [C] CCpCqrCqCpr provable in a proper sub-basis without axioms a, ..., z, of the basis, then a can get replaced by D[C].a, b can get replaced by D[C].b, ... z can get replaced by D[C].z.  For example, for the basis {CCpCqrCCpqCpr, CpCqp, CCNpNqCqp}, [C] can get proved in the sub-basis {CpCqp, CCpCqrCCpqCpr}.  Thus, CCNpNqCqp can get replaced by CpCCNqNpq for the basis {CCpCqrCCpqCpr, CpCqp, CCNpNqCqp}.

The following 4-basis for C-N classical logic is independent:

1. CCCCpqCrqsCCrps
2. CCpqCCNppq
3. CCCNpqrCpr
4. Cpp

Or as a system with fewer symbols, the axioms of the following are independent.

1. CCpqCCqrCpr
2. CCpqCCNppq
3. CpCNpq
4. Cpp

Does there exist a shorter 4-basis with independent axioms for C-N classical logic?

I note also that the following four formulas are not independent

1. CCpqCCqrCpr
2. CCNppp
3. CCCNpqrCpr
4. Cpp

since D3.2 yields Cpp.

Does there exist a 3-basis or a 2-basis for classical logic where one of the axioms is Cpp?

No comments:

Post a Comment