Suggestion — transfer Lean prelude to Minimal Logic

Stream: general

[Nazar Androshchuk]

Overview

I argue that the principle of explosion (EXP) (can refer to both False -> q and p \and \not p -> q) (Used by Empty.elim) is non-constructive. EXP is independent from the other axioms in the default intuitionist prelude, which make minimal logic. In addition, "weak explosion" (W-EXP) (False -> p -> False === False -> \not p) is constructive, derivable in minimal logic, and still an impressive theorem (not an axiom).

Relation to other theorems (in minimal logic)

• EXP is equivalent to disjunctive syllogism
• EXP and the law of the excluded middle together are equivalent to the principle of double negation

Benefits of Omission of the Axiom of the Principle Of Explosion (of the negation of the truth)

1. Constructibility: This is the central argument for this, and I turn to the source below to provide the strongest argument I can.
   _Edgar Campos & Abilio Rodrigues:_

   Heyting provides an informal explanation for the meaning of the implication that
   intends to justify both EQV and EXP :
   The case is conceivable that after the statement a → b has been proved in
   the sense specified, it turns out that b is always correct. Once accepted,
   the formula a → b then has to remain correct; that is, we must attribute
   a meaning to the sign → such that a → b still holds. The same can
   be remarked in the case where it later turns out that a is always false
   (Heyting, 1930, p. 313).
   Heyting’s argument, however, as Johansson will point out in 1937 (Section 3.4 below), is
   not sound. He was thinking of a situation in which the proof of A → B was available,
   and subsequently a proof of ¬A was obtained. But what EXP says is something rather
   different, and stronger, namely, that a proof of ¬A automatically yields a proof of A → B.
   Heyting clearly fails to justify this.

_Johansson "in a letter to Heyting dated September 23rd, 1935"_

I have not been able to make my peace with Axiom 4.1. You say that
when a → b has been proved, and later ¬a is proved, then a → b should
remain correct. Indeed; but ¬a → (a → b) means that when ¬a has
been proved, b at once becomes derivable from a, even when this had
not been proved before. And that contradicts my intuition in the most
violent way (Letter from Johansson to Heyting, apud van Atten, 2017).

2. Classical is unaffected. As said before, EXP is a consequence of the axioms of classical logic. Either you want a constructive proof, for which you shouldn't use EXP; or you don't mind a non-constructive proof, in which case classical axioms are stronger.
3. Paraconsistency: an added benefit. False is just an empty type, until you define an axiom which can populate it; in that case all that happens is p -> False which is very constructively logical when you don't tack on extra semantics to False as a term of Prop. With two uninhabitable types, adding an axiom which serves as an introduction to one, does not necessarily create a proof to the other; this is not the case with EXP.

Drawbacks

1. Breaking change: Removing False.elim and absurd from the prelude will obviously be breaking. I do suggest that, if the opportunity does arise (e.g Lean5 comes with another syntax overhaul as the breaking change to rule them all), 3 logic namespaces be defined:

• _minimal_ — the root namespace, consisting of the current logic prelude excluding the principle of explosion. A proof of W-EXP should be added for convenience.
• a namespace containing the principle of explosion as an axiom, like the current implementation — this is probably equivalent to the popular _Heyting_'s formal intuitionistic logic.
• the _Classical_ namespace, with a proof of EXP

2. Pragmatic non-difference given law of non-contradiction. Why this issue hasn't come up here before (or that often in academics).

   Notice that van Dalen and Troelstra consider Heyting’s explanation (quoted above in
   Section 3.5) as a stipulation that fixes the meaning of ⊥ and →, or ¬ and →, depending
   on what one chooses as primitive. But if this inference were in accordance with Brouwer’s
   ideas, it would not have to be the result of a stipulation. As far as we know, nowhere in
   Brouwer is there evidence in support of the claim that any operation (i.e., a construction),
   applied to an empty domain (i.e., to a non-existent proof of ⊥) yields as a result a proof
   of an arbitrary proposition A.

Enough philosophy. The question is how this can be implemented non-disruptively. I'm very new to Lean, so this is the area I would appreciate help the most.

