1 Introduction
The seminal ‘Essence and Modality’ (Fine 1994a) persuaded many to distinguish between essential features of an object and its merely necessary features: while {Socrates} essentially has Socrates as a member, Socrates is not essentially a member of {Socrates}. In subsequent work, Fine showed how to develop a logic of essence where essentialist claims are expressed using an indexed operator □F: ‘it is true in virtue of the natures of the Fs that …’ (Fine 1995b; Fine 2000b).1 This paper is a plea to explore a path not taken. In two marginally less cited papers (Fine 1994b; Fine 1995a) Fine floats the idea that real definition might be the basic notion and that we, in line with the following slogan, can define essence in terms of it:
| (Slogan) | Something belongs to the essence of an (some) item(s) if and only if it follows from each real definition of that item (those items) |
This paper begins taking some steps down this path by sketching an account where the notion of real definition is taken as primitive and argues that it has at least two advantages over accounts that take essence as the basic notion and attempt to define real definition in terms of it.2
By allowing items to have multiple distinct definitions one can accommodate a wider class of derivative entities.
One can accommodate views where each logical operation is definable independently of the others.
Here is an overview of the paper. We begin in § 2 by presenting a range of cases where taking the notion of real definition as basic would be fruitful. In § 3 we then argue that we should take the notion of immediate and full definition as the basic notion. In § 4 we begin developing a notation for expressing such definitions. To cash out the (Slogan) we need to know what is meant by something’s ‘following from’ a definition. In § 5 we start addressing this question by showing how to give inferentialist definitions of the logical operations. A second—challenging—problem with cashing out the (Slogan) is that we must make sense of something’s following from all the definitions of an item. In § 6 we propose a way of making sense of this. In § 7 we put all this to use by introducing essentialist operators. In § 8 we conclude.
2 The Essential Manifold
Before we turn to the theory of definition itself, it will be useful to present a range of cases where taking the notion of real definition as basic is useful. These cases also allow us to illustrate one of the more striking features of Fine’s proposal: the idea of an essential manifold.
To illustrate the idea, let us look at cardinality abstraction.3 Let us write #(xx,y) to mean that y is the cardinal number that results from abstracting on xx.4 If are some singular terms, let us write for the plurality of exactly .5 Clearly, #([Trump, Biden],2). How, however, may the number 2 itself be defined? We propose that 2 may be defined as the result of cardinal-abstraction on [Trump, Biden].
Of course, there is nothing special about Trump and Biden:6 the number 2 could be defined as the result of cardinal abstraction on any plurality comprising exactly two objects. The number 2 thus has a manifold of permissible definitions, what Fine calls an ‘essential manifold’ (Fine 1994b; Fine 1995a). In accordance wth (Slogan) what is essential to the number 2 is then what follows from each of the definitions of 2. It will thus not be essential to 2 that it can be abstracted from [Trump, Biden]; what will be essential to 2 is just that there is some x and some y such that x≠y and 2 is the result of abstracting on [x,y].
There are many further cases where allowing an essential manifold allows us to state elegant theories. Before we present these cases we should stress that we do not claim that we must avail ourselves of an essential manifold in all these cases.7 However, countenancing an essential manifold allows one to deal with the cases in a natural way, so why not avail oneself of it? And even if, at the end of the day, it turns out that no item has a manifold of definitions, one could argue that this should not be ruled out by the theory of definition itself.
Here, then, are the cases.
Types. We may define a (geometrical) type by defining it as the type of given token; any other token of the same type would work equally well (Fine 1995a, 285).8
Colors. We may define each color by pointing to a thing with that color: ‘thus if the color is red, then red can be defined as the color of x, where x is any red thing’ (Fine 1994b, 67).
Complex Properties. We may define a complex property like being a wise philosopher as the result of abstracting Socrates out of the conjunctive proposition that Socrates is wise and Socrates is a philosopher; we could also have defined it as the result of abstracting Plato out of Plato is wise and Plato is a philosopher (Fine 1995a, 285; Fine 1994b, 67; Fine 2010, 566–568).
Classes. One can define a class as the result of abstracting on a (predicatively definable) property under the equivalence relation of coextensionality; a given class can then be defined as the result of abstracting from any number of (coextensive) properties with no property being canonically associated with the class (Fine 2005, 568n18).
Directions. One can define a given direction as the direction of a particular line. But there is nothing special about the line chosen: any line parallel with it could also have been used to define the direction.
Manners-of-Completion. On an anti-positionalist view of relations (Fine 2000a), a non-symmetric binary relation like loves does not apply to two relata a,b in an order; rather, the relation simply has two distinct completions (states). To account for the relationship between different completions of the same relation, the anti-positionalist defines manners-of-completion by abstraction from states.9 For instance, the manner M in which the state of Abelard’s loving Eloise is the completion by Abelard and Eloise of loves is the same as the manner in which the state of Anthony’s loving Cleopatra is the completion of loves by Anthony and Cleopatra. This tells us when two manners are identical, but how can a given manner M itself be defined?
As Fine (2007, 61) observes it would be absurd to think that there was a privileged state—Adam’s loving Eve perhaps—such that the manner M is uniquely defined as the manner in which Adam’s loving Eve is a completion of loves by Adam and Eve. Rather, for any state t and any objects a,b such that t is a completion of loves by a,b in the same manner as the state of Abelard’s loving Eloise is a completion of the loves by Abelard and Eloise, the manner M may be defined as the manner in which t is a completion of loves by a,b.
While all these cases are naturally accounted for in terms of an essential manifold, the color, direction, and manner-of-completion cases are particularly interesting: in these cases it seems impossible to pick a ‘canonical’ definition, and so one has to rest content with an essential manifold.
3 Definition: Immediate and Full
In developing an account of definition, we face a choice: should we take the basic notion to be immediate or mediate definition? Suppose {{Socrates}} is, by definition, the value of the set-formation operation applied to {Socrates}. It stands to reason that {Socrates} is, by definition, the value of the set-formation operation applied to Socrates. So {{Socrates}} is immediately defined as the value of set-formation applied to {Socrates} and only mediately defined as the value of set-formation applied to the value of set-formation applied to Socrates.
It is clear how the notion of mediate definition can be defined from the notion of immediate definition, but it is not clear how to proceed in the opposite direction. (It is not even clear how to formalize the latter notion.) We will accordingly take the notion of immediate definition as basic.
A different choice point is whether we take the notion of full or partial definition as basic. The notion of partial definition is clearly definable from the notion of full definition: x is partly defined by being F iff that x is F is part of some full definition of x. It is less clear that we can define full definition in terms of partial definition. The obvious idea is that a full definition of x is a partial definition of x that is not part of a larger partial definition; however, this arguably does not work.
Suppose one takes the view that every real number r can be defined as a ‘double limit’ as follows. Take any sequence of numbers that converges to r from below and take any sequence that converges to r from above. Then r may be defined as the number that is greater than l0, greater than l1,…, less than u0, less than u1, …. Any definition of this form is contained within a larger definition of this form; on the proposed account the real r then does not have a full definition.10
For these reasons11 we propose to take the notion of immediate full definition as basic. Let us now turn to developing a notation for this notion.
4 The Grammar of Definition
The simplest approach would be to introduce variable-arity sentential operators with the following grammar: when are any sentences then is a sentence. What would express is that s is, by definition, such that .
A considerable advantage of such an approach is that it keeps the definitional formalism close to the familiar formalisms for the logics of essence. Unfortunately, such a notation has a significant drawback: it makes it impossible to distinguish between occurrences of the item s in the definiendum and in the definiens. To see the issue let us, first, consider whether definitions should be well-founded.
An attractive, foundationalist vision of the world is that there are some indefinable items and that all other items are ultimately definable from these indefinable items. It is natural to think that such a foundationalist view of the world is committed to the idea that nothing may be defined in terms of itself. However, this is wrong. To see this, consider the cardinal number 2. This number can defined as the result of abstracting on any two-membered plurality. Thus it can also be defined as the result of abstracting on the plurality [2,Biden].12
Such cases of self-definition are in fact perfectly compatible with the foundationalist viewpoint: the foundationalist only requires that there be some well-founded system of definitions that links 2 to the indefinables.13 (We return to how to formulate that everything sits atop a well-founded system of definitions in § 6.1 below.)
The possibility of self-definition creates problems for the sentential operator approach. On this approach we would write .14 Intuitively, the right occurrence of 2 in is in a defined position, whereas the left occurrence is in a defining position. But on the sentential operator approach we cannot distinguish the two cases.
Litland (2023) proposed a formalism for real definition that allows us to overcome this problem. He expresses real definitions using a variable-binding operator
with the following grammar. Let be some sentences in which the variable x may occur free. Then

