igl2020 This project is an extension of igl2020 that implements the following constructs: Arithmetic languages and structures Proof of correctness of these definitions Definability of predicates in arithmetic structures Definability preservation theorem