• Ideally, the lean prelude does not introduce False.elim or Empty.elim, which are to be moved to a new Heyting namespace. Classical would open the Heyting namespace.
• If the community (understandably) does not feel traction with this proposal, due to practical infeasibility (breaking change), habit/popularity of Heyting logic, or a metaphysical argument I'm not aware of, then it would still be better than nothing if minimal logic had second class support. Since minimal logic is a strict weakening, this would require "disabling" the EXP axiom by the user, and all dependent theorems, including from imports. Can this be done?
• Also, #print axioms could include the axioms of elimination used. Maybe a second command?

Thank you for reading.

Source: http://lna.unb.br/lna_n01_04_ecampos_arodrigues.pdf

Some remarks on the validity of the principle of
explosion in intuitionistic logic1
Edgar Campos2 & Abilio Rodrigues3
Abstract
The formal system proposed by Heyting (1930, 1936) became the stan-
dard formulation of intuitionistic logic. The inference called ex falso
quodlibet, or principle of explosion, according to which anything follows
from a contradiction, holds in intuitionistic logic. However, it is not clear
that explosion is in accordance with Brouwer’s views on the nature of
mathematics and its relationship with logic. Indeed, van Atten (2009)
argues that a formal system in line with Brouwer’s ideas should be a
relevance logic. We agree that explosion should not hold in intuitionistic
logic, but a relevance logic requires more than the invalidity of explosion.
The principle known as ex quodlibet verum, according to which a valid
formula follows from anything, should also be rejected by a relevantist.
Given ex quodlibet verum, the inference we call weak explosion, accord-
ing to which any negated proposition follows from a contradiction, is
proved in a few steps. Although the same argument against explosion
can be also applied against weak explosion, rejecting the latter requires
the rejection of ex quodlibet verum. The result is the loss of at least
one among reflexivity, monotonicity, and the deduction theorem in a
Brouwerian intuitionistic logic, which seems to be an undesirable result.

[Eric Wieser]

False.elim is just a shorthand for False.rec, which is not even in the prelude, but foundational to the type theory of Lean (CiC)

[Eric Wieser]

I would guess that you might be able to get away with using the HImp symbol of docs#HeytingAlgebra if you want a weaker system of implication

[Nazar Androshchuk]

Could there be potential problems with CiC where explosion is excluded? (apart from being weaker). I can't find a name of such a calculus online.

[Johan Commelin]

What would that even look like?

[Nazar Androshchuk]

The logical components would be isomorphic to Johansson minimal logic. No explosion, but weak explosion. Instead of taking contradiction as a primitive, the existence of an uninhabited type is asserted.

[Johan Commelin]

That doesn't tell me at all how you think CiC should be modified.

[Nazar Androshchuk]

I want to remove the axiom of explosion from CiC. False does not imply an arbitrary proposition.

[Johan Commelin]

You can't just do that. You'll destroy all of CiC along the way.

[Nazar Androshchuk]

What would happen?

[Eric Rodriguez]

What do you think False.rec would look like in this case?

[Johan Commelin]

Nazar, you'll have to explain how you want inductive types to work. CiC gives such a description, and False.rec just falls out of it as a consequence.

[Nazar Androshchuk]

Eric Rodriguez said:

What do you think False.rec would look like in this case?

False.rec is not essential. It is ommited. But what can happen is False \r P \r False.

[Nazar Androshchuk]

Johan Commelin said:

Nazar, you'll have to explain how you want inductive types to work. CiC gives such a description, and False.rec just falls out of it as a consequence.

Thanks, I'll have to read up on inductive types then.

[Floris van Doorn]

As others have said, we cannot easily change the logic of Lean. However, you can do minimal logic in Lean.

axiom MinimalFalse : Prop

def MinimalNeg (p : Prop) : Prop := p → MinimalFalse

notation (priority := high) "¬" p => p → MinimalFalse

example (p : Prop) : MinimalFalse → ¬ p := fun h _ => h

example (p : Prop) : MinimalFalse → p := sorry -- not provable

[Nazar Androshchuk]

Floris van Doorn said:

As others have said, we cannot easily change the logic of Lean. However, you can do minimal logic in Lean.

axiom MinimalFalse : Prop

def MinimalNeg (p : Prop) : Prop := p → MinimalFalse

notation (priority := high) "¬" p => p → MinimalFalse

example (p : Prop) : MinimalFalse → ¬ p := fun h _ => h

example (p : Prop) : MinimalFalse → p := sorry -- not provable

Thanks, this should be a solution.