is a sentence. (In
the variable x is bound.)15 We may gloss this sentence as saying that s may be immediately and fully defined by being such that .
Definitions are clearly factive: if s, by definition, is such that then we had better have . We thus lay down the following principle.

Let us give some illustrations of definitions that are in this format. Our purported definition of the set {{2}} can then be expressed as follows.

The various definitions of the cardinal number 2 can be expressed as follows:

As we can see, the notation allows us to observe the distinction between occurrences of the number 2 in defining versus defined positions.
Note that this format makes all definitions implicit: what is defined is defined in terms of the role(s) it plays. Let us consider how the framework can accommodate standard cases of explicit definition; this will throw some further light on the sense in which definitions are asymmetric. Let us take a stock example: vixens are, by definition, female foxes.
In higher-order logic we can write down an identification like . For us this is not a definition: it is merely a true identity. (In fact, this identity is (higher-order) identical to the self-identity: Vixen=Vixen.) Given that being a vixen is identical to , to define the former just is to define the latter. Fortunately, there are several ways of defining . Perhaps the most elegant one follows Fine’s suggestion that complex properties are defined by subtraction from propositions. Let us write to mean that Q is the property that results from subtracting the object a from the proposition p, and let n be a particular object. An acceptable definition of being a vixen could then be:

Or in words: ‘Vixen, is by definition, the property that result from subtracting n from the conjunctive proposition that n is female and n is a fox’. (Note that we here have an essential manifold.)
But one does not have to subscribe to the subtractive view of complex properties to give a definition of Vixen. Here are two alternatives. First, suppose one accepts β-conversion in the sense that . One could then provide the following definition:

Second, suppose one agrees with Rosen (2015) that one defines a property by specifying its grounds. One could then give the following definition, (writing ≪ for the relation of (immediate, non-factive) full ground):

In words: ‘being a Vixen is, by definition, that property such that some proposition grounds one’s having it iff that proposition is the conjunctive proposition that one is a female and one is a fox.’
5 Defining Logical Operations
In the logic(s) of essence one, in effect, identifies the essence of an object (some objects) with a theory: the set of propositions that hold in virtue of the nature(s) of that (those) object(s).16 In line with the (Slogan), one may view the real definition of an object as an axiomatization of the theory of the object, with the theory of the object(s) being the common consequences of all the permissible axiomatizations.
This raises two issues: (i) we need to make clear what is meant by ‘follows from’ (in general); and (ii) we need to express that something follows from all the definitions of an item.
So far we have seen one way in which something follows from a definition—by application of the principle of Factivity. To see in what other ways something follows from the definitions of an item we turn to how we can define the logical operations themselves.
Disjunction (∨) is an operation such that the proposition p∨q formed by applying ∨ to two propositions p,q is true when p is true and also true when q is true and is true in no other cases. One may thus be tempted by the following definition:17

This approach has two drawbacks.
First, suppose that Socrates is, by definition, rational. Then it should follow from the definition of ∨ together with the definition of Socrates that Socrates is rational or Plato is rational.18 The problem is that Factivity will just give us that Socrates is rational and that . To conclude that Socrates is rational or Plato is rational we would have to apply universal instantiation and modus ponens. The proposed definition lands us in a metaphysical Carroll problem.19
Second, many philosophers are attracted to the view that it should be possible to define each logical operation independently of the others.20 But the above definition of disjunction used the universal quantifier and the conditional!
We can solve both these problems by allowing items to be defined by their role in (rules of) inference (and not just by their role in true propositions). This idea is not novel—see (Correia 2012; Correia 2020; Fine 1994b)—though we take the approach further.
The thought that the logical operations are defined by their inferential role is, of course, familiar from the literature on inferentialism. For instance—to continue with the same example—inferentialists have claimed that the disjunction operation is defined by its introduction and elimination rules:

As usual, the elimination rule means that if we have derived r from some number of occurrences of p using argument 𝒜, and also have derived r using some number of occurrences of q using argument ℬ, we may infer r from p∨q.
When inferentialists say that disjunction is defined by these rules they typically just exhibit the form of the rule; the claim that these rules define disjunction is then made in the meta-language. We want to express these claims in the object language of the theory of definition. We therefore have to treat rules as entities in their own right and have to develop a notation for reasoning about rules, not just reasoning in accordance with them.
For some propositions pp and a proposition q let us write pp⇒q for the rule that allows us to infer q from pp.21 We will further think of rules as being parts of arguments. Thus, if we have a rule pp⇒q, the following is an argument from pp to q using the rule pp⇒q: pp⇒q q. In such an argument the conclusion q depends both on the premisses pp and on the rule pp⇒q. (This will be important later.)22
As a special case, arguments using the disjunction introduction rules have the following form:
We will think of the minor premisses in an application of ∨-elimination as the arguments 𝒜,ℬ themselves.23 Let us write 𝒜[r] to mean that r is the conclusion of the argument 𝒜. A particular instance of the disjunction elimination rule would then be:24
and an application of disjunction elimination would take the form:

Here we allow the discharge of any number of assumptions of p,q from 𝒜, ℬ, respectively. Note that in this argument the conclusion r depends on the rule as well as on the undischarged propositions.
We want to take the disjunction operation ∨ to be (partially) defined as that operation R such that for any p,q we have the rules and for any p,q,r and any arguments 𝒜[r],ℬ[r] we have the rule . To express the generality required here we will let the definitional operator
itself bind and (universally) generalize variables (subject to certain constraints).25
The general formation for expressing definitions now becomes:

