how to represent the predicate member/2 in first order logic?

Question

Lets say we have a predicate that returns true if there is a member in a list. False if not. In prolog I ended up with a code like below

member(B,[B|_]).
member(B,[_|A]):- member(B,A).

Its true for member(1,[3,1,2]). and false for member(1,[4,5,6]). How to use FOL to represent the above function?

Answer 1

In first order logic you might want to use a predicate and not a function to represent your function. If $F$ is a $n$-ary function in a FOL, then if $X_1,\ldots,X_n$ are terms of your language $F(X_1,\ldots,X_n)$ will again be a term. For example, $+(X_1,X_2) \colon = X_1+X_2$ represents the sum function in PA.

Now, $X_1 \in X_2$ is not a term! It's a first-order formula (a thing that you want to put a truth value). When you want $F(X_1,\ldots,X_n)$ to represent a formula (and receive a truth value), then $F$ must be a predicate symbol.

In your case, member$(X_1,X_2) \colon = X_1 \in X_2$

Answer 2

First of all, given a formula $\varphi$, a term $t$ and a variable $x$, let $\varphi[x\gets t]$ denote a substitution instance, that is the result of $t$ substituted for $x$ in $\varphi$. (*)

To introduce membership, first one needs to introduce classes, which are special FOL terms.
Given the formula $\varphi$ and the variable $x$, let the string $$\{x \mid \varphi\}$$ denote a term named class term or simply class.

Given the formulae $\varphi, \psi$ and the variables $x,y,z$ and the term $t$, we set the following abbreviations: $$ \begin{aligned} t \in \{x \mid \varphi\} &\quad\text{short for}\quad \varphi[x \gets t]\\ % \{x \mid \varphi\} \in t &\quad\text{short for}\quad \exists z ( (z \in t) \wedge \forall x ((x\in z) \leftrightarrow \varphi))\\ % \{x \mid \varphi\} \in \{y \mid \psi\} &\quad\text{short for}\quad \exists z (\psi[y \gets z] \wedge \forall x ((x\in z) \leftrightarrow \varphi)) \end{aligned} $$

where $\in$ denotes the membership predicate.

(*) Note that syntactic substitution is a formal FOL operation and not a mere find-and-replace. Particularly, one should introduce fresh variables when substitution terms are bound variables in their formulae.