But because "F" (and the constants) are in the signature of our system with the small universe of discourse, the sentence "Fa ∧ Fb ∧ Fc ∧ Fd ∧ Fe" does make sense.
In the case of "F", there are also questions about precisely what it should mean to quantify over predicates so as to make claims that cover it.
For example, we might have a system S and another system T. The universe of discourse of system S is sets, or sasquatches, or something. The universe of discourse of system T is texts in the alphabet of system S (where by "the alphabet" I mean the symbols from which sentences of the language are made).
Assuming we think of predicates as purely syntactic, and also that we are using a dialect with one-letter predicates, "predicate" and "predicate letter" mean the same thing. Then system T's universe of discourse does include the predicates of system S. It presumably does not include any of the objects.
(System T is all the texts, i.e., all the strings, so there is no need to limit ourselves to the case were the predicates are one-letter long; that's just for simplicity.)
System T might provide the machinery to assert that a particular object (i.e., a particular text in the alphabet of system S) is a true sentence. Like, maybe system T has a predicate "T", where "Tx" means ⌜x is true⌝.
You can imagine that a system such as T could easily be powerful enough to get done -- through a layer of indirection, i.e., by making claims about claims about sets, or sasquatches, or something -- what you would want to get done by being able to quantify over predicates in the system S.
But that is probably not how you would want to do it.
Mainly... it is very cumbersome!
By analogy to programming languages, imagine I am trying to convince you to use my programming language A, and you ask me, "In A, can I store a reference to a subroutine in a variable, and call the subroutine from that variable later?" And imagine if I said, "No, but you don't need that feature. Instead, you should use my programming language B, which is a special-purpose programming language for generating and inspecting source code of A."
You would probably say, "(A) Eliah, you said you were telling me I should use A! And (B) What??!???!??! The actual problems I want to solve are not about, and not reasonably expressed, in terms of the entities B has facilities for."
Therefore, one of the approaches people sometimes take is to use a logic that is powerful enough to permit one to quantify over predicates (and deals with the design decisions and conceptual issues that come along with that).
A system that allows one to quantify over objects but not predicates is a first-order system.
That's why the logic I've been showing is first-order logic.
A system that allows one to quantify over objects and also to quantify over predicates that take objects as their arguments is a second-order system.
A system that allows one to quantify over objects, over predicates that take objects as their arguments, and over predicates that take predicates (and perhaps also objects) as their arguments, is a third-order system.
(It does not have to be limited.)
A logic that is higher order than first-order logic is called a higher order logic.
The things a second-order (or more generally any higher-order) logic can do, and the things a metasystem over a first-order logic such as system T in the above example can do, are not the same.
And they're conceptually quite different.
In a higher order logic, predicates (and function symbols... though my preferred term "function symbol" becomes less reasonable once one gets to second-order logic) are a kind of objects.
A second order system that has (to keep the example simple) constants "a" an "b" lets one express ideas like "Any gadgetary property that holds for a holds for b." In contrast, a metasystem about a system with constants "a" and "b" lets one express ideas like, "Widgetary sentences are true when the name "a" is replaced by b."
"Gadgetary" and "widgetary" are meaningless; I'm just using "is gadgetary" as an example of a second-order predicate (a predicate used to talk about predicates) in a second-order system about some topic, and I'm using "is widgetary" as an example of a first-order predicate (a predicate used to talk about objects) in a first-order system that is used to study a first-order system about that topic.
I believe a higher order logic will typically have quantifiers of different orders, where each quantifies over things of that order or of that order and lower. Unfortunately I don't know much about how second (and higher) order logic works and how it is used.
What I am more familiar with and have used (but that is not the same as saying I'm highly knowledgeable about it) is multi-sorted systems. That's a way to deal with the problem of having objects that you don't (always) want to cover when you quantify. That is, a two-sorted system could solve the problem in the Zeke example above.
Like, suppose you want ∀x ... to mean, "All uncool humans..."
But Zeke is an uncool robot-dog, not a human.
But you sometimes want to say something about Zeke.
Then you could have separate quantifiers for uncool humans and uncool robot-dogs.
Conceptually the quantifiers are what differ, i.e., some mean things like "All uncool humans..." and "Some uncool human..." while others mean things like "All uncool robot-dogs..." and "Some uncool robot-dog..." But the way it is usually (maybe always?) symbolized is to use different symbols for the variables to clarify what sort of thing--i.e., which universe of discourse--they reign over.
You can also have that one sort encompasses another.
