> Can you explain this a bit?

Not very well but I'll try. The idea is I'm trying to describe cannot be restricted to syntax, the summary of FOL you give is strictly syntactical. What I'm trying to observe is how predicates, functions, and variables are all variable. I mean they're all substitute-able; in this sense they're all "variable".

Predicates get evaluated to booleans so I understand them in the same "level of variable" as logical connectives. Functions always end up being evaluated into things in the domain, same as the variables; so I understand both variables and functions in their own "second level of variable".

And so, understanding (trying to) FOL this way, syntactically defined functions aren't really functions, but indirect variables. Which makes me think that the quantifiers are the actual functions (the parenthesis) which I was referring to.

In this sense the real important thing about parenthesis is the binding variables, setting them into a scope. But by this point my intuition tells me I've assumed something wrong or maybe I just leaped over something(?).

All I know is there's a reason quantifiers only take in variables (as syntactically defined) and I am trying to pin down this reason, but as I said, I still *have questions about quantifiers. In any case I've already spent way too long writing this post which might be wrong or slightly wrong/imprecise and I cannot tell how wrong and somebody would need to tell me or ask me something poignant.

I think what you're getting has truth. For myself, I would generalize what you're saying as any given formula/expression is embedded in some context/environment. If one continues to "step back" or go one meta (or repeatedly so), you'll find that at some point, you, the reader/interpreter, will need to fill in some implicit or unreified context. We could call these things (shared) assumptions or axioms. As you say, if I use a function `f` to form a term in my formula written in first-order logic, the definition of `f` is implied because it is expressed "somewhere else". The question is then "where is that expressed?". Since the definition of `f` is assumed from the point of view (semantics) of first-order logic, the definition of `f` could be interpreted as "variable" at a "higher" level.

Going to your parenthesis point, I agree that it is indicating the scope (i.e., the context/environment), and in that sense, I interpret parenthesis here as a kind of meta function, akin to how macros are "compile-time" functions rather than "run-time" functions.

I think first-order logic and relatedly most (all?) logic programming languages are missing a facility for "reasoning" about terms themselves. The reflexive answer to this is types, but this is largely wielded as a developer tool not as a means of expressing meaning. Adding constraints to logic programming is perhaps some of the way there and has the benefit (hope) that type-like ideas could be expressed compositionally as logical formulas rather than as declarations provided by the language.

My own pursuit of this subject is to see if these "levels", as you hint at, can be traversed and integrated into one logical formula language and notation. This all implies some kind of homoiconic metaprogramming, but easier said than done.

Indeed, I feel like I'm reaching towards a generalized understanding of context.

It seems to me that unless the logical languages are restricted from reasoing about themselves they become either incomplete or worse, inconsistent.

I have a sensation that on the computer science side of things, unless "reasoning about terms themselves" is somehow 'handled' (restricted) one can end up with undecidable systems, or worse...

But I still have questions about complexity so I cannot really undesrtand how completeness and soundness realte to decideability.

Thank you for the explanation. I think I understand what you're trying to say, but what you're trying to say doesn't work in FOL. Perhaps it works in the context of programming languages, but I can't really say.

The reason it doesn't work is that in FOL, variables, predicates and functions are not "all substitute-able". Predicates don't "evaluate to booleans". They do in some programming languages, but not in FOL. Perhaps more counter-intuitively, not even functions are "substitute-able": there are no rules for replacing a function with its value in FOL.

Let me back up a bit and point out the terminology again. I appreciate that you think what I said above is "strictly syntactical" but the idea that there is a difference between syntax and semantics is, itself, a programming language idea that does not work in FOL. In FOL, syntax and semantics are one, that's part of its power: FOL is unambiguous; what you see is what you get. For example, P ∧ Q is a conjunction: syntactically and semantically. There is no way to take P ∧ Q as anything but a conjunction, there is no compiler or interpreter translating P ∧ Q into something else. It's how you write a conjunction and it is a conjunction. FOL is WYSIWIG, yes?

So if I tell you that ƒ(x) is a function, coming from a programming language background you'd expect me to tell you how ƒ(x) is defined (as sdbrady says). In FOL, if ƒ(x) is a function, then that's the function, right there. There's nothing else to it: it's a function symbol followed by n comma-separated terms in parentheses. There's no definition of ƒ(x) "somewhere else". There is no "somewhere else". More to the point, ƒ(x) does not evaluate to anything and you can't replace ƒ(x) with its value.

In the same way predicates don't "get evaluated to booleans" - they do in some programming languages, but not in FOL. I think also you're using "predicate" itself in a programming language sense. In FOL, a predicate is the name of a relation between n entities in the domain of discourse, where n is the arity of the predicate. So P(x,y) is not a predicate, it's an atom of the predicate P of arity 2. And note that in P(x,y), x and y are variables.

Here's how this really works. In FOL, an atom is ground when it has no variables. P(x,y) is not ground, P(a,b) is ground if a and b are constants. Ground atoms are assigned truth values by an interpretation. An interpretation can be written as the set of true atoms. So for example, I = {P(a,b), P(c,d)} is an interpretation under which the atoms P(a,b) and P(c,d) are true and all other atoms are false. Note that interpretations are in a sense completely arbitrary, in that the same set of atoms can be assigned different truth values by different interpretations and there can be as many interpretations as subsets of a set of atoms. So it's literally "an interpretation".

