10,964 reputation
2456
bio website andrej.com
location Slovenia
age 43
visits member for 3 years, 11 months
seen 1 hour 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.


2d
comment Turing degree of computing definable reals
This is a duplicate of cs.stackexchange.com/questions/28733/…. Please do not post the same question twice, I already answered the other one.
2d
comment Theorem prover fails to find simple set theory proof?
This is just a case of hit-and-miss, I suppose.
2d
comment Theorem prover fails to find simple set theory proof?
Do you know you can use ordinary LaTeX instead of scary GIFs?
2d
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.
Jul
28
comment Which formalism is best suited for automated theorem proving in set theory?
Many mathematicians will say that set membership is a primitive concept which cannot be defined. How would you define set membership in a rigorous way? The point of the axiomatic method in mathematics is precisely that we do take certain concepts as primitive, describe them through axioms, and assume nothing further about them. In particular, the axioms are all there is to the concepts, on further "explanation" or "definition" is needed.
Jul
28
comment Which formalism is best suited for automated theorem proving in set theory?
True, NBG is likely to be better suited than ZFC, especially since in ZFC classes are not first-class objects. How does FOL prove properties of sets? From the axioms about sets, of course. I don't understand your question. In every formalization there are some things that are necessarily taken as primitive. FOL has exactly the same "problem" with natural numbers, where 0 and successor are "undefined".
Jul
28
comment Which formalism is best suited for automated theorem proving in set theory?
Oops, I am confused, I though I was on Mathoverflow. Apologies! Stay right here :-)
Jul
28
revised How to translate the axiom schema of induction by Curry-Howard?
added 2 characters in body
Jul
28
revised How to translate the axiom schema of induction by Curry-Howard?
deleted 14 characters in body
Jul
28
answered How to translate the axiom schema of induction by Curry-Howard?
Jul
28
comment How to translate the axiom schema of induction by Curry-Howard?
It would be answered on cs.stackexchange, and it is not research-level.
Jul
28
revised Which formalism is best suited for automated theorem proving in set theory?
edited title
Jul
28
answered Which formalism is best suited for automated theorem proving in set theory?
Jul
28
comment Which formalism is best suited for automated theorem proving in set theory?
LISP code will be ignored by mathematicians on this site. You should rewrite it in mathematical notation.
Jul
28
comment Which formalism is best suited for automated theorem proving in set theory?
Rather than closing down the question because it is asked in a technically strange way, how about we try to explain the differences? (In which case this is not research-level and should go to Math SE.)
Jul
19
comment Does hyper-computational power of infinite time Turing machines also require infinite memory?
It's an order-theoretic problem, not one of cardinality. Both $\omega$ and $\omega + \omega$ have the same size, namely $\aleph_0$, but one has a limit point in the middle. Presumably you can't get rid of it with physics. To compute for $\omega + \omega$ steps you'd have to somehow fly into a black hole, emerge from it, and then fly into it again. Or something like that.
Jul
18
comment Does hyper-computational power of infinite time Turing machines also require infinite memory?
Only if you can get black holes to let you compute beyond $\omega$ steps. I am aware of theories that show how you get infinite time, but infinitely many infinite times? That would require some serious black hole engineering.
Jul
18
answered Does hyper-computational power of infinite time Turing machines also require infinite memory?
Jul
8
comment How are these statements about CTT reconcilable?
Judgments are not about being true or false. They are basic "constructors" from which we build derivations. For instance, you can have a judgment which tells you how to build an ordered pair. What's "true" about that?