Skip to main content
SpringerLink
Log in

The Exact Intuitionistic Meaning of the Square of Opposition

  • Chapter
  • First Online:
The Square of Opposition: A Cornerstone of Thought

Part of the book series: Studies in Universal Logic ((SUL))

Abstract

This paper aims at providing a complete analysis of the intuitionistic version of the square of opposition and a reply to an article published by Mélès (Around and Beyond the Square of Opposition, ed. by J.-Y. Béziau, D. Jacquette (Studies in Universal Logic, Birkhaüser, 2012), pp. 201–218) on the same topic.

To David DeVidi and to Sean McLaughlin

Every theorem of this paper has been checked by IMOGEN i.e. Sean McLaughlin’ theorem prover for intuitionistic First Order Logic (https://github.com/seanmcl/imogen).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In this list, only (1.6) is an equivalence in IFOL: except this latter, all conjunctions, from (1.1) to (1.5) have a left component provable in CFOL but not in IFOL.

  2. 2.

    I do not mention the fork rule, because it is not used in this paper. I strongly recommend the reading of Bell et al.’s book.

  3. 3.

    Symbols \(\vdash _{c},\ \nvdash _{c},\ \vdash _{i},\ \nvdash _{i}\) mean respectively: provable in classical logic, unprovable in classical logic, provable in intuitionistic logic, unprovable in intuitionistic logic. I use in this paper the algorithm of refutation trees defined by Bell, DeVidi and Solomon for intuitionistic logic [1, pp. 192–223] (see Sect. 2.1).

  4. 4.

    By transitivity of implication (2.5) is deducible from Fig. 3; but it is true that the other sub-contrariety relation i.e. \(\neg (O) \rightarrow (I)\) is not intuitionistically provable. (See Table 2, page 36).

  5. 5.

    In this context, a “gap” can mean a blank, a missing value.

  6. 6.

    See David et al. [3, p. 156] and von Plato [5, p. 170].

  7. 7.

    Hence Kuroda’s translation recipe: put a double negation just before \(F\) and just before each scope of universal quantifiers in \(F\), e.g. if \(\forall x(Fx)\) is in F, it is translated by \(\forall x\neg \neg (Fx)\).

  8. 8.

    Kuroda’s translation is all what one needs as faithful translation of CFOL into IFOL. Gödel-Gentzen translation goes further because contrary to the former, it translates also classical logic into minimal logic, see [3, pp. 157–158].

  9. 9.

    To reply to a question asked by a referee, it is indeed possible to see this tree method for intuitionistic logic as an automated search of Kripke countermodels. A formula F is intuitionistically proved if and only if its refutation tree shows that it is not possible to give a Kripke countermodel for F, i.e. that the assumption that F is intuitionistically unprovable (i.e.?F) leads to a contradiction.

References

  1. J. Bell, G. Solomon, D. DeVidi, Logical Options: An Introduction to Classical and Alternative Logics (Broadview Press, Peterborough, 2001)

    Google Scholar 

  2. J.-Y. Béziau, D. Jacquette (eds.), Around and Beyond the Square of Opposition (Studies in Universal Logic, Birkhaüser, 2012)

    Google Scholar 

  3. R. David, K. Nour, C. Raffalli, Introduction à la Logique: Théorie de la Démonstration (Dunod, Paris, 2004)

    Google Scholar 

  4. B. Mélès, No group of opposition for constructive logics: the intuitionistic and linear cases, in Around and Beyond the Square of Opposition, ed. by J.-Y. Béziau, D. Jacquette (Studies in Universal Logic, Birkhaüser, 2012), pp. 201–218

    Chapter  Google Scholar 

  5. J. von Plato, Elements of Logical Reasoning (Cambridge University Press, Cambridge, 2013)

    Book  Google Scholar 

Download references

Acknowledgements

Many thanks to

• Baptiste Mélès both for the discussions we had about the intuitionistic version of the square of opposition and for his very useful remarks on a draft of my paper,

• Jean-Yves Béziau who gave to me the occasion of writing this paper,

• My institution, the Archives Poincaré, which funded my participation to the fourth conference on the square of opposition (Vatican, May 5–9, 2014),

• the referees of the final version of this paper.

Author information

Authors and Affiliations

  1. Philosophy Department, Lorraine University, Archives Poincaré - UMR 7117 - CNRS, 91 bd Libération, 54000, Nancy, France

    Joseph Vidal-Rosset

Authors
  1. Joseph Vidal-Rosset
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Joseph Vidal-Rosset .

Editor information

Editors and Affiliations

  1. Research Council, University of Brazil, Rio de Janeiro, Brazil

    Jean-Yves Béziau

  2. Faculty of Philosophy, Pontifical Lateran University, Rome, Italy

    Gianfranco Basti

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Vidal-Rosset, J. (2017). The Exact Intuitionistic Meaning of the Square of Opposition. In: Béziau, JY., Basti, G. (eds) The Square of Opposition: A Cornerstone of Thought. Studies in Universal Logic. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-45062-9_17

Download citation

Publish with us

Policies and ethics

Search

Navigation