# The smallest possible formal definition of FOL

I find the common presentation of first order logic somewhat confusing. I feel that I often don’t understand why we need the exact terms and concepts we do.

My current recapitulation of “standard FOL” is something like this (coming from Ebbinghaus 2021):

First, you have an “alphabet” - a collection of symbols. I do not know if this collection is meant to be a “theory-agnostic” one, in the sense that, it is a not a “set” as defined in ZFC, nor is it a proper class as defined in NBG set theory; but it is a “primitive”, even cognitively indisputable, notion of “some multiplicity of things”.

The alphabet is already subdivided into “types”. Some of the symbols are called “quantifiers”, some “logical symbols”, some “constants”, some “variables”, etc.

Furthermore, some of the symbols have an intrinsic attribute called “arity”, where for example a relation or function can be 2-ary, or n-ary for some natural number.

Thus, even just in defining the alphabet, at least in the common presentation, we are already assuming:

• the existence of some kind of “collections”;
• the ability to group things into named collections;
• and the ability to ascribe “properties” to those “symbols”.

Already, the symbols are not just one-dimensional “referents”; they are already slightly more complex objects; they can have data adjoined to them, for example (in the case of properties, such as arity).

So, that is everything that is implied so far when we define our ‘alphabet’. Next, it is extremely common to define formulas and terms.

Terms are defined through a pretty classic inductive definition. First, you give a few given members of a certain class. Then, you give a rule (or some rules) about the existence of members of that class. Personally, I don’t think it counts as “inductive” if it was a rule where the elements of some other set imply the existence of elements of the set of interest. That would still count as “given”. The key thing about an inductive definition is that it depends on the elements of the set in question. This means that there is a kind of inherent impossibility in knowing what elements are in the set, without simply applying the rules iteratively. It opens the question of if we should think of inductive definitions as merely bring logically accurate descriptors of the elements of a set, which already existed before we proved their existence; or if inductive rules are actually constructors that create a new member of the set when they are applied.

In that case, it seems like the key feature of an inductive definition is not that it is rule-based; nor even that it is recursive; but rather that it is “computationally irreducible”: it is mandatory, in order to specify a particular set of elements; in a way, the elements generated are inherently identifiable with the rule that generated them, in both directions (I think).

Anyway, in FOL, you basically just declare that constants and variables count as terms; and then any application of a function-symbol in the alphabet to a term also counts as a term.

Again, let’s consider the amount of… “conceptual substance” we already require, just to express the idea of an inductive definition of “terms”.

• again, we have named groups
• we also appear to have sub-group relations - for example, every variable is a term, but not every term is a variable. Should variables be considered a “subtype” of terms, or a “subset”? Or should they be considered an independent group, which just happen to have the ancillary property, “happens to count as something called a “term””?
• We apparently already understand rule-following. We need at minimum the ideas of “something exists”, as well as “if-then” comprehension: if x is a term, then f(x, x) is a term. We have the ability to simply declare something’s existence, if we want to, like “this alphabet contains the term c”.
• And so on. There is likely a lot more “hidden assumptions” to be recognized.

A formula is also defined inductively: the designer of the theory can declare that certain terms “equal” each other, or that a certain relation symbol can be applied to certain terms; these both count as formulae; any logical symbol applied to a formula is a formula; quantification over a formula is also a formula.

Formulae technically allow us to create a separation layer amongst our alphabet of symbols, that first hints at the possibility of semantics. Terms can only be declared, or defined in terms of terms; formula can only be (declaratively) defined in terms of terms or formula. Clearly, it feels like formula are “one level higher” than terms.

We haven’t even gotten to interpretations and models yet. But basically, it’s interesting that we probably have a logical connective “->”, implication, defined in our alphabet; and yet, the inductive rules we used to define things like terms and formula already use an “if-then” notion, commonly written with an entailment or turnstile symbol.

We want to use FOL as a meta-theory to describe set theory. But it seems blatantly undeniable that FOL surely has its own meta-theory formally describing it.

