Quantifiers in logic and proof-search using permissive-nominal terms and sets
Murdoch J. Gabbay, Claus-Peter Wirth · Journal of Logic and Computation · 2013
We investigate models of first-order logic designed to give semantics to reductive proof-search systems, with special attention to the so-called γ- and δ-rules controlling quantifiers. The key innovation is the use of syntax and semantics with (finitely supported) name-symmetry, in the style of nominal techniques.