These
pages are
devoted to certain specialized topics having to do with the
second-greatest
love of my life: the investigation of sentential calculi.
The "Twenty-six
open questions" page lists the open questions concerning such calculi
posed explictly
in A legacy recalled and a tradition continued, my introduction to
the August 2001 issue of the Journal of Automated Reasoning, which
was the special issue devoted to finding formal proofs in sentential
calculi. This page also describes any progress I've been informed of that
has been made towards answering those questions since the paper originally
appeared.
Most of the other pages report on some projects currently of primary
interest to me concerning short axiomatic bases for various
logics of pure implication and for the classical equivalential calculus.
These pages include many additional open questions.
Though it is of
course my hope that at least some of the new results presented herein will
be of interest to those who visit, it is the unsolved problems and open
questions that are the heart of the site and its reason for being.
Consequently, more open problems and questions on related topics to be added
to the site will be welcomed as well as solutions and answers to those
already here (dulrich at purdue dot edu).
|
|
|
The notation of choice throughout is Polish
notation (also known as "Łukasiewicz notation", "parenthesis-free
notation", and "prefix notation", ) where 'Cpq', for example, goes short for
standard infix notation's 'p→q'
(or, where it is material implication that is at issue,
'p⊃q').
Except in lines of proofs, most formulas of interest are displayed in both notations,
e.g., like this:
CCCCpqqrCCrsCps /
(((p→q)→q)→r)→((r→s)→(p→s)).
Within proofs, however, lines are shown only in Polish notation.
Typically, the only rule used in proofs
herein is C. A. Meredith's rule D of
condensed detachment, which combines the rule of detachment (i.e.,
modus ponens) with a small amount of substitution.
Briefly, D permits the inference, from a pair of formulas Cαβ
and α,
of the most general result
β'
obtainable--it is
unique, up to renaming of sentence letters--by detaching
α
(or a
substitution instance of α) from
Cαβ
(or a substitution instance of
Cαβ).
|