Syntax (Object logic)

The syntax of an object logic is commonly encoded as an LF type family of kind type.

For example, if the language of our object logic is the natural numbers, its syntax would be declared in the following way.

% declare a type family of kind "type" for natural numbers.
%sort nat %.
% inhabit the nat with the appropriate constructors.
%term nat/z nat %.
%term nat/s %pi nat %-> nat %.

See also

• Read the introductions to STELF to learn how to represent syntax in LF.
• Judgment
• Judgments as types
• Higher-order abstract syntax