{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T10:34:02Z","timestamp":1648982042302},"reference-count":5,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":5763,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1998,6]]},"abstract":"<jats:p>A version of Herbrand's theorem tells us that a universal sentence of a first-order language with at least one constant is satisfiable if and only if the conjunction of all its ground instances is. In general the set of such instances is infinite, and arbitrarily large finite subsets may have to be inspected in order to detect inconsistency. Essentially, the reason that every member of such an infinite set may potentially matter, can be traced back to sentences like<\/jats:p><jats:p>(1) <jats:disp-formula><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" mimetype=\"image\" position=\"float\" xlink:href=\"S0022481200015073_eqnU1.png\" \/><\/jats:disp-formula><\/jats:p><jats:p>Loosely put, such sentences effectively sabotage any attempt to build a model from below in a finite number of steps, since new members of the Herbrand universe are constantly brought to attention. Since they cause an indefinite expansion of the relevant part of the Herbrand universe, such sentences could quite appropriately be called <jats:italic>expanding<\/jats:italic>.<\/jats:p><jats:p>When such sentences are banned, stronger versions of Herbrand's theorem can be stated. Define a clause (disjunction of literals) to be <jats:italic>non-expanding<\/jats:italic> if every non-ground term occurring in a positive literal also occurs (possibly as an embedded subterm) in a negative literal of the same clause. Written as a disjunction of literals, the matrix of (1) clearly fails this criterion. Moreover, say that a <jats:italic>sentence<\/jats:italic> is non-expanding if it is a universal sentence with a quantifier-free matrix that is a conjunction of non-expanding clauses. Such sentences do in a sense never reach out beyond themselves, and the relevant part of the Herbrand universe is therefore drastically reduced.<\/jats:p>","DOI":"10.2307\/2586849","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:01:17Z","timestamp":1146938477000},"page":"555-569","source":"Crossref","is-referenced-by-count":1,"title":["A strong version of Herbrand's theorem for introvert sentences"],"prefix":"10.1017","volume":"63","author":[{"given":"Tore","family":"Langholm","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200015073_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"S0022481200015073_ref004","doi-asserted-by":"publisher","DOI":"10.1145\/151261.151265"},{"key":"S0022481200015073_ref003","first-page":"403","volume-title":"Principles of knowledge representation and reasoning: Proceedings of the third international conference (KR-92)","author":"Givan","year":"1992"},{"key":"S0022481200015073_ref005","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359570"},{"key":"S0022481200015073_ref001","volume-title":"Solvable cases of the decision problem","author":"Ackermann","year":"1954"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200015073","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T12:13:08Z","timestamp":1628597588000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200015073\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,6]]},"references-count":5,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,6]]}},"alternative-id":["S0022481200015073"],"URL":"https:\/\/doi.org\/10.2307\/2586849","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,6]]}}}