Bounded arithmetic is in some sense trivial; it’s just a big lookup table. I don’t think you’re going to get a useful AI that way; if you’re going to avoid Godel by limiting the complexity of statements the system can consider, it has to be so simple that it can’t form a statement of the form “this statement is not provable” (and not because there’s an explicit rule against such statements, the system has to naturally be that simple).
Bounded arithmetic is in some sense trivial; it’s just a big lookup table. I don’t think you’re going to get a useful AI that way; if you’re going to avoid Godel by limiting the complexity of statements the system can consider, it has to be so simple that it can’t form a statement of the form “this statement is not provable” (and not because there’s an explicit rule against such statements, the system has to naturally be that simple).