Expressing "Highest" in First Order Logic

Question

I'm writing a First Order Logic sentence to express a "Highest" function. (ie. highest temperatures in a city) I'm thinking along the lines of something like this:

HighestTemp returns T1 s.t. $$\exists T_1 \forall T_2 T_1 > T_2$$

But I suspect I will need to use an equality operator ("=") to express this. I am defining the HighestTemp function in preparation for use in another FOL sentence.

In regular programming terms I'm looking to define a function like:

   HighestTemp(Toronto,2013)

That spits out the highest temperature recorded that year.

For later use in a sentence expressing:

   The HighestTemp in Toronto 2013 is greater than the HighestTemp in Chicago 2010.

Can someone point me in the right direction?

Im using FOL for this as practice.

Answer 1

Assume $3$ sorts, Temp, Places and Times, and a function $\tau : \mbox{Places} \times \mbox{Times} \rightarrow \mbox{Temp}.$

Now let $P$ denote a unary predicate on places and $T$ a unary predicate on times. For example

1. $P(p)$ iff $p=\mathrm{Toronto}$
2. $T(t)$ iff $\mbox{First Day Of 2013} \leq t < \mbox{First Day Of 2014}$.

Then the maximum temperature recording at places satisfying $P$ within the scope of the times satisfying $T$ is the unique $\eta$ in $\mathrm{Temp}$ with

1. $\exists p \in \mathrm{Places}, t \in \mathrm{Times} : P(p) \wedge T(t) \wedge \tau(p,t) = \eta$
2. $\forall p \in \mathrm{Places}, t \in \mathrm{Times} : P(p) \wedge T(t) \rightarrow \tau(p,t) \leq \eta$

A few remarks.

1. (Obviously) these formulae need to be combined with a conjunction.
2. You need some assumptions on $P$ and $T$ to guarantee existence of $\eta$.