Intuitionistic double negation

Stream: new members

[Thomas Preu]

I am puzzled by the behavior of Lean with regards to double negation. I did not open classical, I just evaluated some expressions

#check ¬ ¬ True  -- yields:   ¬¬True : Prop
#eval ¬ ¬ True   -- yields:   true
#check ¬ ¬ False -- yields:   ¬¬False : Prop
#eval ¬ ¬ False  -- yields:   false

Note, that the evaluations yield terms of type Bool (in the universe Type aka Type 0 aka Sort 1) and not types in the universe Prop (aka Sort 0).
Intuitionistically a proposition of type $\neg\neg P\rightarrow P$ is not provable. Thus you get the Rieger–Nishimura lattice .
But the Lean Prop-s True and False are not variable proposition. Might it be true intuitionistcally that the special cases $\neg\neg \top\rightarrow \top$ and $\neg\neg \bot\rightarrow \bot$ hold?
And then there is the thing that in Lean Bool-s can be coerced to Prop-s, cf. Theorem Proofing in Lean 4, Ch. 10.10 .
Maybe there is a backward mechanism, too? Maybe this is only invoked when evaluations take place?
In any case, if somehow the propositional logic of Prop-s work the same way as propositional logic for Bool-s (which, afaik, behave classically) in Lean, this would also explain the evaluation of double negatives as above.

Since I neither have a background in intuitionistic logic nor in Lean I am a bit lost of what to make of it. Any help and explanation are appreciated.
Also: Is there a way to work with (a substantial version of) intuitionistic logic "out of the box" in Lean 4? I.e. without building customized types and such to emulate intuitionistic logic? If not, is there some "preferred way" to work with intuitionistic logic in Lean?

[Aaron Liu]

Thomas Preu said:

Might it be true intuitionistcally that the special cases $\neg\neg \top\rightarrow \top$ and $\neg\neg \bot\rightarrow \bot$ hold?

Yes, this is correct

[Aaron Liu]

Thomas Preu said:

And then there is the thing that in Lean Bool-s can be coerced to Prop-s, cf. Theorem Proofing in Lean 4, Ch. 10.10 .
Maybe there is a backward mechanism, too? Maybe this is only invoked when evaluations take place?

When you write #eval P, and P has type Prop, this is automatically converted into #eval decide P

[Kenny Lau]

@Thomas Preu the general theorem $\neg \neg P \to P$ is not provable, but that doesn't mean it's not provable for every specific P

[Kenny Lau]

for example, it's provable for every decidable P

[Kenny Lau]

decidability is the link between intuitionalistic logic and classical logic

[Kenny Lau]

and true and false are decidable (they're true and false respectively)

[Aaron Liu]

It also hold intuitionistically that $\neg\neg\neg P \to \neg P$

[Aaron Liu]

this is seen as the contrapositive of $P \to \neg\neg P$

[suhr]

Aaron Liu said:

It also hold intuitionistically that $\neg\neg\neg P \to \neg P$

This is basis of double-negation translation which embeds classical logic into intuitionistic logic.

Thomas Preu said:

Also: Is there a way to work with (a substantial version of) intuitionistic logic "out of the box" in Lean 4?

Lean is already constructive out of the box, you just need to guard against theorems that use Classical (you can write a lint for that). But I can't advice you to use Lean for constructive mathematics. For two reasons. First, you will have to fight against the rest of Lean world who do not care much about constructive math. Second, any kind of HoTT is probably better suited for constructive mathematics than the type theory of Lean.

[Thomas Preu]

Aaron Liu said:

Thomas Preu said:

Might it be true intuitionistcally that the special cases $\neg\neg \top\rightarrow \top$ and $\neg\neg \bot\rightarrow \bot$ hold?

Yes, this is correct

Thanks a lot! That affirmation set me on the right tracks. Of course you can proof those assertion "trivially", but that feels like cheating to me:

theorem double_neg_false_decide : ¬ ¬ False ↔ False := by
  decide

theorem double_neg_true_trivial : ¬ ¬ True ↔ True := by
  trivial

I as a beginner was unsure what's behind it, like magic that you don't understand (reminds me of the White Stripes song Black Math).

With confidence that there is no "classical magic" or "coercion magic" but only "intuitionistic inference" I could find proofs that I have the confidence of understanding:

theorem not_false_equi_true : ¬ False ↔ True := by
  constructor
  · intro
    have h2 := True.intro
    exact h2
  · intro _ h2
    exact h2

theorem not_true_equi_false : ¬ True ↔ False := by
  constructor
  · intro h1
    have h2 := True.intro
    have h3 := h1 h2
    exact h3
  · intro h1
    have h2 : ¬ True := False.elim h1
    exact h2

theorem double_neg_false : ¬ ¬ False ↔ False := by
  rw [not_false_equi_true, not_true_equi_false]

theorem double_neg_true : ¬ ¬ True ↔ True := by
  rw [not_true_equi_false, not_false_equi_true]

[Thomas Preu]

suhr said:

Lean is already constructive out of the box, you just need to guard against theorems that use Classical (you can write a lint for that). But I can't advice you to use Lean for constructive mathematics. For two reasons. First, you will have to fight against the rest of Lean world who do not care much about constructive math. Second, any kind of HoTT is probably better suited for constructive mathematics than the type theory of Lean.

OK, good to know that it is intuitionistic out of the box.

I accept excluded middle and choice. It's more a matter of understanding what's going on, about learning the principles behind Lean from the ground up.

[Kenny Lau]

if you want to get into "details" you should use term mode more

[Kenny Lau]

theorem double_neg_false_decide : ¬¬False ↔ False :=
  Decidable.not_not

theorem double_neg_true_trivial : ¬¬True ↔ True :=
  Decidable.not_not

#print axioms double_neg_false_decide
#print axioms double_neg_true_trivial

[Kenny Lau]

more cheating

[Kenny Lau]

slightly less cheating:

theorem double_neg_false_decide : ¬¬False ↔ False :=
  ⟨fun h ↦ h fun h1 ↦ h1, not_not_intro⟩

theorem double_neg_true_trivial : ¬¬True ↔ True :=
  ⟨fun h ↦ True.intro, not_not_intro⟩

#print axioms double_neg_false_decide
#print axioms double_neg_true_trivial

[Thomas Preu]

@Kenny Lau
Using tactics as I did in my derivation felt a lot like using rules of natural deduction (cf. e.g. here in the table at the end).
In which sense do I get "more details" when using term mode?

[Kenny Lau]

@Thomas Preu in the sense that it's closer to Lean, because tactics generate terms

[Kenny Lau]

if you do #print on a tactic proof you can see the actual term that the tactic generates