Abstract
Various forms of mathematical induction (induction for natural numbers, transfinite induction, structural induction, well-founded induction, Noetherian induction, etc.) are applicable to domains with some kinds of order. This naturally leads to the questions about the possibility of unification of different inductions and their generalization to wider classes of ordered domains. In the paper we propose a common framework for formulating induction proof principles in various structures and apply it to partially ordered sets. In this framework we propose a fixed induction principle which is indirectly applicable to the class of all posets. In a certain sense, this result provides a solution to the problem of formulating a common generalization of a number of well-known induction principles for discrete and continuous ordered structures.
Similar content being viewed by others
Notes
FO means first-order in the extended signature \(\Sigma ^{\texttt {P}}_{\texttt {H}}\) (not in \(\Sigma \)).
References
Gunderson, D.: Handbook of Mathematical Induction. Chapman and Hall/CRC, Theory and Applications (2010)
Wiedijk, F. (ed.): The Seventeen Provers of the World. Foreword by Dana S. Scott. Lecture Notes in Artificial Intelligence, vol. 3600. Springer (2006)
Formal Methods in Computing Handbook, 3rd edition. CRC Press (2014)
Smith, P.: An Introduction To Gödel’s Theorems, 2nd edn. Cambridge University Press, Cambridge (2013)
Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3–80 (2000)
Taylor, P.: Towards a Unified Treatment of Induction (1996)
Stratulat, S.: A Unified View of Induction Reasoning for First-Order Logic. Turing-100, The Alan Turing Centenary Conference, Jun 2012, Manchester, United Kingdom (2012)
Clark, P.: The instructor’s guide to real induction. Math. Mag. 92, 136–150 (2019)
Clark, P.: The instructor’s guide to real induction (2012). arXiv:1208.0973
Kalantari, I.: Induction over the continuum. In: Friend, M., Goethe, N.B., Harizanov, V.S. (eds.) Induction, Algorithmic Learning Theory, and Philosophy, pp. 145–154. Springer, Berlin (2007)
Problem of induction. http://www.britannica.com/topic/problem-of-induction
Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Proceedings of LICS’18, pp. 819–828 (2018)
Signature in logic. http://ncatlab.org/nlab/show/signature+(in+logic)
Buss, S.R.: An introduction to proof theory. In: Buss, S.R. (ed.) Handbook of Proof Theory. Elsevier, Amsterdam (1998)
McKinley, R.: Proof nets for Herbrand’s theorem. ACM Trans. Comput. Logic 14(1), 1–31 (2013)
Ralph, B.: A Natural Proof System for Herbrand’s Theorem. Lecture notes in computer science, vol. 10703, pp. 1–20 (2018)
Jech, T.: Set Theory. Springer, Third Millenium edition (2003)
Ferlez, J., Cleaveland, R., Marcus, S.: Generalized Synchronization Trees. Lecture notes in computer science, vol. 8412, pp. 304–319. Springer (2014)
Cuijpers, P.: Prefix orders as a general model of dynamics. In: Proceedings of the 9th International Workshop on Developments in Computational Models, pp. 25–29 (2013)
Raoult, J.-C.: Proving open properties by induction. Inf. Process. Lett. 29, 19–23 (1988)
A principle of mathematical induction for partially ordered sets with infima. http://mathoverflow.net/questions/38238
Ivanov, I.: On induction for diamond-free directed complete partial orders. In: Proceedings of the 16th international conference on ICT in education, research and industrial applications. integration, harmonization and knowledge transfer, volume 2: workshops. CEUR-WS.org, vol. 2732, pp. 70–73 (2020)
Ogawa, M., Sternagel, C.: Open induction. Archive of Formal Proofs (2012). https://isa-afp.org/entries/Open_Induction.html
Ivanov, I.: On induction principles for diamond-free partial orders. Commun. Comput. Inf. Sci. 1308, 166–190 (2021)
Author information
Authors and Affiliations
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This work was the recipient of Ukrainian Logic Society Prize, 2021.
Appendix A: Isabelle Formalization for Sect. 3.2
Appendix A: Isabelle Formalization for Sect. 3.2
Rights and permissions
About this article
Cite this article
Ivanov, I. On Induction Principles for Partial Orders. Log. Univers. 16, 105–147 (2022). https://doi.org/10.1007/s11787-022-00296-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11787-022-00296-7