Pat Hayes is the final authority.
I think it is a reifying mechanism, and a definition, but not a function.
Being a definition is enough to introduce another level of abstraction
which is why it's so important.
Context Knowledge Systems
Date: Mon, 14 Apr 2014 11:50:52 -0400
Subject: Re: [ontolog-forum] IKL is a decent logic language
To: rhm@xxxxxxxxxxxxx; ontolog-forum@xxxxxxxxxxxxxxxx
CC: phayes@xxxxxxx; sowa@xxxxxxxxxxx; kr-language@xxxxxxxxxxxxxxx; rslatimer@xxxxxxx
To my knowledge in IKL, that() is a way of quoting a proposition or a reifying mechanism for propositions, and is not a function definition or any kind of definition.
I don't think IKL (or Common Logic) supports what has traditionally been called "definitions" in first order predicate logic.
PS: I sent this note to clarify my understanding. If anyone can verify I am right or wrong, I would appreciate a note.