A [[Proof System]]. **Rules for the quantifiers** - Universal elimination ($\forall \text{Elim}$): - Existential introduction ($\exists \text{Intro}$): - Universal introduction ($\forall \text{Intro}$): - Existential elimination ($\exists \text{Elim}$): Rules for $=$ - Identity Elimination ($=\text{Elim}$): - Identity Introduction ($=\text{Intro}$):