$FDE$ is often presented as a purely extensional logic (and the most accessible intro I know for this is Kūro’s excellent page here The simple case for subclassical logic). But what’s less commonly known is that it may also be presented as a logic with an implicational operator. Of course though, there will only be first-degree formulas, i.e. we won’t have any nested implications.

Axioms

  1. $\vdash (A \wedge B) \rightarrow A$ Simplification
  2. $\vdash (A \wedge B) \rightarrow B$ Simplification
  3. $\vdash A \rightarrow (A \lor B)$ Addition
  4. $\vdash B \rightarrow (A \lor B)$ Addition
  5. $\vdash (A \wedge (B \lor C)) \rightarrow ((A \wedge B) \lor C)$ Distribution
  6. $\vdash A \rightarrow \neg \neg A$ Double Negation Introduction
  7. $\vdash \neg \neg A \rightarrow A$ Double Negation Elimination

Rules

R1.

$\vdash A \rightarrow B$

$\vdash B \rightarrow C$


$\vdash A \rightarrow C$ Rule Hypothetical Syllogism

R2.

$\vdash A \rightarrow B$

$\vdash A \rightarrow C$


$\vdash A \rightarrow (B \land C)$ Lattice $\land$

R3.

$\vdash A \rightarrow C$

$\vdash B \rightarrow C$


$\vdash (A \lor B) \rightarrow C$ Lattice $\lor$

R4.

$\vdash A \rightarrow B$


$\vdash \neg B \rightarrow \neg A$ Rule Contraposition