I now get what you meant by keeping the different 'levels' or layers separate – that notion, or record-keeping, of what's happening, in your proof, in PA versus PA+1. I loved my math courses precisely because of the computational logic.

Your meta-ethics: We're not right, nor will any of our descendants [?] ever be right. But we know some things that ARE right, just as a matter of inevitable ev-bio competence. And we've figured out a few ways to learn new things that are right. We've explored a bit of right, and even a bit of right+1. But we don't want to go near self-right – if we ASSUME we're accurate in our current understanding of right or right+1, we can (falsely) justify anything.