To speak about foundations of mathematics, we need some formal logic. Here, a logic is a framework comprising a syntactic language and agreed upon derivation $\text{rules}$, with sentences that typically represent statements of reasoning about certain things.

In doing formal logic on a piece of paper, there is always some choice and meta-reasoning involved. For example, we humans must be capable of the act of reserving such and such letters for such and such concepts, or understand the notion the the choice of variable symbol is arbitrary. The formal notion of sort or type is conceptually not far from an informal set and when we do formal logic, we sure use a lot of informal reasoning about whats in front of us on our paper. A save but cold perspective is to view a logic as a syntactic construct, removed from it's purpose of formalizing reasoning about some objects of interest.

For specifying syntax of the language, and incidentally also for the specification of derivation rules, it's customary to use the notation scheme

$${\large\frac{foo}{bar}}(\text{foobar rule})$$

which one might read as “By the $\text{foobar rule}$, if $foo$ is permissible, then $bar$ is as well.”

Type theory also uses this two-dimensional notation. Note also that, once we set up a bunch of rules for our logic, we might choose to add rules to abbreviate deduction (Admissible rule).

It should be noted that mathematical proofs in mathematical papers are almost always not really formal in the sense of theoretical computer science.

For a small, constructive logic see Intuitionistic propositional logic. For the classical logic, extended with quantifiers which underlies most set theories, see Predicate logic. For reasoning about logical derivations, see Proof theory.

Wikipedia: Theory (formal logic), Table of logic symbols, Admissible rule

About, Specifying syntax