2015/04/30 by Farida Kachapova, Kachapova, Farida
Engineering · Mathematics · #03E70 #03F50 #Advanced Numerical Analysis Techniques #FOS: Mathematics #Logic (math.LO) #math.LO #msc:03E70 #msc:03F50
paper · pdf · doi:10.48550/arxiv.1504.08062
17 pages
arxiv created 2015/04/30 · openalex publication_date 2015/04/30 · arxiv updated 2015/05/01 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
This paper describes an axiomatic theory BT for constructive mathematics. BT has a predicative comprehension axiom for a countable number of set types and usual combinatorial operations. BT has intuitionistic logic, is consistent with classical logic and has such constructive features as consistency with formal Church thesis, and existence and disjunction properties. BT is mutually interpretable with a so called theory of arithmetical truth PATr and with a second-order arithmetic SA that contains infinitely many sorts of sets of natural numbers. We compare BT with some standard second-order arithmetics and investigate the proof-theoretical strengths of fragments of BT, PATr and SA.