Copyright makes no sense

In this article we prove that copyright does not make any sense. Not only that we prove it, but we also verify the proof using Lean theorem prover. The proof is 100% correct!

Definitions

A book is a finite list of symbols (a symbol is a natural number, for simplicity). There exists a set of all copyrighted books. Also, there exists a set of all free books (in this context, by "free" we mean "public domain").

Axioms

All lawyers that I asked told me there are three axioms:

1. At least one book is copyrighted (choose any book you can't download for free from the internet).
2. At least one book is free (this article, for example).
3. If you have some book and there is a reliable way that you can reconstruct a copyrighted book from it, then that book is copyrighted too.

Theorem

If those axioms are consistent, zero is equal to one.

Proof

-- Lean: v3.42.0
-- Mathlib: b6d246a6

import tactic

-- A book is a sequence of symbols
def book : Type := list ℕ

-- There is a set of all copyrighted books
constant copyrighted : set book

-- And the set of all free books (public domain)
def free : set book := set.univ \ copyrighted

-- At least one book is copyrighted
axiom exi_cop : ∃ (b : book), b ∈ copyrighted

-- At least one book is free
axiom exi_free : ∃ (b : book), b ∈ free

-- If you can reconstruct a copyrighted book from some other book,
-- then that book is copyrighted too 
axiom copy_tran : ∀ (b₁ b₂ : book), (∃ (f : book → book), f b₁ = b₂) →
  b₂ ∈ copyrighted → b₁ ∈ copyrighted

-- Copyright makes no sense! (CONFIRMED)
lemma copyright_makes_no_sense : 0 = 1 :=
begin
  obtain ⟨b₁, h₁⟩ := exi_cop,
  obtain ⟨b₂, h₂⟩ := exi_free,
  have h₃ : b₂ ∉ copyrighted,
  { simp [free] at h₂, exact h₂ },
  have h₄ : b₂ ∈ copyrighted,
  { exact copy_tran b₂ b₁ ⟨λ _, b₁, rfl⟩ h₁ },
  contradiction,
end

See Also

• wikipedia:illegal prime