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 'pq' (or, where it is material implication that is at issue, 'pq').  Except in lines of proofs, most formulas of interest are displayed in both notations, e.g., like this:

CCCCpqqrCCrsCps    /    (((pq)q)r)((rs)(ps)).

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αβ).


Dolph Ulrich, 2007 


| Entrance page | Home page | Twenty-six open questions |

Single axioms for:  | BCI | 4 subsystems of BCI | monothetic BCI | C-pure R | C-pure R-Mingle | C-pure LNo |
   
| BCK | C-pure intuitionism | Classical equivalence | A few more systems |

| D-complete axioms for (classical) equivalence | Exit page |