![🌐](data:image/svg+xml,<svg xmlns="http://www.w3.org/2000/svg" width="32" height="30"><rect fill-opacity="0"/></svg>)
![🌐](data:image/svg+xml,<svg xmlns="http://www.w3.org/2000/svg" width="32" height="32"><rect fill-opacity="0"/></svg>)
YouTube
youtube.com
YouTube
YouTube
YouTube
YouTube 
I will briefly describe how to form a first-order term or formula. I believe that will be enough to distinguish between a grounded expression and a non-grounded one. You can find more details in any introduction to mathematical logic book if you want.
In first-order logic, you use a collection of “variable symbols, constant symbols, function symbols and relation symbols” as well as the “logical connectives, quantifiers, commas and parentheses” to create terms and formulas.
The relation symbols are what you called predicate symbols.
Every function/relation symbol has an arity (which is the number of terms it accepts).
The constant symbols and variable symbols are the atomic terms. (They are called atomic terms because they contain no proper sub-terms)
You can use function symbols and terms to create new terms.
If $t_1$, $t_2$ and $t_3$ are terms and $F$ is a function symbol of arity 3, then $F(t_1, t_2, t_3)$ is a term. ($t_1$, $t_2$ and $t_3$ are proper sub-terms of $F(t_1, t_2, t_3)$ because they are sub-terms that are different from the full term. Since $F(t_1, t_2, t_3)$ has proper sub-terms, it is a complex term, not an atomic term.)
You can use relation symbols and terms to create new atomic formulas. (They are called atomic formulas because they contain no proper sub-formulas)
If $t_1$, $t_2$, $t_3$ and $t_4$ are terms and $R$ is a relation symbol of arity 4, then $R(t_1, t_2, t_3, t_4)$ is a formula.
You can use logical connectives and formulas to create new formulas.
If $\phi$ and $\psi$ are formulas and $x$ is a variable symbol, then $(\neg \phi)$, $(\phi \land \psi)$, $(\phi \lor \psi)$, $(\phi \to \psi)$, $(\phi \leftrightarrow \psi)$, $\forall x \phi$ and $\exists x \phi$ are all formulas.
Assume that $x_0, x_1, x_2, …$ are the variable symbols, $b, c$ are the constant symbols, $F$ is a Function symbol with arity 2 and $R$ is a relation symbol with arity 2.
$F(b, F(b, c))$ is a Grounded term because it doesn’t contain any variable symbols.
$F(c, x_1)$ is not a Grounded term because it contains a variable symbol.
$(R(b, c) \lor R(F(b, F(b, c)), F(c, b)))$ is a Grounded formula because it doesn’t contain any variable symbols.
$(R(b, c) \land R(F(b, F(x_1, c)), F(c, b)))$ is not a Grounded formula because it contains a variable symbol.
Constant symbols represent a fixed entity in the domain of discourse, while variable symbols represent an arbitrary element in the domain of discourse. You can quantify over variable symbols with “for all ($\forall$)” and “there exists ($\exists$)” but you can’t quantify over constant symbols.
Let Domain $D=\{0,1,2,3\}$
We might have a Predicate $P_1(n):n^2<1$
Consider the Statement $S_1 \equiv \exists n : P_1(n)$ , which has a variable $n$ , hence it is not ground. Statement $S_1$ can be evaluated : it is true , when $n=0$
We can write that Statement $S_1$ like this too : $P_1(0) \lor P_1(1) \lor P_1(2) \lor P_1(3)$ , which has no variables , hence it is ground. Still , Statement $S_1$ will evaluate to true
Parts of $S_1$ are ground too.
We might have a Predicate $P_2(n):n^2>0$
Consider the Statement $S_2 \equiv \forall n : P_2(n)$ , which has a variable $n$ , hence it is not ground. Statement $S_2$ can be evaluated : it is not true , when $n=0$
We can write that Statement $S_2$ like this too : $P_2(0) \land P_2(1) \land P_2(2) \land P_2(3)$ , which has no variables , hence it is ground. Still , Statement $S_2$ will evaluate to not true
Parts of $S_2$ are ground too.
When we have Statements with Predicates containing variables , the Statements could be true , not true , not yet known.
These are not ground.
When we have Statements with Predicates without variables , the Statements could be true , not true , though always known , generally.
These are ground.
Parts [ Eg $P_1(3)$ , $P_2(0)$ ] & Combinations [ Eg $S_1 \lor \lnot S_2$ , $\lnot S_1 \lor \lnot S_2$ ] are ground too.
Criterion is that there should be no variables involved.
