Encoding the US Government

1. The three distinct branches of government are the president, congress, and the supreme court.
2. A federal law is either an executive order or legislation.
3. Executive orders are created by the president, legislation is created by congress
4. Theorem: The supreme court does not create federal_laws.
5. The supreme court can veto a law (technically, "strike it down") iff the majority (at least 5 of the 9 members) agree.
6. Theorem: No law has been vetoed by the supreme court when less than 5 members were in favour.
7. Legislation is enacted iff it is created by congress, the supreme court has not vetoed the legislation, and either (i) the president has not vetoed the legislation and has signed it, xor (ii) the president has vetoed the legislation and congress has overridden the veto.
8. Theorem: No enacted legislation has been vetoed by the president and not overridden by congress.
9. Executive orders are enacted iff they are created by the president, have not been overridden by congress, and have not been vetoed by the supreme court.
10. Every law (federal laws and state laws) has exactly one topic. Abortion, immigration, and gun control are different law topics.
11. The Immigration and Nationality Act of 1952 is federal legislation about immigration
12. Executive Order 9066 is about immigration
13. The Gun Control Act of 1968 is federal legislation about gun control
14. Executive order 14076 is about abortion
15. All federal laws in existence has been enacted
16. All executive orders have been signed by the president
17. Theorem: All enacted legislation and executive orders have been vetoed by the president or have been signed.
18. Theorem: There is some executive order that was not vetoed by the supreme court.
19. Only 3 members of the supreme court voted to strike down Executive Order 9066.
20. Theorem: Executive Order 9066 was not vetoed by the supreme court.
21. Congress has the power to impeach the president. If there is a majority vote in favour, the president is removed from office.
22. Andrew Johnson, Bill Clinton, and Donald Trump were the only three presidents to be impeached, and none were removed.
23. Theorem: Congress did not have a majority to impeach and remove Trump.
24. Theorem: No president has been impeached and removed.
25. Florida and Texas are different states
26. The Florida state law HB1589 is about immigration
27. The Immigration and Nationality Act of 1952 and Florida state law HB1589 do not conflict
28. The Texas senate bill 4 is about immigration
29. The Texas License to Carry Act of 2021 is about gun control
30. The Gun Control Act of 1968 conflicts with the Texas License to Carry Act of 2021
31. Theorem: There are two different states with laws about the same topic.
32. A federal law and state law can conflict only if they are on the same topic.
33. If a federal law and state law conflict then the federal law supercedes.
34. Theorem: The Immigration and Nationality Act of 1952 does not conflict with the Texas License to Carry Act of 2021.
35. Theorem: There is federal legislation that supercedes the Texas 2021 LTC law.

You must ...

• Formulate the types, axioms, and theorems in TPTP TFF syntax. For numbers 5 and 6 that involve arithmetic, you'll need to use the TPTP arithmetic system, and use Vampire to do proofs.
• Ensure that the axioms are consistent using an ATP system. You'll need to comment out axioms that involve arithmetic.
• Prove the theorems using an ATP system.

Answers

• Answer