Parentheses Are Just Typechecking

Why is is better? It just seems different.

APL's usage of monad predates its use in conjunction with modern functional programming languages, by the way. It goes back to the 60s, and there are plenty of books and papers where these terms are used that way.

https://en.wikipedia.org/wiki/Monad_(functional_programming)...

I can't say I care too much which terms people use, but in context of APL, I prefer the terms that were used by Iverson and have been in print for more than half a century.

Oh, that makes sense. Your explanation made me realize I was assuming a few things about the language that apparently aren't true. Thank you.

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.

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.