That's right. You could list all those propositions and search for proofs of them. In fact this is very similar to Hilbert's very program to which Godel's First Incompleteness Thm was a response (https://en.wikipedia.org/wiki/Hilbert%27s_program).
Godel showed that there are true statements that cannot be proven, and also that among the unprovable statements from within the system is the consistency of the system itself.
As I understand, mathematicians are still trying to figure out how much this matters. One of the best examples of its mattering is may be the Continuum Hypothesis: CH is consistent with ZFC, and ~CH (not CH) is also consistent with ZFC. In other words, you have enough flexibility in constructing your ZFC world such that in some ZFC-consistent worlds CH is true, and in others CH is false.
Litt's statement is not wrong; it's just that what he wrote sounds so much like Hilbert's program, that I'm surprised we didn't get some even minor comment on what kinds of truths we could reach if we embarked on such an effort.
Godel showed that there are true statements that cannot be proven, and also that among the unprovable statements from within the system is the consistency of the system itself.
As I understand, mathematicians are still trying to figure out how much this matters. One of the best examples of its mattering is may be the Continuum Hypothesis: CH is consistent with ZFC, and ~CH (not CH) is also consistent with ZFC. In other words, you have enough flexibility in constructing your ZFC world such that in some ZFC-consistent worlds CH is true, and in others CH is false.
Litt's statement is not wrong; it's just that what he wrote sounds so much like Hilbert's program, that I'm surprised we didn't get some even minor comment on what kinds of truths we could reach if we embarked on such an effort.