[skh]

An important nitpick. His Incompleteness Theorem deals with recursively enumerable axiomatic systems. The second order Peano Axioms are categorical. That is, they have only one model up to isomorphism. It’s easy to come up with a complete axiomatic system for the standard model of the natural numbers. Just take as your axiomatic system the collection of all true statements. This ins’t a useful system since there is no procedure for determining if a statement is an axiom or not.

[whatshisface]

How would you be able to take every true statement as an axiom? Without proving anything I don't see how you could identify any statements as true.

[ginnungagap]

Whenever you have a structure M of some language L you can take the so called complete theory of the structure, denoted Th(M), which is just the set of all L-sentences true in M. In particular if L is the language of PA and M are the standard natural number with the standard operations Th(M) is a theory called true arithmetic. This theory is complete (that's because Th(M) is always complete) and clearly enough to talk about the integers, but it escapes Gödel's theorem since it's axioms are not recursively axiomatizable.

You seem to be confusing "true" and "provable", as far as first order logic is concerned those are equivalent (by another theorem of Gödel, the completeness theorem), but the first in defined in terms of models and the second is purely syntactic

[mietek]

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.

[skh]

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.

[ginnungagap]

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?

[mietek]

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

[antidesitter]

The point is that the set of all true statements about arithmetic [1] exists “out there” (and thus as a “theory” in a very general sense) even if we can’t identify it.

[1] https://en.wikipedia.org/wiki/True_arithmetic

[mietek]

You are invoking a classical notion of existence.

This is not acceptable to a constructivist, for whom “a statement is true if we have a proof of it, and false if we can show that the assumption that there is a proof for the statement leads to a contradiction”[1]. The parent poster, whatshisface, may be a constructivist.

[1] Troelstra A., D. van Dalen (1988) “Constructivism in mathematics: an introduction”

[antidesitter]

In the case of True Arithmetic, the true statements are the axioms. Thus a proof of any true statement consists of just invoking the corresponding axiom, which is a valid proof in any formal system (constructive or otherwise).

The weirdness of True Arithmetic comes not from proofs (which are trivial) but from the axioms themselves. You can object that it’s not a “reasonable” or “proper” theory because it’s not recusively axiomatizable (i.e. there’s no effective procedure for even deciding whether a statement is an axiom), but I don’t think that objection is specifically constructivist.

[mietek]

Indeed, the objection is against the method by which this system is supposed to be defined. As you say, we start with an implicit assumption that we don’t have an effective procedure to construct the set of statements that are true in the ambient metatheory. And so, this set exists in a classical sense, or “weakly exists”, and not in a constructive sense.

[AlexCoventry]

That's the joke.