 Analogous claims hold for the past versions of the above schemes, with \(H\) and \(P\) instead of \(G\) and \(F\). An axiomatic system for the minimal FOTL with constant domain semantics, as well as some important theorems of it, are provided in the supplementary document: