Integrating Event with Modal Logics

This is related to the "Representation Capability" mentioned in Towards ChatGPT Maturity Model.

We need to use formal semantics to represent natural language "meanings" distinctively (so that ChatGPT can find integration points with organization business logic)

In Event Semantics needed for LLM chatbot, I described the Davidsonian event semantics with my first impression reading the paper.

Further study, I found out the Davidsonian event semantics is capable of converting the long VP chain into a long conjunctive clause. The extra hidden event argument does not have natural language correspondence therefore it is not having "conciseness" and succinctness. But it is restrictive, in that it cannot get a "simpler" sentence, everything has to be written into one long clause.

On the other hand, the MTT event semantics does not rely on that extra hidden event argument. The boilerplate codes are much more than the Davidsonian event semantics. But when comes to the final product, the actual sentence, it can support very concise and succinct sentences. In a word, it is capable to be more "natural" than the Davidsonian event semantics.

Come back to yesterday's "Every day may not be good, but there is something good in every day." let us use MTT event to formalize.

It should be

Definition all:=
? fun (A:CN) (P: i->A->Prop) => mforall x:A, fun(i':i)=>P i' x.
Definition some:=
? fun (A:CN) => fun P: i->A-> Prop => mexists x:A, fun(i':i)=>P i' x.


Parameter Day: CN.
Parameter Entity: CN.
Axiom ed: Day->Entity. Coercion ed: Day>->Entity.
Parameter good: i->Entity->Prop.
Parameter in_day_d: i->Entity->Prop.
Parameter Event: Set.
Parameter in': i->Event->Day->Prop.
Definition m(A B:Type)(f: A->B->Prop):= fun(b:B)(a:A)=> f a b.
Definition m2(A B C:Type)(f: A->B->C->Prop):= fun(b:B)(c:C)(a:A)=> f a b c.
Arguments m {A}%type_scope {B}%type_scope _.
Arguments m2 {A}%type_scope {B}%type_scope {C}%type_scope _.


Axiom ee: Event->Entity. Coercion ee: Event>->Entity.



(** Every day may not be good, but there is something good in every day. *)
Check dia (m~ ((all Day) good))
? m/\ (mforall d: Day, (mexists p: Event, m2 in' p d m/\ m good p)).

        

The good thing about MTT events is, they can be specialized with more factors on demand (such as if we know the event involves people or certain items, we can define that event schema and map it to the current "Event" type using coercion sub-typing. And it should be compatible with the modal logic we already integrated. (It is with regard to a certain interpretation of the world)

With some adaptors, the arguments of predicates can change to accommodate the interpretation "i".

Takeaway

MTT events

* Concise than Davisonion events

* More configuration needed

* Able to be integrated with modal logic (with some tweaks on argument ordering)