second order encoding

Stream: Type theory

[Alexandre Rademaker]

This can be a stupid question, but what are the alternatives to encode second-order logic in dependent types?

Image something like this hypothetical second-order language:

forall P, (forall g, GreatGeneral g -> P g) -> P Napoleon

I can only think in the following Lean encoding:

section
 variable (u : Type)
 variable (P : u → Prop)
 variable (GreatGeneral : u → Prop)
 variable (Napoleon : u)

 def my := (∀ g, GreatGeneral g -> P g) -> P Napoleon
end

This gives me that my is parametrized by any predicate u → Prop such as P:

my : (u : Type) → (u → Prop) → (u → Prop) → u → Prop

But can I internalize the quantifier over predicates? Maybe Friday and I am not thinking hard enough...

[Horatiu Cheval]

Is def my := \forall (P : u -> Prop), ... and then the rest what you mean?

[Alexandre Rademaker]

I am just naming the formula...

[Alexandre Rademaker]

I made some editions to the message above... does it clarify?

[Alexandre Rademaker]

The question can be simplified, how can we encode in dependent types, or concretely in Lean, a formula such as ∀ P, ∀ x, P x that is a second-order formula

[Horatiu Cheval]

But if you do

def my := ∀ (P : u → Prop), (∀ g, GreatGeneral g -> P g) -> P Napoleon
 #check my

then

my : (u : Type) → (u → Prop) → u → Prop

So it is no longer parametrized by P, that's the way I interpreted it. Sorry if this is not what you mean

[Floris van Doorn]

Here is another example: you can state the induction principle for natural numbers as a single proposition quantifying over all predicates on ℕ (in fact, you can also prove this statement).

def statement_of_induction_for_nat : Prop :=
  ∀ (P : ℕ → Prop), P 0 → (∀ k : ℕ, P k → P (k + 1)) → ∀ n : ℕ, P n

[Horatiu Cheval]

Or like you can do the second order definition of false, def falsehood : Prop := ∀ p : Prop, p

[Alexandre Rademaker]

Oh good, yes it makes sense the examples. So second-order logic is easily encoded. I guess my confusion was given by an unexpected Lean 4 behaviors:

The example from @Horatiu Cheval parsed without errors:

 def my := ∀ (P : u → Prop), (∀ g, GreatGeneral g -> P g) -> P Napoleon

But if I omit the type of P:

section
 variable (u : Type)
 variable (GreatGeneral : u → Prop)
 variable (Napoleon : u)

 def my := ∀ P, (∀ g, GreatGeneral g -> P g) -> P Napoleon
 #check my
end

Than I got

 Test.lean    31  41 error           function expected at
   P
 term has type
   ?m.50 (lsp)
 Test.lean    31  49 error           function expected at
   P
 term has type
   ?m.50 (lsp)

[Mario Carneiro]

Lean doesn't like to infer function types for variables by seeing them on the left of an application. I'm not entirely sure why, but the type is often underdetermined since it could be a dependent pi type