Gabbay, Murdoch J. - The language of Stratified Sets is confluent and strongly normalising

lmcs:3681 - Logical Methods in Computer Science, May 23, 2018, Volume 14, Issue 2 - https://doi.org/10.23638/LMCS-14(2:12)2018
The language of Stratified Sets is confluent and strongly normalising

Authors: Gabbay, Murdoch J.

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.

Volume: Volume 14, Issue 2
Published on: May 23, 2018
Submitted on: May 23, 2017
Keywords: Computer Science - Logic in Computer Science,D.3.1,F.3.2,F.4.1