The notion of formula is mainly syntactic. A formula may be seen as a sequence of symbols that obeys some formation rules. It is built from four kinds of symbols:

1. primitive symbols that stands for atomic propositions ;
2. logical constants: '$⊥$', and '$⊤$' ;
3. logical connectives: '$→$', '$∧$', '$∨$', and '$¬$' ;
4. auxiliary symbols: '$($' and '$)$'.

The formal definition is given below.

The above definition must be understood literally. For instance, the fifth clause must be read as follows: if $α$ and $β$ are formulas then the expression made of the symbol '$($'  followed by the expression for which $α$ stands, followed by the symbol '$∧$', followed by the expression for which $β$ stands, followed by the symbol ' $)$'  is a formula.

A formula of the form $(α ∧ β)$ is called a conjunction. A formula of the form $(α ∨ β)$ is called a disjunction. A formula of the form $(α → β)$ is called an implication. A formula of the form $(¬α)$ is called a negation.

Intuitively, a negation $(¬α)$ asserts that proposition $α$ does not hold. A conjunction $(α ∧ β)$ asserts that both propositions $α$ and $β$ hold. A disjunction $(α ∨ β)$ asserts that at least one of proposition $α$ or proposition $β$ holds. An implication $(α → β)$ asserts that proposition $α$ holds whenever proposition $β$ holds. Finally, $⊥$ stands for a proposition which is always false, and $⊤$ for a proposition which is always true.

The formulas may be seen as the expressions of a formal language. This formal language is our object of study, and will be called the object language. For instance, if $a$ and $b$ are actual atomic propositions, $(a ∧ b)$ is an expression of the object language. By contrast, when we speak about the object language, we use another language that will be called the metalanguage. This second language is not formalized, and is made of a mixing of English and mathematical expressions. For instance, when we say "let $α$ and $β$ be formulas, and consider the formula $(α ∧ β)$", this expression belongs to the metalanguage. In particular, the expression $(α ∧ β)$ is not, strictly speaking, a formula. It is an expression of the metalanguage that stands for a formula. Indeed, $α$ and $β$ are not atomic propositions, but variables that range over formulas. To stress this fact, $α$ and $β$ will be called metavariables, and an expression such as $(α ∧ β)$ will be called a formula scheme. When an actual formula is an instance of a formula scheme, we will say that it obeys this formula scheme.

We use some notational conventions in order to save parentheses. We do not write parentheses around negation, i.e, we write $¬α$ for $(¬α)$. We consider that conjunction and disjunction associate to the left, i.e., we write $(α_0 ∧ α_1 ∧ α_2 \; … ∧ α_n)$ for $(…((α_0 ∧ α_1) ∧ α_2) \; … ∧ α_n)$. By contrast, we consider that implication associates to the right, i.e., we write $(α_0 → α_1 → α_2 → … \; α_n)$ for $(α_0 → (α_1 → (α_2 → (\; … \;α_n\; … \;))))$. Finally, we do not write the outermost parentheses. For instance, we write $α ∧ (β ∨ γ)$ for $(α ∧ (β ∨ γ))$.

As an example, consider the following formula: Using the above conventions, it may be written as follows: