I'm not sure that my paradox even requires the proof system to prove it's own consistency.
Your argument requires the proof system to prove it's own consistency. As we discussed before, your argument relies on the assumption that the implication
If "φ is provable" then "φ"
Provable(#φ) → φ
is available for all φ. If this were the case, your theory would prove itself consistent. Why? Because you could take the contrapositive
If "φ is false" then "φ is not provable"
¬φ → ¬Provable(#φ)
and substitute "0=1" for φ. This gives you
if "0≠1" then "0=1 is not provable"
¬0=1 → ¬Provable(#(0=1))
The premise "0≠1" holds. Therefore, the consequence "0=1 is not provable" also holds. At this point your theory is asserting its own consistency: everything is provable in an inconsistent theory.
You might enjoy reading about the Turing Machine proof of Gödel's first incompleteness theorem, which is closely related to your paradox.
0 is not equal to 1, so it's not inconsistent. I don't understand what you are trying to say with that.
It would be really silly for a system not to believe it was consistent. And, if it were true, it would also apply to the mathematicians making such statements. The mathematicians are assuming it's true, and it is obviously true, so I don't see why a proof system should not have it.
In any case I don't see how my system requires proving "x is provable implies x". It searches through proofs in a totally unspecified proof system. It then proves the ...
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.