A question regarding the meaning of propositional connectives in "natural deduction" and "tableaux method"

191 Views Asked by At

In Marcello D'Agostino & Dov Gabbay (editors), Handbook of Tableau Methods (1998) I've found in Ch.2 : Tableau Methods for Classical Propositional Logic, by Marcello D'Agostino, an interesting discussion on Tableaux and Natural Deduction (para 3.5, page 63-on).

The relevant point regards some examples and an argument

in favour of tableau methods versus natural deduction methods [...].In fact, natural deduction rules do not capture the classical meaning of the logical operators. This was already remarked in [Prawitz,1965], where the author pointed out that natural deduction rules are nothing but a reading of Heyting’s explanations of the constructive meaning of the logical operators [Heyting, 1956].

The argument of the author

illustrate our claim that ‘natural’ deduction is really natural only for intuitionistic tautologies (and not necessarily for all of them). The difficulties of natural deduction with classical tautologies depend on the fact that a sentence and its negation are not treated symmetrically, whereas this is exactly what one would expect from the classical meaning of the logical operators.

The tableau rules, on the contrary, treat a sentence and its negation symmetrically.

Is it possible to ask for some experts opinions and considerations (pro or contra) about the previous argument ?

2

There are 2 best solutions below

0
On BEST ANSWER

A comment about natural deduction and classical vs intuitionistic logic.

The notion in fact goes back to Gentzen that the introduction rules define the logical operators, and the elimination rules should be in harmony with the introduction rules (allowing us to extract no more from a proposition whose main operator is O than what the relevant introduction rule gives as the canonical grounds for such a proposition). And Gentzen himself already sees that this perspective at most justifies intuitionistic logic. He writes of the schema for double-negation elimination (equivalent of course to the law of excluded middle)

such a schema still falls outside the framework of the NJ-inference figures, because it represents a new elimination of the negation whose admissibility does not follow at all from our method of introducing the ¬ symbol by the ¬I [rule].

This it the theme picked up again by Prawitz, and also famously by the philosopher Michael Dummett, and later by Neil Tennant in their arguments for the special status of intuitionistic logic. (The thought is that, in some domains, we might also assent to the law of excluded middle, but that this isn't forced on us by logic but by a metaphysical assumption that in the relevant domains we are dealing with a world where things conspire to ensure that a proposition is indeed either determinately true or determinately false.)

However, when it comes to the details of working through this line, in particular to getting clear about the relevant notion of harmony between the introduction and elimination rules which classical logic supposedly offends while intuitionistic logic supposedly respects, things do get pretty complex. See for example, Peter Milne, Classical Harmony: Rules of inference and the Meaning of the Logical Constants, Synthese vol 100 (1994) 49-94, and Stephen Read, Harmony and Autonomy in Classical Logic, Journal of Philosophical Logic vol. 29 (2000) 123–154.

1
On

I agree that the natural part of natural deduction is the intuitionistic part, which must be supplemented, say by an axiom scheme $\phi\lor\neg\phi$ to obtain classical logic. Even with this less-natural supplement, though, I think natural deduction is easier for students to learn and use than tableau systems.