3
$\begingroup$

Assume a metatheory that supports lambda-abstraction, and an object language that is merely first-order. Now let $\varphi$ denote a formula in the object language with one free variable $x$. Then we can write $\lambda x. \varphi$ in order to mean the function that accepts an expression $E$ in the object language and returns the formula $\varphi[x/E].$ Hence $\lambda x. \varphi$ works just like a predicate symbol. For example, if $P$ is a predicate symbol in the object language and we let $Q$ equal $\lambda x.\varphi$, then $\forall y(Py \rightarrow Qy)$ is a well-formed formula, despite that $Q$ is not a predicate symbol.

Question. What do we call functions (like $\lambda x. \varphi$) that behave like predicate symbols?

For example, in the following sentence, what word should go in place of [///]?

Let $Q$ denote the [///] $\lambda x.\varphi.$

Obviously, the word "function," but its not really a good fit, being far too general.

Improve this question
$\endgroup$
6
  • $\begingroup$ In some foundations of mathematics, such as type theory, predicates are just functions. In most settings can view a predicate as a function from the domain into the set/type of truth values. $\endgroup$
    – Håkon R. Gylterud
    Commented Jun 2, 2014 at 10:20
  • 1
    $\begingroup$ @HåkonR.Gylterud, note that "predicate" is a distinct concept from "predicate symbol." $\endgroup$
    – goblin GONE
    Commented Jun 2, 2014 at 10:23
  • $\begingroup$ True. But the syntactic and semantic parts are quite closely in correspondence. I may not understand you correctly, but think what you are observing here is that formulas and predicate symbols both represent predicates. And that formulas can be composed in the same way we can compose functions. $\endgroup$
    – Håkon R. Gylterud
    Commented Jun 2, 2014 at 10:53
  • 2
    $\begingroup$ In most formal contexts where $\lambda$ applies to predicates, there is also a type $\mathrm{Prop}$ of truth values and predicates are viewed as functions $X \to \mathrm{Prop}$. $\endgroup$
    – François G. Dorais
    Commented Jun 2, 2014 at 12:53
  • $\begingroup$ @FrançoisG.Dorais, okay but what are you getting at? $\endgroup$
    – goblin GONE
    Commented Jun 2, 2014 at 13:09

2 Answers 2

Reset to default
5
$\begingroup$

I would call such a thing propositional function.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Worth adding: this is a very standard term, dating at least back to Bertrand Russell in 1903. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Oct 6, 2015 at 18:28
  • $\begingroup$ I am quite sure I got it from Russell. When I was young and idealistic I read a lot of what he wrote. $\endgroup$
    – Andrej Bauer
    Commented Oct 6, 2015 at 19:32
1
$\begingroup$

Despite that a question about how to name something is expected to be simple, I believe, this is a difficult question; it took me some time to prepare an answer.

These difficulties are caused by several facts:

  1. The language of $\lambda$- calculus is untyped, but it is used here as a metalanguage for a language whose expressions are of several types.

  2. The $\lambda$- calculus has many interpretations (not only as "functions");

  3. A well-established practice of naming things is not established.

Since all expressions in $\lambda$- calculus language are of one type, we refer to them using one name which coincides with the name of objects in its interpretation. But there are many interpetations of $\lambda$- calculus and with each interpretation intended for the $\lambda$- calculus, we use a name specific for the interpetation. Here are main interpretations of $\lambda$- calculus language terms:

(1) As functions - an interpretation widely used in mathematics, from which this calculus originates;

(2a) As expressions of a language - an interpretation used in linguistics to describe the syntax of languages

(2b) As meanings of expressions of a language - there are many interpretations used in linguistics to describe meaning of expressions (personally, I treat meaning of a name as a set - the set of things to which we refer by using the name).

With interpretation (1), it is natural to refer as "functions" to the objects in the universe of discouse of the $\lambda$- calculus. But with the interpretations of kind (2a), it is not clear which term to use to refer to expressions of a language. I would use in this case the term "symbol", which emphasizes the fact that such an object refers to another object; a long expression is also a symbol - a composite symbol (notice, that Microsoft calls "operator" the symbol of an operation. which is in sync with this).

A metalanguage discusses about another language, and therefore, I would refer to the things in its universe of discourse as "symbols". Here is how $\lambda-$calculus talk about symbols: when in metalanguage we say that $Q$ denotes $\lambda x .\phi$, we inform that we will also use expressions like $Q(x)$, and we are allowed to make substitutions - replace "$x$" with other expressions.

The $\lambda$- calculus language uses only variables, but when it is part of a metalanguage of a language with expression of different types, we must also have constants as proper names for types, "type-names". A first order language has expressions of 2 types, and 2 such type-names are required for this. These are "predicate" and "function".

Thus, in expression "$Q$ denotes [///] $\lambda x .\phi$", instead of [///] we can write "predicate symbol" (or "function symbol").

Notice, that if we use $\lambda$-calculus in metalanguage of a language L, this has nothing to do with how the language L is interpreted. Therefore it is not correct to consider "functions" as a generic name for objects in the universe of discourse of L.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Notice that this is not a direct answer to your question. I just explained a phenomenon, and replied to a question inside the "body" of the question. $\endgroup$
    – Ioachim Drugus
    Commented Jul 27, 2014 at 22:18
  • 1
    $\begingroup$ The $\lambda$-calculus is not necessarily untyped. $\endgroup$
    – Andrej Bauer
    Commented Jul 28, 2014 at 7:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .