Abstract: This a research study about logic. Logic is both part of and has roles in many disciplines, including inter alia, mathematics, computing, and philosophy. The topic covered here — the mathematical theory of reductive logic and proof-search — draws upon the techniques and cultures of all three disciplines, but is mainly about mathematics and computation. Since its earliest presentations, mathematical logic has been formulated as a formalization of deductive reasoning: given a collection of hypotheses, a conclusion is derived. However, the advent of computational logic has emphasized the significance of reductive reasoning: given a putative conclusion, what are sufficient premises? Whilst deductive systems typically have a well-developed semantics of proofs, reductive systems are typically well-understood only operationally. Typically, a deductive system can be read as a corresponding reductive system. The process of calculating a proof of a given putative conclusion, for which non-deterministic choices between premises must be resolved, is called proof-search and is an essential enabling technology throughout the computational sciences. This study suggests that the reductive view of logic is as fundamental as the deductive view, and discusses some of the problems that must be addressed in order to provide a semantics of proof-searches of comparable value to the corresponding semantics of proofs. Just as the semantics of proofs is intimately related to the model theory of the underlying logic, so too should be the semantics of reductions and of proof-search. The study discusses how to solve the problem of providing a semantics for proof-searches in intuitionistic logic, which adequately models both not only the logical but also via an embedding of intuitionistic reductive logic into classical reductive logic, the operational aspects, i.e., control of proof-search, of the reductive system. It concludes with a naturally motivated example of our semantics of proof-search: a class of games.

Keywords: proof-search, computation, deductive reasoning, reductive reasoning, semantics of proofs, intuitionistic logic, classical reductive logic