We de ne a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element JaK which is the denotation of the term a (which is also a variable symbol). Similarly, the algebra interpreting predicates in the model directly interprets open predicates. Because of this models must also incorporate notions of substitution and quanti cation. These notions are axiomatic, and need not be applied only to sets of syntax. We prove soundness and show how every `ordinary' model (i.e. model based on sets and valuations) can be translated to one of our nominal models, and thus also prove completeness.
1 Accessible references for Heyting and Boolean algebra are easily found online. For a
modern and encyclopaedic treatment, see e.g. [
Map of the paper Section 2 presents the technical background: nominal sets
and rst-order logic. Section 3 introduces nominal posets and substitution
algebras. This material is partly new (nominal posets and V#A) and partly a
restatement of [
Nominal sets were introduced in [
We want names to `exist' in the denotation. We do this by endowing sets with a symmetry group action over name permutations (De nition 2.3). We extract from this the key idea of support (De nition 2.4), which captures the degree of asymmetry of an element under the group action. We use this to de ne a nominal set X (De nition 2.6) as a set with a group action all of whose elements x are at most nitely asymmetric (have nite support), where a#x and a 62 supp(x) mean the same thing: \x is symmetric over/does not depend on the name a". We do not a priori assume e.g. a substitution action on names; in our framework this is algebraically de nable just from the more primitive notion of permutable names and nite asymmetry (see e.g. Figure 2).
De nition 2.1. Fix a countably in nite set of atoms A. We use a permutative convention that a; b; c; : : : range over distinct atoms.
that nontriv ( ) = fa j (a) 6= ag is nite.
Write id for the identity permutation such that id (a) = a for all a. Write
0 for composition, so that ( 0 )(a) = 0( (a)). Write -1 for inverse, so
that -1 = id = -1. Write (a b) for the swapping (terminology from
[
underlying set jXj and a permutation action written x which is a group action on jXj, so that id x = x and ( 0 x) = ( 0) x for all x 2 jXj and permutations and 0.
De nition 2.4. Say that A A supports x 2 jXj when for every , if (a) = a for every a 2 A then x = x. If some nite A supporting x exists, then call x nitely-supported. Then de ne the support of x by
supp(x) = \fA j A nite; A supports xg: Write a#x as shorthand for a 62 supp(x) and read this as a is fresh for x. Theorem 2.5. Suppose X is a set with a permutation action and x 2 jXj. Then if x has nite support then supp(x) supports x and is the unique least nite supporting set of x.
Proof. See [12, Theorem 2.21]. A di erent but equivalent formulation of the
result is in [
De nition 2.6. Suppose X is a set with a permutation action.
Call a set with a permutation action X a nominal set when every x 2 jXj has nite support. X, Y, Z will range over nominal sets.
Example 2.7. { A is a nominal set where a = (a). It is easy to check that supp(a) = f g
a .
{ The sets of terms and predicates from De nition 2.12 below, are nominal
sets if we let permutation act in the natural way on the atoms (considered
as variable symbols) inside them. It is easy to check that supp(r) or supp( )
is equal to the atoms occurring in r or if we do not take terms up to
-equivalence, and supp(r) or supp( ) is equal to the atoms occurring free
in r or if we do take r or up to -equivalence. A detailed study of this
is in [12, Section 5]; see also [
Later on in this paper we shall see more examples. Notably, the sets X from
De nition 5.9 are nominal sets, and the set of valuations from De nition 5.3
is a set with a permutation action but not a nominal set (see Remark 5.8 and
associated footnote). For more examples see [
f ( x) for all permutations and x 2 jXj. In this case write f : X ! Y. f (x) = Proposition 2.9. supp( x) = f (a) j a 2 supp(x)g.
Proof. It is not hard to check that A supports x if and only if f (a) j a 2 Ag supports x. We use Theorem 2.5.
Corollary 2.10. 1. If (a) = a for all a 2 supp(x) then 2. If (a) = 0(a) for every a 2 supp(x) then x = 0 x. 3. a#x if and only if 9b:b#x ^ (b a) x = x. x = x.
Proof. Parts 1 and 2 follow from the fact that supp(x) supports x (Theorem 2.5). Part 3 follows using Proposition 2.9. 2.2
First-order logic is of course standard. The reader can nd any number of
presentations in the literature, for instance [
De nition 2.11. Here and for the rest of this paper x a signature = (TermFormers ; PredicateFormers ; arity ) of term-formers and predicate-formers and an arity function arity mapping TermFormers [ PredicateFormers to N = f0; 1; 2; : : : g. We let f range over distinct term-formers and P range over distinct predicate-formers.
inductively by: r ::= a j f(r1; : : : ; rarity(f))
::= ? j P(r1; : : : ; rarity(P)) j ^ j : j 8a: De ne free atoms inductively by: fa(a) = fag fa(f(r1; : : : ; rn)) = Si fa(ri) fa(?) = ? fa(P(r1; : : : ; rn)) = Si fa(ri) fa(: ) = fa( ) fa( 1^ 2) = fa( 1) [ fa( 2) fa(8a: ) = fa( )nfag De nition 2.13. We take predicates up to -equivalence as usual (so for instance 8a:P(a) = 8b:P(b) where arity (P) = 1).
We write r[a:=s] and [a:=s] for the usual capture-avoiding substitution on terms and predicates. For instance, f(a)[a:=b] = f(b) and (8b:P(a))[a:=b] = 8b0:P(b).
De nition 2.14. Let and range over nite sets of predicates. A sequent is a pair ` . We de ne the derivable sequents as usual for classical rst-order logic by the rules in Figure 1. 3
We obtain our nominal semantics for rst-order logic by combining two things: a partial order, and a substitution action. We need the partial order to interpret entailment. We need the substitution action to interpret variables and substitutions. These are Subsections 3.1 and 3.2.
Of course, these two things interact via quanti ers. Thus we introduce the novel notion of V#AX, an A#greatest lower bound for a set X (Notation 3.3). It turns out that this generalises ?, ^, and V#a into a single de nition. ; ? ` (?L)
` ; ; : ` ; [a:=s] ` ; 8a: ` We can now begin to ask what happens if we combine the notion of partially ordered set with the notion of nominal set. In particular, we can think about greatest lower and least upper bounds in the presence of nominal freshness. This leads us to the idea of V#AX and W#AX; greatest lower and least upper bounds amongst elements that do not include A in their support.
De nition 3.1. A nominal poset is a tuple L = (jLj; ; ) such that (jLj; ) is a nominal set and jLj jLj is an equivariant partial order.2
Call L nitely fresh-complete when for every nite subset X jLj and every nite set of atoms A A the set of A-fresh lower bounds
fx0 2 jLj j A \ supp(x0) = ? ^ 8x2X:x0 xg has a -greatest element V#AX.
Similarly call L nitely fresh-cocomplete when for every nite X and A as above the set of A-fresh upper bounds fx0 2 jLj j A \ supp(x0) = ? ^ 8x2X:x x0g has a -least element W#A X.
Lemma 3.2. V#AX and W#AX are unique if they exist.
Proof. From the fact that for a partial order, x y and y x imply x = y.
Notation 3.3. Suppose L = (jLj; ; ) is a nitely fresh-complete and -cocomplete nominal poset. Suppose X jLj and A A are nite. Then: { Call V#AX an A#greatest lower bound (`A-fresh greatest lower bound' ) of X. If A = ? then we may just call this a greatest lower bound. If A = fag we may just call this an a#greatest lower bound and write it V#aX. { Call W#AX an A#least upper bound of X. If A = ? then we may just call this a least upper bound. If A = fag we may just call this an a#least upper bound and write it W#aX.
Notation 3.4. Suppose L = (jLj; ; ) is a nominal poset.
{ Write > for the greatest lower bound and ? for the least upper bound of the empty set ?, where these exist. 2 So x y if and only if x
De nition 3.5. Suppose L is a partial order (it does not matter whether it is nominal). Call x0 2 jLj a complement of x 2 jLj when x ^ x0 = ? and x _ x0 = >. If every x 2 jLj has a complement say that L has complements, and write the complement of x as :x.
Lemma 3.6. Complements are unique if they exist.
Corollary 3.7. Suppose L = (jLj; ; ) is a nominal poset. 1. Suppose X jLj is nite and A A, and V#AX exists.
Then supp(V#AX) Sfsupp(x) j x 2 XgnA. 2. Suppose x2jLj, and suppose :x exists. Then supp(:x) = supp(x). Proof. We can use symmetry (equivariance) properties of atoms: 1. Using [12, Theorems 2.29 and 4.7] supp(V#AX) Sfsupp(x) j x 2 Xg [ A.3
Since by assumption A \ supp(V#AX) = ?, the result follows. 2. By [12, Theorem 4.7] and since the map x 7! :x is injective. 3.2
The reader may be used to seeing substitution as a concrete operation on sets. However, using nominal sets we can powerfully (and axiomatically) generalise substitution to be an abstract (nominal) algebraic structure.
De nition 3.8. A termlike substitution algebra over (jUj; ; atm; sub) where: is a tuple U = { (jUj; ) is a nominal set. { atm : A ! jUj is an equivariant injection, usually written invisibly (so we write atm(a) just as a). { sub : jUj A jUj ! jUj is an equivariant substitution action, written in x v[a7!u]. such that the equalities (Suba) to (Sub ) of Figure 2 hold, where x, u, and v range over elements of jUj. 3 This is just a fancy way of observing that since the de nition of V is symmetric in atoms, the the result must be at least as symmetric as the inputs.
De nition 3.9. Suppose U = (jUj; ; sub; atm) is a termlike substitution algebra. A substitution algebra over U is a tuple B = (jBj; ; sub) where: { (jBj; ) is a nonempty nominal set. { sub : jBj A jUj ! B is an equivariant substitution function satisfying the axioms (Subid) to (Sub ) of Figure 2, where x ranges over elements of jBj and u and v range over elements of jUj.
Example 3.10. 1. The set of atoms A is a termlike substitution algebra where atm(a) = a and a[a7!x] = x and b[a7!x] = b. 2. Terms from De nition 2.12 are a termlike substitution algebra with atm(a) = a and r[a7!s] equal to r[a:=s]. 3. Predicates from De nition 2.12 are not a termlike substitution algebra, because there are no predicate variables or substitution for predicates. Predicates are however a substitution algebra over terms.
In Corollary 5.13 we will prove that jN j from De nition 5.11 is a termlike
substitution algebra, and X from De nition 5.11 is a substitution algebra. For
di erent and non-trivial classes of substitution algebras see [
De nition 4.1 is the culminating de nition of this paper; we de ne a notion of Boolean algebraic structure suitable for giving an `absolute' interpretation of rst-order logic. This means that variables, substitution, and quanti cation must be part of the model just as much as conjunction and negation are part of ordinary Boolean algebras. With our de nitions so far, this is now not di cult.
De nition 4.1 is not quite enough to interpret rst-order logic on its own. For that, we need the notion of model which we develop next in Subsection 4.2. De nition 4.1. Suppose U is a termlike substitution algebra. A nominal Boolean algebra over U is a tuple B = (jBj; ; ; sub) such that: { (jBj; ; ) is a nitely fresh-complete nominal poset with complements. { (jBj; ; sub) is a substitution algebra over U.
{ The partial order is compatible with the substitution action: (Compat V) (V#AX)[a7!u] = V#Afx[a7!u] j x2Xg if A\supp(u)=?; a62A (Compat:) (:x)[a7!u] = :(x[a7!u]): A more accurate name for `nominal Boolean algebra' might be `nominal V#A: partial order'. But that is a bit of a mouthful.4 It is quite easy to derive some basic properties of nominal Boolean algebras, which are useful for Theorem 4.13. 4 A possibly nice classi cation is to de ne a notion of bounded nominal lattice which is equipped with ^, _, ?, >|and also with V#ax. Then our nominal Boolean algebra is just a nominal lattice with complements and a compatible substitution action. Lemma 4.2. If b#u then (V#bx)[a7!u] = V#b(x[a7!u]).
Proof. This is just (Compat V) where A = fbg. Recall that by our permutative convention a 62 fbg.
Lemma 4.3. x
y if and only if x ^ y = x.
Proof. Both hold if and only if x is a greatest lower bound for fx; yg. Lemma 4.4. 1. (x ^ y)[a7!u] = x[a7!u] ^ (y[a7!u]). 2. ?[a7!u] = ?.
Proof. From (Compat V) and (Compat:) respectively.
Corollary 4.5. If x y then x[a7!u] y[a7!u]. As a further corollary, if x and a#x then x y[a7!u] for every u 2 jUj. y Proof. This follows from Lemma 4.3 and part 1 of Lemma 4.4. The further corollary follows using (Sub#) from Figure 2.
Lemma 4.6. Suppose x 2 jBj and u 2 jUj and a 2 A. Then V#ax x[a7!u].
Proof. By Notation 3.4 V#ax is the a#greatest lower bound for fxg. This means that V#ax x and a#V#ax. We use Corollary 4.5.
Lemma 4.7. Suppose x; y2jBj and a2A. Then x y and a#x imply x
V#ay.
Proof. This is the a#greatest lower bound property of V#ay with respect to fyg. Corollary 4.8. V#ax is the greatest lower bound of fx[a7!u] j u 2 jUjg in B. u 2 jUj. In particular then, z Proof. By Lemma 4.6 V#ax is a lower bound. Now suppose z (Subid)
= x[a7!a] x. By Lemma 4.7 z x[a7!u] for every
V#ax. 4.2
De nition 4.9. A model M = (U; B; -M) consists of: { A termlike substitution algebra U (De nition 3.8). { A nominal Boolean algebra B over U (De nition 4.1). { An assignment -M to each term-former f of an equivariant function fM : jUjarity(f) ! jUj and to each predicate-former P of an equivariant function PM : jUjarity(P) ! jBj such that (Commf) (CommP) fM(u1; : : : ; uarity(f))[a7!u] = fM(u1[a7!u]; : : : ; uarity(f)[a7!u])
PM(u1; : : : ; uarity(f))[a7!u] = PM(u1[a7!u]; : : : ; uarity(f)[a7!u]): For the rest of this section x a model M = (U; B; -M).
J 0^ KM = J 0KMM^ J K
J: KM = :J K De nition 4.10. De ne an interpretation function J-KM mapping terms and predicates (De nition 2.12) to elements of jUj and jBj respectively, as follows: JaKM = atm(a) Jf(r1; : : : ; rn)KM = fMM(Jr1KM; : : : ; JrnKM)
J?KM = ? M JP(r1; : :J:8; arn:)KKMM == PV#a(JJrK1MKM; : : : ; JrnKM)
when J KM = > and call valid in M.
Proposition 4.12. Jr[a:=s]KM = JrKM[a7!JsKM] and J [a:=s]KM = J KM[a7!JsKM].
Proof. By routine inductions on r and : { The case of a. Ja[a:=s]KM = JsKM and by (Subid) JaKM[a7!JsKM] = JsKM. { The case of f(r1; : : : ; rn). Using (Commf). { The case of 0^ . Using part 1 of Lemma 4.4.
{ The case of 8a: . Using Lemma 4.2.
` then V
M We have to recall the (standard) de nition of model for rst-oder logic. This is Subsection 5.1. Then in Subsection 5.2 we show how to lift this to a nominal model and obtain completeness as an immediate corollary (Theorem 5.18 and Corollary 5.19). We brie y sketch the ordinary model of rst-order classical logic, with valuations and without atoms. This model is not intended to be sophisticated; we will just need that one exists.
Notation 5.1. To avoid the confusion between sets and nominal sets, we may write ordinary set for the former.
De nition 5.2. An ordinary model N = (jN j; -N ) is a tuple such that: { jN j is some non-empty (ordinary) underlying set. { -N assigns to each term-former f a function fN : jN jarity(f) ! jN j and to each predicate-former P a function PN : jN jarity(P) ! f?; >g.
De nition 5.3. Write A)jN j for the set of functions from atoms to jN j. Let & range over elements of A)jN j and call these valuations (to N ).
Also if x 2 jN j then write &[a:=x] for the function such that (&[a:=x])(a) = x and (&[a:=x])(b) = &(b).
De nition 5.4. f?; >g is a complete Boolean algebra. We use standard de nitions, such as ^, :, V, and W without further comment De nition 5.5. De ne an interpretation function J-KN& mapping terms and predicates (De nition 2.12) to elements of jN j and f?; >g (considered as a Boolean algebra) respectively, as follows:
JaKN& = &(a)
J?KN& = ? J 0^ KN& = J 0KN& ^ J KN&
J: KN& = :J K&
N
Jf(r1; : : : ; rn)KN& = fN (Jr1KN& ; : : : ; JrnKN& )
JP(r1; : :J:8; arn:)KKNN&& == PVNx(2JjrN1KjJN& ; :KN:&[a::;=Jx]rnKN& )
Theorem 5.6 expresses the usual soundness and completeness result for rstorder logic; for details and proofs see e.g. [27, Subsection 1.5]: Theorem 5.6. ` is derivable if and only if for every ordinary model N and every valuation & to N it is the case that V 2 J KN& = > implies W 2 J KN& = >. 5.2
We now show how to `lift' a model over ordinary sets to a nominal model (Proposition 5.16). We then deduce completeness for nominal Boolean algebras (Corollary 5.19).
De nition 5.7. Give valuations & 2 A)jN j a permutation action by ( &)(a) = &( -1(a)): Remark 5.8. A)jN j forms a set with a permutation action (De nition 2.3). This is not in general a nominal set because it has elements without nite support5 for our purposes that will not be a problem.
In fact, the action from De nition 5.7 is a special case of the standard conjugation action ( &)(a) = &( -1(a)) where we use the trivial action x = x for every x 2 jN j. This is standard; for a speci cally `nominal' discussion see [14, De nition 2.4.2].
De nition 5.9. Given an ordinary set X write X = (jX j; ) for 5 The nitely-supported & are such that there exists a nite A A such that for all a; b 62 A, &(a) = &(b); it is not worth our while to impose this restriction, though it would do no harm to do so. { jX j is the set of functions f from A)jN j to X such that there exists a nite set A such that if &(a) = &0(a) for every a 2 A then f (&) = f (&0), and { the permutation action is de ned by
( f )(&) = f ( -1 &): We will be most interested in jN j and f?; >g .
Lemma 5.10. For any ordinary set X, X nominal set (De nition 2.6). from De nition 5.9 determines a Proof. It is routine to verify that the permutation action is indeed a group action. It remains to check nite support.
Suppose (a) = a for every a 2 A (notation from De nition 5.9). By Definition 5.9 ( f )(&) = f ( -1 &). By De nition 5.7 ( -1 &)(a) = &( (a)). Now by assumption &(a) = &( (a)) for every a 2 A. Therefore, ( -1 &)(a) = &(a) for every a 2 A, and so f (&) = f ( -1 &), and so ( f )(&) = f (&). Thus, f has nite support (and is supported by A).
De nition 5.11. Suppose N is an ordinary model (De nition 5.2). Specify a tuple (jjN j j; ; atm; sub) by: { atm is de ned by atm(a)(&) = &(a).
{ sub is de ned by f [a7!g](&) = f (&[a:=g(&)]).
We may write jN j for (jjN j j; ; atm; sub).6
Furthermore if X is any ordinary set then (abuse notation again and) write X = (jX j; ; sub) where f [a7!g](&) = f (&[a:=g(&)]) for f 2 jX j and g 2 jjN j j. Lemma 5.12. Suppose X is an ordinary set and f 2 jX j. Then if &(a) = &0(a) for every a 2 supp(f ) then f (&) = f (&0).
Proof. Suppose &(a) = &0(a) for every a 2 supp(f ). It su ces to show that if a 2 A n supp(f ) and x 2 jN j then f (&[a:=x]) = f (&).
Choose fresh b : (so b 62 A). By part 1 of Corollary 2.10 (b a) f = f , since a; b 62 supp(f ). We reason as follows:
f (&[a:=x]) b62=A f (&[a:=x][b:=&(a)]) (b a)=f=f f (&[b:=x]) b62=A f (&) Corollary 5.13. N from De nition 5.11 is indeed a termlike substitution algebra, and X is indeed a substitution algebra over N .
Proof. We examine De nitions 3.8 and 3.9 and see that we need to check equivariance and the axioms (Suba) (for the termlike case) and (Subid) to (Sub ) from Figure 2. This is routine; we use Lemma 5.12.
De nition 5.14. Suppose g0; g 2 jf?; >g j. Write g0 g when 8&:g0(&) g(&). 6 So we abuse notation by overloading with the nominal set, and jjN j j is: the underlying set of the substitution algebra obtained from the underlying set of the ordinary model N . What could be simpler? Lemma 5.15. (jf?; >g j; ; ) is a ments.
nitely fresh-complete lattice with compleProof. It is easy to check that :g de ned by (:g)(&) = :(g(&)) is a complement to g.
Now suppose X jf?; >g j and A A are nite, and suppose A\supp(u) = ? and a 2 AnA. De ne
(V#AX)(&) = ^fg(&[a:=xa]a2A) j g 2 X; 8a2A:xa 2 jN jg: It is routine to verify that this is an A#greatest lower bound for X. Proposition 5.16. (jf?; >g j; ; ; sub) is a nominal Boolean algebra over jN j . Proof. We unpack De nition 4.1.
{ (jf?; >g j; ) is a nominal set by Lemma 5.10. { (jf?; >g j; ; ) is by Lemma 5.15 a nitely fresh-complete lattice with complements. { (Compat V) and (Compat:) follow by easy calculations, since De nition 5.14 is pointwise on valuations.
De nition 5.17. The interpretation of term-formers and predicate-formers is simple: fI(f1; : : : ; farity(f))(&) = fN (f1(&); : : : ; farity(f)(&))
PI(f1; : : : ; farity(f))(&) = PN (f1(&); : : : ; farity(f)(&)) Theorem 5.18. (jN j ; f?; >g ; -I) determines a model in the sense of Def. 4.9. Proof. jN j is a termlike substitution algebra by Corollary 5.13. f?; >g is a nominal Boolean algebra over jN j by Proposition 5.16. The commutation conditions (Commf) and (CommP) are by easy calculations.
Corollary 5.19. If 6` , then there exists a termlike substitution algebra U and a nominal Boolean algebra M over U such that V 2 J KM 6 W 2 J KM.
As a corollary, if is inconsistent (that is, if ` ?) then has a model. Proof. By completeness of rst-order logic there exists some ordinary model N (?D. eItnfiotliloonw5s.f2r)omandDevanluitaitoinon5.&1t4otNhatsuVch2thJatKMV6 2WJ2KN&J=KM>. and W 2 J KN& =
It is also possible give a direct proof of completeness of rst-order logic with
respect to the models of De nition 4.9, using a model based on syntax quotiented
by derivable equality. The advantage of the proof of completeness used here is
that it also shows that completeness does not hold just because the only models
available are syntax-based. Topological models [
The usual Tarski semantics, based on valuations, has names in the syntax but not in the semantics. Names can be used to name semantic objects but these objects do not themselves contain names. We have challenged the prejudice that only syntax contains names, and proposed a framework where names are (also) in denotation.
This is related to a broad debate in philosophy about to what extent names
are real. One investigation in that literature deserves special mention: Kit Fine's
notion of arbitrary object [
This paper is part of a broader research context. For instance in [
In this paper we apply the technology to the theory of lattices, in particular identifying A#fresh limits as the single unifying notion of greatest lower bound needed to model both conjunction and universal quanti cation. This is another step towards a `nominal' view of logic and computation whereby names, and associated structures, are treated as integral to denotation.
Related and future work A nominal style semantics related to the semantics
of this paper has been given for the -calculus [
A relative of nominal lattices is cylindric set algebras [
There are two natural avenues for future work: 7 Fine did not have permutations or nite support independently of and preceding the notion of substitution.
Add binders to the term-language. Part of the challenge of this is to develop a suitable new syntax extending rst-order logic with term-formers that can bind. Once we have this, it is easy to interpret binders, because our (nominal) denotation supports atoms-abstraction as primitive.8
In particular, we see this being applied computationally in formalising mathematics, where binders are everywhere, as an improvement over rst-order logic (where term-formers cannot bind) or higher-order logic (which may already be unnecessarily powerful).
This would be related to the permissive-nominal logic of [
Slightly less ambitiously, we can simply consider a general notion of nominal
lattice, which enriches ordinary lattices with V#ax (a greatest a#lower bound for
x) but without necessarily assuming a substitution action.9 Clearly, there is a
rich theory of nominal preorders which remains to be explored.
8 Atoms-abstraction [a]x is the native (non-functional) notion of abstraction in
nominal techniques. It was introduced in [
Acknowledgements. The second author acknowledges the support of the Leverhulme trust.