The notion of LDFOB logic is revised in order to use formulae as the basic unit of reasoning (instead of judgements) and to incoporate freshness conditions in provisos. A completeness theorem is established encompassing a suitably large class of such logics. Several interesting examples are discussed. The fibring of such logics is sketched.