What this means is that s is, by definition, such that if x0 is any ψ0, x1 is any ψ1, … one has the propositions , and the rules .26
Since an inference is not a proposition, Factivity has to be understood not just as licensing us to assert some propositions, but also as allowing us to apply certain rules.

What this extended Factivity rule says is that if we have established that meet conditions respectively and we have an argument to some conclusion r where r depends on some number of occurrences of the premisses and some number of applications of the rules then we can discharge any number of these assumptions and conclude r outright.
To show how this works we will propose a definition of ∨ and show we can derive from u∨v and w using just the definition of ∨ and the instances , of the conjunction introduction rule. Here is the proposed definition of the disjunction operation ∨ itself:

And here is the derivation in question:

(To save space we have written 𝒞 for the subordinate argument from u,w to and similarly for 𝒟.)
Notice that the final conclusion does not depend on the disjunction rules. While we used those rules in the subordinate arguments, the applications of those rules are discharged by an application of Factivity.
The proposed definition ensures that disjunctions can be inferred from each of their disjuncts; and that anything which follows from each disjunct follows from the disjunction. However, two things are missing. First, it should follow from the definition of disjunction that but nothing in the proposed definition ensures that ∨ is a symmetric relation in this (strict) sense. Second, it should follow that if s is the disjunction of p and q then it is necessary that s follows from each of p and q. But this does not follow: the problem is that it does not follow from the proposed definition of the disjunction operation itself that its values are, by definition, values of the operation. These defects are remedied in the following definition.

Thus the disjunction operation ∨ is defined, in part, by the fact that its values on input p,q are fully defined by being the values of that operation on input p,q.27
This shows how we can capture the inferentialist account of the logical operations within this framework of definitions. A number of points should be made.
First, these definitions should be taken to be definitions of the logical operations themselves. They are not intended as metasemantic accounts of how a sign for the operation comes to denote the operation in question. For better or worse, this is metaphysical inferentialism.
Second, and relatedly, we are not making any claims about the epistemological significance of the fact that disjunction is defined in this way. Williamson may be right that inferentialism is epistemologically impotent,28 but this has no bearing on whether the above is a correct real definition of the disjunction operation.
Third, we have taken disjunction to be defined by its introduction and elimination rules combined. This is potentially risky. As we know from the case of tonk (Prior 1961) unless the introduction and elimination rules are in some sense ‘harmonious’ things can go amiss. It is obviously extremely important to determine which putative definitions are safe and so in fact succeed in defining a logical operation.29
Fourth, one has to admit that this definition has a certain notational complexity. However, this notational complexity only makes explicit in the object language what was already present in the inferentialist view about the nature of disjunction.
Fifth, while we have just exhibited the definition of a single logical operation, it should be clear how to generalize the above account. In particular, it should be clear how one can recast the standard introduction and elimination rules for intuitionistic logic in this format.
Sixth, one of the motivations for defining the logical operations inferentially was to ensure that one could define each logical operation separately. While the format allows one to define each logical operation separately this does not mean that one has to do so. So far we have only considered definitions of particular items. But the format for definition also allows for simultaneous definition. When we write

what we mean is that are together defined by being those such that . By allowing simultaneous definition we can accommodate views where (some of) the logical operations are holistically defined by the rules governing them taken together. In particular, we can make sense of views where disjunction and negation are jointly defined so that excluded middle holds.30
6 What follows from all definitions
According to the (Slogan), it is essential to s that ϕ if ϕ follows from all the definitions of ϕ. How can we reason about all the definitions of a given item?
Ideally, we would like to be able to define a relation T between items and properties of propositions such that T(s,P) holds iff
. However, given that there could be any number of variables of any type there does not seem to be any hope of defining this relation T in a type-theoretic setting.31
So we will simply take the relation T as primitive.32
While T is taken as primitive we can constrain it somewhat. In particular, if
then s has some definitions and
is one of them. Thus we accept the schemes:

and

Using T we can now express that s is indefinable: .
6.1 Well-founded systems of definitions
To express that everything is definable from the undefinable in a well-founded manner we introduce a relation ⪰ that, intuitively, holds between a definition p and some propositions iff, for each item ti figuring in a definiens position of p, either qi says that qi does not have a definition (and ti does not have a definition) or else qi is a definition of ti. More precisely, p⪰qq should hold iff p is of the form
and where qi is either a true proposition of the form or else ti does not have a definition and qi is . (Here are all the items that figure in the relevant definition of s.) Unfortunately, just like it seems that there is no way of defining the relation T there appears to be no way of defining the relation ⪰; we thus propose to take it as primitive.
While we take ⪰ as primitive, given its intended meaning we may partially characterize it by laying down two inference schemes. The first scheme expresses that if there are no definitions of s, then no propositions stand in the ⪰ relation to the proposition that there are no definitions of s.

