# Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning

In We Will Show Them! Essays in Honour of Dov Gabbay, volume 1. pp. 701-null (2005)
 Abstract In this paper we make some observations about Natural Deduction derivations [Prawitz, 1965, van Dalen, 1986, Bell and Machover, 1977]. We assume the reader is familiar with it and with proof-theory in general. Our development will be simple, even simple-minded, and concrete. However, it will also be evident that general ideas motivate our examples, and we think both our specific examples and the ideas behind them are interesting and may be useful to some readers. In a sentence, the bare technical content of this paper is: Extending natural deduction with global well-formedness conditions can neatly and cheaply capture classical and intermediate logics. The interest here is in the ‘neatly’ and ‘cheaply’. By ‘neatly’ we mean ‘preserving proof-normalisation’,1 and ‘maintaining the subformula property’, and by ‘cheaply’ we mean ‘preserving the formal structure of deductions’ (so that a deduction in the original system is still, formally, a deduction in the extended system, and in particular it requires no extra effort to write just because it is in the extended system). To illustrate what we have in mind consider intuitionistic first-order logic (FOL) [van Dalen, 1986] as a paradigmatic example of a formal notion of deduction. A natural deduction derivation (or deduction) is an inductively defined tree structure where each node contains an instance of a formula. A deduction is valid when each successive node follows from its predecessors in accordance with some predetermined inference rules. A particular attraction of Natural Deduction is its clean and economical presentation. Here for example are deduction (fragments) proving A ∧ B from A and B, and ∀x. (P (x) ∧ Q(x)) from ∀x. P (x) and ∀x. Q(x): ∀x. P (x) (∀E). Keywords No keywords specified (fix it) Categories (categorize this paper) Options Save to my reading list Follow the author(s) Edit this record My bibliography Export citation Mark as duplicate Request removal from index
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 30,133

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
References found in this work BETA

No references found.

Citations of this work BETA

No citations found.

Similar books and articles
The Proof Structure of Kant's A-Deduction.Michael Barker - 2001 - Kant-Studien 92 (3):259-282.
Natural Deduction for First-Order Hybrid Logic.Torben BraÜner - 2005 - Journal of Logic, Language and Information 14 (2):173-198.
A Brief History of Natural Deduction.Francis Jeffry Pelletier - 1999 - History and Philosophy of Logic 20 (1):1-31.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
Harmonising Natural Deduction.Hartley Slater - 2008 - Synthese 163 (2):187 - 198.
A Natural Deduction System for First Degree Entailment.Allard Tamminga & Koji Tanaka - 1999 - Notre Dame Journal of Formal Logic 40 (2):258-272.