As is well-known, the Bernays-Schonfinkel-Ramsey class of all prenex there exists *for all* V-sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are is an element of and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach the remaining part of the decidability result being postponed to a forthcoming paper.
The Bernays Schoenfinkel Ramsey class for set theory: semidecidability
POLICRITI, Alberto
2010-01-01
Abstract
As is well-known, the Bernays-Schonfinkel-Ramsey class of all prenex there exists *for all* V-sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are is an element of and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach the remaining part of the decidability result being postponed to a forthcoming paper.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