The second scheme is the following:

Here are all the constants and free variables that occur in . (They do not have to occur in all of them) and ti? is either of the form
or is . It is this inference scheme that ensures that if p is a (true) definition where are all the items occurring in the definienda and the propositions are such that qi either is a definition of ti or else (truly) says that ti does not have a definition then .
To express that everything is definable from the indefinable in a well-founded manner we proceed as follows. Let D be the property that applies to the propositions that express the definition of some item or else says some item is indefinable.33 Let I be the property that applies to those propositions p that have D and are such that for no qq do we have p⪰qq. I applies to the propositions that (correctly) say that some item does not have a definition. The claim that everything is definable in a well-founded manner is then the claim that D is the closure of I under ⪰.34
6.2 P-restriction
A given item s may have many distinct definitions, but it is tempting to think that these distinct definitions have something ‘in common’, that they are all of a certain ‘form’. Moreover, it is plausible to think that this form is contained in each definition of s, in the sense that if q is a particular definition of s then there is a P such that T(s,P) where P is definable from q. Before we state this constraint precisely, it will be useful to give some examples illustrating what we have in mind.
Let us return to the definition of
. This just expresses that {{2}} may be fully and immediately defined as the result of applying set-formation to {2}. But we intend more: we mean to say that {{2}} can only be defined in this way. (Without this further claim it would not be essential to {{2}} that it is the result of applying set-formation to {2}.)
While any property P such that T({{2}},P) is thus a property that applies exactly to the proposition
, one of these properties stands out, namely the property
. This property has two important features.
First, this property P is clearly definable from the definition
itself. Second, it lies in the nature of this property P itself that it only applies to
. It will be convenient to express this fact about the property P by means of a rule of the following form:

That is, if q is an arbitrary definition of {{2}} then q is in fact the definition
. We will take the property P to be partly defined by this rule.35
This was an easy case—there was only one definition of the item in question. Cases involving an essential manifold are more intriguing. We may define 2 as the cardinal number abstracted from the plurality of Trump and Biden:
. Of course, any plurality xx that is equinumerous with [t,b] would do equally well; moreover, all the permissible definitions of 2 have this form. So in accepting that
we should accept that where P[t,b] is the property that applies to q iff q is of the form
where xx is equinumerous with [t,b]. (Written in λ-notation, we have
. Thus, P[t,b] is partly defined by the rule:

The property P[t,b] is definable from the definition
as long as one makes the reasonable assumption that the equinumerosity relation ≈ figures in the definition of the cardinality-abstraction operation #. There is, of course, nothing special about the property P[t,b]. The property P[a,j] that applies to those q that are of the form
, where xx is equinumerous with the plurality of Adams and Jefferson would also apply to exactly the definitions of the number 2.
Let us now consider the case of color. Red, let us suppose, can be defined as the color of a, where a is in fact a red thing—that is,
. In accepting this definition we presumably also accept that if q is also a definition of Red, then q is of the form
, where y is chromatically equivalent to a. That is, if we let Pa be the property that applies to some q iff
for some y that is chromatically equivalent to a then we have T(Red,Pa). This property Pa is partly defined by the following rule (writing ∼) for chromatic equivalence):

If the relation ∼ of chromatic equivalence is contained in the definition of the relation ColOf, then the property Pa is definable from the definition
.
In the above three cases we could, for a given definition p of s, define a property P such that T(s,P) using just the resources contained in the given definition p. We wish to say that this is always possible. On the assumption that everything that has a definition at all is ultimately definable from the indefinables, this general claim can be stated as follows.
| (Definitional Unity) | Suppose q is such that Pq where T(s,P). Then there is some Q such that (i) T(s,Q); and (ii) whenever I are some indefinables such that q is in the closure of I under ⪰ then there is some proposition r in the closure of I under ⪰ and some property R such that T(Q,R) and Rr |
Generalizing from these three cases a P-restriction rule (where P applies to all and only the definitions of s and P is definable from a given definition of s) takes the following form:36

