TERMIUM Plus^®

Record 1,  Textual support,  English

Record number: 1, Textual support number: 1 CONT

Even if the denotations of terms were the same for all agents (and for use), we would need to have a way of referring to the constants used by agents for denoting objects (because the constants used by these agents might not appear in our theory). Suppose we were to Skolemize a nested belief formula by replacing the existential variable by a Skolem constant, say Sk. Sk denotes an object - we do not know which one, but A does know! (We know that A knows which object Sk denotes because the semantics of B tells us that there is an expression of the form P(C) in A's theory such that C denotes whatever Sk is supposed to denote.) Therefore, we need a constant to denote whatever it is that Sk denotes. We introduce an operator o. called the bullet operator, that transforms any term inside the context of the B operator to a constant denoting, for the believer, whatever that term is supposed to denote for us.  1, record 1, English, - bullet%20operator

Record 1,  Textual support,  French

Record 1,  Textual support,  Spanish