I'm curious, why have you concluded that it's naive to build a formal model out of a legal document?
I'm not sure about making laws better, but surely a machine can replace lawyers for trivial and well-defined things (where you don't really need a lawyer - and there are a lot of such cases), saving time for a layman person finding appropriate clauses and navigating them while investigating some well-defined (minimally ambiguous and least likely to raise any exceptions) happy paths. Some companies make a lot of money from formalizing tax codes, after all.
To be specific I believe it's naive to think that formally specified laws will be an improvement on the legal system.
I believe laws ultimately are subject to Godel's theorem. They can either be complete or consistent, but not both (and likely neither). We should recognize the difference. A complete legal system can render a verdict in every case. A consistent legal system has no contradictions. We prioritize the former.
What would it look like for a case to be presented to a judge and for them to respond, "We simply cannot determine if this is legal or not." What would you even do in such a scenario? Rather, we have judges render decisions and deal with the consequences that they are inconsistent and we have further cases to untangle those inconsistencies, in an ever growing patchwork of legal epicycles.
I'm not sure I agree with the idea of us prioritizing completeness. I don't think the laws can or need to cover any possible life situation. I mean, there aren't any laws about whenever someone can or cannot wave a toy chainsaw or whenever guests of the Oval Office must wear a costume. We just look at this, make our opinions, but when we need to make a legal one we check out that laws say nothing on the matter, then dismiss it as "nothing against the law" (of course, we can always make or amend the new laws if we think we need some).
I'm not a lawyer, but from my crude understanding I believe it's rather the norm for the laws to be incomplete and have intentional ambiguity so the lawmakers aren't spending their time down the rabbit hole of determining the theory of truth (which they cannot do, if Godel's theorem is applicable - I'm not entirely sure because laws are not really self-defining and we don't have or need it to be a closed system with its own set of axioms and stuff - that'd probably mess up the reasons we have laws), but rather write something that works for the majority of their intent, and leave the edge cases to whoever hits them and goes to the court or legislators. I'd say the whole legal system is deliberately designed to "crash" at an undefined behavior at any time and require a human in the loop to look at it.
So I suspect that consistency makes more sense for a legal system than completeness. We probably want rule of the law to be universal and fair (and thus, more consistent) than complete, because no one needs a law to describe every single life situation. People don't normally think of such law (save for thought experiments), and it would probably violate Kant's categorical imperative (as we'll all become just the means for such law) to design it so. I could argue that it's because life changes with every passing moment, with someone doing something novel and never done before.
I hope I understood you correctly (my apologies if I didn't get something right), and my arguments here make sense.
I want to clarify that I'm considering the legal system as a whole. When I say completeness I'm referring to the legal system's ability to render a judgement: is something legal or illegal? That's different than having a law for every case. We can have ambiguous laws and still have a judge say that something is legal or illegal.
What we don't have or can't have is a court case where the judge says, "The legality of this is indeterminate." Our ability to always render a judgement is completeness.
Hm. I was also thinking about the whole system, and I'm really not sure why a legal system needs to be able to answer such questions.
> What we don't have or can't have is a court case where the judge says, "The legality of this is indeterminate."
Why not? In reality judges can say "the legality of this is not for this court to decide" after all, can't they? And while (IIRC) the Supreme Court must use the law to establish new law, even then they can say "the law says nothing about this - go bug the legislative, not judicial". And then the legislative doesn't really need to use the existing law itself to codify new laws (as I get it, they can even pass laws that contradict the Constitution - it'll be up to the judicial to strike them down as such).
The way I understand how things are in real world, a legal system should be able to state if something is illegal, but it has no need to be able to universally state whenever something is legal or (and doesn't normally do so, save for doing it as a way to make exceptions from broader rules) or not. Kinda like how criminal law decrees one as "guilty" (proven to have done something illegal) or "not guilty" (not proven to have done something illegal) but never declares one innocent (and it doesn't need to - it works without it). Maybe this is where I'm possibly getting confused?
Can you please help me understand why do you think a legal system needs to be able to always answer that legality question, and particularly what's the use case for it (what does such property tries to achieve in practice)?
I'm not sure about making laws better, but surely a machine can replace lawyers for trivial and well-defined things (where you don't really need a lawyer - and there are a lot of such cases), saving time for a layman person finding appropriate clauses and navigating them while investigating some well-defined (minimally ambiguous and least likely to raise any exceptions) happy paths. Some companies make a lot of money from formalizing tax codes, after all.