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).
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?
Your mistake is right at the beginning where you say:
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,
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”.
I agree with @Makholm that there is no pre-requisite sorting algorithm for sets (assuming the Axiom of Choice, which allows such an arbitrary collections of elements), but there is another point to be made here.
Any statement which is undecideable (also called “unprovably true”) can be considered an axiom, assumed true, and tossed into the set of true statements. That means the set of true statements will be infinitely large and will mostly consist of axioms (statements that are assumed to be true). Each time you toss a new axiom into this set, there will be another undecideable statement that you need to assume is either true or false and throw into its respective set.
You see, the undecideable statements do not belong to both sets, you just have to choose which set they do belong to (and it doesn’t matter which).
Church’s theorem named after Alonzo Church, says there is no algorithm for deciding which first-order sentences are universally valid.
Also, a first order statement can only be a member to a set if there is an identity defined for it. But there is no obvious identity relation for statements, between alphabetical identity and logical equivalence.