What measures 'real'? — Isaac
That question translates into: How much of a fragment of the system is sufficient to still achieve the goal of adjudicating the question of
halal (permissible) versus
haram (impermissible) behaviour?
Unfortunately, the exercise has never been done with Jewish or Islamic law. It would require a complete encoding of their foundational rules in an executable version of the language of first-order logic. This is considered "hard work":
What is Coq? Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
It is considered much "harder" than encoding the basic rules in traditional
prenex normal form. Prenex is unfortunately not unambiguous enough to successfully achieve machine-mechanical verifiability.
This exercise has been done, however, with the theory of arithmetic (which is simpler). The default, standard theory is Dedekind-Peano, while several simplified theories of arithmetic have been tested for their system-level properties, such as,
Presburger,
Skolem, and
Robinson. The exercise was systematized into the
Z2 second-order theory of arithmetic by David Hilbert.
The Koreans have sponsored the entire encoding of Z2 (and its main subsystems) in Coq. It was undoubtedly a costly affair.
If I could find sufficient funding to do this for Jewish law and/or Islamic law, I would certainly want to work on the project, and hire a team to try to pull it off. It is a "hard" project, because successfully encoding theory of arithmetic was already a feat.
Even if you had your stupid machine someone would still have to program it and you'd still have to decide whether to trust this programmer or that one, each time they delivered an edict. — Isaac
A machine is a program, and a program is a machine. In this context, the term "machine" does not mean hardware. It probably means the Coq or
Isabelle proof assistants. Coq is spearheaded by a French team and Isabelle by a German team. In my impression, Coq has gained more traction than Isabelle, but that situation could still end up reversed in the future.
The profile for this kind of work is not really a programmer but a mathematician. Still, this person must be able to handle machine-verifiable formalisms, which are notoriously harder than standard prenex. Furthermore, unlike what you may expect, the scripts are not 100% declarative. The proof verification tactics have important imperative aspects. So, he will end up doing some programming too. In that sense, these scripts are not pure math either.
Yes it does, the device in question is a brain. — Isaac
No, no, no. Atheism is system-less bullshit. There is simply nothing to encode in a proof assistant. So, what brain would you need for atheism? What skills? Atheism is stuff for idiots. Either you reason within a system, or else about a system, because in all other cases, you are doing system-less bullshit.
How do you know the other systems have worked out the complete implications of what they say? — Isaac
Theory of arithmetic has important system-wide, emergent properties. Theory of logic too. You can check e.g. the
Hilbert-Ackermann calculi for that.
For example, Dedekind-Peano (=standard arithmetic) is semantically complete, syntactically incomplete, and system-wide consistent (according to Gentzen's proof).
It is not sure what the "complete implications" would mean as a system-wide property.
For example, statements in arithmetic are recursively enumerable at or below the maximum treshold
in the
arithmetic hierarchy. If the set of such statements is not even recursively enumerable (=above treshold), then their "complete implications" cannot be determined (meaning: the list of all statements provable in that system). There will simply be no algorithm possible to traverse that set.
Religious law is a rigorous axiomatic system which rests on a finitary number of basic beliefs. Still, it may take even more work than for arithmetic theory or logic theory to uncover its formal system properties. But then again, that looks like an interesting challenge to me.