Hacker News Reader

You seem to be forgetting that constructive truth means provability.

Also, it doesn’t seem right to use the informal “take” when the object in question is not computable.

Informally speaking we can take the set of all real numbers. Assuming we are using standard mathematics that most working mathematicians use then this includes non-computable numbers. Sets don’t have to be computable to be used unless you are someone who works with non-standard models of set theory.

I specified I'm working in standard first order logic. And I'm not sure what do you mean with the informal take.

Also intuitionist logic is not my area, but isn't it divided in inference rules for provability and (Heyting or Kripke) semantic for model theory and truth just like FOL?

You may be working in classical logic, but that doesn’t mean the parent poster is. You asserted the parent poster seems to be confused, but what the parent poster said makes sense in a constructive setting. Please see my other comment:

https://news.ycombinator.com/item?id=18756974

Reply on news.ycombinator.com