In one of my lectures, the lecturer put a bunch of examples of sets on the board, stuff like the set of all humans, set of all well typed programs in some programming language, the set of all true statements of first order logic, the set of all proofs of them, and the set of all sets.
Now, for the last one, he drew a big line through it, claiming that it introduced issues. It would seem to me that the two before also introduce fairly massive issues, but when I asked a friendly academic, he brushed me off without any real explanation, saying there would be no such issues. I'm going to give my argument below; I hope that anyone can either tell me I'm right, or at least tell me how I'm wrong, so I can better understand the mistakes I made.
Ok, so it would seem to me that for the set of all true statements of first order logic to be useful to us, it would first be necessary for us to be able to check whether a statement is in the set, and also that it's complement is the set of all false statements of first order logic.
Now, by Gödel any formal logical system that can reason about arithmetic must be incomplete (there are true statements of arithmetic that cannot be proved to be true or false in the logical system) or inconsistent (there are statements that can be proved to be both true and false).
So, a simple way of proving whether a statement is in the set is to define a proof program. We have our simple laws of inference ($\vee$-introduction, elimination etc), so it's fairly easy to, looking at a proof in FOL see whether the prover's done something not allowed. So, we go through every string of length 1, then every string of length 2, etc until we find a valid proof of the statement; if the program terminates and there are no syntax errors, it is known that the statement is true. To avoid going on forever with statements which are not in the set, we also check to see whether the negation of the formula is true, since by the law of excluded middle, if something's not true it's false.
Now, by Gödel, the program must
a) go on forever for some statements, since if FOL is incomplete, there will be no proof in the system that certain statements are in the set (even though they are true).
or
b) there will be certain statements for which testing both the statement and its negation will result in an affirmative answer (i.e. FOL is inconsistent).
This implies that a useful set containing all true statements of first order logic cannot exist.
At which point have I gone wrong here?
Best Answer
Your mistake is right at the beginning where you say:
First of all "is useful to us" is a somewhat vague description, and it is not clear at all that it would mean the same as "is a set".
Moreover, there is no rule demanding that for something to be a "set", there needs to be a definite computable procedure for finding out what its elements are. It needs to be true that everything is either an element or not an element, but there's no demand that we're able to know with certainty which is the case for every prospective element.
It is certainly possible to consider the concept of "collections where we have a definite procedure for telling whether something as a member of the collection". This leads to constructive mathematics, which is an interesting and respectable area of study. It just happens not to be what mathematicians in general mean when they say "set".