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:


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.

  • $\begingroup$ Why you need FOL for this task? $\endgroup$ – Kaa1el Apr 3 '14 at 5:11
  • 1
    $\begingroup$ You're going to have to be clearer about what you want. Are you just trying to define the greatest element $x$ satisfying a predicate $P$? $\endgroup$ – goblin GONE Apr 3 '14 at 5:12
  • 1
    $\begingroup$ In LaTeX you can use \exists to get $\exists$ and \forall to get $\forall$. $\endgroup$ – David Apr 3 '14 at 5:12
  • 1
    $\begingroup$ If you want $f(x)=y$ to be defined, then you can't quantify over $x$ and $y$. These need to be free variables. (Also using underscore will subscript the index, T_1 rather than T1. If you have several characters to put in the subscript use braces, e.g. T_{42}. For superscript you can use ^. $\endgroup$ – Asaf Karagila Apr 3 '14 at 5:18
  • $\begingroup$ @user18921 I've edited my question in response. Please have a look. Thanks. $\endgroup$ – user1846359 Apr 3 '14 at 5:23

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$.
  • $\begingroup$ I feel like the last logical sentence is nonsense but I am at work and do not have time to really analyze it. $\endgroup$ – Trismegistos Apr 3 '14 at 9:41
  • $\begingroup$ @Trismegistos, I think it was correct (I was trying to express the universal property of joins) however it suddenly occurs to me that we don't need joins or suprema here, we just need the maximum. So I've edited. $\endgroup$ – goblin GONE Apr 3 '14 at 9:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.