It seems to me that there is 2 family of statements that I call "logically undecidable" (to distinguish with computationally undecidable which is define by turing machines), i.e. of statements for which it doesn't exist any proof that the statement is true nor a proof it is false :
The first family is defined like this : If you take a statement of this family, if you add it to the axioms as an axiom, you get a new consistent theory. And if you add its negation you get an other new consistent theory. A proof of such a statement has been done for the axiom of choice regarding ZF as theory.
The second family is defined like this : If you take a statement of this family, if you add it to the axioms as an axiom, you get an inconsistent theory (you can prove false), and if you add its negation you get an inconsistent theory too. I think any paradoxal statement, like the liar paradox, falls in this family.
A first question is : Does it really make sense to consider the statements of the second family as well defined ?
It seems to me that by accepting such a statement as well defined we are adding some incompleteness in the mathematics. Let's me explain, what arises to Godël 1st theorem if indeed these statements are considered as not well defined.
Let's say Godël is proving his 1st theorem from ZF, actually doesn't matter we could say he is doing the proof from axioms A and do the same reasoning with very acceptable hypothesis on A. Let's consider any problem proved as computationally undecidable, still from ZF, not necessarily the one Godel exhibits in his proof, let's consider the Halting Problem.
Let's show by contradiction that some part of the Halting Problem is actually independent of ZF. Assume that for any TM, there exists a proof that the TM halts or there exists a proof that the TM doesn't halt. But then you could solve the Halting Problem just like this : enumerate the proofs of ZF until you find either a proof that your input machine halts or a proof that your input machine doesn't halt. This is a contradiction since the Halting Problem is proved computationally undecidable. So, there exist a TM, let's call it U, such that the statement S : 'U halts on input x' is "logically undecidable". By the same method, for any computationally undecidable problem, it exists such a logically undecidable statement.
So now I am asking, in which of my 2 categories fall such a statement (any of them actually) ? If you add the statement to ZF, you get a theory $ZFS$ in which you can both prove S trivially and prove that you can't prove S (since the proof of undecidability still apply, you can still "write" it using the axioms of ZF in $ZFS$), so $ZFS$ is inconsistent. Well and if you add the opposite, you get a theory $ZF\overline{S}$ where you can prove both 'not S' and that that you can't prove 'not S', by exactly the same argument, so $ZF\overline{S}$ is inconsistent too. By the same method, all of these logically undecidable statement that come from computationally undecidable problems fall in the second family.
So what happens if we consider all the statement of the second family as not well define (which actually is pretty natural regarding the liar paradox) ? By contraposition, there is no longer something well define on which 1st Godël theorm apply ! Thus there is no longer any undecidable problem which is fully well defined, but you can restrict any problem to the inputs for which it is logically decidable and then the resulting restricted problem is both well defined and computationally decidable (still by enumeration of the proofs).
Even better : if we consider all the statement of the second family as not well define there is no longer anything on which the 2nd theorem of Godël apply and we could have the hope of proving the self-consistency of a well defined theory from this theory.
So my second question is, why, why are we considering such strange paradox like liar paradox as well define ? What does it add to mathematics except incompleteness ? Are you sure we really need that for anything ?
Philosophically, it seems to me that we are unnecessarily authorizing some local inconsistency and, since this inconsistency can not interact with anything, the all mathematics stay consistent, but become incomplete.
