I'll try a couple more edits, but keep in mind that this isn't aimed at logicians concerned about Hilbert's program, it's aimed at improving gibberish-detection skills (sentences that can't mean things) and avoiding logic abuse (trying to get empirical facts from first principles) and improving people's metaethics and so on.