|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
In logic, a variable is a symbol that stands for an arbitrary instantiation of some given type (although in single-typed theories the type is trivial). Thus, every variable of type is a term of type (although typically there are other terms).
Logicians have developed several ways to precisely specify what variables are and how to keep track of them, and the only thing more annoyingly pedantic than learning one of these is translating between different ones.
If we keep track of context, every introduction of a variable changes the context. Thus, whatever terms of type there may (or may not) be in a given context , in the context —which is extended by a free variable of type — there is (at least) one more term of type , and that term is itself.
Conversely, we may be able to take a term in the context and apply some operation to it to create a term (possibly of a different type) in the context ; then any appearances of the variable in the term have become bound variables in the term . That is, the appearances of are bound by the operator , and has no meaning outside of its scope.
So for example, if (say in something simple like Peano arithmetic?, supplemented with the abbreviations used in practice) I write , this is a term (for a natural number) in a context with a free variable , whereas if I write , this is a term (also for a natural number) in a context with no free variables; here, is bound. The variable has a meaning after the operator (whose notation also specifies the variable that will have a meaning inside it) and before the plus sign (which, following the standard order of operations, marks the end of the scope of ) but has no meaning outside of that (where the and are, or even where the and are). And indeed, the ultimate meaning of depends on what is, but the ultimate meaning of is simply .
We may think of the free variables here as being placeholders for all the generalized elements of .
Then the assertion
indicates that with given we may send to the composition
(universal quantifier) in which now is a bound variable.
A textbook account with an eye towards applications in computer science is in section 1.2 of
An exposition on the relation between free variables and universal quantification is in