When we try to make our description of FOL as formal as FOL is itself a formal language to describe other things, do we just end up re-inventing FOL one level up? Is the entailment relation of the meta-theory precisely the implication relation of the under-theory?

I read in one book a logician say that logic is not circular; it is more like using a formal system to study and analyze a second lower level copy of itself. So, it’s like we actually need to differentiate between two copies of the same thing, to be able to say a lot of the interesting things we can say in meta-mathematics.

It makes me think of an M.C. Escher tesellation where the beginning of a theory is defined in terms of the end of the previous theory; which turns out to be the same theory.

I feel like the lesson may be that if circularity is unavoidable, the more interesting question is how large or small a self-specifying, self-symmetric theory we can make - either a tiny amount of information that is capable of defining itself, or a very large amount of information that has no subpart fully capable of defining its entire self.

So, what is the simplest, smallest formal specification of FOL? For example, “named groups” are often enabled by a “substitution” rule, which itself depends on some notion of “equality”. So, we could define a symbol t in our alphabet as “equivalent” to the set of elements we inductively defined as terms; this would be a kind of formal naming. And so on.

• See a Math Log textbook, like Enderton, Mendelson, van Dalen. Commented May 8 at 16:33
• See e.g. here and here Commented May 8 at 17:28
• And here Commented May 8 at 17:32
• But also Ebbinghaus' textbook is fine: it is a little bit terse but all the basic machinery of logic is there: syntax, semantics, proof system, basic meta-theory. Commented May 8 at 19:13
• Well, I recently had a peek into Quine’s Mathematical Logic and it seems like a really good book because it thoroughly discusses so many conceptual issues/questions about logic, not just a terse formalized presentation as so many other texts do. It touches on many questions I’ve been asking myself. And he explicitly says he explores a formalization of the meta-theory of FOL at one point, I think. Commented May 12 at 14:08

With the premise that I do not have Ebbinghaus, so I cannot check what the book exactly is saying or quote from it:

First, you have an “alphabet” - a collection of symbols. I do not know if this collection is meant to be a “theory-agnostic” one

Yes, it belongs to the meta-theory, whether that is formalized or not: the informal notion at play is (in my own words) "potential infinity", as in "the endless": meaning we assume that we can take symbols out of that "collection" without limitation, to write down our formulas. We also implicitly assume we know how to distinguish these symbols from one another. And no other intrinsic property.

The alphabet is already subdivided into “types”.

Could be "sorts" or "categories". That too is informal, indeed we (meta-)assume we can do that much. And the list of "types" is finite, so we can definitely do that much for any given symbol, recognize (by the given rules) to which "type" it belongs. -- I say "we", though that extends to a formalization of the meta-theory: but that we can in principle (and even in practice) do those things is in fact a prerequisite to any (effective) formalizability of the meta-theory.

Furthermore, some of the symbols have an intrinsic attribute called “arity”

Which is again a meta-property that has to do with the syntactic structure, of a function or predicate definition in this case.

Already, the symbols are not just one-dimensional “referents”

What the symbols "refer" to, strictly speaking, is a matter of semantics, while here we are still defining the syntax of a/the logical system. And, from the symbols to the terms to the complex formulas, the syntactic construction indeed is inductive.

It opens the question of if we should think of inductive definitions as merely bring logically accurate descriptors of the elements of a set

Sets proper (unless for a specific formalization of our meta-theory and, more broadly, a specific formalization of a theory of deductive systems), have nothing to do with it. Indeed, induction is crucial (and its dual recursivity), but induction per se is "just" the principle that we can have infinite structures if defined in terms of, to put it simply, a base case and a successor case. We don't need or want sets for that: in fact, on the contrary, that, i.e. induction, is what justifies (at the meta-level) the usual axiom of infinity or equivalent.

We haven’t even gotten to interpretations and models yet.

That's the semantic side: and, at least typically, the formal or semi-formal semantic construction together with the syntax-semantics correspondence also are defined inductively, and for the same reasons as before (re induction).

We want to use FOL as a meta-theory to describe set theory.

