With all due respect, @Bumble (and all your voters), I find your answer radically wrong by multiple reasons.
From here on, I use the term formalism meaning formal expression, not as in QM, where the term implies a theoretical and philosophical account. From here on, I address the OP.
To start, logic is already expressed as a formal system (formal means founded on axioms/concepts with inferred theorems, using a formal language). The system of legal rules in books has not funny symbols like
/iif, but it has exactly the same --and perhaps more appropriate-- relational elements between objects.
Perhaps you assume logic will provide a formality to law if it is expressed with FOL: wrong. Logic is already a formalism. A formalism is essentially something written with logical consistency. The informal expression of law is morals. You might think morals and laws are different in content, yes, that's true, but that is for pragmatic reasons. Laws tend to be equivalent to morals, but the process of formalizing morals is quite complex and subject to human errors and interests. Morals are the informal rules, law is the formal expression of morals.
Following, the legal formalism is not founded on logic (the formalism) but on the reason (the actual tool, the dynamics of thinking):
F(Law) ⊆ Reason
Switching to an alternative formalism, which depends on ANOTHER formalism (logic) implies introducing multiple complexities that I will discuss at the end, on my answer:
F(Law) ⊆ F(Logic) ⊆ Reason
Following, the obstacle is far from being what is presented as problematic in the answer:
Statutes inevitably rely on background knowledge of legal terminology, principles and practice.
That is not a problem. All language is based on "background knowledge of [
legal LIFE] terminology, principles and practice". The application of propositional logic already implies a dependency on such background. This is not a problem of expressing law with logic, this is a problem of semantics.
My company once bought 70 printers that powered on at the tenth click of the ON button, and the contract didn't mentioned that, which is normal, nobody expects a statement about the "ON" button. Our lawyer said "sorry, contracts can't and don't describe all default facts" (yes, they tried to sell us refurbished material as new). We've got the money back, but not due to the contract: because it is a default fact of life: having a button implies pressing ONCE, not ten times. That's not a legal issue. That's a pure semantics problem, which was solved not by the lawyer, but by an IT guy.
Statutes can never cover all possible cases that might arise. This is why courts have to interpret the law. Typically within a few years of a new statute being passed a body of supporting case law will arise.
This is the same case, for a similar issue: all laws having the form
forall x, x is A (e.g. all people having an income is subject to pay taxes). The problem is not logic, it is semantics.
Some parts of the statute were difficult to interpret, e.g. it contained counterfactual conditionals, which are notoriously difficult to evaluate.
Again, a problem of semantics. And if the statement is difficult to interpret, the problem is hermeneutics, not the use of logic.
The law required reasoning about events and times, so it needed a temporal logic.
This is not a problem of the application of logic to law. It is the natural consequence of any formalism: expressing empirical facts with a formal notation implies introducing dimensional resources that propagate to all result.
Some of the reasoning is of a default nature, which required a logic that is non-monotonic and non-classical.
This occurs not only in the case of laws, not even in any discipline, but in any possible rational judgement. All words in a dictionary are circular definitions. Their meaning comes from life experience. So, ALL terms used in traditional law or law expressed in FOL involve a lot of by default meaning.
The law permits the appropriate authority, the Home Secretary, to waive requirements.
In addition to by default hermeneutics, all logic, not only legal logic, is always applied in a context of conditions which include culture, tradition, morals, religion, beliefs, etc. This is not a problem of logic, but a problem of law.
Under some circumstances, the law can have retroactive effects, which leads to very weird situations in which some proposition is true at a time t, but from a later perspective was not true at time t.
This is exactly the previous case.
Now, my answer
Since law is already a formal system without funny symbols, I assume the question goes in the direction of expressing law using some sectorial formalism as first order logic.
Let's start with the problem of deepness, using simple FOL: to what extent of depth should law be expressed? In order to express the rule "all (P)eople getting an (I)ncome and is not payin(G) taxes should pay (T) them" we can use:
∀x(I(x) → T(x))
∀x(P(x) ∧ ∃y(I(x, y) ∧ ¬G(x) → T(x)))
Sorry if any mistakes. Consider that:
- Case-1: the lesser the depth, the simplest the logical understanding and the heavier the semantics loads associated to each object, which implies an open and subjective interpretation.
- Case-2: the deeper the target, the lighter the semantic load associated with each term, while there is the need of a more strict and rigid / precise definition of the object.
The actual case, I mean, how law is expressed currently, corresponds to Case-1. Almost all laws can be expressed as
A(x), which leaves to the legal domain the hermeneutics about the objects and properties,
In addition, such case, actually being applied, is another proof that law is already a formal system.
Your question suggests to switch to Case-2, which would imply (1) a huge effort (decades, probably) on finding precise object definitions and properties, and all such effort for what? Just (2) to express laws as extremely complex equations, only machines and experts would understand. This raises a new issue (3), which could be positive: in the process, such analysis and definition of rules would allow finding logical inconsistencies, and fixing them... implies changing the actual laws!
The marks (1) and (2) show the two NEGATIVE key points that emerge if legal rules are expressed using some type of logical formalism which is not the current one. The point (6) marks a POSITIVE aspect, while there are more.
So, my direct answer to can law be expressed using some sectorial formalism of logic? is yes, considering this pros and cons:
- A gigantic measure of complexity and effort to find precise definitions about objects and relations. Some terms that are generic and subject to open interpretation should be replaced by subclasses, according to strict taxonomies.
- A lot of complexity in writing/expressing and reading/interpreting the rules. Now, lawyers should not only need years to study laws, but years to study the actual discipline that allows using the rules in court.
- Applying law would not really be a matter of invoking rules, but to accept and verify that empirical facts correspond to legal objects (e.g. do you fulfill the conditions to be accepted as a (P)erson? who is not (D)educing your (T)axes? Are the 72 proofs provided valid?)
- While perhaps more precise, legal services would be extremely costly to the citizen.
- Such actual implementation would not prevent skipping the law, just by not marking a checkbox in a filling form, and perhaps would simplify finding and exploiting legal holes.
- Detecting inconsistencies in actual laws, which implies noticing and fixing them (changing current laws).
- Trials would be simpler, online, lawyers would just introduce the facts as standard objects, and would invoke a law by its identifier. The judge application, equivalent to a PROLOG prompt, would just accept the objects and instantly compute the result and the sentence. Perhaps trials will disappear as such to become mobile phone applications where we just receive punishments sent by some computer server, which might replace the Judicial Power of the State.
All of this, considering that I've never been in court, don't know many lawyers, and spend my time walking without direction. Lawyers would surely find many more issues when introducing an additional formalism to law. Perhaps you should ask this in https://law.stackexchange.com/ including the link of this discussion, in order to find more legal perspectives, which might be quite interesting.