Proof-finding algorithms for classical and subclassical propositional logics
type: Item
instance of: scholarly article
title: Proof-finding algorithms for classical and subclassical propositional logics
zbMATH Open document ID: 1202.03024
DOI: 10.1215/00294527-2009-011
author: R. M. Rizkalla
author: Martin W. Bunder
published in: Notre Dame Journal of Formal Logic
publication date: 2010-01-13T00:00:00Z
review text: 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}}
reviewed by: Viorica Sofronie-Stokkermans
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B47
zbMATH DE Number: 5657219
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1215/00294527-2009-011
OpenAlex ID: W1998289751
description: scientific article; zbMATH DE number 5657219