In such a rule specifies a condition on and
is some or other definition of s (in which may occur free).
6.3 Types, colors, and classes: a concern
The proposed definitions of the color red, of a given type of shape, and of a given class raise a subtle issue.37 A given red thing a is not necessarily—much less essentially—red. Thus it would not follow from the nature of the object a, together with the fact that C is the color of a that C is the color red. Or take the case of classes. There is a property P that has its extension contingently. Suppose then that c is the class abstracted from P. We can know the nature of the property P without knowing that the class abstracted from P is the class c. Or take a material object which has a given shape S and so is a token of that type of shape. The shape S is defined as the shape of the object. However, it is contingent that the object has the shape it does, and so we can know the nature of the object without knowing that its shape is the shape S.
What is at issue is the following principle.
| (Definitional Internality) | Suppose that . Then it follows from any definition of s and any definitions of the constituents in that ![]() |
While (Definitional Internality) is perhaps not obvious it seems attractive: how could one change the above definitions of color, type, and class to accommodate it?
The class case is straightforward: insist that classes are defined by abstraction from properties that have their extension necessarily. The color and shape-type cases are trickier. Fine (1994b, 72n16) suggests—for the color case—that one could require the object defining the color red to be ‘a red’—an object that by its very nature is red. But why believe that there are any reds? The following is, perhaps, a way of proceeding. Distinguish between the object and the object-as-it-actually-intrinsically-is. The definition of red is then not simply ‘red is, by definition, the color of x’ but rather ‘red is, by definition, the color of x-as-it-actually-intrinsically-is’. (One could propose something similar for the token case.)38
7 Essentialist Operators
Having seen how to define logical operations inferentially we can now put this to use to define an essentialist operator □ inferentially.39
Only the items that have definitions should have essences. Thus in order to infer □sϕ we should require that s has some definitions; that is, we must require that P(q) for some P and q where T(s,P) and P is definable from q in the way indicated in § 6.2. The (Slogan) suggests that if ϕ follows from each q such that Pq then ϕ belongs to the essence of s. However, this assumes that it is necessary that s has the definitions it in fact has. And for several of the examples given above in § 2 this is doubtful. No matter how many red objects we have that may be used to define being red, could there not be a further red object? And no matter how many two-membered pluralities we have that could be used to define 2, could there not be a further two-membered plurality?40
This suggests that for □sϕ to hold we should require that if q is arbitrary such that Pq then ϕ follows from q together with Pq. However, this is not enough: we need two further restrictions.
First, we have to put some restrictions on how the conclusion ϕ can be derived from q,Pq. In deriving ϕ we can only use rules that are licensed by q’s being an arbitrary definition of s. This amounts to the idea that in the argument from Pq and q to ϕ we can only use and Factivity and P-restriction.
Second, suppose q is an arbitrary definition of 2. Then, by using P[t,b]-restriction, we can conclude that
. By logical reasoning (that would be licensed by Factivity applied to the definitions of the logical operations) and Factivity we can then conclude that . However, it should not be essential to the number 2 (and the logical operations) that 2 can be abstracted from a plurality that is equinumerous with the plurality of Trump and Biden. The number 2—as the saying goes—‘knows nothing’ of these presidents.
We thus impose the restriction that any constant (and free variable) in ϕ must occur inside the scope of a definitional operator in the argument from Pq and q to ϕ. While P[t,b]-restriction allows us to conclude that
, the occurrence of [t,b] is outside the scope of the definitional operator.
We thus arrive at the following introduction rule for the essentialist operator:

Here the only rules that are applied in 𝒜 are applications of Factivity and P-restriction, and every constant and free variable in ϕ occurs in 𝒜 within the scope of the definitional operator.
Using this introduction rule we can conclude that it is essential to {{2}} that it is the result of applying set formation to {2}.

Contrast, this with the case of the number 2. Using the above rule we cannot derive any essentialist facts about 2. It does not lie in the essence of 2 that it can be abstracted from the plurality of Trump and Biden; nor does it lie in the essence of 2 that it is abstracted from some plurality with two members.
The above rule covers just the special case where we are considering what is in the essence of s alone. What is in the natures of taken together is what follows from arbitrary definitions of . Thus the more general introduction rule is:

The above gives us rules for the immediate essence of : what follows from the definitions of itself. As stated the rules do not allow us to use the definitions of the items that figure in the definitions of . For instance, the above rules would not allow us to conclude that it is essential to {{2}} that {2} is the result of applying set formation to 2.
To remedy this, and thus allow us to capture a notion of mediate essence, we could say something along the following lines. Say that ss is a system of definitions for iff (i) whenever there is Pi such that T(si,Pi) there is some pi amongst the ss such that Pipi; and (ii) if p is amongst the ss and there is qq such that s⪰qq then there are some rr amongst the ss such that s⪰rr; and (iii) there are some indefinables in ss, such that ss is contained in the closure of those indefinables under ⪰. We can then introduce iff ϕ follows from each system of definitions for . (As before we would have to restrict the rules used in deriving ϕ and also the constants and variables occurring in ϕ.)41
We will not attempt to write down a rule corresponding to this idea here; we will rather consider what the elimination rule for the original rule should look like. Suppose it is the case that □sϕ. (The case of will be similar.) Then we should be able to assume that for some P and p; and we should be able to assume that for arbitrary q such that Pq we have an argument 𝒜 from Pq,q to ϕ. Thus we get:

