A finite analog to the Löwenheim-Skolem theorem (Q1338480)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A finite analog to the Löwenheim-Skolem theorem |
scientific article |
Statements
A finite analog to the Löwenheim-Skolem theorem (English)
0 references
27 August 1995
0 references
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''.
0 references
Buridan-Volpin model
0 references
location sensitive interpretation
0 references
deductive system
0 references
Gentzen's LK without the contraction rules
0 references