Proof-finding algorithms for classical and subclassical propositional logics (Q1049689): Difference between revisions

The Curry-Howard isomorphism allows proofs and theorems of intuitionistic implicational logic to be represented as combinators or lambda-terms and their types. The results in this paper rely on work by Trigg, Hindley and Bunder who showed that, for a large class of logics weaker than intuitionistic implication logic, proofs can be represented by restricted classes of lambda terms or combinators. This work was used by Bunder to develop proof-finding algorithms, most of which have a bound on the number of steps required to produce a \(\lambda\)-term proof, or a guarantee that there is no proof, based on the structure of the formula being examined. In this paper, the authors extend these algorithms to the following logics with additional connectives: {\parindent5mm \begin{itemize}\item[1)] Logics with minimal negation, i.e.\ extensions obtained by adding a constant type \(f\), which is used to define minimal negation. \newline A general class of Q-logics (Q-type theory), called MQ-logics -- which include connectives defined using \(f\), and, in particular, also minimal negation -- is introduced. A proof-finding algorithm for MQ-logics is given. \newline Intuitionistic versions of the relevance logics \(R_{\rightarrow}\) and \(T_{\rightarrow}\) are among the logics to which this algorithm applies. \item[2)] Logics with implication and intuitionistic negation, i.e.\ extensions of type theory to include the axiom \(\vdash F: f \rightarrow \alpha\). (Here, \(F\) is treated as a combinator with \(f \rightarrow \alpha\) as its type.) \item[3)] Implicational logics with Peirce's Law and minimal negation, i.e.\ extensions with a ``combinator'' \(P\) with Peirce's Law as its type. \item[4)] Full classical propositional logic (based on the types of \(F\) and \(P\) and of the standard combinators \(K\) and \(S\)). \end{itemize}}