Skip to main content
added 187 characters in body
Source Link
goblin GONE
  • 3.8k
  • 18
  • 39

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.

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?

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.

Source Link
goblin GONE
  • 3.8k
  • 18
  • 39

What do we call functions that behave like predicate symbols?

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?