-3
$\begingroup$

Suppose that we only have propositional variables and connectives. Suppose our rules of inference are detachment {C$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$, and uniform substitution. Suppose that we have a binary connective "C" and a unary connective "N". In 1953 C. A. Meredith found what is currently the shortest single axiom of classical C-N (Conditional-Negation) propositional calculus [p. 302 of A. N. Prior's Formal Logic indicates this and references Prior's paper " 'Single Axioms for the Systems (C, N), (C, O), and (A, N) of the Two-valued Propositional Calculus' JCS, vol. i, No. 3 (July 1953), pp. 155-64. Systems 1.5, 3.13, 6.13, 6.14.):

CCCCCpqCNrNsrtCCtpCsp.

Or using another prefix notation

→→→→→pq→¬r¬srt→→tp→sp.

So given the first notation, the formation rules are:

  1. All lower case letters of the Latin alphabet, as well as any lower case letters of the Latin alphabet sub-scripted by Hindu-Arabic numerals are formulas.
  2. If x is a formula, then so is Nx.
  3. If x and y are formulas, then so is Cx y. The space between the x and the y in "Cx y" is not necessary.
  4. Nothing else is a formula in this context.

To determine what is and what is not a formula the following suffices.

  1. Assign -1 to all lower case letters, as well as all lower case letters which are sub-scripted.
  2. Assign 0 to N.
  3. Assign 1 to C.
  4. Sum the assigned numbers as you precede from left to right throughout any given string.
  5. A string will qualify as a formula if and only if it either starts and ends with -1, or if it starts with a member of {0, 1} and -1 is only reached at the spot corresponding to the last letter of the string, and that string ends with -1.

Now, via the above it turns out that any formula that starts with "C", has its antecedents corresponding to the longest subformulas which have a "0" corresponding to their last letter. So looking at the above formula, we have

C  C  C  C  C  p  q  C  N  r  N  s  r  t  C  C  t  p  C  s  p
|  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |
1  2  3  4  5  4  3  4  4  3  3  2  1  0  1  2  1  0  1  0 -1

The longest subformula which ends with the first "t" is thus CCCCpqCNrNsrt. The longest subformula which ends with the second "p" is thus "Ctp", and "s" is the longest subformula corresponding to the third "0" spot. Thus, the main breaks of the formula can get located by the following "|" marks.

 C|CCCCpqCNrNsrt|C|Ctp|C|s|p.

Furthermore, the main breaks of CCCCpqCNrNsrt is given by C|CCCpqCNrNsr|t, and so on.

Suppose we have a 2-valued model of C and N given by the following table:

C  0  1  N
0  1  1  1
1  0  1  0

Does there exist any shorter single axiom, which under the rules above allows us to deduce all tautologies, and only those tautologies in the 2-valued model? Does there exist another single axiom of the same length?

If there exists a unique shortest axiom up to re-symbolization of variables and connectives, what is the shortest axiom (which is a tautology) that allows us to deduce a known axiom system for classical propositional calculus, such as the following axiom set?

  1. CpCqp. [p$\rightarrow$(q$\rightarrow$p)].
  2. CCpCqrCCpqCpr. [(p$\rightarrow$(q$\rightarrow$r))$\rightarrow$((p$\rightarrow$q)$\rightarrow$(p$\rightarrow$r))].
  3. CCNpNqCqp. [($\lnot$p$\rightarrow$$\lnot$q)$\rightarrow$(q$\rightarrow$p)].

If there exists more than one shortest axiom, what is the set of such shortest axioms up to re-symbolization of variables and connectives?

The length of an axiom is defined by the number of symbols it has when fully expressed as a well-formed formula in Polish/Lukasiewicz notation.

I've tried to find a way to compute all tautologies of a certain length in OTTER, but had no success. There has existed some similar work for shortest axioms in classical propositional calculus with the Sheffer Stroke, but in a private communication with one of the authors I've learned that they didn't do a search for the shortest axioms of the conditional-negation formulas for classical propositional calculus.

Improve this question
$\endgroup$
18
  • 7
    $\begingroup$ I would expect that many more people will understand the axiom if you were to write it in infix notation, rather than prefix notation. Also, you can use $\to$ and $\neg$ rather than C and N. $\endgroup$
    – Joel David Hamkins
    Oct 2, 2014 at 6:56
  • 6
    $\begingroup$ There is no reason not to write the formula in a human-readable form, and just define its length to be the number of variables and connectives, ignoring brackets. $\endgroup$
    – Emil Jeřábek
    Oct 2, 2014 at 16:19
  • 4
    $\begingroup$ In infix notation, perhaps slightly more readable than prefix: [(((p→q)→(¬r→¬s))→r)→t] → [(t→p)→(s→p)]. $\endgroup$
    – Peter LeFanu Lumsdaine
    Oct 2, 2014 at 19:30
  • 7
    $\begingroup$ No, I find it much easier. There is no way I can visually count 20+ letters of line noise without making a mistake, whereas the redundant structure of the infix formula makes the task feasible. Anyway, this is quite besides the point. You are communicating with humans, and thus you should strive to use notation that is clearly readable for others. When the length of a formal expression is an issue, you need to state it in the post, not make people count it themselves. $\endgroup$
    – Emil Jeřábek
    Oct 3, 2014 at 15:04
  • 7
    $\begingroup$ Doug's comment "If, if, if, if, if p..." above, which surely helps to make the statement completely transparent, reminds me of the perfectly grammatical sentence, "Dogs dogs dogs bite bite bite." Or similarly, "Cats dogs people pet chase purr." And in the English class, while Mary had had "had," John had had "had had"; "had had" had had a greater effect on the teacher. $\endgroup$
    – Joel David Hamkins
    Oct 3, 2014 at 16:17

1 Answer 1

Reset to default
6
$\begingroup$

I don't know, but it is quite possible that the first question is an open problem, see Ulrich's list of open problems.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.