In:
Journal of Symbolic Logic, Cambridge University Press (CUP), Vol. 65, No. 3 ( 2000-09), p. 1183-1192
Abstract:
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 (∃ x ) ϕ it also contains some substitution ϕ ( y / x ) of a variable y for x . In Feferman's review [5] of [13] , an improvement, due to Tarski, is given by which the proof gets a simple algebraic form. 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. 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 ⊲ DM . 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, ⊲ I , on the set of formulae, which can also be used to give canonical models, see Coquand and Smith [3].
Type of Medium:
Online Resource
ISSN:
0022-4812
,
1943-5886
Language:
English
Publisher:
Cambridge University Press (CUP)
Publication Date:
2000
detail.hit.zdb_id:
2010607-5
SSG:
5,1
SSG:
17,1
