A Note on the Use of Sum in the Logic of Proofs

The Logic of Proofs~LP, introduced by Artemov, encodes the same reasoning as the modal logic~S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application~$\cdot$, positive introspection~!, and sum~+) are sufficient to mimic provability concealed in S4~modality. While the first two operations go back to G{\"o}del, the exact role of~+ remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP.

Governance of Massive Multiauthor Collaboration – Linux, Wikipedia, and Other Networks: Governed by Bilateral Contracts, Partnerships, or Something in Between?

Open collaborative projects are moving to the foreground of knowledge production. Some online user communities develop into longterm projects that generate a highly valuable and at the same time freely accessible output. Traditional copyright law that is organized around the idea of a single creative entity is not well equipped to accommodate the needs of these forms of collaboration. In order to enable a peculiar network-type of interaction participants instead draw on public licensing models that determine the freedoms to use individual contributions. With the help of these access rules the operational logic of the project can be implemented successfully. However, as the case of the Wikipedia GFDL-CC license transition demonstrates, the adaptation of access rules in networks to new circumstances raises collective action problems and suffers from pitfalls caused by the fact that public licensing is grounded in individual copyright. Legal governance of open collaboration projects is a largely unexplored field. The article argues that the license steward of a public license assumes the position of a fiduciary of the knowledge commons generated under the license regime. Ultimately, the governance of decentralized networks translates into a composite of organizational and contractual elements. It is concluded that the production of global knowledge commons relies on rules of transnational private law.