Loading...

Kolmogorov and kuroda translations into basic predicate logic

Ardeshir, M ; Sharif University of Technology | 2024

9 Viewed
  1. Type of Document: Article
  2. DOI: 10.1093/jigpal/jzac067
  3. Publisher: Oxford Academic , 2024
  4. Abstract:
  5. Kolmogorov established the principle of the double negation translation by which to embed Classical Predicate Logic CQC into Intuitionistic Predicate Logic IQC. We show that the obvious generalizations to the Basic Predicate Logic of [3] and to BQC of [12], a proper subsystem of IQC, go through as well. The obvious generalizations of Kuroda’s embedding are shown to be equivalent to the Kolmogorov variant. In our proofs novel nontrivial techniques are needed to overcome the absence of full modus ponens in Basic Predicate Logic. In [3] we argued that IQC is not the logic of constructive mathematics. Our doubts were far from new. New was that we put forward an alternative, BQC. One concern is that BQC is too weak for serious mathematics, or even trivial. This paper is one step to alleviate such concerns. © The Author(s) 2022. Published by Oxford University Press
  6. Keywords:
  7. Computational complexity ; Constructive mathematics ; Embeddings ; Generalisation ; Intuitionistic predicate logic ; Kolmogorov ; Modus Ponens ; Predicate logic ; Computer circuits
  8. Source: Logic Journal of the IGPL ; Volume 32, Issue 1 , 2024 , Pages 47-63 ; 13670751 (ISSN)
  9. URL: https://academic.oup.com/jigpal/article-abstract/32/1/47/6679414