> Another feature is proof by contradiction, where you can prove something by showing that the alternative is unsound.

As far as lean is concerned, this isn't an example of classical logic. It's just the definition of "not" - to say that some proposition implies a contradiction, and to say that that proposition is untrue, are the same statement.

Most "something"s that you'd want to prove this way will require a step from classical logic, but not all of them. (¬p ⟶ F) ⟶ p is classical; (p ⟶ F) ⟶ ¬p is constructive.

▲

zozbot234 3 hours ago | parent | next [-]

More generally, any negative statements can be proven classically, even in intuitionistic logic. Intuitionistic logic does not have the De Morgan duality found in classical logic, you have to go to linear logic if you want to recover that while keeping constructivity. (The "negative" in linear logic actually models requesting some object, which is dual to constructing it. The connection with the usual meaning of "negative" in logic involves a similar duality between "proposing" a proof and "challenging" it.)

▲

smj-edison 3 hours ago | parent | prev [-]

So proof by contradiction proves ¬p, but it requires the law of excluded middle to prove p (in the case of ¬p -> F)? I didn't realize that was constructive in the first case.

▲

thaumasiotes an hour ago | parent [-]

Well, at some point you have to define what you mean by "proof by contradiction". I was responding to your statement, "prove something by showing that the alternative is unsound". You can prove that something is false that way without needing classical logic.

Mathlib defines `by_contradiction` as a theorem proving `(¬p → False) → p` for any proposition p. ( https://leanprover-community.github.io/mathlib4_docs/Mathlib... ) This does require classical logic.

For what's happening with `¬p -> F`, recall that this is by definition the statement `¬¬p`; classical logic will let you conclude `p` from `¬¬p`, or it will let you apply the law of the excluded middle to conclude that either `p` or `¬p` must be the case, and then show that since it isn't `¬p`, it must be `p`. (Again, not really different approaches, but perhaps different in someone's mental model.)

On the other hand, if you have `p -> F`, that is by definition the statement `¬p`, and if you've established `¬p`, you've already finished proving that p is false.

Something that I find particularly absurd about the hypothetical distinction between intuitionistic and classical logic is that intuitionistic logic is sufficient to prove `¬p` from `¬¬¬p`. (This is quite similar to how 'proof by contradiction' is constructive if you're proving a negative but not if you're proving a positive; it might be the same result.) So for any proposition that can be restated in a "negative" way, the law of the excluded middle remains true in intuitionistic logic. The difference lies only in "fundamentally positive" propositions. (You can do that proof yourself at https://incredible.pm/ ; it's in section 4, `((A→⊥)→⊥)→⊥` -> `A→⊥`.)

There's a fun article on this very blog telling a similar story: https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.h...

> Martin-Löf designed his type theory with the aim that AC should be provable and in his landmark Constructive mathematics and computer programming presented a detailed derivation of it as his only example. Briefly, if (∀x : A)(∃y :B) C(x,y) then (∃f : A → B)(∀x : A) C(x, f(x)).

> Spoiling the party was Diaconescu’s proof in 1975 that in a certain category-theoretic setting, the axiom of choice implied LEM and therefore classical logic. His proof is reproducible in the setting of intuitionistic set theory and seems to have driven today’s intuitionists to oppose AC.

> It’s striking that AC was seen not merely as acceptable but clear by the likes of Bishop, Bridges and Dummett. Now it is being rejected and the various arguments against it have the look of post-hoc rationalisations. Of course, the alternative would be to reject intuitionism altogether. This is certainly what mathematicians have done: in my experience, the overwhelming majority of constructive mathematicians are not mathematicians at all. They are computer scientists.

▲

smj-edison 36 minutes ago | parent | next [-]

Yeah, I suppose I was playing fast and loose with the terminology to make it more approachable. iirc, the definition of proof by contradiction is you assume the negation, show that the negation has something that is both true and not true, and hence the negation is logically unsound. Since you can technically derive anything from an unsound system, you derive that the negation is false, and then by the laws of excluded middle and non-contradiction, you know that p must be true.

But now I see from what you mentioned that this means that if you don't do the negation elimination, then you can still show `¬¬p` in an intuitionistic logic system.

Is proof by contradiction of a false statement just a counterexample? Because a counterexample shows that the statement is incoherent, so the negation must be true. And you have to construct a counterexample.

	▲	zozbot234 26 minutes ago \| parent [-]
		A counterexample as generally understood would be a constructive refutation: it takes ~p as a request to provide p constructively and does just that. Proof by contradiction is much more general than that. Of course the problem of extracting the residual constructive content from a proof by contradiction (explaining how it is in some sense constructing some vastly generalized counterexample) is non-trivial.

▲

zozbot234 an hour ago | parent | prev [-]

Constructivists don't call a proof of ¬p a "proof by contradiction", they just call it a proof of ¬p. To them, a "proof by contradiction" of some p that isn't in the negative fragment is just nonsense, because constructive logic doesn't have the kind of duality that even makes it necessary to talk about contradiction as a kind of proof to begin with. They'd see the classical use of "proof by contradiction" as a clunky way of saying "I've actually only proven a negative statement, and now I can use De Morgan duality to pretend that I proved a positive."