De Morgan dual nominal quantifiers modelling private names in non-commutative logic

DOI10.1145/3325821MaRDI QIDQ4972161zbMATH OpenOpenAlexWikidataFDO

Authors Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu

Publication date 22 November 2019

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1602.06043, http://orbilu.uni.lu/handle/10993/41612

zbMATH Keywords

nominal logicnon-commutative logiccalculus of structures

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.

Recommendations

• scientific article; zbMATH DE number 6851953
• Quantifiers in logic and proof-search using permissive-nominal terms and sets
• Foundations of Software Science and Computational Structures
• A simple sequent calculus for nominal logic
• Subatomic proof systems: splittable systems

Cited in

(6)

• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• scientific article; zbMATH DE number 6851953 (Why is no real title available?)
• A deep inference system for differential linear logic
• scientific article; zbMATH DE number 7559289 (Why is no real title available?)
• Constructing weak simulations from linear implications for processes with private names
• An Analytic Propositional Proof System on Graphs

This page was built for publication: De Morgan dual nominal quantifiers modelling private names in non-commutative logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4972161)