1
$\begingroup$

I am really interested in exploring if (legal) laws can be proven to be self-consistent using a formal programming language / proof assistant, and modeling the laws using category theory, perhaps David I. Spivak’s “Categorical Query Language”, or a “process algebra” language like TLA+.

Could anyone please give me a primer on that or refer me to more relevant ideas in research?

(“Purposive law” comes in as the idea that laws could somehow be evaluated as achieving a purpose, not a declaration of what is or is not allowed, by what the intended outcome is.)

Thank you very much.

https://dblp.org/pid/59/5301.html

https://iecscience.org/uploads/jpapers/202102/sXyiWTBC21PLv0RLjTbKS3vuHTzTcVttiy1rKHpB.pdf

https://inria.hal.science/hal-03159939/file/paper.pdf

Improve this question
$\endgroup$
5
  • $\begingroup$ Possible overlap with ai.stackexchange.com/questions/5652/… $\endgroup$
    – Bruce Adams
    Commented Jun 18, 2023 at 20:44
  • 3
    $\begingroup$ I believe catala-lang.org does what you're asking for to the extent possible... $\endgroup$
    – Alex Chichigin
    Commented Jun 20, 2023 at 7:07
  • 1
    $\begingroup$ @AlexChichigin: you could publish your comment as an answer. $\endgroup$
    – Andrej Bauer
    Commented Jun 20, 2023 at 9:02
  • $\begingroup$ It could be fascinating to write a political constitution as an ontology log (olog) - a category-theoretic model of human “nature”, “needs”, “rights” or “rules”, logically determined to lack inconsistency. Gödel reportedly said he found an inconsistency in the US Constitution once. $\endgroup$
    – Julius Hamilton
    Commented Jun 24, 2023 at 7:40
  • $\begingroup$ The title of your question reads like you're asking about a formal proof of some particular law (a theorem) as in "formal proof of the law of excluded middle". I suggest reformulating it. $\endgroup$
    – Alex Chichigin
    Commented Jun 26, 2023 at 15:46

1 Answer 1

Reset to default
4
$\begingroup$

As a preamble, let me point out that complete (logical) formalization of a legal system is a very long-standing dream. Back in 1987 at the first international conference on Artificial intelligence and law there was a paper on this topic.

We all know such attempts didn't quite land for various reasons. One of the conceptual ones is that no legal system is complete and set in stone: we constantly get new legislations as we go, and resolve holes and clashes in old ones as we discover them. Thus a legal system is always self-contradictory but routinely resolves these contradictions. While we claim that we invented Agile processes, huh? Anyway, most formal logics can't handle contradictions...

That being said, I think the most modern and probably most successful attempt at formalizing and mechanizing (part of) a legal system is Catala language.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.