Using definition 4, and the truth table method, we may distinguish, among the formulas, the ones that we consider to be true. This way of proceeding, however, does not quite reflect the kind of logical reasoning used when trying to prove some statement. A proof, typically, proceeds by deduction, and consists of a chain of inferences that leads to some conclusion. In order to give a theoretical account of such a notion of proof, we will introduce the notion of a provable (or derivable) formula. To this end, we first provide propositional logic with an axiomatic system.

Intuitively, an axiomatic system consists of a set of statements that we take for granted (these statements are called axioms) together with ways of reasoning that allows new statements to be deduced from already established facts (these ways of reasoning are called inference rules).

By abuse of language, we will often say axiom instead of axiom scheme. For instance, we will say "the second axiom" to refer to the second axiom scheme of Definition 7.

An inference rule is a pair $((α_0, …, α_n),α)$ where:

• the first component, $(α_0, …, α_n)$, is a finite sequence of formulas that are called the premises of the rule;
• the second component, $α$, is a formula that is called the conclusion of the rule.

Traditionally, inference rules are written by using a fraction-like notation, with the premises over the bar, and the conclusion below. Accordingly, an inference rule $((α_0, …, α_n),α)$ is written as follows:

The above inference rules is called modus ponens.

Given an axiomatic system, one may define a notion of provable formula.

When a formula $α$ is provable, one writes $⊢ α$. Take, for instance, the formula $a → a$, where $a ∈ \sc A$. It is derivable, as is shown by the following sequence of formulas:

1. $a → (b→a) → a$   —  instance of axiom scheme 1.
2. $(a → (b→a) → a) → (a → b→a) → a → a$   —  instance of axiom scheme 2.
3. $a → b→a$   —  instance of axiom scheme 1.
4. $(a → b→a) → a → a$   —  by modus ponens from (a) and (b).
5. $a → a$   —  by modus ponens from (c) and (d).

The above sequence of provable formulas is called a formal derivation or a formal proof. Taking advantage of the fraction-like notation used for the inference rules, it can be pictured as a tree:

Such a tree is called a derivation tree.

In practice, formal derivations are often used in a schematic way in order to show that all the formulas that obey a given scheme are derivable. For example, the following derivation scheme shows that every formula which is an instance of the formula scheme $α → α$ is derivable: