Substitution Rules with Respect to a Context

  • Michal FaitEmail author
  • Marie Duží
Conference paper
Part of the Lecture Notes in Electrical Engineering book series (LNEE, volume 554)


In this paper, we deal with Leibniz’s rule of substitution of identicals, and describe how the rule can be applied in the TIL-Script language. The main goal is to introduce the algorithm of valid application of the substitution rules in all the three kinds of context that we distinguish in the TIL-Script language. The language is a computational variant of TIL, which is a hyperintensional, partial typed Open image in new window -calculus. Hyperintensional, because the meaning of TIL Open image in new window -terms are procedures producing functions rather than the denoted functions themselves. Partial, because TIL is a logic of partial functions, and typed, because all the entities of TIL ontology receive a type. Based on the results of context recognition the algorithm makes it possible to validly apply the substitution rules and derive relevant new pieces of analytic information.


TIL Substitution rules Three kinds of context TIL-Script Algorithm of valid substitution 



This research was supported by the Grant Agency of the Czech Republic, project No. GA18-23891S “Hyperintensional Reasoning over Natural Language Texts”, by the internal grant agency of VSB-Technical University of Ostrava, project No. SP2018/172, “Application of Formal Methods in Knowledge Modelling and Software Engineering”, and also by the Moravian-Silesian region within the program “Support of science and research in Moravian-Silesian region 2017” (RRC/10/2017).


  1. 1.
    Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics 103), 2nd edn. North-Holland, Amsterdam (1985)Google Scholar
  2. 2.
    Duží, M., Jespersen, B., Materna, P.: Procedural Semantics for Hyperintensional Logic. Foundations and Applications of Trasnsparent Intensional Logic. Springer, Berlin (2010)CrossRefGoogle Scholar
  3. 3.
    Duží, M.: Extensional logic of hyperintensions. In: Lecture Notes in Computer Science, vol. 7260, pp. 268–290 (2012)Google Scholar
  4. 4.
    Duží, M.: Towards an extensional calculus of hyperintensions. Organon F 19(1), 20–45 (2012)zbMATHGoogle Scholar
  5. 5.
    Duží, M.: Structural isomorphism of meaning and synonymy. Computacion y Sistemas 18(3), 439–453 (2014)Google Scholar
  6. 6.
    Duží, M.: If structured propositions are logical procedures then how are procedures individuated? Synthese special issue on the Unity of propositions (2017).
  7. 7.
    Duží, M., Fait, M.: The algorithm of context recognition in TIL. In: Rychlý, P., Horák, A., Rambousek, A. (eds.) 10th Workshop on Recent Advances in Slavonic Natural Language Processing, RASLAN 2016, pp. 51–62. Tribun, EU s.r.o (2016)Google Scholar
  8. 8.
    Duží, M., Fait, M., Menšík, M.: Context recognition for a hyperintensional inference machine. In: The AIP Proceeding of ICNAAM 2016, International Conference of Numerical Analysis and Applied Mathematics, vol. 1863 (2017). Article No. 330004Google Scholar
  9. 9.
    Duží, M., Materna, P.: Validity and applicability of Leibniz’s law of substitution of identicals. In: Arazim, P., Lavička, T. (eds.) The Logica Yearbook 2016, pp. 17–35. College Publications, London (2017)Google Scholar
  10. 10.
    Duží, M., Jespersen, B.: An intelligent question-answer system over natural-language texts. In: These Proceedings (2018)Google Scholar
  11. 11.
    Faroldi, F.L.G.: Co-hyperintensionality. Ratio 30(3), 270–287 (2017)CrossRefGoogle Scholar
  12. 12.
    Jespersen, B., Carrara, M., Duží, M.: Iterated privation and positive predication. J. Appl. Log. 25, S48–S71 (2017)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Nolan, D.: Hyperintensional Metaphysics. Philos. Stud. 171(1), 149–160 (2014)CrossRefGoogle Scholar
  14. 14.
    Revesz, G.E.: Lambda-Calculus, Combinators, and Functional Programming. Cambridge University Press, Cambridge, reprinted 2008 (1988)Google Scholar
  15. 15.
    Tichý, P.: The Foundations of Frege’s Logic. Walter de Gruyter, Berlin (1988)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Department of Computer Science FEIVŠB-Technical University of OstravaOstravaCzech Republic

Personalised recommendations