2

In the intuitionistic natural deduction (NJ) we have a nice symmetry : each logical connective has an introduction rule and an elimination rule.

But when we want to switch to classical logic (NK) we have to add some rules to be able to prove classical properties like the Peirce Law, the excluded middle and such. Therefore, we break the symmetry we had.

Why is it an interesting thing to state ? Is there something wrong with that ?

Maybe it has something to do with proof normalization or another technical detail ?

Improve this question
2
  • No, and I'm not so sure about the symmetry... In both NJ and NK all conncetives (except negation) have intro- ed elim-rules, with a "perfect symmetry". Then you add EFQ : ⊥ ⊢ A to have NJ. If instead we add RAA : [¬A] ...⊥ ⊢ A we get NK. In NK, from RAA we get EFQ: thus, a perfect symmetry is not present... The rules for negation are dispensable in NJ (with the def ¬A = A → ⊥) while in NK we have to use ¬ anyway for RAA. If instead we have it as primitive in NK, they are not expressed with a intro- ed elim- couple.
    – Mauro ALLEGRANZA
    Commented Mar 5, 2017 at 19:42
  • See the post What is the “correct” reading of ⊥ ? as well as Natural Deduction rules for ¬ in classical and intuitionstic logic for a discussion.
    – Mauro ALLEGRANZA
    Commented Mar 5, 2017 at 19:44

2 Answers 2

Reset to default
3

The symmetry between introduction and elimination rules for the logical constants is called harmony. The idea of logical harmony has been defended by several logicians, including Gentzen and Prawitz, as being a requirement for a proof-theoretic justification of logic. Harmony guarantees that the introduction of a logical constant is conservative with respect to implication. Michael Dummett has taken the argument further and claimed that any language, including natural languages like English, should have harmonious and stable rules for its terms. Dummett proceeds on this basis to argue that since classical negation is not harmonious, it has no defensible meaning, and he takes this to be an argument for adopting intuitionism and a verification based semantics for language.

These claims are disputed. Ian Rumfitt argues that harmony is overkill as a condition of admissability, and that defective logical constants such as Arthur Prior's 'tonk' can be ruled out because they lack truth conditions.

There is quite a good explanation of this issue in Nils Kurbis "Proof-Theoretic Semantics, a Problem with Negation and Prospects for Modality" Journal of Philosophical Logic 44 (6):713-727 (2015) which can be found on PhilPapers.org at https://philpapers.org/rec/KRBPSA

Other useful references are: Steinberger, F. (2011) “What harmony could and could not be”. Australasian Journal of Philosophy 89: 617-639; and Rumfitt, Ian (2016) “Against Harmony”. Forthcoming in Robert Hale, Crispin Wright, and Alexander Miller, eds., The Blackwell Companion to the Philosophy of Language, 2nd edition. Oxford: Blackwell.

Improve this answer
2
  • Thanks for you answer ! Do you have more general references on the proof-theoretic justification of logic for instance and what you call "verification-based semantics for language" ?
    – Boris
    Commented Mar 6, 2017 at 18:33
  • 1
    The mature statement of Michael Dummett's position can be found in his book, The Logical Basis of Metaphysics, Harvard UP, 1991. For Prawitz's view, see Dag Prawitz, The epistemic significance of valid inference, Synthese, Vol. 187, No. 3, 2012, pp. 887-898.
    – Bumble
    Commented Mar 6, 2017 at 23:32
0

Honestly, I don't see the symmetry of NJ you are referring to. There may be some symmetries in the introduction and elimination rule for "and", perhaps even for "implication", but calling the rules for "or" symmetric feels strange.

But you can get a similar symmetry as in the sequent calculus by using the rule

A -> (B V C)
------------
(A -> B) V C

for characterising classical logic. This is independent of issues related to negation and falsehood.

Improve this answer
1
  • In Girard's Proofs and Types we can read the following quotes about the natural deduction : "The deep symmetry of the calculus is shown by the introduction and elimination rules which match each other exactly" and "The fundamental symmetry of the system is the introduction/elimination symmetry, which replaces the hypothesis/conclusion symmetry that cannot be implemented in this context.". It's the symmetry I'm referring to.
    – Boris
    Commented Mar 6, 2017 at 18:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .