The first-order syntax of variadic functions

DOI10.1215/00294527-1731380zbMath1280.03008arXiv1105.4135OpenAlexW2067714768MaRDI QIDQ1934953

Samuel A. Alexander

Publication date: 30 January 2013

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1105.4135

zbMATH Keywords

ellipsissyntaxextension of first-order logicsubstitution lemmabounded quantifier eliminationdefinability of Borel setsvariadic function symbols

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)

Uses Software

• Coq
• miniKanren

Cites Work

• A variadic extension of Curry's fixed-point combinator
• Braids and self-distributivity
• On Guessing Whether A Sequence Has A Certain Property
• Accessible Independence Results for Peano Arithmetic
• The effective Borel hierarchy
• Symmetric and Self-Distributive Systems

This page was built for publication: The first-order syntax of variadic functions