Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Advances in natural deduction : a celebration of Dag Prawitz’s work
Pereira L., Haeusler E., de Paiva V., Springer Publishing Company, Incorporated, Dordrecht, the Netherlands, 2014. 310 pp. Type: Book (978-9-400775-47-3)
Date Reviewed: Aug 1 2014

Natural deduction was proposed as a formalization of classical reasoning that could mirror the use of assumptions as used in mathematical reasoning. Initial formulations toward that goal were made by Lukasiewicz and Jaskowski in the late 1920s, but two logicians had a definitive impact in the area. One was Gentzen, who in 1934 proposed the discipline of introduction and elimination rules for each logical connective, but did not succeed in proving the existence of normal-form proofs. The other is Dag Prawitz, who in 1965 finally proved the normalization of classical and intuitionistic proofs. It was later shown that there exists a close connection between Prawitz’s normalized proofs and the Curry-Howard isomorphism between proofs as lambda terms, in which normal proofs are associates with irreducible, normal-form lambda terms.

This book had its genesis at a seminar in Rio de Janeiro, in 2001, celebrating the work of Dag Prawitz. It is a collection of 12 papers from several active researchers in the area, combining and composing the mathematical, philosophical, computational, and linguistic aspects of the work initiated by Prawitz. This review highlights four of these papers.

The first paper, “Generalized Elimination Inferences, Higher-Level Rules, and the Implication-as-Rules Interpretation of the Sequent Calculus,” by Peter Schroeder-Heister, investigates higher-level elimination rules in which structured proofs are hypothesized (as opposed to standard-level elimination rules in which only formulas are hypothesized). Several properties of these generalized proofs, such as strong uniformity and closure, are presented. Then these ideas are moved from natural deduction proofs to Gentzen’s sequent calculus, in which a new view of implication-as-rules is discussed. A weak form of cut elimination is shown to hold for such systems, which is also related to natural deduction normal-form proofs. The paper finishes with a discussion of the conceptual merits of the implication-as-rules interpretation vis-à-vis the more usual implication-as-links, concluding that the former is both more plausible and more elementary than the latter.

The Curry-Howard isomorphism lies at the basis of the eight logics that are the vertices of Barendregt’s cube, which is studied by Jonathan Seldin in “Type Theories from Barendregt’s Cube for Theorem Provers.” The whole paper explores the expressive power of those logics. Initially, all logics in the cube are shown to be consistent and able to represent its consistency, but not to prove it. Furthermore, by adding the consistency statement as an unproven assumption, as well as by adding another very simple unproven assumption that allows for double negation elimination, arithmetic is shown to be expressible, and thus the logics are recursively complete. Furthermore, some logics in the cube are shown to represent sets and basic set assumptions. The conclusion is that Barendregt’s cube, with the addition of two simple and small unproven axioms, generates a very simple bit expressive logic system that is provably consistent and is sufficient for a lot of mathematical reasoning.

The largest contribution to the collection is Gianluigi Bellin’s “Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory,” which studies the representation of hypotheses and expectations, as well as declarative statements, using bi-intuitionistic logic. This logic composes traditional intuitionistic reasoning (logic of assertions) with co-intuitionistic logic (logic of hypotheses), in which the proof theory is developed by a sequent calculus with a unary antecedent and many-place consequent. This logic can also be mapped into a modal logic S4, such that bi-intuitionistic logic is translated into a S4 bimodal logic. In fact, by varying the forms of interactions between intuitionistic and co-intuitionistic connectives, several bi-intuitionistic logics are definable. Sequent calculi for three of these logics are proposed. It is shown that safe expectations and conjectures are dual concepts, and that a logic with safe expectations (defined in modal terms) is classical, that is, obtains double negation elimination. A semantics for bi-intuitionistic logic is presented in terms of rough sets, a topological concept coupled with an equivalence relation in which two sets are roughly equal if they have the same interior and the same closure (modulo the equivalence relation). The proof theory of bi-intuitionistic logic is then presented, and co-intuitionistic deductions are shown to enjoy normalization and therefore the subformula property as well. Finally, a form of Curry-Howard isomorphism is shown to hold for bi-intuitionistic proofs.

The last contribution this review will cover is a paper by Prawitz: “An approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited.” Prawitz discusses a still open conjecture he formulated in the early 1970s, according to which the usual introduction and elimination intuitionistic rules are maximal in the sense that the elimination rules are determined by the semantics induced by the introduction rules. The greatest difficulty of proving that conjecture lies in the formalization of it. Prawitz discusses two existing approaches and proposes a new one. In that new formulation, the notion of validity is defined in terms of interpreted proof terms instead of in terms of usual definition base in arguments. The conjecture itself is not proved, but we can see that Prawitz’s work continues to open new paths for investigation.

Reviewer:  Marcelo Finger Review #: CR142576 (1411-0938)
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Learning (I.2.6 )
 
Would you recommend this review?
yes
no
Other reviews under "Deduction And Theorem Proving": Date
Noninteractive zero-knowledge
Blum M., De Santis A., Micali S., Persiano G. SIAM Journal on Computing 20(6): 1084-1118, 1991. Type: Article
Jan 1 1993
Cut elimination and automatic proof procedures
Zhang W. Theoretical Computer Science 91(2): 265-284, 1991. Type: Article
Apr 1 1993
A non-reified temporal logic
Bacchus F., Tenenberg J., Koomen J. Artificial Intelligence 52(1): 87-108, 1991. Type: Article
Oct 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy