An important goal of this chapter is to provide a clear, understandable picture of constructive inverse semigroups with apartness in the Errett Bishop’s style of constructive mathematics, BISH. The theory of constructive semigroup with apartness is a new approach to semigroup theory (and not a new class of semigroups). It presents novelty within both mathematics: classical and constructive. The theory of semigroups with apartness was developed by M. Mitrović and co-authors: M. N. Hounkonnou, M. A. Baroni, S. Crvenković, D. A. Romano, and S. Silvestrov; see, for example, Crvenković et al. (Math. Logic Q. 59(6), 407–414, 2013; Semigroup Forum 92(3), 659–674, 2016), Mitrović et al. (Fundamenta Informaticae 184(3), 233–271, 2021; Constructive semigroups with apartness—a state of the art, 2024), Mitrović and Silvestrov ((Apartness) Isomorphism theorems for basic constructive algebraic structures with special emphasize on constructive semigroups with apartness—an overview, 2020), Mitrović et al. (J. Phys. Conf. Ser. 1194, 012076, 2019). In establishing our theory we were inspired by results obtained in interactive theorem proving the approach of formal verifications (more in Mitrović et al., Fundamenta Informaticae 184(3), 233–271, 2021). So how do we achieve all this? Simply by changing the logic with which we do our mathematics! Instead of using classical logic, we systematically use intuitionistic logic, and our work is based on the notion of apartness (between elements of the set and, later, between elements and its subsets). Based on the results presented in (Crvenković et al., Math. Logic Q. 59(6), 407–414, 2013; Crvenković et al., Semigroup Forum 92(3), 659–674, 2016), A. Cherubini and A. Frigeri introduced in 2019 constructive inverse semigroups with apartness (Cherubini and Frigeri, Semigroup Forum 98, 571–588, 2019). M. Mitrović and D. A. Romano contributed to the area too (Mitrović and Romano, Co-congruence on an inverse semigroup with apartness that separates idempotents; Romano, Acta Universitatis Apulensis 73, 101–138, 2023).

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Journey Through Constructive Inverse Semigroups with Apartness

  • Melanija Mitrović,
  • Mahouton Norbert Hounkonnou,
  • Daniel Abraham Romano

摘要

An important goal of this chapter is to provide a clear, understandable picture of constructive inverse semigroups with apartness in the Errett Bishop’s style of constructive mathematics, BISH. The theory of constructive semigroup with apartness is a new approach to semigroup theory (and not a new class of semigroups). It presents novelty within both mathematics: classical and constructive. The theory of semigroups with apartness was developed by M. Mitrović and co-authors: M. N. Hounkonnou, M. A. Baroni, S. Crvenković, D. A. Romano, and S. Silvestrov; see, for example, Crvenković et al. (Math. Logic Q. 59(6), 407–414, 2013; Semigroup Forum 92(3), 659–674, 2016), Mitrović et al. (Fundamenta Informaticae 184(3), 233–271, 2021; Constructive semigroups with apartness—a state of the art, 2024), Mitrović and Silvestrov ((Apartness) Isomorphism theorems for basic constructive algebraic structures with special emphasize on constructive semigroups with apartness—an overview, 2020), Mitrović et al. (J. Phys. Conf. Ser. 1194, 012076, 2019). In establishing our theory we were inspired by results obtained in interactive theorem proving the approach of formal verifications (more in Mitrović et al., Fundamenta Informaticae 184(3), 233–271, 2021). So how do we achieve all this? Simply by changing the logic with which we do our mathematics! Instead of using classical logic, we systematically use intuitionistic logic, and our work is based on the notion of apartness (between elements of the set and, later, between elements and its subsets). Based on the results presented in (Crvenković et al., Math. Logic Q. 59(6), 407–414, 2013; Crvenković et al., Semigroup Forum 92(3), 659–674, 2016), A. Cherubini and A. Frigeri introduced in 2019 constructive inverse semigroups with apartness (Cherubini and Frigeri, Semigroup Forum 98, 571–588, 2019). M. Mitrović and D. A. Romano contributed to the area too (Mitrović and Romano, Co-congruence on an inverse semigroup with apartness that separates idempotents; Romano, Acta Universitatis Apulensis 73, 101–138, 2023).