Which of the following expressions are formulas of predicate logic?

(i) $\forall X \, \forall Y \ (X \subseteq Y \leftrightarrow (\forall x \ x \in X \to x \in Y))$

(ii) $\forall P \ P(0) \land \forall n \ (P(n) \to P(n+1) ) \to (\forall n \, P(n))$

(iii) $\forall t\, G(P(t) \, U \, P(t))$, where $P$ is a predicate symbol.

Currently doing some past papers and I wanted to confirm this...

For a formula to be of a predicate logic it must follow the well-formed rules.

Only (iii) is a formula of predicate logic because it follows the well-formed rules. (i) and (ii) use predicates instead of variables after the quantifiers therefore not well-formed and not a formula of predicate logic. Is there any other reasons why they may not be of predicate logic?

  • 1
    $\begingroup$ If a string is well-formed it can get demonstrated by listing out each step in the construction of the formula with citations to the formation rules on the side. If it's not a well-formed formula, we can usually cite a violation of the formation rules. $\endgroup$ – Doug Spoonwood Aug 3 '18 at 22:53
  • 1
    $\begingroup$ Also assuming $U$ as $\lor$ (disjunction), (iii) is not: if $P$ is a predicate symbol, then $P(t)$ is a formula and not a term; thus $G(P(t) \lor P(t))$ is wrong, because the predicate $G$ needs a term in its argument-place and not a formula. $\endgroup$ – Mauro ALLEGRANZA Aug 4 '18 at 8:26

I don't know what your underlying language is, but if your set of variables includes $X,Y,x$ and your signature is just consisting of $\in$, taking $\subseteq$ as exactly the abbreviation as the right hand side, then (i) is a well-formed formula in the language of set theory. You may even add $\subseteq$ as a binary relation symbol to make it well-formed in some other signature of your taste.

(ii) seems to suggest that $P$ is a unary predicate which is quantified at the beginning, thus this formula seems not be well-formed in first-order logic.

If you assume for (iii) that $t$ is a variable symbol, and $G,U$ are unary/binary predicate symbols respectively and $P$ is a unary predicate, then this formula does not really make sense, as we have a predicate applied to another predicate.

I think there is needed information missing to really answer the questions for which you should search yourself(in the book where this question is from). The question

Is the formula $\phi$ a well-formed $FO$-formula?

