The language of Stratified Sets is confluent and strongly normalising

Abstract

We study the properties of the language of Stratified Sets (first-order logic with $\in$ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to $\beta$-conversion.

arXiv admin note: text overlap with arXiv:1406.4060

References in corpus (5)

• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
• Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
• Semantics out of context: nominal absolute denotations for first-order logic and computation
• Equivariant ZFA with Choice: a position paper