A sequent calculus for a logic of contingencies

We introduce a sequent calculus that is sound and complete with respect to propositional contingencies, i.e., formulas which are neither provable nor refutable. Like many other sequent and natural deduction proof systems, this calculus possesses cut elimination and the subformula property and has a simple proof search mechanism.     

Chunk and Permeate,a Paraconsistent Inference Strategy. Part I: The Infinitesimal Calculus

In this paper we introduce a paraconsistent reasoning strategy, Chunk and Permeate. In this, information is broken up into chunks, and a limited amount of information is allowed to flow between chunks. We start by giving an abstract characterisation of the strategy. It is then applied to model the reasoning employed in the original infinitesimal calculus. The paper next establishes some results concerning the legitimacy of reasoning of this kind – specifically concerning the preservation of the consistency of each chunk – and concludes with some other possible applications and technical questions.     

Gentzen-Type Methods for Bilattice Negation

A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension of CL) and CLS_cw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect to phase semantics, for SLK (a conservative extension and fragment of LK and CLS_cw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw, respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi into LK, S4 and CL.     

Towards a Semantic Characterization of Cut-Elimination

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.     

A Phenomenological Calculus for Anisotropic Systems

The phenomenological calculus is a relational paradigm for complex systems, closely related in substance and spirit to Robert Rosen’s own approach. Its mathematical language is multilinear algebra. The epistemological exploration continues in this paper, with the expansion of the phenomenological calculus into the realm of anisotropy.     

Program Extraction from Normalization Proofs

This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.