I suppose you could that: after all the epsilon predicate is a predicate. Just notice that this is in the opposite direction than the rest of your question, where FOL is the object, not the meta-theory.

So, what is the simplest, smallest formal specification of FOL?

I do not know what the "smallest" such formal specification is/would be, nor FWIW I have seen this question asked before. It is not even obvious relative to which metric: some systems have less rules of inference at the cost of needing more axioms to develop theories, and vice versa...

This is not a definition of FOL, just some notes, too long to be a comment, for your analysis, in a simple language. I will soon delete this, for experience, I know posts about the core of the philosophy of Logic attract a lot of downvotes, even when there is a lot of disagreement.

To start, logic is a set of rules. For rules to be useful, they must be applied to something.

Remark that something means essentially a thing. What is the discipline of knowledge that deals about things? Personally, I find that things are studied by the Systems Theory.

The General Systems Theory says that a system is a set of interrelated parts. Anything is a system (that is, things are systems and vice versa), and anything has parts. but such anything is much more than a collection, hence the "interrelated" quality. From a different perspective, a system is just a set, a group of things. There is a lot more about the Systems Theory that you can find in the common literature.

Let's go back to "For rules to be useful, they must be applied to something". Now, we can identify what is that "something" that logic applies to: systems. Traditionally, the object of logic is said to be arguments, judgements, predicates, facts, etc. For example, a negation: "it is false that I sleep". Logic is the set of rules that deal about the negation, but the object, the predicate or the judgement "I sleep" is essentially a system. In simple words, in the proposition `~ A`, A is a system, and the proposition is a logical fact. A is an object, whatever, and such object is just a system.

This approach, that the object of logic are systems, provides multiple advantages:

First: it formally determines the object. The Systems Theory define all attributes of a system, how are they formed, how are their boundaries determined, how do they interact with other systems (inputs/outputs), etc.

Second, it allows logic to be applicable to any physical fact (e.g. "not upwards"), metaphysical fact ("not positive"), and even to rules itself ("not logical").

Third, it provides logic, which is a strong, solid and consistent structure of rules, with an object of equivalent attributes.

So, here's part of your answer: as shown, FOL DOES DEPEND on parts and groups (systems).

Now, let's understand what is Logic.

The best definition of logic that I've come to find is that Logic is the formal expression of the rules of Reason (I use uppercase to refer to the domain of knowledge). Reason is the potential to think. Notice that reason allows inconsistencies (we all have contradictions, always, otherwise we would be perfect beings), but Logic doesn't. That's why Logic is a formalism, while Reason is not. There is no informal logic, logic is always Formal, or otherwise, it is not Logic, we are referring to Reason.

Formal means that something is expressed with a language and it is logically consistent, and here is the circularity you refer to: the fact that Logic is a formalism essentially would imply that Logic is logical, which is at least a pleonasm, it is circular.

But Logic is in fact circular, tautological. Although we can refer to Russell, it is simpler to analyze it: what are the rules that validate Logic? Logic is not validated by Reason (remember that rationally, we have contradictions!). Logic is valid by means of logical rules.

In the case of Logic, circularity and tautology are not bad. A circular argument in a discussion about earth being flat is fallacious. But in the case of Logic, it is not. Logic has no other way to be valid than to validate itself.

This is even better: Logic being a formal system (a set of axioms and rules, validated by its own rules), it provides the basis FOR ALL other formal systems. That is, the rules of chess, which is a formal system, is essentially based upon logic. And what is logic based upon? On Logic. All logical systems are based upon Logic.

Now, what is the simplest form of Logic? It is propositional logic, not FOL. FOL is a form of propositional logic focused on variable quantification. Perhaps what you look for are Copi's rules.

First, you have an “alphabet” - a collection of symbols. I do not know if this collection is meant to be a “theory-agnostic” one, in the sense that, it is a not a “set” as defined in ZFC, nor is it a proper class as defined in NBG set theory; but it is a “primitive”, even cognitively indisputable, notion of “some multiplicity of things”.

