[sunday_serif]

For me, proof by contradiction only clicked (recently!) once I understood that logical consequence and unsatisfiability are equivalent.

Once I understood that and reframed the contradiction as a statement about unsatisfiability… I could then see directly how the positive result you get is the equivalent logical consequence.

Unfortunately, I feel like this intuition only really helps if you are pretty immersed in formal logic… otherwise it just sounds like jibberish.

[SkiFire13]

If you are into constructive logic then this will only work for proving negative statements (where indeed the definition is the same as what a proof by contradiction would give you). For positive statements you won't get back a direct proof term of your initial statement, but rather a proof of a double negation of it.