You're welcome, but I think you're still mixing up programming language concepts with FOL concepts.

>> The point I'm trying to note is that predicates, and constant atomic terms are on the ground level; maybe we can say that they get interpreted into boolean. And functions, constants (0-arity functions) are on a different level; maybe I'll say they get evaluated into elements in the domain; i.e. they are not interpreted into boolean truth/false values.

Not in FOL. There are no "boolean truth/false values" in FOL. That is to say, there are two truth values that can be assigned to atoms by an interpretation, but they do not have any concrete representation in FOL. There isn't any FOL entity, term, atom, or formula, that means "true" nor one that means "false". Accordingly, nothing "evaluates" or "is interpreted" into "true" or "false" or to anything else. There's no way to write, in FOL something like "P(a,b) = true" and even equality is not a FOL concept. You certainly can't magically replace P(a,b) with its truth value in a formula, because there's nothing that can represent a truth value in a formula in FOL. Neither can you replace ƒ(x,y) with the constant "a" in some atom, because there are no rules for replacing anything with anything else at all, in FOL.

I appreciate that you find it hard to believe, and think that I'm somehow confusing your "semantic analysis" with a syntactic description of FOL because that's how it works in programming languages, but like I said before, that is part of the power of FOL: syntax and semantics are one. All of FOL is right there in the four logical operators, the sets of predicate and function symbols and the parentheses and commas used to form well-formed formulae. Well-formed formulae have a truth value that depends on the truth values assigned to atoms by the current interpretation but there's no "evaluation" or "interpretation", or even "computation" and there isn't any rule for replacing anything with "true" and "false" values or "elements in the domain" because there is nothing representing truth values and there are no rules for replacing atoms or functions with anything. You form a FOL formula and it is either true or false, depending on how you formed it. You might misread it or misunderstand it, but that's another matter.

The reason for all this weirdness is that FOL is made to be used by humans, not computers. FOL was created before computers and computers were modelled after mathematical logic concepts some of which were borrowed from FOL. But FOL is not for computers, it's for human beings. And human beings don't need to do and probably are even incapable of, the semantic analysis that a computer must, to process a statement in a formal language. So if you're trying to understand FOL in the context of computers, you're in the wrong context.

Anyway, good luck with what you're doing, but I think it will help you to try to clear up your understanding of the various terminologies and formalisms you are trying to use. Unfortunatly I don't know what text to recommend for this puprose. My go-to source for FOL is Foundations of Inductive Logic Programming by Nienhuys-Cheng and De Wolf. It's about ILP, but to understand ILP it is necessary to understand logic programming, to understand logic programming it is necessary to understand FOL and to understand FOL it is necessary to understand propositional logic so the first couple of chapters are about propositional logic and FOL. Still, it's probably not the kind of source you need. You can probably find a suitable textbook with an online search though.