Some logicians believe first order logic must be independent of set theory, because they want to use FOL as a metalanguage, in order to formulate the axioms of a particular set theory. After formulating the axioms of some theory of sets, a set would then be precisely the kind of entity that satisfies all the axioms. I was on the fence about this issue, but after thinking about it, I see that you need the "primitive" notion of set in order to

• Design the alphabet, which is the set of symbols.

• Formulate the Axiom of Restricted Comprehension

We want to use FOL as a meta-theory to describe set theory. But it seems blatantly undeniable that FOL surely has its own meta-theory formally describing it.

The meta-theory that formally describes FOL, is the propositional calculus+axiom of Identity+axiom of restricted comprehension, as I will show.

So to develop FOL, you can use the concept of a set. You can define what terms are to be considered constants and variables recursively. That leads to an unlimited supply of those terms. Then you can list all the other terms of FOL, separated by commas, and call them all the set of symbols. Then you can name five kinds of symbols.

1. Constants
2. Variables
3. Logical symbols
4. Quantifiers
5. Punctuation symbols

From Axiomatic Set Theory, by Patrick Suppes:

We begin with a five fold classification of the symbols of the object language into constants, variables, sentential connectives, quantifiers or operators, and punctuation or grouping symbols. This classification originates with von Neumann [1927].

The set of logical symbols = {¬, ∧, ∨, →, ↔}

The set of quantifiers = {∀, ∃}

The set of punctuation symbols = { (, ), [, ], {, } }

The set of constants can be subdivided into the set of specific constants, and the set of arbitrary constants. Some specific constants must be individual constants, the rest are predicate constants. Some arbitrary constants are arbitrary individual constants, the rest are arbitrary predicate constants.

Undesignated Specific Individual Constants

{x_1, x_2, x_3,..}

Furthermore, some of the symbols have an intrinsic attribute called “arity”, where for example a relation or function can be 2-ary, or n-ary for some natural number.

Yes, you need to be able to ascribe the property "arity" to some of the symbols.

All n-ary relation symbols are a subset of the set of predicate constants. All function symbols, better known as operation symbols, aren't needed to define the relational signature of FOL. A relational signature is a signature with no function symbols. So, it is not necessary to further subdivide the set of symbols into relation symbols, and function symbols. Ebbinghaus 2021, divides the symbols of FOL into eight groups: quantifiers, variables, constants, relations, functions, connectives, punctuation, and equality.

Already, the symbols are not just one-dimensional “referents”; they are already slightly more complex objects; they can have data adjoined to them, for example (in the case of properties, such as arity).

Some constants refer, and those that do are called referrers, and the things they refer to are called referents. I think Julio was incorrect when he said

What the symbols "refer" to, strictly speaking, is a matter of semantics, while here we are still defining the syntax of a/the logical system. And, from the symbols to the terms to the complex formulas, the syntactic construction indeed is inductive.

The symbols of FOL do not refer at all. In FOL, the constants are undesignated. That means they have no referent. So you haven't reached the semantic level, as Julio seems to believe. Take the constant 'Socrates'. It's not a constant of FOL, although it is a constant. It is a referrer, and if someone asks, "who do you mean?", you can say 'Socrates'' refers to "the philosopher who drank the hemlock". Take the undesignated specific individual constant x_1 of FOL. If someone inquires "who or what does x_1 mean," you can respond "it's currently meaningless.". The reason the specific individual constants of FOL must be undesignated, is so that Existential Instantiation can be valid.

Existential Instantiation

∃ x[P(x)]; therefore P(x_n), where x_n is some undesignated specific individual constant, with no previous occurrence in the reasoning event. In this rule of inference, n denotes some specific natural number.

If an individual constant of FOL refers to something specific, and you are permitted to Instantiatte an individual variable with a designated specific individual constant then EI is invalid, as the following argument shows.

Some men are Buddhists; therefore Socrates is a Buddhist.

The constant 'Socrates' has no previous occurrence in the reasoning event, it was instantiated for the variable x, in the statement

∃ x[M(x) ∧ B(x)]

But the conclusion is false.

