pith. sign in

arxiv: 2312.16487 · v1 · submitted 2023-12-27 · 💻 cs.LO

Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits

Gilles Dowek , Murdoch J. Gabbay This is my paper

Pith reviewed 2026-05-24 05:24 UTC · model grok-4.3

classification 💻 cs.LO
keywords nominal semanticspredicate logicalgebrassubstitutionquantifierssoundnesscompletenessabsolute denotation
0
0 comments X

The pith

Predicate logic admits models in which every term and predicate receives an absolute denotation independent of variable valuations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs models for predicate logic in which terms and predicates receive fixed meanings regardless of variable assignments. This requires building substitution and quantification directly into the algebraic structure of the model. Ordinary set-based models can be embedded into these new models, which establishes both soundness and completeness for the approach. The construction treats substitution and quantification as operations on the algebra itself rather than operations derived from syntax.

Core claim

The central claim is that predicate logic can be interpreted in algebras where the denotation of any term or predicate is absolute and independent of a valuation. For each variable a the domain contains an element [[a]] that denotes the term a, and open predicates are interpreted directly by the algebra. Substitution and quantification are axiomatic operations on this structure, every ordinary model translates into one of these nominal models, and soundness holds.

What carries the argument

Nominal algebras in which substitution and quantification act as direct operations on model elements, allowing absolute denotations for open terms and predicates.

If this is right

  • Soundness holds for the logic with respect to these nominal models.
  • Every ordinary model based on sets and valuations translates into a nominal model.
  • Completeness of the logic follows from the existence of such translations.
  • The models interpret both closed and open formulas uniformly through the algebraic structure.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This structure may allow direct algebraic manipulation of formulas containing free variables without first closing them under valuations.
  • The same algebraic treatment of substitution could be applied to other logical systems that currently rely on variable assignments.
  • Limits mentioned in the title may provide a way to construct infinite models algebraically from finite approximations.
  • Nominal models might simplify proofs that involve simultaneous substitution across multiple open formulas.

Load-bearing premise

Substitution and quantification can be treated as axiomatic operations on the model that do not need to arise from concrete syntax.

What would settle it

An ordinary set-based model of predicate logic whose interpretations of terms and predicates cannot be preserved under any translation to a nominal algebra with the required substitution and quantification operations.

Figures

Figures reproduced from arXiv: 2312.16487 by Gilles Dowek, Murdoch J. Gabbay.

Figure 1
Figure 1. Figure 1: Derivability in first-order classical logic 3.1 Nominal posets (nominal partially ordered set) 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 amo… view at source ↗
Figure 2
Figure 2. Figure 2: Nominal algebra axioms for substitution action – Write x∧y for the greatest lower bound and x∨y for the least upper bound of {x, y}, where these exist. – Write V#ax for the a#greatest lower bound and W#ax for the a#least upper bound of {x}, where these exist. Definition 3.5. Suppose L is a partial order (it does not matter whether it is nominal). Call x ′ ∈ |L| a complement of x ∈ |L| when x ∧ x ′ = ⊥ and … view at source ↗
read the original abstract

We define 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 [[a]] 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 quantification. 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper defines a class of 'nominal' models for predicate logic in which every term and predicate (open or closed) receives an absolute denotation inside an algebra; for each variable a the domain contains a distinguished element [[a]] denoting the term a, and open predicates are interpreted directly. Substitution and quantification are treated as axiomatic operations on the algebra rather than derived from syntax. The authors prove soundness of predicate logic with respect to these models and construct a translation that embeds every ordinary set-and-valuation model into a nominal model, thereby obtaining completeness.

Significance. If the constructions and proofs hold, the work supplies an algebraic semantics that interprets open formulas without external valuations and integrates substitution and quantifiers directly into the model structure. The translation from standard models yields a completeness theorem. The approach credits the use of axiomatic operations and the explicit embedding construction as strengths.

