This proof system can be extended with countably many sequents.
Although these logics may be non-compact, strong completeness proofs are provided for infinitary hybrid versions of non-compact logics like ancestral logic and Segerberg's modal logic with the bounded chain condition.