Maaay-be, but I'm not at all convinced this is the right way to think about this. Suppose that we can become consistent, and suppose that there is some program P that could in principle be written down that simulates a humanity that has become consistent, and human mathematicians are going through all possible theorems in lexicographical order, and someone is writing down in a simple format every theorem humanity has found to be true -- so simple a format that given the output of program P, you can easily find in it the list of theorems found so far. Thus, there is a relatively simple recursive enumeration of all theorems this version of humanity will ever find -- just run P and output a theorem as soon as it appears on the list.

Now suppose humanity does figure out that it's living in a simulation, and figures out the source code of P. Then it knows its own Gödel sentence. Will this lead to a logical contradiction?

Well, if humanity does write down "our Gödel sentence is true" on the List, then that sentence will be false (because it says something equivalent to "this sentence does not appear on the List"). That actually doesn't make humanity inconsistent, but it makes it wrong (unsound), which we'll take to be just as bad (and we'll get inconsistent if we also write down all logical consequences of this statement + the Peano axioms). So what if humanity does not write it down on the list? Then the statement is true, and it's obvious to us that it's true. Not a logical contradiction -- but it does mean that humanity recognizes some things as true it isn't writing down on its list.

Paul Christiano has written some posts related to this (which he's kindly pointed out to me when I was talking about some related things with him :-)). One way I think about this is by the following thought experiment: Suppose you're taking part in an experiment supposedly testing your ability to understand simple electric circuits. You're put in a room with two buttons, red and green, and above them two LEDs, red and green. When you press one of the buttons, one of the lights will light up; your task is to predict which light will light up and press the button of the same color. The circuit is wired as follows: Pressing the red button makes the green light light up; pressing the green button makes the red light light up. I maintain that you can be able to understand perfectly how the mechanism works, and yet not be able to "prove" this by completing the task.

So, I'd say that "what humanity wrote on its list" isn't a correct formalization of "what humanity understands to be true". Now, it does seem possible that there still is a formal predicate that captures the meaning of "humanity understands proposition A to be true". If so, I'd expect the problem with recognizing it not to be that it talks about something like large ordinals, but that it talks about the individual neurons in every human mind, and is far too long for humans to process sensibly. (We might be able to recognize that it says lots of things about human neurons, but not that the exact thing it says is "proposition A will at some point be understood by humanity to be true".) If you try to include "human" minds scaled to arbitrarily large sizes (like 3^^^3 and so on), so that any finite-length statement can be comprehended by some large-enough mind, my guess would be that there is no finite-length predicate that can accurately reflect "mind M understands proposition A to be true" for arbitrarily large "human" minds M, though I won't claim strong confidence in this guess.

Everyone seems to be taking the phrase "human Gödel sentence" (and, for that matter, "the Gödel sentence of a turing machine") as if its widely understood, so perhaps it's a piece of jargon I'm not familiar with. I know what the Gödel sentence of a computably enumerable theory is, which is the usual formulation. And I know how to get from a computably enumerable theory to the Turing machine which outputs the statements of that theory. But not every Turing machine is of this form, so I don't know what it means to talk about the Gödel sentence of an arbitrary Turing machine. For instance, what is the Gödel sentence of a universal Turing machine?

Some posters seem to be taking the human Gödel number to mean something like the Gödel number of the collection of things that person will ever believe, but the collection of things a person will ever believe has absolutely no need to be consistent, since people can (and should!) sometimes change their mind.

(This is primarily an issue with the original anti-AI argument; I don't know how defenders of that argument clarify their definitions.)

I think it's perfectly reasonable to encounter your Gödel sentence and say you don't know it's true. You just have to think "this is only true if the logic I use is consistent. I'd like to think it is, but I don't actually have an ironclad proof of that (Luckily for me - if I did have such a proof, I'd know I was inconsistent). So I can't actually prove this statement"

"Stuart Armstrong does not believe this sentence."

Doesn't this argument presume some sort of Platonism? If F is a formal system that fully captures the computational resources of our brains, then a Godel sentence for F, G, will be true in some models of the axioms of F and false in others. When you say that we have a meta-proof that G is true, you must mean that we have a meta-proof that G is true in the intended model. But how do we pick out the intended model? After all, our intentions are presumably also beholden to the computational limitations of our brains. How could we possibly distinguish between the different models of F in order to say "I'm talking about this model, not that one"?

If you're a Platonist, perhaps you can get around this by positing that only one of the many models of F actually obtains, in the sense that only the numbers that appear in this model actually exist. So while we can't pick out this model as the intended model from the inside, perhaps there's some externalist story about how this model is picked out and other models (in which G is false) are not. Maybe there's a quasi-causal connection between our brain and the numbers which makes it the case that our mathematical statements are about those numbers and not others. But Platonism, especially the sort of Platonism proposed here, is implausible.

Is there any other way to make sense of the claim that our mathematical claims are about a model in which G is true, even though there is no computational procedure by which we could pick out this model?

Humans have a meta-proof that all Gödel sentences are true.

That's not true. Gödel sentences are true for (most?) consistent systems, and false for all inconsistent systems.

There is nothing like the Goedel theorem inside a finite world, in which we operate/live.