We prove that Wilkie's identity holds in those natural HSI-algebras where each element has finite decomposition into components.Further, we construct a bunch of HSI-algebras that satisfy all the identities of the set of positive integers ℕ. Then, based on the constructed algebras, we prove that the identities of ℕ hold in the HSI-algebra of finite posets when the value of each variable is a poset having an isolated point.

We give a general method for constructing lattices L whose equational theories are inherently nonfinitely based. This means that the equational class generated by L is locally finite and that L belongs to no locally finite finitely axiomatizable equational class. We also provide an example of a lattice which fails to be inherently nonfinitely based but whose equational theory is not finitely axiomatizable.

Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of arithmetic expressions using a constant for the number one and the operations of product and exponentiation is affirmative, and the complete equational theory also characterises isomorphism in the typed lambda calculus, where the constant for one and the operations of product and exponentiation respectively correspond to the unit type and (...) the product and arrow type constructors. This paper studies isomorphisms in typed lambda calculi with empty and sum types from this viewpoint. Our main contribution is to show that a family of so-called Wilkie–Gurevič identities, that plays a pivotal role in the study of Tarski’s high school algebra problem, arises from type-theoretic isomorphisms. We thus close an open problem by establishing that the theory of type isomorphisms in the presence of product, arrow, and sum types is not finitely axiomatisable. Further, we observe that for type theories with arrow, empty and sum types the correspondence between isomorphism and arithmetic equality generally breaks down, but that it still holds in some particular cases including that of type isomorphism with the empty type and equality with zero. (shrink)

All arithmetical identities involving 1, addition, multiplication and exponentiation are valid in every 2-element HSI-algebra.

All arithmetical identities involving 1, addition, multiplication and exponentiation will be true in a 2-element model of Tarski's system if a certain sequence of natural numbers is not bounded. That sequence can be bounded only if the set of Fermat's prime numbers is finite.