Converting formal proofs to conform to sound deduction

[Speakpigeon]

As Quine says, we have a systems of beliefs and we can revise our beliefs.

When beliefs contradict tautologies beliefs can be known to be lies with 100% perfect certainty.

A and B implies A... Is that true? It's for you to decide and you will say yes it's true if you have in mind the usual definition of the conjunction. But you will say no, it isn't, provided you had a different definition in mind. And then, there's no "correct" definition. You don't know that the definition of conjunction is true outside the fact that you have one in mind at the moment you have it. Maybe tomorrow you'll have a different definition and you'll say it's not true that A and B implies A.
All we can do is assume there is some real brain process which computes conjunction for us as we usually think of it. But it sounds much like an empirical fact to me and therefore potentially revisable. Wait till you get old enough to become confused about who you are or indeed "what" you are.

Quine seems to be pretty thick-headed when he can't see that analytical truth is perfectly delineated by expressions of language known to be true entirely based on the meaning of their words.

Possibly, I haven't tried to understand exactly what Quine's thesis was.
I don't think his argument was conclusive.
But it's still true we have a system of beliefs and we can revise our beliefs.
I also agree with you that there are truths we know but I have a very different perspective on how to characterise them.
In a sense, I agree with Quine but coming from the other end of the spectrum. There is no truly a priori anything. Most analytical is in fact empirical. Logic is empirical. We know (human) logic by observing the logical reasoning we humans do. That's entirely empirical. That's what Aristotle did. That's not what mathematicians did, because, well, they are mathematicians, not scientists. They like to make up stuff without being stopped by empirical concerns. But, it can't work for logic. It's only right that they should have got into a tangle around the notion of self-reference. Mathematics doing logic is already self-referential. Serve them right!
And, I believe therefore we could get to revise our theory of logic. In a way, mathematicians already did. Is ECQ a tautological truth? Many people would say so. Aristotle would have said it isn't. So, mathematical logic is a revision of our theory of logic.
EB