meaning of ɑ, β in proof headers about logical equivalence

Stream: new members

[rzeta0]

I've just started Chapter 5 Logic of MoP.

Without explanation or discussion, the proofs have introduced the use of ɑ and β in the proof headers. Two examples follow:

Example 1

example {P Q : α → Prop} (h1 : ∀ x : α, P x) (h2 : ∀ x : α, Q x) :
    ∀ x : α, P x ∧ Q x := by
  intro x
  constructor
  · apply h1
  · apply h2

Example 2

example {P : α → β → Prop} (h : ∃ x : α, ∀ y : β, P x y) :
    ∀ y : β, ∃ x : α, P x y := by
  obtain ⟨x, hx⟩ := h
  intro y
  use x
  apply hx

I can only guess what the alpha and beta are: placeholders to allow the variables to be of any type?

Question: I'd welcome guidance and explanation of what these alpha and beta are.

---

I notice they don't appear in simpler poofs that don't use quantifiers:

example (P Q : Prop) : P → (P ∨ ¬ Q) := by
  intro hP
  left
  apply hP

[Edward van de Meent]

these are implicit arguments/variables.
adding set_option autoImplicit false will make lean throw errors for these kinds of implicit variables.

[Edward van de Meent]

rzeta0 said:

I can only guess what the alpha and beta are: placeholders to allow the variables to be of any type?

that's exactly right :100:

[rzeta0]

so is it only greek letters that are taken as such implicit variables / placeholders?

[Edward van de Meent]

when the autoImplicit option is true, any identifier that is not bound to a declaration or a variable, gets added as an implicit argument.

[Kyle Miller]

Let's not assume it's autoImplicit at work @Edward van de Meent without verifying. Are there any variable commands before this @rzeta0? Edit: Edward already checked, and the answer is "no".

[Edward van de Meent]

Kyle Miller said:

Let's not assume it's autoImplicit at work Edward van de Meent without verifying. Are there any variable commands before this rzeta0?

this is in Mechanics of proof, and i checked the file...

[Kyle Miller]

Thanks, that's not something I could tell from reading the thread.

[Kyle Miller]

Your first example @rzeta0 could be written equivalently as

example {α : Sort _} {P Q : α → Prop} (h1 : ∀ x : α, P x) (h2 : ∀ x : α, Q x) :
    ∀ x : α, P x ∧ Q x := by
  intro x
  constructor
  · apply h1
  · apply h2

[Edward van de Meent]

rzeta0 said:

I've just started Chapter 5 Logic of MoP.

it was mentioned at the top of the thread

[Kyle Miller]

(I just didn't know that you checked it Edward. I wanted to be sure this wasn't misguided advice.)