Skip to main content
SpringerLink
Log in
Book cover

Indian Conference on Logic and Its Applications

ICLA 2019: Logic and Its Applications pp 121–131Cite as

Satisfaction Classes via Cut Elimination

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11600))

Abstract

We present a construction of a satisfaction class in an arbitrary countable recursively saturated models of first-order arithmetic. Our construction is fully classical, namely, it employs nothing more than the classical techniques of formal proof theory.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Notes

  1. 1.

    See [5]. For an overview, see also [4, 6].

  2. 2.

    In their proof it is assumed that arithmetic is formulated in the relational language. See [1] for extending the result to the language with function symbols.

  3. 3.

    This is the first difference between our proof and the original KKL’s construction.

  4. 4.

    Proof systems with similar infinitary rules have already been studied in the literature in the context of cut elimination. See, for example, [9].

  5. 5.

    This will happen if all the numerical instantiations of \(\varphi (x)\) are seen as false by the model, that is, if for all numerals a, the sentence \(\lnot \varphi (a)\) belongs to T.

  6. 6.

    Without cut, (Tr-Lit) is the only rule that permits us to eliminate sentences in the proof and (Tr-Lit) can eliminate literals only.

  7. 7.

    Thus, sequents which are initial in P have height 0 and the maximal height of a sequent in P is not larger than the height of P.

  8. 8.

    Here the argument proceeds by cases, corresponding to various ways in which elements of \(Sent_{i}\) can be obtained from elements of \(Sent_{i+1}\).

  9. 9.

    The case of the existential mix formula is closely analogous and I do not discuss it separately.

References

  1. Cieśliński, C.: The Epistemic Lightness of Truth: Deflationism and its Logic. Cambridge University Press, Cambridge (2017)

    Book  Google Scholar 

  2. Enayat, A., Visser, A.: New constructions of satisfaction classes. In: Achourioti, T., Galinon, H., Martínez Fernández, J., Fujimoto, K. (eds.) Unifying the Philosophy of Truth. LEUS, vol. 36, pp. 321–335. Springer, Dordrecht (2015). https://doi.org/10.1007/978-94-017-9673-6_16

    Chapter  Google Scholar 

  3. Gentzen, G.: Investigations into logical deduction. Am. Philos. Q. 1(4), 288–306 (1964)

    Google Scholar 

  4. Kotlarski, H.: Full satisfaction classes: a survey. Notre Dame J. Formal Logic 32(4), 573–579 (1991)

    Article  MathSciNet  Google Scholar 

  5. Kotlarski, H., Krajewski, S., Lachlan, A.: Construction of satisfaction classes for nonstandard models. Can. Math. Bull. 24(3), 283–293 (1981)

    Article  MathSciNet  Google Scholar 

  6. Kotlarski, H., Ratajczyk, Z.: Inductive full satisfaction classes. Ann. Pure Appl. Logic 47(3), 199–223 (1990)

    Article  MathSciNet  Google Scholar 

  7. Krajewski, S.: Non-standard satisfaction classes. In: Marek, W., Srebrny, M., Zarach, A. (eds.) Set Theory and Hierarchy Theory: A Memorial Tribute to Andrzej Mostowski. LNM, vol. 537, pp. 121–144. Springer, Heidelberg (1976). https://doi.org/10.1007/BFb0096898

    Chapter  Google Scholar 

  8. Robinson, A.: On languages which are based on non-standard arithmetic. Nagoya Math. J. 22, 83–117 (1963)

    Article  MathSciNet  Google Scholar 

  9. Yasugi, M.: Cut elimination theorem for second order arithmetic with the \({\Pi }^{1}_{1}\)-comprehension axiom and the \(\omega \)-rule. J. Math. Soc. Jpn. 22(3), 308–324 (1970)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

The author was supported by a grant from the National Science Centre in Cracow (NCN), project number 2017/27/B/HS1/01830.

Author information

Authors and Affiliations

  1. Institute of Philosophy, University of Warsaw, Warsaw, Poland

    Cezary Cieśliński

Authors
  1. Cezary Cieśliński
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cezary Cieśliński .

Editor information

Editors and Affiliations

  1. Indian Institute of Technology Indore, Madhya Pradesh, India

    Md. Aquil Khan

  2. Indian Institute of Technology Goa, Goa, India

    Amaldev Manuel

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer-Verlag GmbH Germany, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cieśliński, C. (2019). Satisfaction Classes via Cut Elimination. In: Khan, M., Manuel, A. (eds) Logic and Its Applications. ICLA 2019. Lecture Notes in Computer Science(), vol 11600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-58771-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-58771-3_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-58770-6

  • Online ISBN: 978-3-662-58771-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation