Up until now, I had never read a legal statute in my life and I wouldn't be able to tell you a single thing about tax law. Today, I just spent 5 hours learning everything about the exclusion of gain from sale of principal residence.

That's because I wanted to understand the default logic behind law and this statute shows it very clearly.

Law isn't naturally formalised in standard logic. It contains rules along with many exceptions to those rules.

For example, in the statute above we have "(a) gross income shall not include gain from the sale or exchange of property... unless (b)(3) there was another property sale within 2 years of the recent sale... unless (c) the sale was due to employment, health or unforeseen circumstances in which case, we calculate a prorated cap."

This makes law's logic non-monotonic (adding new information can remove earlier conclusions) while in standard logic, the set of conclusions can only get bigger as new premises are added. This is an example of default logic.

So, when we work with many legal statutes, there are many (possibly infinitely many) exceptions to rules that just aren't written down. This is when default logic must be used.

But since, for us, we're working with just one statute, we can actually stick to using classical logic in Lean.

To do this, we first define our types: person, property, date. This statute specifically aggregates the duration of time in which the seller has owned / lived in the house, so we also have to make this aggregate function explicit.

Extract in English:

"Gross income shall not include gain from the sale or exchange of property if, during the 5-year period ending on the date of the sale or exchange, such property has been owned and used by the taxpayer as the taxpayer's principal residence for periods aggregating 2 years or more."

Extract In Lean:

def ownershipDuration (p : Person) (property : Property) (d : Date) : Duration :=
  aggregate (owns p property) (d - fiveYears) d

def useDuration (p : Person) (property : Property) (d : Date) : Duration :=
  aggregate (usesAsResidence p property) (d - fiveYears) d

-- Taxpayer has owned the property for periods aggregating 2 years or more
def ownershipRequirement (p : Person) (property : Property) (d : Date) : Prop :=
  twoYears ≤ ownershipDuration p property d

-- Taxpayer has used the property for periods aggregating 2 years or more
def useRequirement (p : Person) (property : Property) (d : Date) : Prop :=
  twoYears ≤ useDuration p property d

-- Does the sale meet the requirement?
def meetsRequirements (p : Person) (property : Property) (d : Date) : Prop :=
  ownershipRequirement p property d ∧ useRequirement p property d

Once we've formalised the domain (U.S.C IRC121), we can now verify any conclusions we make about how the sale of a person's property contributes to their gross income. Hooray.

Given a fixed set of facts about the person, the formalised statute becomes a closed, static program. Any legal argument (proof) made about U.S.C. IRC121 is also a closed, static program. The proof doesn't require any input from an external environment and the internal rules of the law never change.

But there's a caveat.

Of course, in reality, the law does change. We're assuming the proof we make is about a specific instance of the law at a certain point in time. We're also assuming that this proof doesn't at any point need a decision from an outside authority e.g. a tax court.

In practice, the above assumptions are often wrong. This is what makes formalising the law more nuanced.

For example: Section (2)(B) defines "unforseen circumstances" as a term that depends on the "extent provided in regulations". Already we can see there is a dependence on this thing called "regulations" that exists outside of the statute.

So, even here, in the most rule-based domain there is, proofs only hold given some assumptions about the external world. Formalising the domain of law is not just writing down its rules. The hard part is actually about deciding what to assume about everyone who interprets those rules and making those assumptions explicit.