We present a case example on how to conduct computer aided reasoning on legal texts. The basis is an anecdote of Kurt Godel's citizenship hearing in which he claimed that the US Constitution allowed for the erection of a dictatorship. We shall model relevant parts of the US Constitution and conduct reasoning on them. This is done using the language of classical Higher Order Logic (HOL) and proof assistant Isabelle/HOL.
There is an infamous anecdote on how logician Kurt Godel tried to explain a
fault of the US Constitution to the judge hearing him for citizenship. When
preparing for the hearing Godel found that the US Constitution allowed for the
introduction of a constitutional dictatorship. He set out to explain this to the
judge once the discussion turned towards the governmental system of the United
States. The judge was not interested in hearing Godel's argument but did grant
him the US citizenship. [
In the following we shall model an argument for installing lawful dictatorship
on the basis of the US Constitution. It is not, however, Godel's own argument,
but rather one suggested by legal scholar Guerra-Pujol [
We will model Guerra-Pujol's argument with the language of Higher Order
Logic (HOL) using Isabelle/HOL [
In the following the Constitution and US Constitution shall be used interchangeably. 2 2.1
Below, we outline the argument as provided by [
The constitution does not allow for the direct installation of a dictatorship,
since dictatorship requires the consolidation of legislative, executive and judicial
powers in one person or institution [
Art.V needs to be amended since it regulates the amendment process and protects some articles from being amended altogether, such as U.S. Const. Art.I, x3., cl.1. and U.S. Const. Amend.XXVII which ensure that each state has two votes in Senate. Directly introducing an amendment that would abolish the distribution of powers and thus strip the states of their su rage rights would not be constitutional. One can however remove the protection of certain articles from Art.V with a rst amendment, amd1, and then introduce dictatorship with a second amendment, amd2. This is constitutional since Art.V does not protect itself.
Consequently, the outline for our model is as follows: time instance t1 t2 t3 Constitution state Current Constitu- Constitution of t1 Constitution of t2 tion + amd1 + amd2 Distribution of Distribution of No distribution of powers powers powers No dictatorship No dictatorship Dictatorship
Proposal of amd1 Proposal of amd2 2.2
On representing time As seen above, we want to represent the changes of the Constitution over di erent instances of time.
We choose to do this via temporal logic. Generally, such a logic would be
expressed by a set T of instances of time and a precedence relation on T T ,
such that is both irre exive and transitive [
To understand why this is sensible in our case, consider above given table which outlines what we would like to express. Assume that T = ft1; t2; t3g and t1 t2,t2 t3 and ti 6 tj for all other combinations of ti and tj in T :
The basis for changes in t2 is set out with amd1 at t1. Likewise the basis for changes in t3 is set out with amd2 at t2. At each ti 2 T the furthest we look into the future is the immediate successor, thus we do not need to be transitive.
In addition to it not being necessary, there is another reason to omit transitivity as requirement for the precedence relation. For a formula ', we would like X ' to be valid at point t i for any t0, s.t. t t0, holds: ' is valid at t0. If were transitive, then X ' would not mean \' is valid at the next instance after t", but \' is valid at all instances after t". If not used very carefully, this could easily lead to inconsistencies. After all, amendments do not necessarily stay valid once rati ed.4 Since we do not need a transitive relation , it is advisable to avoid it altogether.
Custom data types and operators See the following code snippet for de nitions of basic data types and operators that we will use to reason about the US Constitution.
There are two data types g and time and one derived data type . The operators thopi are time dependant versions of operators hopi.
Type g represents the governmental institutions Congress , P(resident) and Courts. The legislative, executive and judicial powers shall later be bestowed upon these three institutions.
There are four instances of time: t1-t3 as above and te, the instance that marks the end of time. We need te to avoid inconsistencies in connection with X. We shall point out where it is necessary when it becomes relevant below.
Since we will only consider a formula's validity at a certain point in time we need time dependant type for them, as well as operators lifted to that type, i.e. of type 0a ) , rather than just 0a ) bool.
Observe that the quanti ers de ned may each only be used for one type
of argument. This helps with computation times when using tools like Nitpick
[
We also introduce operator X. This requires a precedence relation. To stress
the fact that we are talking about a future instance of time when using X we call
the relation succ for successor, rather than pred for predecessor. So in Kripke
semantics [
Lastly, we want to de ne a notion of validity. We distinguish between global and local validity.
A formula shall be globally valid when it is valid independently of the current time. This is useful for universally valid de nitions such as what we mean by dictatorship. A formula shall be locally valid for a speci c t if it is valid at that instance of time. De nitions based on the US Constitution Having laid the technical foundations, we provide basic de nitions with respect to the Constitution.
We introduce a predicate that expresses whether or not g is a certain branch of government. We require each of the branches to be unique, i.e. each branch has to have a unique governmental institution associated with it. Otherwise, the fact that for example Congress is legislative would not imply that P isn't which would make for an unnecessarily complex model.
There is a dictatorship at t if at that instance of time a dictator d exists that represents all branches of government.
Below follow some predicates for formulas ' :: . With these we will de ne properties of the Constitution.
Above predicates help us de ne the following time dependant properties that will be used in describing the Constitution's state: oap Only amendments may be proposed. This time dependant formula is used for technical reasons. It helps to distinguish between generic formulas ' of type and what we call amendments. For example oap itself may not be proposed if it isn't also declared an amendment. osp Only if an amendment has the support of the legislative, can it be proposed.
This is a simpli ed version of what Art. V says on the amendment process. omsp Only amendments that maintain su rage may be proposed. opr Only proposed amendments may be rati ed at the next time instance. osr Only if an amendment has the support for rati cation, can it be rati ed in the future. psr If an amendment is proposed and has the support for rati cation, it will be rati ed at the next time instance. This will be used to show that an amendment proposed at ti is rati ed and thus valid at ti+1, given that it also has support for rati cation at ti. Note that together with opr this makes proposition and rati cation of an amendment a two-step process. rv If an amendment is rati ed, it is also valid. Here the framework for reasoning about amendments is entwined with the content of the amendments. In combination with psr this property is a precarious one to work with for, as soon as rv is declared to be valid for some t, it will be possible to prove anything as long as it has been proposed with support for rati cation in the preceding instance of time. 3
We shall now look into the Constitution's states at instances t1, t2 and t3 by stating axioms and proving properties based on them.
Instance t1 First we state a few axioms and then give two suggestions of what amd1 might look like. Observe that all of the properties describing an instance of time, as de ned above, are valid at t1. Neither amd1a nor amd1b are optimal solutions. Indeed, there is no optimal solution for the presented framework.
This is because what we want amd1 to say is that it is not necessary for all proposed amendments to maintain all states' su rage in Senate. In other words we want condition omsp to be omitted at t2. This, however, is not the same as requiring the amendment to be the negation of omsp as amd1a does. The negation would require at least one ' :: to expressly not maintain su rage rights for some state and be proposed. Yet, it were acceptable both if such a ' existed and if it didn't. We do not want to demand such a ' into existence.
One could therefore choose to use amd1b that states a proposed ' may either satisfy the maint suf condition or it may not. Unfortunately, this is a tautology.
Although the suggested amendments do not constitute ideal amendments for the desired outcome, we shall still use them. They help to illustrate how one can reason about amendments within this framework.
Next there are a few axioms that pave the way for the state at t2. Amendments amd1a and amd1b are both proposed and have support for rati cation at t1, so they may be rati ed at the next instance.
Observe that all Constitution state properties de ned above are valid next time, except for omsp. This is to ensure that we can introduce an amendment at t2 that does not satisfy maint suf.
In a way the amendment to Art. V is implemented by simply not using bX omspct1 as axiom, rather than by working with one of the above suggested amendments amd1a and amd1b.
Using the axioms provided above, we shall prove that there is no dictatorship at t1. This requires the proof of facts only g power t1 meaning that g is the only governmental institution with (legislative, executive, judicial) power at t1. Since g is di erent for each power no dictatorship can be in place at t1.
Finally we check whether the axioms so far are even satis able by asking Nitpick to nd a satisfying model for True. Note that we will repeat this test for time instances t2 and t3. Since we only ever add axioms and don't remove any, proceeding from one time instance to the next, it is su cient to only consider the last model provided. We will present this when checking for satis ability at t3.
Instance t2 For t2 we do not need to provide as many axioms as for t1 since we can deduce bhpropertyict2 from axiom bXhpropertyict1 .
Below are proofs for the amendments proposed previously. The outline for a validity proof where an amendment amd is concerned is as follows: ti psrti is prop amd sup rat amd ti+1 rvti+1 o p)srti is rat amd rv)ti+1 amd This is exactly what we do with amd1a.
See below that we can prove bamd1bct2 with or without these axioms since amd1b is a tautology. Indeed, we can also show amd1b's validity for t1 and its global validity. This is not possible with amd1a.
Now we introduce amd2 which will transfer all governmental power to the President. Also, we set the stage for t3 with relevant axioms. As with t2 we keep all time dependant conditions except for omsp.
When introducing time instances we mentioned that we needed te for technical reasons. This is because we want to use above given axiom bXoprct2 without creating inconsistencies due to a missing successor for t3.
bXoprct2 ) boprct3 , b8 ':(:(is prop ')) ! (:(X(is rat ')))ct3 , b8 ':(X(is rat ')) ! (is prop ')ct3 , 8':((X(is rat '))t3) ! (is prop ')t3 , 8':8t0:((succt3 t0) ! (is rat ')t0) ! (is prop ')t3 If t3 does not have a successor (succt3 t0) will always be false, making (succt3 t0) ! (is rat ')t0 always true which it shouldn't be. As soon as term (is prop ')t3 is not true for some ', axiom bXoprct2 will cause an inconsistency.
We therefore want t3 to have a successor. In order to avoid circular succession we introduce dummy instance te.
Analogously to t1, we prove properties only g power t2 to prove noDictatorship t2 and check for satis ability.
Instance t3 The remainder of this section is rather simple. We prove properties for new time instance t3 using previously provided axioms X property t2. We then proceed to show that amd2 is valid with the reasoning given above and use it to prove that there is now a dictatorship.
As before we check that our axioms are satis able. For this last instance of time we also give a representation of Nitpick's satisfying model. The following satisfying model is the result:5
t1 5This is a heavily truncated presentation of the model provided by Nitpick. The successor relation's values are just as de ned in \Custom data types and operators".
In the course of this work we have explored an argument on how to introduce a dictatorship in the USA without violating the rules laid out in the US Constitution. We did so using proof assistant Isabelle/HOL.
It is an example on how to conduct legal reasoning with the aid of a computer. In this case, there were four main tasks involved: (1) Determining which aspects of the text are relevant. (2) Deciding on a suitable way to represent these concepts in higher order logic. (3) Translating the concepts modelled with HOL to the computer. (4) Conduct reasoning based on the model.
We mainly focused on presenting (3) and (4) in this work since the products of these steps are, by nature, presentable. One can simply provide code. A large part of the bene t of conducting (1) and (2) is nding out what does not work for the text at hand. Presenting ndings of this kind would have gone beyond the scope of this paper. That is not to say, however, that they aren't of interest. This brings us to potential further tasks.
The rst would be to extend the discussion of a text's modelling to the points that may be considered but that turn out to be unsuitable. This would help others doing similar work. We did this to some degree when explaining about e.g. the necessity of te or discussing a suitable representation of amd1 but many other points could have been mentioned here.
Furthermore, this work only dealt with the contents of the Constitution relevant to the argument formalized. It was a mere case example. In order to conduct general legal reasoning with respect to the US Constitution it is necessary to analyse and represent more of its contents, rather than just one small part.
Lastly, when it comes to formalizing legal concepts in general the collaboration of logicians and legal scholars is essential to achieve better results. Given that the problems presented above are in nature interdisciplinary they should also be solved in an interdisciplinary context.