Reductive logic

Reductive logic is a paradigm of symbolic logic where rules in a Proof calculus and system are thought of as operators on the syntax via their reductive readings. Given a Proof calculus for a Mathematical logic and formal logic, reductive proof-search is characterised precisely by the backward reading of rules in the calculus taking a putative conclusion to sufficient premises. The study of reductive logic aims to establish semantics (Denotational semantics and Operational semantics), for such procedures, and can therefore be regarded as the mathematical study of (reductive) proof-search.
== Concept ==
Logics are traditionally defined via a Formal language generated for grammar and an Mathematical induction defined Validity (logic)judgement acting as a calculus of inference. The inductive definition manifests the deductive paradigm of logic, where from established or supposed premises one proceeds to a conclusion, regulated by the application of inference rules e.g., 
\Downarrow	
{| style="margin:auto; text-align: center" border="0"	Established Premiss1 ... Established Premissn
 		
Conclusion		
A trace of inferences resulting is called a derivation, or a proof, of the last conclusion called the endsequent. In contrast, reductive inference proceeds from a putative (i.e., supposed) conclusion to sufficient premises, regulated by reduction operators,
\Uparrow 	
{| style="margin:auto; text-align: center" border="0"	Sufficent Premiss1 ... Sufficent Premissn
 		
Putative Conclusion		
Typically the reduction operators are the simply Admissible rule inferences applied in backward. The essential idea is summarised as follows:
# There is a logic \mathcal{L} with a proof-system LL;
# We have a putative conclusion which is an assertion in \mathcal{L}, and we would like to know whether or not the sequent is provable in LL;
# Each inference rule LL, including any admissible rules, gives rise to a reduction operator. To apply a reduction operator to particular assertion we must find an instance of a reduction operator such that instance of the putative conclusion matches the assertion;
# The assertions which must be proved in order to have a proof of the initial assertion, or sub-goals, are then given by the corresponding instances of the sufficient premises of the operator.
Reduction was first explained in these terms by Stephen Cole Kleene, but the first formal study of the subject in itself is attributed to a monograph by David Pym and Eike Ritter. Arguably the first theorems of reductive logic are Cut-elimination theorem|cut-elimination for LK and LJ, and the various Completeness theorem|completeness theorems of early formal logic.
Note, however, that a reduction may fail to yield a proof e.g., in LK one may encounter the sufficient premise p \implies q, for distinct atoms p and q. Such possible failures have no counterpart in deductive logic, but Automated theorem proving have to have strategies which ensure that a proof of a given endsequent is found if one exists. In general, not only the choice of reduction operators but also the order in which they are applied matters: the application of the same reduction operators in one order may yield a proof, where after applying the same reduction operators in a different order a completion to a proof may be impossible. As a consequence reductive logic has been characterised by the gestalt:
: Reductive Logic = Structure + Control
The structure component is the framework in which the proof-search procedure is performed; and control is the mechanism for regulating the behaviour of the computation e.g, the disjunct to process, goal to reduce, clause to Resolution (logic)|unify, or when to Backtracking. Majority of research has been focused on sequent calculi for Classical logic and Intuitionistic logic|intuitionistic logic, particularly with respect to the structure component. The reductive logic of non-classical logics e.g., Substructural logic, Bunched logic, and Modal logic, has not yet been studied; and no uniform mathematical background has been given for modelling control.
== Motivation ==
Theorem proving, or algorithmic proof-search, is both an essential enabling technology within the Computational science and of independent Philosophy and Mathematics interest. More specifically, in computing, many problems are formulated as judgements about formal texts, typical representable in logical formalisms. For example, well-formedness (parsing), well-typedness (Type checking|type-checking), as well as logical consequence (e.g., for specification and correctness) itself.
There are many useful Formal language and, for each language, typically many useful procedures for judging properties of sentences. As the complexity of the languages and their properties increases, the possibility of obtaining efficient, Computability theory and total procedures recedes, but Computable function and partial procedures which fail quickly are of great value and Proof assistant and interactive theorem provers, such as the Boyer-Moore theorem prover.Boyer-Moore system, the LCF theorem prover|LCF system and its derivatives, such Isabelle (proof assistant)|Isabelle, as well as more complex systems, such as Coq, based on Dependent type|dependent type theory, are used in a wide range of system-critical applications.
== Models ==
The inherent partiality of reductions presents a clear semantic difficulty i.e., how to interpret those reductions which cannot be completed to be proofs. Meanwhile, proofs as mathematical objects have been given general and rigours treatment though the Curry-Howard-Lambek correspondence theorem:
File:Curry-Howard-Lambek_Correspondence.pdf|center|frameless|331x331px
The advantage is that proofs become subject to the mathematical tools developed in the corresponding formalisms e.g., they can be reasoned about as a arrows in a Category theory|category. Research in reductive logic has largely focused on extending such models to the failed reductions.
== Notes ==
== References ==
* Pym, David J. and Ritter, Eike (2004). "Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control". Oxford University Press.
Category:Symbolic Logic
Category:Denotational semantics
Category:Mathematical induction