Abstract:
For infinite linear spaces, in our previous works, we have shown that theories of figures and subspaces are of high undecidability degree. They allow interpreting elementary arithmetic or second-order arithmetic (for infinite figures). For finite linear spaces, such a claim doesn't hold. It is because we can algorithmically enumerate all finite linear spaces and find all formulas with finite models. So, for finite linear spaces, theories of figures and subspaces are in the class $\Pi_1$. It is the class of problems whose complements are recursively enumerable. In the present paper, we prove that these theories are $\Pi_1$-complete, therefore, they are algorithmically undecidable and not recursively axiomatizable.