minor comments (3)
  1. §3, Definition 3.4: the axioms for substitution and quantification are stated without an accompanying diagram or commutative diagram showing how they interact with the algebra operations; adding such a diagram would clarify the structure for readers.
  2. §4.2, Theorem 4.7: the translation from ordinary models to nominal models is described at a high level; a short worked example with a concrete two-element model would help verify that the embedding preserves the interpretation of open formulas.
  3. Notation: the double-bracket notation [[·]] is used both for the denotation map and for the distinguished elements [[a]]; a brief remark distinguishing the two uses would avoid potential confusion.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful summary of the paper and for the positive assessment of the nominal semantics approach, including the soundness and completeness results via the embedding construction. The recommendation of minor revision is noted; however, the report contains no specific major comments requiring response or changes.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper introduces a definitional construction of nominal models for predicate logic by equipping algebraic structures with axiomatic substitution and quantification operations, enabling absolute denotations [[t]] and [[P]] for open terms and predicates. Soundness follows directly from the model axioms, and completeness is obtained via an explicit translation embedding every ordinary set-and-valuation model into a nominal model. No derivation step reduces a claimed result to a fitted parameter, self-referential equation, or load-bearing self-citation; the central claims are self-contained definitions and translations whose properties are verified independently of the target results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The approach rests on treating substitution and quantification as primitive axiomatic operations rather than derived from syntax; the domain elements [[a]] for each variable are introduced as part of the model definition.

axioms (1)
  • domain assumption Substitution and quantification are axiomatic operations on the model structure and need not be applied only to sets of syntax.
    Stated directly in the abstract as a requirement for the models to interpret open predicates and terms.
invented entities (1)
  • Element [[a]] in the domain for each variable a no independent evidence
    purpose: Serves as the absolute denotation of the term a independently of any valuation.
    Introduced in the abstract as the key device that removes dependence on valuations.

