The rectify operation maps formulas to formulas. In particular, it maps formulas of the form to .It is defined as follows:

Directly from the definition on sets it follows that:

**Proof**

We prove it with structural induction on the derivation.

**Case** trivial proof:
A trivial proof is a derivation step of the form
, where .

**Case** deduction:
Deduction is the introduction of implication by derivation:

If , then .

Using deduction, we may instantiate:

If , then .

From here we can derive, under the assumption :

**Cases** axioms of predicate logic:
As an example, we prove our claim for the introduction of .Other introductions and eliminations
(, , , )have analogous proofs.

**Case** Rationality:
Let .
We prove .

**Case** axiom:

For every axiom , we will prove , by deriving .

**case** Believing Modus Ponens:
We prove it for the equivalent form

**case** Saying contents of an encrypted message:

**case** Awareness:

**case** Possessing believed keys:

The remaining axioms do not contain a believe operator, so they do not change under the rectify function.