Copyright makes no sense

The aim of this article is to question the foundational aspects of copyright law from the perspective of information theory and computability. There are many difficulties when it comes to the formalization of copyright as a concept, and we discuss current approaches and their issues.

One of the many possible (simplified) formulations of copyright law is the one based on the idea of reconstructibility. For instance, one may formulate three axioms:

• At least one work is free
• At least one work is copyrighted (the opposite of being free)
• For any work x, if it is possible to reconstruct a copyrighted work from x, then x is copyrighted as well

We demonstrate that these axioms are unsound. We perform the demonstration using Lean 4, a modern interactive theorem prover:

import Mathlib

structure World where
  Work : Type -- Abstract type representing intellectual work (book, software, movie, etc.)
  Free : Set Work -- The set of all free works
  Copy : Set Work -- The set of all copyrighted works
  copy_eq_compl_free : Copy = Freeᶜ -- Copyrighted works are exactly these that are not free
  nonempty_free : Free.Nonempty -- There is at least one free work
  nonempty_copy : Copy.Nonempty -- There is at least one copyrighted work
  mem_copy_of_apply {x : Work} : (∃ (f : Work → Work), f x ∈ Copy) → x ∈ Copy

This is called the naive formulation because the reconstructibility axiom is represented as the existence of an arbitrary (not even necessarily computable) function that outputs a copyrighted work. One may argue that it does not accurately represent the idea of reconstructibility in real-world legal systems.

In this formalization it is easy to demonstrate that no world satisfies these axioms:

theorem isEmpty_world : IsEmpty World := by
  constructor; intro w -- Assume there is some world `w` satisfying the axioms
  obtain ⟨x, hx⟩ := w.nonempty_free -- Let `x` be some free work
  obtain ⟨y, hy⟩ := w.nonempty_copy -- Let `y` be some copyrighted work
  let f (_ : w.Work) : w.Work := y -- We define constant function `f` that returns `y`
  have h := w.mem_copy_of_apply (x := x) ⟨f, hy⟩ -- Since `f x` gives `y`, `x` must be copyrighted
  simp_all [w.copy_eq_compl_free] -- `x` cannot be free and copyrighted at the same time

This "demonstration" is meant to ridicule the naive understanding of copyright and to point out that, in the absence of a solid foundational definition, this formulation is the "best" one can do when formalizing copyright. This is not because formal methods are incapable of reasoning about intricate concepts such as copyright, but because, at least currently, copyright is purely a sociological construct with no solid foundation in mathematics.

There have been many attempts to formalize copyright, but as of today, none have succeeded. One approach that some believe could be promising is to leverage the idea of forgeability. Just as in a strictly typed programming language, objects of a certain type can only be constructed using the provided constructors, and if no public constructors are provided, values of that type are said to be unforgeable. (Note: this is a very simplified definition of forgeability).

Take, for instance, the Symbol primitive in JavaScript. The only way to construct a symbol is by using the global Symbol function. However, it returns a new symbol every time, one that is not equal to any previously constructed symbol. Therefore, if a function retains a private reference to a symbol and checks whether a given argument is equal to that symbol, it can simulate a private function. Even though users can call the function from outside, it is impossible to forge the exact symbol the function expects; consequently, the function may reject all calls that do not originate from the library itself.

In the context of information theory, forgeability can be replaced by guessability. That is, even though in theory we can construct any finite string of symbols, in practice we have limited time and space. For a string of a given length, the set of all possible strings is exponentially larger than that length. Roughly speaking, with linear resources and an exponential number of possibilities, most possibilities remain inaccessible simply because we cannot explore them all. Some possibilities are derivable only if a specific source of entropy is provided. Thus, certain works "embed" that entropy in a cryptomorphic manner, unexaminable without access to the entropy itself.

Whether this approach could yield a useful formalization remains a point of debate. It is tightly related to the P vs NP problem. Without deeper insight into the very nature of complexity classes and how the world actually works in the context of information theory, it is difficult to decide whether copyright can ever make sense as a solid foundational framework. Until a good candidate formalization appears, copyright cannot be regarded as anything more than a purely social concept, invented only to artificially constrain the sharing of knowledge and make life in this world more difficult and miserable.

See Also

• wikipedia:illegal prime