is always to be read with some appropriate context.

  1. There is no pure $FO$(at least not per se). First-order logic is defined, in its classical form, over a signature $\sigma=(\mathrm{Fun},\mathrm{Rel},\mathrm{Con},\mathrm{ar})$ with $\mathrm{Fun},\mathrm{Rel},\mathrm{Con}$ being the sets of function, relation and constant symbols respectively(it may be that the formalism you were introduced to is slightly different, don't worry about that too much). The object of discourse is thus always $FO(\sigma)$, i.e. first-order logic of/to a signature $\sigma$. $\mathrm{ar}$ is a function, associating every predicate and function symbol with the arity, i.e. how many arguments they are required(and permitted) to take.
  2. The set of variables needs to be formally specified. $FO(\sigma)$ is built over a set of variables, here denoted $Var$. Similarly as the set of function symbols, relation symbols, etc., this set in general may have any size, i.e. cardinality, but is usually either assumed to be finite or countably infinite. With formally specified, I mean that e.g. taking $Var=\{x_1,x_2,\dots\}$, then my variable symbols for $FO(\sigma)$ are(technically) only the syntactical constructs $x_1,x_2,\dots$

Now, what is the set of well-formed formulas, $FO(\sigma)$? This set is generated in the following way from the before mentioned sets:

First, we form the set of terms of this signature $\sigma$.

  1. Every variable $x$(note that I take $x$ here as a variable for a variable symbol which is a concrete object, a string, and a member of $Var$) is a term.
  2. Every constant $c$(similar note as to the variables) is a term.
  3. If $t_1,\dots,t_n$ are terms, and $f$(similar note as to the variables) is a $n$-ary function symbol($\mathrm{ar}(f)=n$), then $f(t_1,\dots,t_n)$ is a term.

Then $FO(\sigma)$ is formed using this set of terms and $\sigma$ again:

  • If $t_1,\dots,t_n$ are terms and $P$(similar note as to the variables) is an $n$-ary predicate symbol($\mathrm{ar}(P)=n$), then $P(t_1,\dots,t_n)$ is a formula.
  • If $\phi\land\psi$ are formulas, then $(\phi\land\psi)$, $\neg\phi$ and $(\phi\lor\psi)$ are formulas.
  • If $\phi$ is a formula and $x$ is a variable, then $\forall x\phi$ is a formula

We remark a few things on the process of forming the set of well-formed first-order logic formulas over a signature $\sigma$ and a set of variable $Var$ I just sketched:

  • Every variable symbol in a formula is a member of $Var$ and concretely specified as a syntactical object(I omit that comment in the following).
  • Every predicate symbol in a formula is a member of $\mathrm{Rel}$
  • Every function symbol in a formula is a member of $\mathrm{Fun}$
  • The arity is also a syntactical feature, e.g. a function symbol is ought to have $n $ argument strings syntactically to be well defined.

So for you to analyse if a formula is well-formed, your first question has to be over what signature and over what set of variables. Then you may assert membership in $FO(\sigma)$.

As I said before, this is just a sketch. First, what I was describing was first-order logic without equality, but the differences are marginal(on the syntactical level).

We all use shorthand notations and deviate from this formal specification. Thus e.g. even when some author formally defined $Var=\{x_1,x_2,\dots\}$, you're likely to see $\forall x\phi$ as a formula. This is meant to be a shorthand but it is not technically fine, but such a minor detail that normally no one gets hurt. A good mantra is that you are allowed to deviate if you can always rephrase it properly.

Another common shorthand also used in your example is that binary predicates are often denoted in infix notation, that is, instead of writing $>(x,y)$ you write $x>y$.

There are however situations where the concrete syntactical structure matters, that is why this is set on such a firm ground.

I want to end with, that working with these objects is a purely syntactical matter. There is no meaning attached to these strings(yet) and that is how they ought to be treated. Two strings differ if they differ in one symbol already. It is not about representing (semantically) the same.

EDIT: I tried to not give you an answer but to explain to you the context of how to find an answer yourself(which some of my perspective on the top). I could not have given a precise answer as you we're asking about a syntactic technicality for which I don't know the complete surrounding to, i.e. the signature, etc. This answer turned out longer than expected and thus if something is unclear, we should clarify this together in the comments.

  • $\begingroup$ If ∈ is a binary predicate, (i) is not well-formed, since we have x ∈ X instead of the well-formed ∈(x, X). $\endgroup$ – Doug Spoonwood Aug 3 '18 at 22:52
  • 1
    $\begingroup$ @DougSpoonwood You are perfectly right I preached firm grounds and you caught me using an abbreviation. Let me add this in. Thank you. This just comes with the length $\endgroup$ – blub Aug 3 '18 at 22:53
  • $\begingroup$ Wow, comprehensive, thank you. There is no other context given I can assure you. I think it's assumed the lowercase characters are the variables. For (iii) I mistook the U for a disjunction instead of a function. $\endgroup$ – Philip D'Souza Aug 3 '18 at 23:12
  • $\begingroup$ I thought so. But taking these assumptions you can now re-verify your findings. $\endgroup$ – blub Aug 3 '18 at 23:13
  • 1
    $\begingroup$ Well, under your assumptions that $X,Y$ are predicate symbols, the whole formula becomes rather broken. The main point I wanted to make is that it always depends on the signature and more generally the surroundings on which you built the set of well-formed formulas like the set of variable symbols. Once you've specified these, there is a definite procedure to assert membership. $\endgroup$ – blub Aug 3 '18 at 23:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.