Legal systems typically use non-monotonic logic. Most formal logic systems, particularly in mathematical fields, use monotonic logic. Monotonic logic isn't well suited for the law or most other areas of human activity.

If you want an entire legal system formally defined in logic, you're going to have to do a ton of novel work in expanding the understanding of and application of non-monotonic logic because there isn't much scholarship compared to monotonic logic systems.

That said, France is one of the only countries that has tried anything like this. Their tax system is required to be defined and expressed algorithmically, and they even built a programming language and compiler tool chain to do this. I think it uses monotonic logic, though, and I don't think anybody has seriously suggested the French tax code is something to be copied, neither as a tax code nor an approach to legal codification more generally.

> But the Rodin Museum and the Ministry of Culture simply ignored the court’s order. To be clear, they did not appeal it, they ignored it.

No formulation of the law will solve this. The problem is clearly not that the law was unclear. Either the people with real power do what's right, or they don't.

> People always get upset when I propose mathematical formalization of law and using e.g. metamath verifier as a judge.

I don’t get upset. I just don’t know what that means. What would that look like in practice?

Lets see some simple example. 18 U.S. Code § 912: “Whoever falsely assumes or pretends to be an officer or employee acting under the authority of the United States or any department, agency or officer thereof, and acts as such, or in such pretended character demands or obtains any money, paper, document, or thing of value, shall be fined under this title or imprisoned not more than three years, or both.”

How would you write that in mathematical formalization?

And then how would you make a metamath verifier judge if Robert J. Rippee committed it on January 1, 1991? I’m sure you can google the case(United States v. Rippee, 961 F.2d 677), but a short summary: “On January 1, 1991, officers from the National City, Illinois, Police Department stopped Rippee for making an illegal U-turn. The officers let Rippee go without a ticket, however, when he told them he was a United States Marshal on his way to break up a fight at Fannies' Night Club in Brooklyn, Illinois. […] Rippee stipulated that he was not and had never been a United States Marshal.“

How would something like that look like under your proposed system?

Are laws expected to be completely self and cross consistent?

I wanted programmatic law in the past and then after thinking and talking a bit, concluded that self and cross consistency in the law is not considered necessary.

Formalisation can't save you from determining what is and isn't a document. The judges main task is formalising reality and lawd, the rest of the inference is typically easy.

Nobody gets upset, they just think you’re silly. Law simplification is just a classic time waste discussion. But I’ll waste 30 seconds on it for you.

Consider a simple crime, murder. Let’s simplify it to “if you kill someone, that’s murder and you get life”

But then what if I’m being stabbed by the person I kill?

Okay so self defence.

But then what if I say it’s self defence but factually that’s incorrect, but I genuinely believed it was self defence?

What if I’m a soldier and I’m shooting an enemy?

What if I shoot them because they’re raping my child?

What if I’m shooting them because they raped my child ten years ago and I’ve been plotting my revenge ever since?

What if someone said they’ll shoot me if I didn’t shoot them?

What if I was in psychosis and thought they were going to kill me?

What if I thought they were a deer and shot them by mistake while hunting?

It turns out we have all these laws in this particular way because of thousands of years of work dealing with all of these issues.

I'm not upset, but what you're proposing is just stupid. If you think that mathematical formalization is a desirable quality then you clearly don't understand the purpose of having a legal system in the first place.