In general the law is absolutely not so rigorous. It's more like general philosophical literature in terms of logical rigor--diverse, disjoint, etc. But certain subdomains of the law can be closer to a formal system.
The French tax code is peculiar (though I'm not sure its unique) in literally being defined by the rules encoded in an official program. A recent paper on a new language for compiling those rules, "A Modern Compiler for the French Tax Code" (https://arxiv.org/pdf/2011.07966.pdf, via HN a couple of weeks ago), contains a blurb at the very end,
> Closer to the topic of this paper, the logical structure of the US tax law has been extensively studied by Lawsky [18, 19], pointing out the legal ambiguities in the text of the law that need to be resolved using legal reasoning. She also claims that the tax law drafting style follows default logic [24], a non-monotonic logic that is hard to encode in languages with first-order logic (FOL). This could explain, as M is also based on FOL, the complexity of the DGFiP codebase.
See https://en.wikipedia.org/wiki/Default_logic and https://en.wikipedia.org/wiki/Non-monotonic_logic But note that it's written in that "style", not that it's done consistently or correctly. Unfortunately I couldn't easily find a copy of the cited papers, but I made a note for later reference.
EDIT: I once took a class in law school taught by a Professor of Systems Engineering from the parent university. I forget why, but long ago he took an interest in the rules of evidence in the common law. While the rules evolved organically over more than a thousand years, they actually strongly reflect a formal system of abductive reasoning: https://en.wikipedia.org/wiki/Abductive_reasoning. And there's significant, hidden rigor. In one project he had everyone in class create a tree consisting of evidence (e.g. size 7 shoe) at the leaves, with the branches as inferences all the way up to the top, which was the core legal claim--1) Jim did 2) break and 3) enter into 4) said building.... Anyhow, being a programmer I decided to create my tree using the DOT language and render it using Graphviz. While I was doing that it occurred to me that some of the more esoteric, technical rules of evidence, such as that any piece of evidence can only be used to prove a single element, actually ensures that the tree is an acyclic graph. I'm not sure precisely why (perhaps the professor had more insight), but I believe it's because the rules are in part crafted to ensure that the finder of fact is presented with a tractable problem to solve. The process would get too confusing (and possibly logically inconsistent?) if you didn't keep the tree of evidence and inference simple. No judge or lawmaker likely ever had in mind the literal shape of the evidence tree. In fact, AFAIU nobody thought to represent it as a tree until the late 19th century, when the famous scholar of common law evidence, John Wigmore (https://en.wikipedia.org/wiki/John_Henry_Wigmore), developed a system for analyzing and preparing trial evidence in that manner.
Anyhow, a proper and infinitely more rigorous treatment of this is presented in the book, "Analysis of Evidence, 2nd Ed." by Terence Anderson, David Schum, and William Twining. (Schum taught the class.) A large part of the book explores and explains the law of evidence as a system of Bayesian reasoning. (Oh, that's why! I think Prof. Schum first stumbled into the legal realm after he got the idea of using Bayesian statistics to resolve historically famous and contentious legal trials.)