  Cirquent calculus is a new proof-theoretic and semantic approach introduced
for the needs of computability logic by G.Japaridze, who also showed that,
through cirquent calculus, one can capture, refine and generalize
independence-friendly (IF) logic. Specifically, the approach allows us to
account for independence from propositional connectives in the same spirit as
the traditional IF logic accounts for independence from quantifiers.
Japaridze's treatment of IF logic, however, was purely semantical, and no
deductive system was proposed. The present paper constructs a formal system
sound and complete w.r.t. the propositional fragment of Japaridze's
cirquent-based semantics for IF logic. Such a system can thus be considered an
axiomatization of purely propositional IF logic in its full generality.
