People always get upset when I propose mathematical formalization of law and using e.g. metamath verifier as a judge.
At least the metamath verifiers will not bend over backwards and come up with absurd inconsistent counterarguments.
It's the most humiliating thing for citizens when the legal cadre of a nation pretends in the national journal that everybody falls for its lies... openly mocking the concept of truth itself with absurdism.
> 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?
> I don’t get upset. I just don’t know what that means.
metamath is an open source formal verification system, the current metamath project (not focussed on law, but mathematics) has roughly 3 parts:
1) the formal verifier (there are multiple re implementations)
2) the databases of axioms (including definitions), theorems and proofs: currently most math is in set.mm the database for set theory (which includes numbers, etc)
3) documentation, among which a thorough book describing how the formal verifier works, the book is creative commons
A proof is basically a series of invocations (by label) of axioms, or previously concluded facts or rules, in the right order so that the verifier comes to the desired conclusion. The algorithm performs all the substitutions and after the last invocation either the string it arrived at matches the proclaimed theorem or it doesn't. Of course it can also error out earlier, say if an invocation to an unknown label happened.
Precisely because natural language is ambiguous, the conversion of our natural laws into formal ones would have to happen under democratic control.
If academic mathematicians want to preserve a human mathematical academy in the face of governments potentially making the future mistake of abolishing mathematical academia, their strong move would be for them to define a "government for and by mathematicians", the database would contain definitions of their choosing, formally regulating how to award public funds into research, formalizing front-running resistant timestamping of work-in-progress etc, so that mathematicians can freely talk and communicate advances ("just wait a sec, let me sync my insights with the network first, ... aaand done, ok now I can speak freely").
Ultimately from a survival perspective, which type of system do we believe to be more robust against corruption and conflicts of interest? one where due process is formally defined in a rigorous manner? or one where those who corrupt the system happen to corrupt it towards actual progress?
Can you walk through the process for the proposed example?
The problem in most suites is checking if a specific act in real life meets some definition of a crime and not figuring out the wording of the law, right?
You kill someone without a reasonable excuse -> You get punished x years for murder
wouldn't really make murder trials easier because you would still have to formalize what you put into the proof.
DoctorOetker · · focus · HN ↗
At least the metamath verifiers will not bend over backwards and come up with absurd inconsistent counterarguments.
It's the most humiliating thing for citizens when the legal cadre of a nation pretends in the national journal that everybody falls for its lies... openly mocking the concept of truth itself with absurdism.
krisoft · · focus · HN ↗
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?
DoctorOetker · · focus · HN ↗
metamath is an open source formal verification system, the current metamath project (not focussed on law, but mathematics) has roughly 3 parts:
1) the formal verifier (there are multiple re implementations)
2) the databases of axioms (including definitions), theorems and proofs: currently most math is in set.mm the database for set theory (which includes numbers, etc)
3) documentation, among which a thorough book describing how the formal verifier works, the book is creative commons
A proof is basically a series of invocations (by label) of axioms, or previously concluded facts or rules, in the right order so that the verifier comes to the desired conclusion. The algorithm performs all the substitutions and after the last invocation either the string it arrived at matches the proclaimed theorem or it doesn't. Of course it can also error out earlier, say if an invocation to an unknown label happened.
Precisely because natural language is ambiguous, the conversion of our natural laws into formal ones would have to happen under democratic control.
If academic mathematicians want to preserve a human mathematical academy in the face of governments potentially making the future mistake of abolishing mathematical academia, their strong move would be for them to define a "government for and by mathematicians", the database would contain definitions of their choosing, formally regulating how to award public funds into research, formalizing front-running resistant timestamping of work-in-progress etc, so that mathematicians can freely talk and communicate advances ("just wait a sec, let me sync my insights with the network first, ... aaand done, ok now I can speak freely").
Ultimately from a survival perspective, which type of system do we believe to be more robust against corruption and conflicts of interest? one where due process is formally defined in a rigorous manner? or one where those who corrupt the system happen to corrupt it towards actual progress?
echoangle · · focus · HN ↗
The problem in most suites is checking if a specific act in real life meets some definition of a crime and not figuring out the wording of the law, right?
You kill someone without a reasonable excuse -> You get punished x years for murder
wouldn't really make murder trials easier because you would still have to formalize what you put into the proof.