Interpretations assign truth values to atoms so given an interpretation we can derive the truth values of more complex formulae. Remember that atoms are "atomic formulae", i.e. the simplest FOL formulae. We can make more complex formulae by using the four logical operators. So for instance, we can write the formula P(a,b) ∧ P(c,d). Under the interpretation I in my example above, the preceding formula is true, because both of the operands of the conjunction are true under I. The formula P(a,b) ∧ P(d,e) is not true under I because P(d,e) is not true under I.

How about variables and quantifiers? Remember that an atom is a predicate symbol followed by n comma-separated terms in parentheses and that terms are variables or functions (including constants, i.e. functions of arity 0). So P(x,y) is an atom with variables as terms. But, interpretations assign truth values to ground atoms, so what is the truth value of P(x,y)? It depends on the quantification of its variables. Essentially, quantifiers are a convenience that allow us to avoid having to write every formula as a -possibly infinite- set of ground atoms in order to determine the truth of the formula.

So for example, if we write ∃x,y: P(x,y) (I read that as: "there exist x and y such that P(x,y) is true") that ... does what it says on the tin. P(x,y) is true under the current interpretation for any values of x and y. If we write instead ∃x∀y: P(x,y) then we're saying that P(x,y) is true under the current interpretation for at least one value of x and all values of y.

In our example, ∃x,y: P(x,y) is true under I because there exist at least two values of x and y that make P(x,y) true, under I. ∃x∀y: P(x,y) is false because there exists no value of x that makes P(x,y) true for all y under I.

Now let's go back to functions and how they're not actually replaced by their values. The canonical example of a function in FOL is probably the Peano axiom that describes the natural numbers. Here it is, in all its quantified glory:

  ∀x: n(0) ∧ n(x) → n(s(x)) (1)

In plain English "0 is a natural nuber and if x is a natural number the successor of x, s(x), is a natural number". So s(x) is a function. But where is it that s(x) is replaced with, substituted for, its value? Where is it even that s(x) is evaluted? It's not!

Insted, FOL enables us to define rules of inference such as the method of analytical Tableaus or the Resolution principle. Inference rules in turn allow us to determine logical equivalences between FOL formulae. That's how it all comes together. So, under Tableau or Resolution, we can prove that (1) is equivalent to the following atomic formulae:

  n(0), n(s(0)), n(s(s(0))), n(s(s(s(0)))), ...  (2)

And so on - all the natural numbers in Peano's notation. Again, note there's no substitution of "predicates" (actually, their atoms) or functions, there's no evaluation of "predicates" (actually, their atoms) to booleans and there is no evaluation of functions to their values. The manipulation is purely algebraic. We're just shifting symbols around.

Oh, but you'll notice that a substitution has happened: all instances of the variable x in (1) have been substituted for ground terms in (2). Variable sustbistitutions (but not "predicate" or function substitutions!) are a mechanism introduced by Tableau and Resolution (full disclosure: I have only a hazy idea of Tableau, but I think variable subsitutions are defined slightly differently than in Resolution). They are not part of FOL, as such, but more like plug-ins. In FOL, variables are quantified over terms, and that's all. Inference rules allow us to derive new atoms (or entire new theorems) from FOL formulae with quantified variables by substituting those variables with other terms, but that's inference rules, built on top of FOL and not FOL itself. Inference rules perform reasoning over FOL expressions. In a sense, FOL is the language and the inference rules are the speakers of the language.

Well, that's my interpretation. You'll be hard pressed, unfortunately, to find all that in one place all together, and you may find bits and pieces of it lying around scattered in papers or books about logic programming and in particular Prolog. I assume that's where you get your definitions from, perhaps from functional programming books that also discuss logic programming? This is a rather large comment already but suffice it to say that logic programming is _yet another_ extension of FOL (usually based on the Resoultion inference rule) and that the most popular logic programming language, Prolog, takes many liberties with both logic programming principles and FOL principles. Prolog definitely has "syntax" and "semantics" that are two different things. In particular, Prolog syntax has a declarative semantics and a procedural semantics, and neither of the two is quite exactly FOL. To make matters worse, Prolog runs roughshod over FOL terminology, so for example what are called "atoms" in Prolog are actually constants in FOL, and that can cause much confusion (true story). But like I say, that's a different story, for another Saturday, perhaps.

Maybe I should have said 'interpretation instead of 'evaluation' (now wondering about the subtle difference between these two, if any)

Everything concerning interpretation is on the semantic side of any analysis of any logical system, such as FOL.

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.

All these because personally I find something dissatisfying about quantifiers...

So maybe I'm just trying to reinterpret quantifiers as some sort of a generalized function-like object which corresponds to parenthesis and their context-defining abilities?

Finally, I'll add that I've never learned prolog, and that a lot of these thoughts are not limited to classic FOL. I'm also thinking about modal logic, µ-calculus with it's quantifier-like fixed point operators, etc...

thanks btw.

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.