Skip to main content
SpringerLink
Log in

About Truth and Types

  • Chapter
  • First Online:
Advances in Proof Theory

Part of the book series: Progress in Computer Science and Applied Logic ((PCS,volume 28))

Abstract

We investigate a weakening of the classical theory of Frege structures and extensions thereof which naturally interpret (predicative) theories of explicit types and names à la Jäger.

Dedicated to Gerhard Jäger on occasion of his 60th birthday.

This paper originates from the slides for the talk presented at the Jäger conference, Bern, December 12–13, 2013. We wish to thank the organizers for the nice hospitality. Thanks to an anonymous referee for comments and criticism.

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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.

    E.g. \(\dot{\exists }f:=\dot{\lnot }(\dot{\forall }(\lambda x.\dot{\lnot }(fx)))\); \(\dot{\rightarrow }\) is assumed as primitive in Sect. 4.

  2. 2.

    We use the standard abbreviations \(\langle t,s \rangle :=\mathsf {PAIR}ts\); \((t)_0:=\mathsf {LEFT}t \), \((t)_1:=\mathsf {RIGHT}t\). Below 1, 2, ... stand for the corresponding numerals.

  3. 3.

    Among them \(\mathsf {nat}\), \(\mathsf {id}\), \(\mathsf {co}\), \(\mathsf {int}\), \(\mathsf {inv}\), \(\mathsf {dom}\); we leave the obvious statement to the reader, in analogy to (3), (4).

  4. 4.

    This makes sense, since we can identify individual variables of \(\mathbf {{EET}}\) with \(\mathbf {CT}\)-variables with odd indices, and type variables of \(\mathbf {{EET}}\) with \(\mathbf {CT}\)-variables with even indices.

  5. 5.

    Concerning (32), we are thus left only with \(\forall x P([P(x)])\).

  6. 6.

    NB: this operator is distinct from \(\mathcal {C}(x,-)\) of Remark 1 and schema (18), since it embodies the initial condition ensuring P[(P(x))].

  7. 7.

    Hence (3), (4) are expanded so as to include \(\dot{\rightarrow }\).

  8. 8.

    This is a sequential conjunction introduced by Aczel in [1].

  9. 9.

    Indeed Feferman [10], noting that Aczel’s approach is based on \(\lambda \)-calculus which allows for more general interpretations, adds that “further work on systems like \(\mathbf {{DT}}\) might usefully incorporate similar features.”

  10. 10.

    Recall footnote 2 of Sect. 2.4: think of \(\langle a,b \rangle \), \((u)_0\), \((u)_1\) as values of the terms \(\mathsf {\mathsf {PAIR}} a b \), \(\mathsf {LEFT} u\), \(\mathsf {RIGHT} u\).

  11. 11.

    In the standard sense, see [25].

  12. 12.

    \(\mathbf {FL}\) is reminiscent of Feferman’s logic.

  13. 13.

    In general, if \(\Gamma :=\lbrace A_1,\ldots , A_q\rbrace \), \(\Gamma [m, n]:=\lbrace A_1[m,n],\ldots , A_q[m,n]\rbrace \).

  14. 14.

    For a precise definition, see [11].

  15. 15.

    See [26, 27].

  16. 16.

    This means: the set of all \(a\in \mathcal M\) satisfying T(I(A)x in \(\mathsf {MIN_M}\) is the least fixed point of the operator defined by A in \(\mathsf {MIN_M}\).

  17. 17.

    As for \(\mathbf {KF}\), a warning: we keep using the same label of [2] for a theory \({\mathbf {KF}}_\mu \), which is not an extension of Peano Arithmetic.

  18. 18.

    So \(\prec \) is determinate in the sense of (2).

  19. 19.

    We will not spell them explicitly for the sake of brevity.

References

  1. P. Aczel, Frege structures and the notions of proposition, truth and set, in The Kleene Symposium, ed. by J. Barwise, H.J. Keisler, K. Kunen (North Holland, Amsterdam, 1980), pp. 31–59

    Chapter  Google Scholar 

  2. J. Burgess, Friedman and the axiomatization of Kripke’s theory of truth, in Foundational Adventures: Essays in Honor of Harvey M. Friedman, ed by N. Tennant (College Publications, London, 2014), pp. 125–148

    Google Scholar 

  3. A. Cantini, Levels of implications and type free theories of partial classifications with approximation operator. Zeitschrift f. Math. Logik u. Grundlagen 38, 107–141 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  4. A. Cantini, P. Minari, Uniform inseparability in explicit mathematics. J. Symbolic Logic 61, 313–326 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  5. A. Cantini, On a Russellian paradox about propositions and truth, in One Hundred Years of Russell’s Paradox. Mathematics, Logic and Philosophy ed by G. Link (Walter de Gruyter, Berlin, 2004), pp. 259–284

    Google Scholar 

  6. A. Cantini, Logical Frameworks for Truth and Abstraction, Studies in Logic and the Foundations of Mathematics, vol. 135 (North Holland, Amsterdam, 1996)

    MATH  Google Scholar 

  7. B.A. Davey, H.A. Priestley, Introduction to Lattices and Order, 2nd edn. (Cambridge, 2002)

    Google Scholar 

  8. S. Eberhard, T. Strahm, Weak theories of truth and explicit mathematics, in Logic, Construction, Computation, ed. by U. Berger, H. Diener, P. Schuster (Ontos Verlag, 2012), pp. 156–183

    Google Scholar 

  9. S. Feferman, Constructive theories of operations and classes, in Logic Colloquium ’78 ed by M. Boffa, et al. (North-Holland, 1979), pp. 159–224

    Google Scholar 

  10. S. Feferman, Axioms for determinate truth. Rev. Symbolic Logic 1, 204–217 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  11. S. Feferman, Reflecting on incompleteness. J. Symbolic Logic 56, 1–49 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  12. S. Feferman, Does reductive proof theory have a viable rationale? Erkenntnis 53, 63–96 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  13. K. Fujimoto, Relative truth definability of axiomatic truth theories. Bull. Symbolic Logic 16, 305–344 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  14. R. Flagg, J. Myhill, Implication and analysis in classical Frege structures. Ann. Pure Appl. Logic 34, 33–85 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  15. H. Friedman, M. Sheard, An axiomatic approach to self-referential truth. Ann. Pure Appl. Logic 33, 1–21 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  16. T. Glass, On power set in explicit mathematics. J. Symbolic Logic 61, 468–489 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  17. V. Halbach, Axiomatic Theories of Truth (Cambridge University Press, Cambridge, 2011)

    Book  MATH  Google Scholar 

  18. G. Jäger, Type theory and explicit mathematics, in Logic Colloquium ’87, Studies in Logic and the Foundations of Mathematics, vol. 129 (North-Holland, Amsterdam, 1989), pp. 117–135

    Google Scholar 

  19. G. Jäger, Power types in explicit mathematics? J. Symbolic Logic 62, 1141–1146 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  20. G. Jäger, R. Kahle, A. Setzer, T. Strahm, The proof theoretic analysis of transfinitely iterated fixed point theories. J. Symbolic Logic 64, 53–67 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  21. G. Jäger, T. Strahm, Totality in applicative theories. Ann. Pure Appl. Logic 74, 105–120 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  22. R. Kahle, Truth in applicative theories. Studia Logica 68, 103–128 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  23. R. Kahle, T. Studer, A theory of explicit mathematics equivalent to \(ID_1\), in Computer Science Logic (Fischbachau), Lecture Notes in Computer Science, 1862 (Springer, Berlin, 2000), pp. 356–370

    Google Scholar 

  24. G.E. Leigh, Conservativity for theories of compositional truth via cut elimination. J. Symbolic Logic, 80, 845–865 (2015)

    Google Scholar 

  25. Y.N. Moschovakis, Elementary Induction on Abstract Structures, Studies in Logic and the Foundations of Mathematics, vol. 77 (North Holland, Amsterdam, 1974)

    Google Scholar 

  26. W. Pohlers, Proof Theory (Springer, Berlin-New York, 2009)

    MATH  Google Scholar 

  27. H. Schwichtenberg, S. Wainer, in Proofs and Computations, Perspectives in Logic (ASL and Cambridge University Press, Cambridge, 2012)

    Google Scholar 

  28. T. Strahm, Theories with self-application and computational complexity. Inf. Comput. 185, 263–297 (2003)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Lettere e Filosofia, Università degli Studi di Firenze, Florence, Italy

    Andrea Cantini

Authors
  1. Andrea Cantini
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrea Cantini .

Editor information

Editors and Affiliations

  1. Campus de Caparica DM FCT, Univ Nova de Lisboa, Caparica, Portugal

    Reinhard Kahle

  2. Inst.of Computer Sci. applied math., University of Bern, Bern, Switzerland

    Thomas Strahm

  3. Institute of Computer Science and A, University of Berne, Berne, Switzerland

    Thomas Studer

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Cantini, A. (2016). About Truth and Types. In: Kahle, R., Strahm, T., Studer, T. (eds) Advances in Proof Theory. Progress in Computer Science and Applied Logic, vol 28. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-29198-7_2

Download citation

Publish with us

Policies and ethics

Search

Navigation