When we write we mean that 𝒜 is an argument from Pq,q to ϕ where the only rules used are Factivity and P-restriction, and where the constants and variables in ϕ meet the relevant conditions.
Armed with this elimination rule we can show that □s satisfies the T-principle.

More interestingly, we can argue that the 4 principle in the form is correct.42 The key is to take the introduction and elimination rules specified above to provide a definition of the essentialist operator □. We will not write it out, but let us write
for this definition. Moreover, this is the only definition of □. Thus there is a Q such that T(□,Q) and we have the following rule of Q-restriction:

We can then informally argue as follows. Suppose that □sϕ. Then we may assume that s has some definitions; so let P and p be such that we have and p. Suppose that q0 is such that Pq0 and q0 and let q be arbitrary such that Pq and q. By □-elimination, we may assume that we have an argument 𝒜 from Pq and q to ϕ where the only rules used in 𝒜 are P-restriction and instances of Factivity; moreover, the constants in ϕ occur inside definitional contexts in 𝒜. By using the □-I rule with as premisses, we can conclude □sϕ. This conclusion depends only on T(s,P), Pq0 and q0, as well as the introduction and elimination rules for □. Suppose next that , and r. Since the rules given for □ are the only way of defining □, from Qr and r we can use Q-restriction to conclude that
. By using Factivity we can then discharge the applications of □-I and □-E. We have thus derived □sϕ from , . By another application of □-I with and
as premisses we can derive □□,s□sϕ discharging the assumptions of .
While we have given a plausible argument in favor of the 4-principle, the situation is less clear with the 5-principle. In its inferential form the 5-principle is
(Here |¬□ϕ| is a list of the constants and free variables occurring in ϕ.) In the current setting what this says is that if ϕ does not follow from an arbitrary definition of s, then it follows from an arbitrary definition of s together with the definitions of □, ¬, and the constants in ϕ that it does not follow from an arbitrary definition of s that ϕ.
It is not clear to whether this principle should be accepted, nor is it clear how to augment the proof system in such a way that this principle is derivable.43
8 Conclusion
Taking real definition as the basic notion and defining essence in terms of it—that is the path not taken. This paper made a case for exploring that path and took some small steps down it.
It should be obvious that much more work needs to be done in order to determine whether one should continue further down that path. In particular, more needs to done to put the approach on a solid technical footing. First, the proof-theoretic approach sketched in the present paper must be fully and rigorously worked out. Secondly, having done that, the relationship between the logic of essence sketched in § 7 and Ditter’s logic of essence should be studied. Thirdly, it would be of considerable interest to develop a model theory for the account of real definition and establish soundness and completeness results.
Notes
[1] This type of approach to the logic of essence has recently been extended to the higher-order setting by Ditter (2022), greatly increasing the expressiveness of the formalism.
[3] It is natural to think that all sorts of items can be defined—objects, properties, logical operations, quantifiers. This raises the question whether an account of definition should be developed in a higher-order or a first-order language. We will here opt for a higher-order formulation. As we will see we will need a wide range of types. For now let us work with us work with the types of Ditter’s higher-order logic of essence. We have the basic type e of objects. Whenever are some types then is a type—the type of relations between items of type . Whenever τ is a type [τ] is a type—the type of pluralities of items of type τ. As a special case we have ⟨⟩—-the type of propositions—and [e]—the type of pluralities of objects. We will use as plural variables (i.e., variables of type [e]). Later we will introduce types for rules and arguments.
[7] In the case of cardinal abstraction on may offer the following alternative approach. For every (set-sized) plurality xx there is a property, definable in purely logical terms, that is had by all and only the pluralities equinumerous with xx. In particular, there is a property TWO that applies to all and only the two-membered pluralities. We may then offer the following single definition of the number 2: ‘2 is, by definition, the cardinal that can be abstracted from any plurality having the property TWO.’
[9] For details, see Fine 2000a, 23–24.
[10] Fine (1994b, 72n17) gives a related example.
[12] This is a case of so-called ‘auto-abstraction’; for further discusion see (deRosset and Linnebo 2023; Litland 2020; Zanetti 2020).
[13] The sense in which definition is well-founded is thus similar to the sense in which ground is well-founded (see Dixon 2016; Litland 2016; Rabin and Rabern 2016).
[14] On could object to this example by saying that, strictly speaking, 2 does not figure in this definition—what figures is just a plurality that comprises 2. Fair enough, but we can change the example. Consider a case of structural abstraction where we abstract the ordinal number n from the n’th entry in an ω-sequence (Linnebo 2008). We can abstract the number 2 from itself with respect to any ω-sequence where 2 is the 2nd entry.
[15] Fine (1994b, 69n1) briefly considers an approach similar to this for expressing essentialist claims.
[16] The theories are not closed under full logical consequence. The theories only contain propositions that can be formed from objects (properties, relations) that figure in the nature(s) of the given object(s).
[17] Or perhaps one wants to formulate this in terms of ground: disjunctions are grounded in their disjuncts. This will not help with either of the problems below.
[18] If one is worried about the extraneous content introduced by Plato, add Plato’s definition to the mix.
[19] We hasten to add that this observation is not novel: see (Correia 2012; Fine 1994b).
[20] See, e.g., (Dummett 1991; Tennant 1997).
[21] If one—like Rosen, Fine, and many others—want it to be part of the nature of disjunctions that they be grounded in the disjuncts, one could draw a distinction between explanatory and non-explanatory inferences, and insist that inferences in accordance with these rules are explanatory. (See Litland 2017 for details.)
[22] To be rigorous we would have to extend our type system to accommodate both the type of rules and the type of arguments. Moreover, we would have to be precise about how particular arguments are built up of rules and other arguments. We hope to return to this elsewhere.
[24] The idea that premisses of rules that discharge assumptions are arguments is suggested by Fine (1985, 70) and endorsed and developed (in different ways) by Schroeder-Heister (1984) and Schroeder-Heister (2014).
[25] Another approach would be to follow (Schroeder-Heister 2014) and let the rule-arrow ⇒ bind and generalize variables. Since we will need the definitional operator to bind and generalize variables anyway, we opt to let it do all the variable-binding.
[26] Some may find it helpful to read this account in terms of arbitrary objects à la Fine 1985; Fine 2017. Let x0 be an arbitrary ψ0; let x1 be an arbitrary ψ1, …. The above then says that s0 is by definition such that . There are interesting connections between the present account of definition and the account of essence in terms of arbitrary objects presented in (Fine 2015; Fine 2016). Further examination of this has to await another occasion.
[27] This is a place where taking full definition as the basic notion is at the very least convenient. If we had worked with the notion of partial definition we would have to say that the values of ∨ on input p,q were defined, in part, by being the values of that operation on input p,q and that this partial definition is not part of any larger definition.
[28] For Williamson’s arguments for this conclusion see his papers in (Boghossian and Williamson 2020).
[29] This issue does not just arise for inferentialism: as the literature on the so-called ‘bad company objection’ shows abstraction operations give rise to much the same problems.
[33] More precisely: D applies to the propositions p such that either p⪰qq for some qq or else there are r and qq such that r⪰qq where p is one of the qq.
[34] More precisely. Say that Q is preserved by ⪰ (writing this ) iff . (Here r≺pp means that r is one of pp.) The claim is then:
[35] Note that while there are many properties Q such that T({{2}},Q), few of these properties are partly defined by the corresponding inference:

