How do I explicitly see the propositional or logical constructors in Lean 4?

Question

I have the following goal:

⊢ ∃ δ, 0 < δ ∧ ∀ (x : ℝ), 0 < x - 0 ∧ x - 0 < δ → M < f x

I am curious and want to see how the propositional constructors are applied to my expressions (especially AND and IMPLIES and perhaps EXSITS) e.g., I want to know if it's Implies( And( Exists(delta, delta > 0), ∀ (x : ℝ), 0 < x - 0 ∧ x - 0) , M < f x or something else. Can I have Lean4 show this info to me, at least temporarily?

I tried it the following:

Hover over an operator in the info view and it will highlight the arguments passed to that operator. Alternatively try setting some option like pp.notation (see https://leanprover.github.io/reference/other_commands.html#options) to false.

but it didn't work for forall and I think also it didn't work for implies (it did for exists) see:

---

In addition, I don't understand. I am trying to click the forall definition or the implication, but it doesn't take me to either in vscode. Why doesn't it work for those? I assumed perhaps forall is defined in terms of exists but even if that was the case I should be able to see it's declaration/definition.

Answer 1

After reading this question many times, I think the main question is as follows:

Why do implications and forall behave differently from other notations, for example in the info-view hover feature, the click-through to see the definition, and print settings like set_option pp.notation false/set_option pp.all true?

As I state in my comment above, implication and forall are special in dependent type theory. They are not defined, but instead built into the logic itself. They are just instances of dependent function types (Pi types). An implication p -> q can be thought of as the type of functions which take "proofs" of p to "proofs" of q. Similarly, ∀ (x : A), r x can be thought of as the type of dependent functions which take x : A to a "proof" of r x. Lean prints the term with one of three notations depending on circumstance, but they are all internally represented the same as the following examples show:

import Mathlib

-- logical implication
axiom p : Prop
axiom q : Prop
#check p → q         -- p → q : Prop
#check ∀ (a : p), q  -- p → q : Prop
#check Π (a : p), q  -- p → q : Prop
#check (a : p) → q   -- p → q : Prop
theorem ex1 (a : p) : q := sorry
#print ex1           -- theorem ex1 : p → q


-- function types
axiom A : Type
axiom B : Type
#check A → B         -- A → B : Type
#check ∀ (a : A), B  -- A → B : Type
#check Π (a : A), B  -- A → B : Type
#check (a : A) → B   -- A → B : Type
def ex2 (a : A) : B := sorry
#print ex2           -- def ex2 : A → B

-- forall
axiom r : A -> Prop
#check ∀ (x : A), r x  -- ∀ (x : A), r x : Prop
#check Π (x : A), r x  -- ∀ (x : A), r x : Prop
#check (x : A) → r x   -- ∀ (x : A), r x : Prop
theorem ex3 (x : A) : r x := sorry
#print ex3             -- theorem ex3 : ∀ (x : A), r x

-- dependent function types
axiom C : A -> Type
#check ∀ (x : A), C x  -- (x : A) → C x : Type
#check Π (x : A), C x  -- (x : A) → C x : Type
#check (x : A) → C x   -- (x : A) → C x : Type
def ex4 (x : A) : C x := sorry
#print ex4             -- def ex4 : (x : A) → C x

Now, it is also probably true Lean 4 could be better at conveying this information in the hovers, info view, and print settings. There is no print setting I know of which prints these all the same.

---

Also, you mention forall or exists being defined in terms of the other. This is common in classical first order logic, but it isn't generally true of dependent type theory (even dependent type theory with classical logic). There are many advantages of defining forall and exists in the way Lean does, where Exists is defined as a structure and forall is a Pi type.

---

I highly recommand the first four sections of Theorem Proving in Lean 4 for an explanation on this.