The language of Stratified Sets is confluent and strongly normalising
Logic in Computer Science
2023-06-22 v3
Abstract
We study the properties of the language of Stratified Sets (first-order logic with 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 -conversion.
Keywords
Cite
@article{arxiv.1705.07767,
title = {The language of Stratified Sets is confluent and strongly normalising},
author = {Murdoch J. Gabbay},
journal= {arXiv preprint arXiv:1705.07767},
year = {2023}
}
Comments
arXiv admin note: text overlap with arXiv:1406.4060