How about a sequent calculus, with standard rules:
$$ \frac{\Gamma, P, P\vdash Q}{\Gamma, P\vdash Q}CL \qquad
\frac{}{\Gamma,P \vdash P}Ax \qquad \frac{}{\Gamma, \bot \vdash P}{\bot}L $$
$$ \frac{\Gamma\vdash Q\quad \Gamma,P\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_1
\quad \frac{\Gamma\vdash P\quad \Gamma,Q\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_2
\quad \frac{\Gamma,P\vdash Q\quad \Gamma,Q\vdash P}{\Gamma\vdash P\leftrightarrow Q}{\leftrightarrow}R$$
$$ \frac{\Gamma,P\vdash R \quad \Gamma,Q\vdash R}{\Gamma,P\lor Q\vdash R}{\lor}L
\quad \frac{\Gamma\vdash P}{\Gamma\vdash P\lor Q}{\lor}R_1
\quad \frac{\Gamma\vdash Q}{\Gamma\vdash P\lor Q}{\lor}R_2 $$
This is complete for the $\{{\leftrightarrow},{\lor},\bot\}$ fragment because the full intuitionistic sequent calculus satisfies cut elimination.
To show that this fragment is complete in expressivity, express $P\to Q$ as $(P\lor Q)\leftrightarrow Q$ -- this equivalence is intuitionistically valid, and the usual left and right rules for $\to$ are easily built as combinations of the above rules.
Similarly, $\neg P$ is of course equivalent to $P\leftrightarrow \bot$.
For conjunction, contrary to speculation in comments, it turns out that $(P\lor Q)\leftrightarrow(P\leftrightarrow Q)$ is indeed intuitionistically equivalent to $P\land Q$. The difficult direction is to see that the usual ${\land}L$ rule is admissible, which can be done as follows in the above sequent calculus:
$$\begin{array}{rll}
0. & \Gamma,~ P,~ Q \vdash R & \text{premise of derived rule} \\
1. & P\vdash P\lor Q & \text{easy} \\
2. & P\leftrightarrow Q,~ P \vdash Q & \text{easy} \\
3. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P \vdash Q & 1, 2, {\leftrightarrow}L_2 \\
4. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ Q \vdash P & \text{mutatis mutandis} \\
5. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash P\leftrightarrow Q & 3,4, {\leftrightarrow}R \\
6. & P\lor Q \vdash P\lor Q & \text{axiom} \\
7. & \Gamma,~ P\lor Q,~ P\leftrightarrow Q \vdash R & \text{easy consequence of }0 \\
8. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P\lor Q \vdash R & 6,7, {\leftrightarrow}L_2 \\
9. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~
(P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 5,8, {\leftrightarrow}L_1 \\
10. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 9, CL
\end{array}$$
(Proof found by exhaustive search!)
Or, for those that favor the Curry-Howard isomorphism for intuitionistic proofs, the idea in Haskell-like pseudosyntax for the ${\leftrightarrow}{\lor}{\bot}$ fragment is to replace
conj :: (P,Q)
let (x::P,y::Q) = conj
in <..x..y..>
by
conj :: (Either P Q) <-> (P <-> Q)
let eq1 :: P <-> Q
eq1 (x :: P) = let eq2 :: P <-> Q = conj (Left x) in eq2 x
eq1 (y :: Q) = let eq2 :: P <-> Q = conj (Right y) in eq2 y
disj :: Either P Q = conj eq1
in case disj of
Left(x::P) -> let y::Q = eq1 x in <..x..y..>
Right(y::Q) -> let x::P = eq1 y in <..x..y..>
where P <-> Q
is supposed to behave like a function that can be applied to either P
or Q
and produces an output of the opposite type, and disjunction is represented by the standard Either
type.