I read this and thought, since I havent really blogged much about mathematics yet, I could do so once again (even though I should do some work now), and since I have something related to it which could be interesting to all people not too familiar with logic. Hence, I will not be too formal, even though I want to show why it is sometimes necessary to be more formal than „obviously necessary“.
I want to show a mistake I already have made.
Let T be the First-Order Peano Arithmetic. By M(A) we mean the Number-Theoretical code for „A is decidable“, i.e. there exists a proof for A or a proof for ¬A . ¬M(A) states that there doesnt exist such a proof. Now consider ¬M(¬M(A)) .
This states that it is neither provable nore refutable that A is neither provable nor refutable. Assume there was a proof for A . Then ¬M(¬M(A)) cannot hold, because the proof of A would also proof that there exists a proof of either A or ¬A . Same for ¬A . So neither A nor ¬A can be provable, if ¬M(¬M(A)) holds. But from this would follow that ¬M(A) , which contradicts ¬M(¬M(A)) . Hence, ¬M(¬M(A)) would be wrong.
From this we could draw the conclusion that ¬M(A) is always decidable. Hence, there would be an algorithm which at least decides whether an arbitrary Proposition is decidable or not.
Hence, we can recursively define: Let a1, a2, … be the sequence of all propositions, such that a1, …, an are the axioms of peano arithmetic. Use an arbitrary Proof-Calculus (i.e. natural deduction) and extend it by the following rule: Let i be the smallest index such that ai isnt decidable yet. Then define ai as being true. I.e., just „iterate“ the sequence of all propositions, and set anything thats not decidable by the axioms or other propositions with smaller indices which are already set to be true to be true. Then the set of true propositions is decidable – remember, we have M(M(A)), i.e. we can always decide whether some proposition is decidable – and hence we can give any of these propositions a value. We get a complete consistent decidable theory which is at least as strong as number theory (since it satisfies the axioms of number theory). We could do the same thing for set theory either. But this contradicts Goedel’s Incompleteness Theorem.
So what went wrong?
Lets get a little deeper into it. For simplicity, lets say we are not in number theory anymore, but in ZFC. Prf(A) shall mean „A is
provable“. By the completeness theorem, this is equivalent to saying „All Models of our Theory (i.e. all structures satisfying our axioms) Satisfy A“. Or – the negative form – „There does not exist a Model of our Theory satisfying ¬A „. Obviously, M(A) <=> Prf(A) | Prf(¬A) . Talking of Models, ¬M(A) sais „There are Models of our Theory satisfying A and also Models of our Theory satisfying ¬A „. In fact, thats (almost) how the independence of the Axiom of Choice from ZF was proven.
So now M(M(A)) states „There does not exist a Model of our Theory satisfying that there exist both models of A and models of ¬A inside it“ – thats why I have chosen ZFC – it is a little clearer what „Model“ means in terms of sets than in terms of numbers – since ZFC is our Meta-Theory. Now let us consider ¬M(M(A)) .
Take a deep breath before reading the verbose version of this statement … „There exists a Model of ZFC of which the models inside it either all satisfy A or all satisfy ¬A , as well as a Model of ZFC of which there are models inside it satisfying A as well as models inside it satisfying ¬A“.
One thing you have to keep in mind: If a Model X of ZFC contains another Model B of ZFC inside it, then B is also a model of ZFC „from the outside“. Thats how the above „contradiction“ can be derived when talking about models:
Assume ¬M(M(A)) . Then let C be a model of ZFC containing a model D satisfying A as well as a model E satisfying ¬A – which must exist since ¬M(M(A)) . Then D is also a model satisfying A „from the outside“, as well as E is a model „from the outside“ satisfying ¬A. Hence, „from the outside“, ¬M(A) holds, and hence, M(M(A)). This contradicts ¬M(M(A)). That is, M(A) is decidable – there exist only models satisfying M(A) or only models satisfying ¬M(A) . Or differently: If some proposition A is undecidable in some model of ZFC, then it is undecidable in all models of ZFC. Well, its not this statement which is wrong – at least as far as I know, this statement is correct.
Actually I never really found the time to formalize this completely, so it could also be wrong, but at least it sounds plausible. And it doesnt contradict Goedels Theorem.
First of all, we considered our meta-theory as a model, too. That is, how things are „in real“ (whatever that means). And „in real“, of course, either there is a proof of A or a proof of ¬A , or there is none – its not asking whether some „higher object far away from reality“ exists, it is asking if there is a finite sequence of propositions and derivations proving or refuting A (ok, there are some philosophers afaik which do not believe that the tertium non datur holds „in real“, but that wold go too far). Hence, „in real“ it is indeed the fact that M(M(A)) holds.
Another reason why this doesnt contradict Goedel: Goedel uses representations of proofs in our metatheory inside the theory itself, i.e. a mapping from „outside“ to „inside“ the model we are looking at. Of course, then, we have to have some clear description of this model inside our metatheory. Actually, I am pretty sure that it is not trivial to get such a description for a model of the form we would get in the above way. Actually it is likely that this model we get would have another „understanding“ of finity, which means that with the default encoding of proofs inside numbers, we would also allow
proofs of infinite length, and I am not sure whether this is easy to compensate, or possible at all.
Well, I dont have the time to really think about this. But I couldnt find a book or something so far about „multiple“ undecidabilities – maybe because this topic is trivial or not considered interesting. To me this used to be interesting. Meanwhile, I am doing too much (boring) university-lecture-math to really enjoy this in my free time.