Reductive logic

From Wikitia
Jump to navigation Jump to search

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.[1] 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.,

<math>\Downarrow</math>
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,

<math>\Uparrow</math>
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:[2]

  1. There is a logic <math>\mathcal{L}</math> with a proof-system LL;
  2. We have a putative conclusion which is an assertion in <math>\mathcal{L}</math>, and we would like to know whether or not the sequent is provable in LL;
  3. 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;
  4. 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[3], but the first formal study of the subject in itself is attributed to a monograph by David Pym and Eike Ritter.[2] 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 <math>p \implies q</math>, for distinct atoms <math>p</math> and <math>q</math>. 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:[2]

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,[4] the LCF theorem prover|LCF system and its derivatives,[5] such Isabelle (proof assistant)|Isabelle,[6] as well as more complex systems, such as Coq,[7] based on Dependent type|dependent type theory, are used in a wide range of system-critical applications.[8]

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.[2]

Notes

  1. ↑ Dalen, D. van (Dirk), 1932- (2004). Logic and structure (4th ed.). Berlin: Springer-Verlag. ISBN 3-540-20879-8. OCLC 54529334.{{cite book}}: CS1 maint: multiple names: authors list (link)
  2. ↑ 2.0 2.1 2.2 2.3 Pym, David J. (2004). Reductive logic and proof-search : proof theory, semantics, and control. Ritter, Eike. Oxford, UK: Clarendon Press. ISBN 0-19-852633-4. OCLC 54865392.
  3. ↑ Kleene, Stephen Cole, 1909-1994. (1967). Mathematical logic. New York. ISBN 0-471-49033-4. OCLC 523472.{{cite book}}: CS1 maint: location missing publisher (link) CS1 maint: multiple names: authors list (link)
  4. ↑ Boyer, R. S.; Kaufmann, M.; Moore, J. S. (1995-01-01). "The Boyer-Moore theorem prover and its interactive enhancement". Computers & Mathematics with Applications. 29 (2): 27–62. doi:10.1016/0898-1221(94)00215-7. ISSN 0898-1221.
  5. ↑ Boyer, Robert S.; Moore, J Strother (1988), "Mechanized Proofs in the Logic", A Computational Logic Handbook, Elsevier, pp. 167–175, doi:10.1016/b978-0-12-122952-8.50010-x, ISBN 978-0-12-122952-8
  6. ↑ Carbonell, Jaime G. (2002). Isabelle : a Proof Assistant for Higher-Order Logic. Springer Berlin Heidelberg. ISBN 978-3-540-45949-1. OCLC 958524177.
  7. ↑ "Proof Search by Logic Programming", Certified Programming with Dependent Types, The MIT Press, 2013, doi:10.7551/mitpress/9153.003.0017, ISBN 978-0-262-31787-0
  8. ↑ Schneier, Bruce. (2015). Secrets and lies : digital security in a networked world. John Wiley & Sons. ISBN 978-1-119-09243-8. OCLC 911788931.

References

This article "Reductive logic" is from Wikipedia. The list of its authors can be seen in its historical. Articles taken from Draft Namespace on Wikipedia could be accessed on Wikipedia's Draft Namespace.

  • Pym, David J. and Ritter, Eike (2004). "Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control". Oxford University Press.
Retrieved from "https://wikitia.com/index.php?title=Reductive_logic&oldid=53267"