{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T21:01:22Z","timestamp":1770411682934,"version":"3.49.0"},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4940,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2000,9]]},"abstract":"<jats:p>The completeness proof for first-order logic by Rasiowa and Sikorski [13] is a simplification of Henkin's proof [7] in that it avoids the addition of infinitely many new individual constants. Instead they show that each consistent set of formulae can be extended to a maximally consistent set, satisfying the following existence property: if it contains (\u2203<jats:italic>x<\/jats:italic>)<jats:italic>\u03d5<\/jats:italic>it also contains some substitution<jats:italic>\u03d5<\/jats:italic>(<jats:italic>y<\/jats:italic>\/<jats:italic>x<\/jats:italic>) of a variable<jats:italic>y<\/jats:italic>for<jats:italic>x<\/jats:italic>. In Feferman's review [5] of [13], an improvement, due to Tarski, is given by which the proof gets a simple algebraic form.<\/jats:p><jats:p>Sambin [16] used the same method in the setting of formal topology [15], thereby obtaining a constructive completeness proof. This proof is elementary and can be seen as a constructive and predicative version of the one in Feferman's review. It is a typical, and simple, example where the use of formal topology gives constructive sense to the existence of a generic object, satisfying some forcing conditions; in this case an ultrafilter satisfying the existence property.<\/jats:p><jats:p>In order to get a formal topology on the set of first-order formulae, Sambin used the Dedekind-MacNeille completion to define a covering relation \u22b2<jats:sub><jats:italic>DM<\/jats:italic><\/jats:sub>. This method, by which an arbitrary poset can be extended to a complete poset, was introduced by MacNeille [9] and is a generalization of the construction of real numbers from rationals by Dedekind cuts. It is also possible to define an inductive cover, \u22b2<jats:sub><jats:italic>I<\/jats:italic><\/jats:sub>, on the set of formulae, which can also be used to give canonical models, see Coquand and Smith [3].<\/jats:p>","DOI":"10.2307\/2586694","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:02:41Z","timestamp":1146938561000},"page":"1183-1192","source":"Crossref","is-referenced-by-count":10,"title":["Formal topologies on the set of first-order formulae"],"prefix":"10.1017","volume":"65","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Sara","family":"Sadocco","sequence":"additional","affiliation":[]},{"given":"Giovanni","family":"Sambin","sequence":"additional","affiliation":[]},{"given":"Jan M.","family":"Smith","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200011853_ref013","doi-asserted-by":"publisher","DOI":"10.4064\/fm-37-1-193-200"},{"key":"S0022481200011853_ref014","volume-title":"Topologie formali sull'insieme delle formule","author":"Sadocco","year":"1996"},{"key":"S0022481200011853_ref005","first-page":"72","volume":"17","author":"Feferman","year":"1952","journal-title":"Review of \u201cA proof of the completeness theorem of G\u00f6del\u201d by H. Rasiowa and R. Sikorski"},{"key":"S0022481200011853_ref001","volume-title":"Foundations of constructive analysis","author":"Bishop","year":"1967"},{"key":"S0022481200011853_ref008","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/030\/749770"},{"key":"S0022481200011853_ref006","first-page":"107\u2013122","volume-title":"Brouwer Centenary Symposium","author":"Fourman","year":"1982"},{"key":"S0022481200011853_ref011","volume-title":"Programming in Martin-L\u00f6f's type theory. an introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0022481200011853_ref002","unstructured":"Cederquist J. , A pointfree approach to constructive analysis in type theory, Ph.d. thesis , Chalmers University of Technology and University of G\u00f6teborg, Sweden, 1997."},{"key":"S0022481200011853_ref015","first-page":"187\u2013204","volume-title":"Mathematical logic and its applications","author":"Sambin","year":"1987"},{"key":"S0022481200011853_ref016","first-page":"861\u2013878","volume":"60","author":"Sambin","year":"1995","journal-title":"Pretopologies and completeness proofs"},{"key":"S0022481200011853_ref007","first-page":"159\u2013166","volume":"14","author":"Henkin","year":"1949","journal-title":"The completeness of first-order functional calculus"},{"key":"S0022481200011853_ref003","first-page":"76\u201384","volume-title":"Proceedings of the Workshop TYPES '95, Torino, Italy, June 1995","author":"Coquand","year":"1996"},{"key":"S0022481200011853_ref004","first-page":"369\u2013389","article-title":"An explicit Boolean-valued model for non-standard arithmetic","volume":"42","author":"Dragalin","year":"1993","journal-title":"Publicationes Mathematicae Drebecen"},{"key":"S0022481200011853_ref009","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1937-1501929-X"},{"key":"S0022481200011853_ref010","first-page":"1448\u20131460","volume":"62","author":"Moerdijk","year":"1997","journal-title":"Minimal models of Heyting arithmetic"},{"key":"S0022481200011853_ref012","unstructured":"Persson H. , Constructive completeness of intuitionistic predicate logic: A formalisation in type theory, Licentiate Thesis, Chalmers University of Technology and University of G\u00f6teborg, Sweden, November 1996."},{"key":"S0022481200011853_ref017","doi-asserted-by":"crossref","first-page":"221\u2013244","DOI":"10.1093\/oso\/9780198501275.001.0001","volume-title":"Twenty-five years of constructive type theory","author":"Sambin","year":"1998"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200011853","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,26]],"date-time":"2021-07-26T20:10:38Z","timestamp":1627330238000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200011853\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,9]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,9]]}},"alternative-id":["S0022481200011853"],"URL":"https:\/\/doi.org\/10.2307\/2586694","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,9]]}}}