formal semantics

Stream: lean4

[Alexandre Rademaker]

Formals Semantics is a branch of linguistics that studies the representation of sentences meaning. Dependent Types in Formal Semantics is not new, see this paper and here.

I was trying to convert some approaches for formal semantics previous implemented in Coq to Lean. But the Donkey sentence from second link above already didn't work as expected. It doesn't make sense to have a different type for to ditransitive verbs: own and beat. But f I say that own is Prop, the formula is not typed checked in Lean 4. Any idea? I should be missing something...

section MTT

  universe CN

  variable (_farmer_n_1 : Type CN)
  variable (_donkey_n_1 : Type CN)
  variable (_own_v_1 : _farmer_n_1 → _donkey_n_1 → Type)
  variable (_beat_v_to : _farmer_n_1 → _donkey_n_1 → Prop)

  #check ∀ z : (Σ x : _farmer_n_1, Σ y : _donkey_n_1, _own_v_1 x y), _beat_v_to z.1 z.2.1

end MTT

[Henrik Böving]

Sigma is a notation for

structure Sigma {α : Type u} (β : α → Type v) where
  fst : α
  snd : β fst

which as you can see requires its 2nd argument to return a type, there is a way to fix this using a

structure PSigma {α : Sort u} (β : α → Sort v) where
  fst : α
  snd : β fst

or just the existential quantor instead of sigma types.

[Henrik Böving]

There might also be notation for PSigma but I wouldnt know which /o\

[Alexandre Rademaker]

I found Σ', and it works with own and beat constructing a Prop. Thank you... Now I need to really understand PSigma...

[Alexandre Rademaker]

and indeed, the ∀ z : (∃ x : _farmer_n_1, ∃ y : _donkey_n_1, _own_v_1 x y), _beat_v_to z.1 z.2.1 also works. So now I have to understand the difference between PSigma, Sigma and Exists.

[Henrik Böving]

Their definitions are here https://github.com/leanprover/lean4/blob/0d03c6e3198c7c01f222be567b401e594cdedbd6/src/Init/Core.lean#L69-L80 and here is the docs for std lib, compiler and mathlib https://leanprover-community.github.io/mathlib4_docs