Modelling the US Constitution to establish constitutional dictatorship Valeria Zahoransky1,2[0000−0002−6304−9720] and Christoph Benzmüller2,3,∗[0000−0002−3392−3093] 1 University of Oxford, Oxford, Great Britain valeria.zahoransky@maths.ox.ac.uk 2 Freie Universität Berlin, Berlin, Germany c.benzmueller@fu-berlin.com 3 University of Luxembourg, Esch-sur-Alzette, Luxembourg Abstract. We present a case example on how to conduct computer aided reasoning on legal texts. The basis is an anecdote of Kurt Gödel’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. Keywords: legal reasoning · US Constitution · higher order logic. 1 Introduction There is an infamous anecdote on how logician Kurt Gödel tried to explain a fault of the US Constitution to the judge hearing him for citizenship. When preparing for the hearing Gödel 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 Gödel’s argument but did grant him the US citizenship. [3,10,12,14]. In the following we shall model an argument for installing lawful dictatorship on the basis of the US Constitution. It is not, however, Gödel’s own argument, but rather one suggested by legal scholar Guerra-Pujol [8]. Gödel’s original argu- ment was not to be found in letters to his mother [6], letters to his colleagues [4] or in character witness Oskar Morgenstern’s account of the hearing [10]. Morgen- stern does mention conversations with Gödel on the alleged fault in the account and his diary but does not go into detail about Gödel’s reasoning [10,11]. ∗ Benzmüller received support by VolkswagenStiftung under grant Consistent Rational Argumentation in Politics (CRAP). Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). 2 V. Zahoransky et al. We will model Guerra-Pujol’s argument with the language of Higher Order Logic (HOL) using Isabelle/HOL [13]. Throughout this paper we will present Isabelle code together with explanations of what the code does. In the following the Constitution and US Constitution shall be used inter- changeably. 2 Developing a model 2.1 On the argument used Below, we outline the argument as provided by [8]. 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 [9]. This is not possible due to the separation of powers as set out in U.S. Const. Art.I-III. In order to allow for this kind of consolidation of powers the Constitution has to be amended in a two-step pro- cess. First, an amendment that changes Art.V has to be introduced and secondly an amendment that actually installs dictatorship by consolidating power 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, §3., 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 suffrage rights would not be constitutional. One can however remove the protection of certain articles from Art.V with a first 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 Modelling the argument On representing time As seen above, we want to represent the changes of the Constitution over different 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 irreflexive and transitive [7]. We shall not require a relation to be transitive, however. Neither will we use modal operators to express that Modelling the US Constitution to establish constitutional dictatorship 3 certain events will always occur in the future or that an event will occur at some point in the future. The same goes for events in the past. We only require an operator X that refers to the immediate successor of an instance of time. The operator is denoted by X for the “x” in “next”. To understand why this is sensible in our case, consider above given table which outlines what we would like to express. Assume that T = {t1 , t2 , t3 } 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 ∈ 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 transi- tivity as requirement for the precedence relation. For a formula ϕ, we would like X ϕ to be valid at point t iff 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 ratified.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 defi- 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 0 a ⇒ σ, rather than just 0 a ⇒ bool. Observe that the quantifiers defined may each only be used for one type of argument. This helps with computation times when using tools like Nitpick [1] and Sledgehammer [2] since Isabelle won’t have to try different types of arguments. 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 [5] a visualisation of the instances with succ as accessibility relation would look as follows: 4 For example Amend.XVII, the prohibition of intoxicating liquors, was repealed by Amend. XXI, §.1 4 V. Zahoransky et al. t1 t2 t3 te Based on succ we can then define X. Lastly, we want to define 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 definitions such as what we mean by dictatorship. A formula shall be locally valid for a specific t if it is valid at that instance of time. Modelling the US Constitution to establish constitutional dictatorship 5 Definitions based on the US Constitution Having laid the technical foun- dations, we provide basic definitions 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 define properties of the Constitution. Above predicates help us define the following time dependant properties that will be used in describing the Constitution’s state: 6 V. Zahoransky et al. 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 simplified version of what Art. V says on the amendment process. omsp Only amendments that maintain suffrage may be proposed. opr Only proposed amendments may be ratified at the next time instance. osr Only if an amendment has the support for ratification, can it be ratified in the future. psr If an amendment is proposed and has the support for ratification, it will be ratified at the next time instance. This will be used to show that an amendment proposed at ti is ratified and thus valid at ti+1 , given that it also has support for ratification at ti . Note that together with opr this makes proposition and ratification of an amendment a two-step process. rv If an amendment is ratified, it is also valid. Here the framework for reason- ing 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 ratification in the preceding instance of time. 3 Reasoning with the model 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 defined above, are valid at t1 . Modelling the US Constitution to establish constitutional dictatorship 7 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’ suffrage 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 suffrage 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 . Amend- ments amd1a and amd1b are both proposed and have support for ratification at t1 , so they may be ratified at the next instance. Observe that all Constitution state properties defined 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 different for each power no dictatorship can be in place at t1 . 8 V. Zahoransky et al. Finally we check whether the axioms so far are even satisfiable by asking Nit- pick to find 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 sufficient to only consider the last model provided. We will present this when checking for satisfiability 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: Modelling the US Constitution to establish constitutional dictatorship 9 ti ti+1 psrti rvti+1 o is prop amd ⇒ is rat amd ⇒ amd sup rat amd psrti rvti+1 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 Pres- ident. 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 10 V. Zahoransky et al. creating inconsistencies due to a missing successor for t3 . bXoprct2 ⇒ boprct3 ⇔ b∀σ ϕ.(¬(is prop ϕ)) → (¬(X(is rat ϕ)))ct3 ⇔ b∀σ ϕ.(X(is rat ϕ)) → (is prop ϕ)ct3 ⇔ ∀ϕ.((X(is rat ϕ))t3 ) → (is prop ϕ)t3 ⇔ ∀ϕ.∀t0 .((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 noDictator- ship t2 and check for satisfiability. 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 satisfiable. For this last instance of time we also give a representation of Nitpick’s satisfying model. Modelling the US Constitution to establish constitutional dictatorship 11 The following satisfying model is the result:5 t1 t2 t3 te is exe P is exe P is exe P is exe P is jud Courts is jud Courts is jud P is jud P is leg Congress is leg Congress is leg P is leg P maint suf amd1a sup prop Congress amd1a is prop amd1a sup rat amd1a is rat amd1a maint suf amd1b sup prop Congress amd1b is prop amd1b sup rat amd1b is rat amd1b ¬ (maint suf amd2) sup prop Congress amd2 is prop amd2 sup rat amd2 is rat amd2 5 This is a heavily truncated presentation of the model provided by Nitpick. The suc- cessor relation’s values are just as defined in “Custom data types and operators”. 12 V. Zahoransky et al. 4 Conclusion 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 Consti- tution. 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 benefit of conducting (1) and (2) is finding out what does not work for the text at hand. Presenting findings 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 first 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 rel- evant to the argument formalized. It was a mere case example. In order to con- duct 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 collabora- tion 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. Modelling the US Constitution to establish constitutional dictatorship 13 References 1. Blanchette, J.C.: Picking Nits–A user’s guide to nitpick for Isabelle/HOL (2019), http://isabelle.in.tum.de/dist/doc/nitpick.pdf 2. Blanchette, J.C., Paulson, L.C.: Hammering away– A user’s guide to Sledge- hammer for Isabelle/HOL (2019), https://isabelle.in.tum.de/dist/doc/ sledgehammer.pdf 3. Dawson, J.W.: Logical dilemmas: The life and work of Kurt Gödel. AK Peters/CRC Press (1997) 4. Feferman, S., Dawson, J.W.J., Goldfarb, W., Parsons, C., Sieg, W. (eds.): Collected Works, vol. 5. Oxford University Press ; Clarendon Press (2003) 5. Garson, J.: Modal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Phi- losophy. Metaphysics Research Lab, Stanford University, fall 2018 edn. (2018) 6. Gödel, K.: Briefe an marianne gödel 1906-1978. https://www.digital. wienbibliothek.at/wbr/nav/classification/2559756 (1906-1978), accessed: 2019-08-20 7. Goranko, V., Galton, A.: Temporal logic. In: Zalta, E.N. (ed.) The Stanford En- cyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2015 edn. (2015) 8. Guerra-Pujol, F.: Gödel’s loophole. Cap. UL Rev. 41, 637 (2013) 9. Levinson, S., Balkin, J.M.: Constitutional dictatorship: Its dangers and its design. Minn. L. Rev. 94, 1789 (2009) 10. Morgenstern, O.: Oskar morgenstern’s account of kurt gödel’s naturalization. Dorothy Morgenstern Thomas collection (1971) 11. Morgenstern, O.: Tagebuch. digitale edition: 1917 bis 1977. http: //gams.uni-graz.at/archive/objects/o:ome.b47-47/methods/sdef: TEI/get?mode=b47-47 (2016), accessed: 2019-08-07 12. Wang, H.: Reflections on Kurt Gödel. MIT Press (1987) 13. Wenzel, M.: The Isabelle/Isar Reference Manual (2019), https://isabelle.in. tum.de/doc/isar-ref.pdf 14. Yourgrau, P.: A world without time: The forgotten legacy of Gödel and Einstein. Basic Books (2006)