Variables are terms that symbolize nothing, specific constants are terms that symbolize exactly one thing, and arbitrary constants are terms that symbolize at least one thing.

I think the following theorem is necessary for FOL.

Theorem of the Existence of a Universal Set

∀ x [x ∈ U]

Definition x is a thing iff x ∈ U

If you need that theorem, then you need the elementhood symbol of naive set theory for the smallest possible specification of FOL.

From the web:

In logic, a signature is a collection of data that describes the non-logical symbols of a formal language. The signature defines the language's syntactic structure and vocabulary, and includes symbols like constant symbols, variables, and function symbols. The signature also identifies each symbol as a constant, function, or predicate symbol.

You need Hao Wang's axiom of Identity, in order to reduce FOL, to the propositional calculus. Using his axiom, you can prove the substitution principle, reflexivity, symmetry, and transitivity of equality.

Axiom of Identity

∀ y [φ(y) ↔ ∃ x[x=y ↔ φ(x)]]

Since the equality symbol '=' was not included in the set of logical symbols it must be included in the signature. The signature of a formal language is a list and description of all its non-logical constants. A logical constant is a symbol of symbolic logic that has the same meaning in all models. A model of a sentence is an interpretation under which the sentence is true.

According to Irving M. Copi's 'Symbolic Logic', page 320:

An interpretation of a WFF S with respect to a given domain of discourse is an assignment of meanings such that

1. To each propositional symbol in S we assign a truth value, either T or F.
2. To each individual constant in S, and to each variable with free occurrence in S, we assign an element of the domain of discourse.
3. To each predicate symbol in S we assign an attribute or binary or ternary or n-ary relation according as it is of degree (has right superscript) 1, 2, 3, or n.

He continues:

This notion of interpretation of a well-formed formula with respect to a given domain of discourse is incomplete, however, because no mention is made of what to do with the logical symbols ¬, ∧, and the quantifier symbol ∀ x. Our intended or normal interpretation of a well-formed formula S with respect to a given domain of discourse is defined as an interpretation of S with respect to that domain of discourse, subject to the following conditions:

(a) Any well formed part ¬ W is assigned the truth value T or F according as the well-formed part W is assigned the truth value F or T.

(b) Any well formed part of the form X ∧ Y is assigned the truth value T if and only if both X and Y are assigned the truth value T.

(c) Any well formed part ∀ x[R] is assigned the truth value T if and only if R is assigned the truth value T, regardless of which element of the domain of discourse is assigned to all free occurrences of X in R.

(d) Any well-formed part P^n(x1, x2,..., xn) is assigned the truth value T if and only if the elements of the domain of discourse assigned to x1, x2,.. ,xn, in that order, stand to each other in the n-ary relation assigned to P^n.

Note that Copi's usage of the phrase, "domain of discourse," is equivalent to the phrase, "subset of U", where U is the set of all things.

If you don't put '=' in the signature then no axiom about it will be given. On the other hand, if equality is included in the signature then some axiom must be given about it. Similarly, the symbol '∈' can be included in the signature by the adoption of the axiom of restricted comprehension.

Axiom of Restricted Comprehension

∀ F ∃ y [y is a set ∧ ∀ x [~(F(x) ↔ x ∉ x) → (x ∈ y iff F(x))]].

What the axiom of Restricted Comprehension says is for almost every property, there is a corresponding set of just the things having that property. The one and only exception is the property of "being an element of yourself."

Using the axiom of restricted comprehension you can prove the following

Theorem: U is a set ∧ ∀x[x ∈ U]

Rosser's system RS_1, described by Copi in 'Symbolic Logic', has 5 axioms or postulates:

P 1. P → (P ∧ P)

P 2. (P ∧ Q) → P

P 3. (P → Q) → [¬(Q ∧ R) → ¬ (R ∧ P)]

