Authors - Phillip G. Bradford, Henry Orphys, Dmitry Udler, Nadia Udler Abstract - This paper discusses a bi-modal AI system applied to legal reasoning for tax law. The results given here are very general and they apply to similar systems beyond tax law. These results use the downward and upward L¨owenheim–Skolem theorems to contrast the two modalities of this AI approach to tax law. One modality focuses on the syntax of proofs and the other focuses on logical semantics. Particularly, one modality uses a rule-based theorem-proving system to perform legal reasoning. The objective of this theorem-proving system is to provide proofs as evidence of valid legal reasoning. These proofs are syntactic structures that can be presented in court. The second modality uses large language models (LLMs). An objective of our application of LLMs is to enhance and simplify user input and output for the theorem-proving system. In addition, the LLMs may help in the translation of the natural language tax law into logic for the theorem proving system. The combination of these two modalities empowers our vision. The LLMs leverage notions of semantics for tax law inputs and they may help translate tax law statutes. While the theorem proving system gives syntactic proof-trees for legal arguments for potential justifications of tax statements.
