11,214 reputation
2859
bio website andrej.com
location Slovenia
age 43
visits member for 4 years
seen 12 hours ago

I am a professional mathematician and theoretical computer scientist (what is the difference?) . My area of work is a mix of logic, semantics, programming languages, category theory, constructive mathematics and computability.


13h
awarded  Yearling
Aug
15
awarded  Enlightened
Aug
14
awarded  Nice Answer
Aug
13
comment To what extent can the mathematics of Reals be applied to Computable Reals?
@Kaveh: yeah, we could wish for better terminology...
Aug
13
comment To what extent can the mathematics of Reals be applied to Computable Reals?
@Yakk: Bishop's definition of reals never mentions any "computability". He may talk about it in the accompanying text, but the definition is "just math": real is represented by a sequence $(a_n)_n$ of rational numbers such that $|a_n - a_m| < 1/n + 1/m$ for all $n, m$. The word "computable" does not appear, nor is it implied.
Aug
13
comment To what extent can the mathematics of Reals be applied to Computable Reals?
It's a bit of an oxymoron to say "true both constructively and classically". That's like saying I have "more than 50 and more than 30 euros in my pocket" -- remember that constructive implies classical.
Aug
12
comment To what extent can the mathematics of Reals be applied to Computable Reals?
I added a note to about the fact that intuitionistic logic is not the same thing as intuitionism. Also, the Wikipedia page on intuitionistic logic is awful.
Aug
12
revised To what extent can the mathematics of Reals be applied to Computable Reals?
added 161 characters in body
Aug
12
comment To what extent can the mathematics of Reals be applied to Computable Reals?
If you want $[0,1]$ to be Heine-Borel compact you should use Type Two Computability, i.e., the relative Kleene function realizability. There $[0,1]$ is computably Heine-Borel compact.
Aug
12
comment To what extent can the mathematics of Reals be applied to Computable Reals?
No, no, you need to distinguish between intuitionistic logic and Brower's intuitionism. Brouwer's intuitionism has extra axioms which imply that $[0,1]$ is Heine-Borel compact. Intutionistic logic is just classical logic without excluded middle (and no extra axioms), so it is compatible with classical logic. In intuitionistic logic we can show that $[0,1]$ is complete and totally bounded as a metric space, which is another kind of compactness. But we cannot show intuitionistically that $[0,1]$ is Heine-Borel compact.
Aug
12
answered To what extent can the mathematics of Reals be applied to Computable Reals?
Aug
11
awarded  Good Answer
Aug
6
awarded  Enlightened
Aug
6
awarded  Nice Answer
Aug
4
awarded  type-theory
Aug
3
comment Can affine lambda calculus solve every problem in P?
Excuse my ignorance, but what's an example of a $P$-complete problem, and more importantly, what notion of reduction are you using?
Jul
29
comment Theorem prover fails to find simple set theory proof?
This is just a case of hit-and-miss, I suppose.
Jul
29
comment Theorem prover fails to find simple set theory proof?
Do you know you can use ordinary LaTeX instead of scary GIFs?
Jul
29
comment Theorem prover fails to find simple set theory proof?
Please, can we have these formulas in non-LISP form? There seem a lot of undefined concepts here. How is part-of defined or axiomatized? Same for sum-of (not in words, in LaTeX)?
Jul
28
comment Which formalism is best suited for automated theorem proving in set theory?
Euclid tried to "define" points as "that which has no part" and lines as "breadthless length". These definitions are much less clear than his axioms. Hilbert said that instead of points, lines and planes one might just as well talk of tables, chairs and beer mugs -- his point being that the primitive terms are just empty shells, place holders if you will, and have no intrinsic properties. In other words we should not try to define these. The same goes with the primitive concepts in any other theory.