P 4. ∀ x[P → Q(x)] → [P → ∀ x[Q(x)], where x is any individual variable, P is any wff containing no free occurrences of x, and Q(x) is any propositional function of x.

P 5. ∀ x [P(x)] → Q, where X is any individual variable, y is any individual constant, P(x) is any propositional function of x, Q is the result of replacing each free occurrence of x in P by y.

In Rosser's System RS for the propositional calculus, you need only the first three postulates, and one underived rule of inference, namely Modus Ponens. You prove the rule of replacement as a Metatheorem, and the rule of replacement allows you to replace a a WFF that is part of a larger WFF by any WFF that is materially equivalent to the part being replaced. Thus, you don't need the equality symbol or the axiom of Identity to prove all the theorems of the propositional calculus. The problem with RS, is that it's extremely unintuitive, and thus only understandable by skilled logicians. For example, the theorem if P then P, is difficult to prove in RS. The pros of using RS, is that you can prove the propositional calculus is analytic and complete fairly easily.

My way around the adoption of axioms, is to use an axiomless system of natural deduction based on 8 underived rules of inference.

Conjunction A, B; therefore A and B

Simplification 1 A and B; therefore A

Simplification 2 A and B; therefore B

Double Negation 1 A; therefore not(not A)

Double Negation 2 not(not A); therefore A

Conjunctive Syllogism

A, not(A and not B); therefore B

Universal Instantiation

∀ x [P(x)]; therefore P(α), where α is an arbitrary individual constant.

Universal Generalization

P(α); therefore ∀ x[P(x)], where P(α) is not inside the scope of any assumption containing the special symbol α.

Using the first six rules of inference, you can prove any theorem of the propositional calculus.

Note: To pull off that feat, you need three meta-theoretical axioms.

Axiom I. If 'A if and only if B' is a theorem of the propositional calculus then A = B.

Axiom II. Any Underived or derived rule of inference of the propositional calculus is a valid argument.

Axiom III. If "A1, A2,..., An; therefore B" is a valid argument then (if A1 and A2 and... and An then B).

With these meta-theoretical axioms, and the first six underived rules of inference, you can prove the all important deduction theorem.

Using the last two rules of inference, you can prove any theorem of the first order function calculus, and derive Existential Instantiation, and Existential Generalization.

Ultimately, FOL can be reduced to the propositional calculus using the following definition:

∀ x [P(x)]=P(x1) ∧ P(x2) ∧ P(x3) ∧ ..., where the X's are undesignated specific individual constants, and P is an arbitrary 1-ary predicate constant. An undesignated specific individual constant, is a specific individual constant that has not been assigned a referent. Incidentally, the above definition is the reason you need equality in the signature of FOL; you need to be able to reduce FOL statements to statements in the propositional calculus, in order to grasp their semantics.

Generalization of the previous definition to arbitrary n-ary predicate constants is trivial.

As RudolphoAP stated:

Now, what is the simplest form of Logic? It is propositional logic, not FOL. FOL is a form of propositional logic focused on variable quantification. Perhaps what you look for are Copi's rules.

He is correct, based on the equational definition of the universal quantifier. But to use that definition, you need to know the meaning of the equality symbol, and you need Hao Wang's axiom of Identity for that. So the answer to the question, depends on whether or not '=' is in the signature. Let's say it isn't. Then you need the five postulates of RS_1.

So without equality in the signature, the minimum amount of information for the specification of FOL, would be the 5 postulates of RS_1, and the axiom of restricted comprehension. You need the latter, to prove there is a universal set, containing all individuals. And the reason you need U, is to prove RS_1 is functionally complete.

If equality is in the signature, then you need the three postulates of RS, the axiom of Identity, and the axiom of restricted comprehension.

Without Identity you need 6 axioms, and two underived rules of inference.

R 1. From P, and P → Q to infer Q.

R 2. From P to infer ∀ x [P].

With Identity you only need 5 axioms, and modus ponens. So this is the smallest possible formal specification of FOL.

In Irving M. Copi's 'Symbolic Logic' he refers to any sequence of symbols of FOL as a formula. Then he defines the notion of well formed formula recursively. There's nothing more than the propositional calculus required to understand the definition.

• Would be nice to know why I got the downvotes since I successfully answered the question. You need 5 axioms, and one underived rule of inference. Commented May 12 at 22:15