From Ref
Jump to: navigation, search

Formalisms are formal expression systems, usually involving symbols, that may be used to define a term, state a fact, or describe a relationship between existing ideas. Formalisms range from mathematically and technically rigorous specifications to loose analogical formalisms.

Each subject wiki has its own collection of formalisms. This article discusses, with examples and illustrations, the general principles behind the use of formalisms.

How formalisms arise

Formalisms as a common pattern

The idea behind formalisms for defining terms is that, often, a lot of closely related definitions have a similar structure, with some inputs to the structure changed. For instance, many definitions of group properties have the form: a group where every subgroup has property . Many definitions of topological space properties, closely related to compactness, have the form: a topological space where every open cover satisfying property has a refinement having property . A formalism for definitions of this structure helps unite all these definitions and provides insight into how to manipulate the common features across all the terms. The advantages are:

  • It allows for grouping together of terms expressible using the same formalism
  • It helps in reverse search
  • It helps provide a better understanding of the relation between different terms
  • It sometimes suggests general tools for reasoning that can be applied whenever something is expressible in the given formalism, allowing for a better understanding of individual proofs.

Formalisms as a language at the right level of generality

While some formalisms are simply a way of recognizing and acknowledging existing patterns, other formalisms involve a more proactive approach in creating formalisms. These may involve certain special language tools within the subject that specialize in expressing a diverse range of ideas, while at the same time cannot be used to express everything. For instance, the languages of model theory, category theory, and universal algebra provide some general frameworks in which a large number (though far from all) of definitions, facts and relationships can be stated.

Presenting formalisms

Formalisms in definition articles

In articles about terminology (called terminology articles or definition articles), there may be a separate section title Formalisms. This section is usually after the History, Definition, and Examples sections. One subsection is devoted to each formalism. The heading of the subsection usually states the name of the formalism, or the operator used to obtain that formalism. Just below the heading is a box stating the general name of the formalism or operator, along with a link to more information about the formalism and to other terms expressible using the formalism. This is followed by a precise explanation of how the given term is expressed using the formalism.

Formalisms in proof articles

Proofs involving terms expressible using a certain formalism can occasionally be simplified using general techniques for manipulating expressions in that formalism. Usually, a standard proof is given in any case, and an alternative proof in terms of the formalism is provided in a separate section or subsection. This proof clearly translates the statement in terms of the formalism and explains the manipulation rules being used.



Here are some examples of definition articles on Groupprops that have formalisms sections:

  • Groupprops:Normal subgroup#Formalisms: This gives several different formal expressions for the property of normality. It begins with a first-order description of normality, then proceeds to give function restriction expressions for normality, then proceeds to describe normality in terms of relations with other subgroups, and finally describes how normal subgroups can be defined in the language of universal algebra.
  • Groupprops:Directly indecomposable group#Formalisms: This gives only one formalism for the notion of directly indecomposable group: viewing it as a consequence of applying the simple group operator to the subgroup property of being a direct factor.
  • Groupprops:Dedekind group#Formalisms: This gives two formalisms for the property of being a Dedekind group.


Here are some examples of definition articles on Topospaces that have formalisms sections: