Can There Get Found Single Axioms for Some Subsystems of Propositional Calculus?

Question

I use Polish notation. All systems have detachment and uniform substitution as the only primitive rules of the system.

A user named John told me in an answer "On the question of a single axiom, the answer is yes... many are known as you were pointed at above. But more generally, Tarski announced in 1930 that any system with substitution and modus ponens and that has as theorems either of the sets: {CpCqp, CpCqCCpCqrr} or {CpCqp, CpCqCCpCqrCsr} has a single axiom basis. (Adrian Rezus published a proof in 1982 of the first basis, Dolph Ulrich presented a proof of the second some years ago) John Halleck recently showed that (Cpp, CpCqCCpCqrCsr} and {CpCqp, CCpCqrCqCpr} were also suffice show that there is a single axiom basis for a system."

I'm not sure if his statement applies to any logical calculus, or just implicational calculi (and he doesn't have much activity on the stackexchange network).

Can there get found single axiom(s) for the positive implicational conjunctive calculus {CpCqp, CCpCqrCCpqCpr, CKpqp, CKpqq, CpCqKpq}? The positive equivalential calculus... {{CpCqp, CCpCqrCCpqCpr, CEpqCpq, CEpqCqp, CCpqCCqpEpq}? Does there exist single axiom(s) for these systems if we join Perice CCCpqpp as an axiom also? Does there exists a single axiom for the system {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp, CpCqKpq, CKpqp, CKpqq, CpApq, CpAqp, CCpqCCrqCAprq, CEpqCpq, CEpqCqp, CCpqCCqpEpq} where inter-definability of connectives is prohibited?

Any tips as to how to go about finding a single axiom for a logical system?

Answer 1

"... (Cpp, CpCqCCpCqrCsr} and {CpCqp, CCpCqrCqCpr} were also suffice to show that there is a single axiom basis for a system. ... I'm not sure if his statement applies to any logical calculus, or just implicational calculi."

Short answer: True of any logical calculus that has the given theorems.

The proof is (as Rezus' proof is) a contructive proof that given either set you can package up ANY axiomatic basis of the system into a single axiom. While the proofs are mine, they were found using approaches that are due to Dolph "Ted" Ulrich. [And they produce shorter axioms than Rezus' techniques produce.] To the best of my knowledge, there are currently no constructive techniques (like Rezus', or Ulrich's, or mine) that produce shortest single axioms.

Answer 2

You may see this useful collection of axiom systems for propositional calculus.

Answer 3

Cross ref. to “Examples of mathematical discoveries which were kept as a secret” [Nov 3, 2014]

The Question was:

“What are examples of mathematical discoveries which were kept as a secret when they discovered and then became unfolded after a while by any reasons?” [asked Nov 3, ’14 at 14:17, by Ali Sadegh Dagighi, edited Nov 15 ’14 at 10:32] [ Examples of mathematical discoveries which were kept as a secret, commented upon by Doug Spoonwood, Nov 10 '14, etc.]

[Adrian Rezus: 20150323] Actually, Tarski’s result is of 1925. It was not “kept secret”, his (Polish) colleagues and collaborators (Lesniewski, Lukasiewicz, etc.) were duly informed about the finding, Tarski just did not find it interesting enough to advertise it. (Another example — more relevant, perhaps — is the so-called “Deduction Theorem”, usually credited to Jacques Herbrand, cca 1930, which Tarski found already around 1921-1922, about a decade before the Frenchman; he mentioned the result in print only much later.) The original proof of the axiomatixability result was lost, indeed. As to “data retrieval”, I was a able to prove the result around 1979 [in print 1982][1], not just “a few years later” (unless 1979-1925 = 54 years would count as “a few”!), by a method based on [typed] lambda-calculus. (As an aside: lambda calculus was invented by the end of the twenties, and appeared first in print in 1932-1933, while typed lambda-calculus dates of 1937-1938; so I still wonder what could have been Tarski’s “original method” of proof!) Around 2010, John Halleck found another proof of Tarski's Claim (1925) by using specific software (an automated theorem prover) of his own design. [For details, see also my [notes][2] of Oct 1, 2010],

[1] “On a Theorem of Tarski”, Libertas Mathematica [Arlington TX] vol 2, 1982, pp 63-97 [MR 84b:03019] [online @ https://www.academia.edu/293942/_On_a_theorem_of_Tarski_Libertas_Mathematica_Arlington_TX_vol._2_1982_pp._63-97_MR_84b_03019_]

[2] “Tarski’s Claim - Thirty years later”, Oct 1, 2010 [online @ https://www.academia.edu/999512/_Tarskis_Claim_Thirty_Years_Later_Preprint_Nijmegen_October_1_2010_]