Suppose that one day, someone comes up with a proof of consistency of Peano arithmetic (PA) within itself. Then, does it mean that PA is actually inconsistent? Because, by the Gödel's incompleteness theorem, it is impossible to do so if PA is consistent. So, by contradiction it means that PA is inconsistent. Is my reasoning right? If not, why? If yes, in what theory/set of axioms it is inconsistent by that reasoning?
What if someone comes up with a proof of consistency of arithmetic under the following conditions
first-order-logicincompletenesslogicpeano-axiomsphilosophy
Related Solutions
First, as others have pointed out, your characterization of GIT1 is not right. What it actually roughly says is that any complete and consistent theory stronger than PA cannot be generated by a decidable set of axioms. This does kill the prospects of a single formal system that decides “all of mathematics” which was one of Hilbert’s loftier goals.$^*$
But another big aspect was to have a finitary proof on the consistency of such a system that underlies mathematics, which still makes sense as a goal even if that system is necessarily incomplete. For example. we could say the system is ZFC, which we know allows us to formalize most of known mathematics, even if we also know there are statements it can’t decide (provided it is consistent).
I have a few qualms with the argument that a proof of Con(S) in S would not tell us much, but for the most part I agree, so I’ll grant it for the purposes of this answer. However, the goal is much more ambitious than this: we want to prove the consistency of our system of mathematics (say ZFC) in a very weak finitary theory of arithmetic (say PRA), not merely in ZFC. Surely it would be desirable and meaningful if that could be carried out. However, if GIT2 tells us ZFC can’t prove it, then certainly a weaker theory like PRA can’t either. So GIT2 is indeed bad news for this aspect of the program.
$^*$ I’m a lousy mathematician but an even worse historian. What I say is based on my understanding from the folklore of what Hilbert’s Program was and may or may not correlate with anything Hilbert actually said or believed.
You're right that a $T$-proof of the consistency of $T$ itself isn't very compelling (although if $T$ purports to be able to resolve all arithmetical questions then via Godel coding this is something $T$ would need to do). However, that's sort of missing the point.
Pre-Godel, the hope was that an "ambitious" theory $T$ could have its consistency proved in a "restrictive" subtheory $S\subset T$ (more precisely, that "infinitistic" mathematics could be proven consistent by "finitistic mathematics," whatever exactly that means). Of course this consistency proof would depend on our acceptance of $S$ itself, but that could still be of value to those who accept $S$ but are skeptical of $T$. The second incompleteness theorem kills this possibility in a very strong way: even if we take $T=S$ itself, we'll still be unable to get what we want (given mild assumptions on $T$ of course).
This is the "negative" force of the theorem, and the sense in which it was shocking at the time it was proved. The "positive" force, so to speak, is in its introduction of the notion of consistency strength, a concept which plays a fundamental role in proof theory and set theory.
Best Answer
You are correct. Even more is true:
When we appropriately formulate the expressions "Con(PA)" and "PA proves ---" in the language of arithmetic, it is the case that PA proves "If PA proves Con(PA), then $\neg$ Con(PA)." That is, PA proves that you are correct.
In fact, the initial PA can be weakened and the later PAs can be vastly strengthened: e.g. PRA proves "If ZFC proves Con(ZFC), then $\neg$ Con(ZFC)." That is, Godel's theorem is provable from very little and applies to very much.
Moreover, this is all done constructively. Specifically - taking PA as an example - there is an explicit (if messy to write down) algorithm $\alpha$ which would convert any PA-proof of Con(PA) into (say) a PA-proof of "$0=1$," and the fact that $\alpha$ does this can be proved in a very weak system. It's this last bit that makes this statement non-vacuous, since - assuming PA is in fact consistent - there are no PA-proofs of "$0=1$" at all, and hence any $\alpha$ will do if we drop the "provable behavior" requirement.