A finite analog to the Löwenheim-Skolem theorem (Q1338480)

The author presents an interpretation of formulas that depends, not only on the formulas itself, but also on their position in the given (formal) deduction. Thus he associates with a deduction a Buridan-Volpin structure, which consists of the domain \(D\) (of discourse), relations and functions on \(D\), and a function \(r\) that specifies subsets of \(D\) as ranges of variables occurring in the deduction. Of course, the function \(r\) cannot be arbitrary to retain soundness, etc., and the author provides many definitions and much machinery (and examples) to make a coherent setting. He shows that, in the deductive system that is, roughly, Gentzen's LK without the contraction rules, each range \(r(x)\) can be required to be finite. This has ``some curious consequences'', as he points out. For instance, a theorem in set theory ``has an equivalent form which has finite BV model''.