There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative ...
I want to know why we add an intensional equality in type theory to definitional equality ? What is the aim with this intensional equality ? thanks
According to constructivism a mathematical object to prove that it exists". There are several formulas to calculate pi, such as: so I take it ...
Is there a finite-dimensional vector space whose dimension cannot be found? Assume, we have somehow constructed a vector space whose dimension is finite, but yet unknown. Is there always an algorithm ...
Ultrafinitism is (I believe) a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to wikipedia, it has been ...