[36] The reason for calling rules like this ‘P-restriction’ is that the rule, in effect, allows us to restrict our attention to those q that meet P—those q, that is, that express definitions of s.
[37] This issue is noted—in connection with the color red by Fine (1994b, 72n16) who attributes the concern to Rogers Albritton.
[38] For this to work, it is important that the essence of the object-as-it-actually-intrinsically-is does not depend on the property of being red.
[40] Fine (1994b, 72n18) raises a similar concern.
[41] If this is along the right lines it will be mediately essential to 2 and the logical operations that 2 is abstracted from a two-membered plurality. We reason informally. Let q be an arbitrary definition of 2. Then P[t,b]-restriction allows us to conclude that
. Consider now some arbitrary definitions of the logical operations and ≈. By the relevant instances of P-restriction we can assume that these definitions are unique and that allow us standard logical reasoning. We can thus conclude that
. It will follow from the definitions of [t,b] and ≈ that if xx∀[t,b] then . Thus we can derive . Since any system of definitions for 2 will contain definitions for # and thus for ≈ this suffices to show that is derivable from any system of definitions for 2.
[42] That is, if it is essential to s that ϕ, then it is essential to s and the essentialist operator □ that it is essential to s that ϕ.
[43] See (Ditter 2022) for some worries about the principle in an essentialist setting.
Acknowledgements
A version of this paper was presented at the 2024 Pacific APA at a session on ‘Essence and Modality’. Thanks to the participants in that session. Thanks to the editors and the anonymous referees. Thanks especially to Kit Fine for his critical and deep engagement with the ideas of this paper.
Competing Interests
The author has no competing interests to declare.

. Then it follows from any definition of s and any definitions of the constituents in that
, the premiss is the argument 𝒜 itself.
.