scholarly journals Constructive Logic and the Medvedev Lattice

2006 ◽  
Vol 47 (1) ◽  
pp. 73-82 ◽  
Author(s):  
Sebastiaan A. Terwijn
Author(s):  
KHROMUSHIN V.A. ◽  
◽  
VOLKOV A.V. ◽  
KHADARTSEV A.A. ◽  
◽  
...  

The article presents the relevance of the problem, defines the research purpose: to compare the average life expectancy of the population in the areas of the Tula region with different contents of heavy metals in the class of causes of death “Respiratory diseases ”. The authors used the data of the regional mortality register, the results of analyzes of the content of heavy metals (copper, lead, zinc, nickel) in the soil by atomic absorption spectroscopy, and the calculation of the average life expectancy by the algebraic model of constructive logic. The results indicate a decrease in average life expectancy due to the presence of heavy metals in the soil, but the average life expectancy in both contaminated and non-contaminated areas is gradually increasing.


2007 ◽  
Vol 72 (1) ◽  
pp. 81-97 ◽  
Author(s):  
Christopher P. Alfeld

AbstractA class is the set of paths through a computable tree. Given classes P and Q, P is Medvedev reducible to Q, P ≤MQ, if there is a computably continuous functional mapping Q into P. We look at the lattice formed by subclasses of 2ω under this reduction. It is known that the degree of a splitting class of c.e. sets is non-branching. We further characterize non-branching degrees, providing two additional properties which guarantee non-branching: inseparable and hyperinseparable. Our main result is to show that non-branching iff inseparable if hyperinseparable if homogeneous and that all unstated implications do not hold. We also show that inseparable and not hyperinseparable degrees are downward dense.


2018 ◽  
Vol 24 (1) ◽  
pp. 90-106
Author(s):  
ERIK PALMGREN

AbstractIn this article we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos.


Author(s):  
David Charles McCarty

Constructivism is not a matter of principles: there are no specifically constructive mathematical axioms which all constructivists accept. Even so, it is traditional to view constructivists as insisting, in one way or another, that proofs of crucial existential theorems in mathematics respect constructive existence: that a crucial existential claim which is constructively admissible must afford means for constructing an instance of it which is also admissible. Allegiance to this idea often demands changes in conventional views about mathematical objects, operations and logic, and, hence, demands reworkings of ordinary mathematics along nonclassical lines. Constructive existence may be so interpreted as to require the abrogation of the law of the excluded middle and the adoption of nonstandard laws of constructive logic and mathematics in its place. There has been great variation in the forms of constructivism, each form distinguished in its interpretation of constructive existence, in its approaches to mathematical ontology and constructive logic, and in the methods chosen to prove theorems, particularly theorems of real analysis. In the twentieth century, Russian constructivism, new constructivism, Brouwerian intuitionism, finitism and predicativism have been the most influential forms of constructivism.


Sign in / Sign up

Export Citation Format

Share Document