Zulip Chat Archive

Stream: Type theory

Topic: second order encoding


Alexandre Rademaker (Apr 01 2022 at 15:26):

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 (Apr 01 2022 at 15:35):

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

Alexandre Rademaker (Apr 01 2022 at 15:48):

I am just naming the formula...

Alexandre Rademaker (Apr 01 2022 at 15:50):

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

Alexandre Rademaker (Apr 01 2022 at 15:52):

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 (Apr 01 2022 at 15:53):

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 (Apr 01 2022 at 15:55):

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 (Apr 01 2022 at 15:57):

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

Alexandre Rademaker (Apr 01 2022 at 16:06):

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 (Apr 01 2022 at 16:10):

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


Last updated: Dec 20 2023 at 11:08 UTC