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.
- nominal techniques
- higher-order logic
- CAPTURE-AVOIDING SUBSTITUTION
- VARIABLE SEMANTIC TABLEAUX