Quantifiers in logic and proof-search using permissive-nominal terms and sets

摘要

We investigate models of first-order logic designed to give semantics to reductive proof-search systems, with special attention to the so-called gamma- and delta-rules controlling quantifiers. The key innovation is the use of syntax and semantics with (finitely supported) name-symmetry, in the style of nominal techniques.