Can Gödel's theorem be proved within PA?

93 Views Asked by At

Gödel proves his theorem informally by using natural languages. However, is there a way to carry out his proof in PA itself? (so that maybe PA could prove that itself could not prove its own consistency) If there isn't (and we have to carry out his proof in some stronger background theory such as ZFC), what makes his proof inexpressible in PA?