pith-pipeline@v0.9.0 · 5650 in / 1251 out tokens · 21818 ms · 2026-05-24T05:24:31.966591+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

  1. [1]

    Lambda logic

    Michael Beeson. Lambda logic. In Second International Joint Conference on Automated Reasoning (IJCAR 2004) , volume 3097 of Lecture Notes in Computer Science , pages 460–474. Springer, 2004

    work page 2004

  2. [2]

    Equational logic for names and binding

    Ranald Clouston. Equational logic for names and binding . PhD thesis, University of Cambridge, UK, 2009

    work page 2009

  3. [3]

    Nominal Lawvere theories

    Ranald Clouston. Nominal Lawvere theories. In Proceedings of the 18th International Workshop on Logic, Language, and Information (WoLLIC), volume 6642 ofLecture Notes in Computer Science . Springer, 2011

    work page 2011

  4. [4]

    Roy L. Crole. α-equivalence equalities. Theoretical Computer Science, 2012. In press

    work page 2012

  5. [5]

    Gilles Dowek and Murdoch J. Gabbay. Permissive Nominal Logic. In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010), pages 165–176. ACM Press, 2010. 8 Atoms-abstraction [a]x is the native (non-functional) notion of abstraction in nom- inal techniques. It was introduced in [20]. 9 T...

    work page 2010

  6. [6]

    Gilles Dowek and Murdoch J. Gabbay. Permissive Nominal Logic (journal version). Trans- actions on Computational Logic , 2012. In press

    work page 2012

  7. [7]

    Binding logic: Proofs and models

    Gilles Dowek, Th´ er` ese Hardin, and Claude Kirchner. Binding logic: Proofs and models. In Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002) , pages 130–144. Springer, 2002

    work page 2002

  8. [8]

    Reasoning with Arbitrary Objects

    Kit Fine. Reasoning with Arbitrary Objects. Blackwell, 1985

    work page 1985

  9. [9]

    Term equational systems and logics

    Marcelo Fiore and Chung-Kil Hur. Term equational systems and logics. Electronic Notes in Theoretical Computer Science, 218:171–192, 2008

    work page 2008

  10. [10]

    Fiore, Gordon D

    Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS 1999), pages 193–202. IEEE Computer Society Press, 1999

    work page 1999

  11. [11]

    Murdoch J. Gabbay. A study of substitution, using nominal techniques and Fraenkel- Mostowski sets. Theoretical Computer Science, 410(12-13):1159–1189, March 2009

    work page 2009

  12. [12]

    Murdoch J. Gabbay. Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic , 17(2):161–229, 2011

    work page 2011

  13. [13]

    Murdoch J. Gabbay. Stone duality for First-Order Logic: a nominal approach. In Howard Barringer Festschrift. December 2011

    work page 2011

  14. [14]

    Murdoch J. Gabbay. Nominal terms and nominal logics: from foundations to meta- mathematics. In Handbook of Philosophical Logic, volume 17. Kluwer, 2012

    work page 2012

  15. [15]

    Gabbay and Vincenzo Ciancia

    Murdoch J. Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In Foundations of software science and computation structures, 14th International Conference (FOSSACS 2011) , volume 6604 of Lecture Notes in Computer Science, pages 365–380. Springer, 2011

    work page 2011

  16. [16]

    Gabbay, Tadeusz Litak, and Daniela Petri¸ san

    Murdoch J. Gabbay, Tadeusz Litak, and Daniela Petri¸ san. Stone duality for nominal Boolean algebras with NEW. In Proceedings of the 4th international conference on algebra and coalgebra in computer science (CALCO 2011) , volume 6859 of Lecture Notes in Computer Science, pages 192–207. Springer, 2011

    work page 2011

  17. [17]

    Gabbay and Aad Mathijssen

    Murdoch J. Gabbay and Aad Mathijssen. Capture-avoiding Substitution as a Nominal Algebra. In ICTAC 2006: Theoretical Aspects of Computing , volume 4281 of Lecture Notes in Computer Science , pages 198–212, November 2006

    work page 2006

  18. [18]

    Gabbay and Aad Mathijssen

    Murdoch J. Gabbay and Aad Mathijssen. Capture-Avoiding Substitution as a Nominal Algebra. Formal Aspects of Computing , 20(4-5):451–479, June 2008

    work page 2008

  19. [19]

    Gabbay and Dominic Mulligan

    Murdoch J. Gabbay and Dominic Mulligan. Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets. In Proceedings of the 6th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2011), volume 71 of EPTCS, pages 58–75, September 2011

    work page 2011

  20. [20]

    Gabbay and Andrew M

    Murdoch J. Gabbay and Andrew M. Pitts. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing , 13(3–5):341–363, July 2001

    work page 2001

  21. [21]

    Donald Monk, and Alfred Tarski

    Leon Henkin, J. Donald Monk, and Alfred Tarski. Cylindric Algebras. North Holland, 1971 and 1985. Parts I and II

    work page 1971

  22. [22]

    An introduction to cylindric set algebras

    Donald Monk. An introduction to cylindric set algebras. Logic journal of the IGPL , 8(4):451–492, 2000

    work page 2000

  23. [23]

    Andrew M. Pitts. Categorical logic. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Struc- tures, chapter 2. Oxford University Press, 2000

    work page 2000

  24. [24]

    Abstract syntax: Substitution and binders: Invited address

    John Power. Abstract syntax: Substitution and binders: Invited address. Electronic Notes in Theoretical Computer Science, 173:3–16, 2007

    work page 2007

  25. [25]

    The semantic conception of truth and the foundations of semantics

    Alfred Tarski. The semantic conception of truth and the foundations of semantics. Phi- losophy and Phenomenological Research, 4, 1944

    work page 1944

  26. [26]

    David C. Turner. Nominal Domain Theory for Concurrency . PhD thesis, University of Cambridge, 2009

    work page 2009

  27. [27]

    Logic and Structure

    Dirk van Dalen. Logic and Structure . Universitext. Springer, 1994. Third, augmented edition

    work page 1994

  28. [28]

    Topology via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science

    Steve Vickers. Topology via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. Acknowledgements. The second author acknowledges the support of the Leverhulme trust. Proc. CILC 2012, CEUR Vol. 857. VoR: urn:nbn:de:0074-857-8 15

    work page 1989