#jsDisabledContent { display:none; } My Account |  Register |  Help

# General set theory

Article Id: WHEBN0009373204
Reproduction Date:

 Title: General set theory Author: World Heritage Encyclopedia Language: English Subject: Collection: Publisher: World Heritage Encyclopedia Publication Date:

### General set theory

General set theory (GST) is axiomatic set theory Z. GST is sufficient for all mathematics not requiring infinite sets, and is the weakest known set theory whose theorems include the Peano axioms.

## Ontology

The ontology of GST is identical to that of ZFC, and hence is thoroughly canonical. GST features a single primitive ontological notion, that of set, and a single ontological assumption, namely that all individuals in the universe of discourse (hence all mathematical objects) are sets. There is a single primitive binary relation, set membership; that set a is a member of set b is written ab (usually read "a is an element of b").

## Axioms

The symbolic axioms below are from Boolos (1998: 196), and govern how sets behave and interact. The natural language versions of the axioms are intended to aid the intuition. The background logic is first order logic with identity.

1) Axiom of Extensionality: The sets x and y are the same set if they have the same members.

\forall x \forall y [\forall z [z \in x \leftrightarrow z \in y] \rightarrow x = y].

The converse of this axiom follows from the substitution property of equality.

2) Axiom Schema of Specification (or Separation or Restricted Comprehension): If z is a set and \phi\! is any property which may be satisfied by all, some, or no elements of z, then there exists a subset y of z containing just those elements x in z which satisfy the property \phi\!. The restriction to z is necessary to avoid Russell's paradox and its variants. More formally, let \phi(x)\! be any formula in the language of GST in which x is free and y is not. Then all instances of the following schema are axioms:

\forall z \exists y \forall x [x \in y \leftrightarrow ( x \in z \land \phi(x))].

3) Axiom of Adjunction: If x and y are sets, then there exists a set w, the adjunction of x and y, whose members are just y and the members of x.[1]

\forall x \forall y \exist w \forall z [ z \in w \leftrightarrow (z \in x \or z=y)].

Adjunction refers to an elementary operation on two sets, and has no bearing on the use of that term elsewhere in mathematics, including in category theory.

## Discussion

GST is the fragment of Z obtained by omitting the axioms Union, Power Set, Infinity, and Choice, then taking Adjunction, a theorem of Z, as an axiom. The result is a first order theory.

Setting φ(x) in Separation to xx, and assuming that the domain is nonempty, assures the existence of the empty set. Adjunction implies that if x is a set, then so is S(x) = x \cup \{x\}. Given Adjunction, the usual construction of the successor ordinals from the empty set can proceed, one in which the natural numbers are defined as \varnothing,\,S(\varnothing),\,S(S(\varnothing)),\,\ldots, (see Peano's axioms). More generally, given any model M of ZFC, the collection of hereditarily finite sets in M will satisfy the GST axioms. Therefore, GST cannot prove the existence of even a countable infinite set, that is, of a set whose cardinality is ℵ0. Even if GST did afford a countably infinite set, GST could not prove the existence of a set whose cardinality is \aleph_1, because GST lacks the axiom of power set. Hence GST cannot ground analysis and geometry, and is too weak to serve as a foundation for mathematics.

Boolos was interested in GST only as a fragment of Z that is just powerful enough to interpret Peano arithmetic. He never lingered over GST, only mentioning it briefly in several papers discussing the systems of Frege's Grundlagen and Grundgesetze, and how they could be modified to eliminate Russell's paradox. The system Aξ'0] in Tarski and Givant (1987: 223) is essentially GST with an axiom schema of induction replacing Specification, and with the existence of a null set explicitly assumed.

GST is called STZ in Burgess (2005), p. 223.[2] Burgess's theory ST[3] is GST with Null Set replacing the axiom schema of specification. That the letters "ST" also appear in "GST" is a coincidence.

## Metamathematics

The most remarkable fact about ST (and hence GST), is that these tiny fragments of set theory give rise to such rich metamathematics. While ST is a small fragment of the well-known canonical set theories ZFC and NBG, ST interprets Robinson arithmetic (Q), so that ST inherits the nontrivial metamathematics of Q. For example, ST is essentially undecidable because Q is, and every consistent theory whose theorems include the ST axioms is also essentially undecidable.[4] This includes GST and every axiomatic set theory worth thinking about, assuming these are consistent. In fact, the undecidability of ST implies the undecidability of first-order logic with a single binary predicate letter.[5]

Q is also incomplete in the sense of Gödel's incompleteness theorem. Any axiomatizable theory, such as ST and GST, whose theorems include the Q axioms is likewise incomplete. Moreover, the consistency of GST cannot be proved within GST itself, unless GST is in fact inconsistent.

GST is:

## Footnotes

-- Module:Hatnote -- -- -- -- This module produces hatnote links and links to related articles. It -- -- implements the and meta-templates and includes -- -- helper functions for other Lua hatnote modules. --

local libraryUtil = require('libraryUtil') local checkType = libraryUtil.checkType local mArguments -- lazily initialise Module:Arguments local yesno -- lazily initialise Module:Yesno

local p = {}

-- Helper functions

local function getArgs(frame) -- Fetches the arguments from the parent frame. Whitespace is trimmed and -- blanks are removed. mArguments = require('Module:Arguments') return mArguments.getArgs(frame, {parentOnly = true}) end

local function removeInitialColon(s) -- Removes the initial colon from a string, if present. return s:match('^:?(.*)') end

function p.findNamespaceId(link, removeColon) -- Finds the namespace id (namespace number) of a link or a pagename. This -- function will not work if the link is enclosed in double brackets. Colons -- are trimmed from the start of the link by default. To skip colon -- trimming, set the removeColon parameter to true. checkType('findNamespaceId', 1, link, 'string') checkType('findNamespaceId', 2, removeColon, 'boolean', true) if removeColon ~= false then link = removeInitialColon(link) end local namespace = link:match('^(.-):') if namespace then local nsTable = mw.site.namespaces[namespace] if nsTable then return nsTable.id end end return 0 end

function p.formatPages(...) -- Formats a list of pages using formatLink and returns it as an array. Nil -- values are not allowed. local pages = {...} local ret = {} for i, page in ipairs(pages) do ret[i] = p._formatLink(page) end return ret end

function p.formatPageTables(...) -- Takes a list of page/display tables and returns it as a list of -- formatted links. Nil values are not allowed. local pages = {...} local links = {} for i, t in ipairs(pages) do checkType('formatPageTables', i, t, 'table') local link = t[1] local display = t[2] links[i] = p._formatLink(link, display) end return links end

function p.makeWikitextError(msg, helpLink, addTrackingCategory) -- Formats an error message to be returned to wikitext. If -- addTrackingCategory is not false after being returned from -- Module:Yesno, and if we are not on a talk page, a tracking category -- is added. checkType('makeWikitextError', 1, msg, 'string') checkType('makeWikitextError', 2, helpLink, 'string', true) yesno = require('Module:Yesno') local title = mw.title.getCurrentTitle() -- Make the help link text. local helpText if helpLink then helpText = ' (help)' else helpText = end -- Make the category text. local category if not title.isTalkPage and yesno(addTrackingCategory) ~= false then category = 'Hatnote templates with errors' category = string.format( '%s:%s', mw.site.namespaces[14].name, category ) else category = end return string.format( '%s', msg, helpText, category ) end

-- Format link -- -- Makes a wikilink from the given link and display values. Links are escaped -- with colons if necessary, and links to sections are detected and displayed -- with " § " as a separator rather than the standard MediaWiki "#". Used in -- the template.

function p._formatLink(link, display) -- Find whether we need to use the colon trick or not. We need to use the -- colon trick for categories and files, as otherwise category links -- categorise the page and file links display the file. checkType('_formatLink', 1, link, 'string') checkType('_formatLink', 2, display, 'string', true) link = removeInitialColon(link) local namespace = p.findNamespaceId(link, false) local colon if namespace == 6 or namespace == 14 then colon = ':' else colon = end -- Find whether a faux display value has been added with the | magic -- word. if not display then local prePipe, postPipe = link:match('^(.-)|(.*)$') link = prePipe or link display = postPipe end -- Find the display value. if not display then local page, section = link:match('^(.-)#(.*)$') if page then display = page .. ' § ' .. section end end -- Assemble the link. if display then return string.format('%s', colon, link, display) else return string.format('%s%s', colon, link) end end

-- Hatnote -- -- Produces standard hatnote text. Implements the template.

function p.hatnote(frame) local args = getArgs(frame) local s = args[1] local options = {} if not s then return p.makeWikitextError( 'no text specified', 'Template:Hatnote#Errors', args.category ) end options.extraclasses = args.extraclasses options.selfref = args.selfref return p._hatnote(s, options) end

function p._hatnote(s, options) checkType('_hatnote', 1, s, 'string') checkType('_hatnote', 2, options, 'table', true) local classes = {'hatnote'} local extraclasses = options.extraclasses local selfref = options.selfref if type(extraclasses) == 'string' then classes[#classes + 1] = extraclasses end if selfref then classes[#classes + 1] = 'selfref' end return string.format( '
%s
', table.concat(classes, ' '), s )

end

return p-------------------------------------------------------------------------------- -- Module:Hatnote -- -- -- -- This module produces hatnote links and links to related articles. It -- -- implements the and meta-templates and includes -- -- helper functions for other Lua hatnote modules. --

local libraryUtil = require('libraryUtil') local checkType = libraryUtil.checkType local mArguments -- lazily initialise Module:Arguments local yesno -- lazily initialise Module:Yesno

local p = {}

-- Helper functions

local function getArgs(frame) -- Fetches the arguments from the parent frame. Whitespace is trimmed and -- blanks are removed. mArguments = require('Module:Arguments') return mArguments.getArgs(frame, {parentOnly = true}) end

local function removeInitialColon(s) -- Removes the initial colon from a string, if present. return s:match('^:?(.*)') end

function p.findNamespaceId(link, removeColon) -- Finds the namespace id (namespace number) of a link or a pagename. This -- function will not work if the link is enclosed in double brackets. Colons -- are trimmed from the start of the link by default. To skip colon -- trimming, set the removeColon parameter to true. checkType('findNamespaceId', 1, link, 'string') checkType('findNamespaceId', 2, removeColon, 'boolean', true) if removeColon ~= false then link = removeInitialColon(link) end local namespace = link:match('^(.-):') if namespace then local nsTable = mw.site.namespaces[namespace] if nsTable then return nsTable.id end end return 0 end

function p.formatPages(...) -- Formats a list of pages using formatLink and returns it as an array. Nil -- values are not allowed. local pages = {...} local ret = {} for i, page in ipairs(pages) do ret[i] = p._formatLink(page) end return ret end

function p.formatPageTables(...) -- Takes a list of page/display tables and returns it as a list of -- formatted links. Nil values are not allowed. local pages = {...} local links = {} for i, t in ipairs(pages) do checkType('formatPageTables', i, t, 'table') local link = t[1] local display = t[2] links[i] = p._formatLink(link, display) end return links end

function p.makeWikitextError(msg, helpLink, addTrackingCategory) -- Formats an error message to be returned to wikitext. If -- addTrackingCategory is not false after being returned from -- Module:Yesno, and if we are not on a talk page, a tracking category -- is added. checkType('makeWikitextError', 1, msg, 'string') checkType('makeWikitextError', 2, helpLink, 'string', true) yesno = require('Module:Yesno') local title = mw.title.getCurrentTitle() -- Make the help link text. local helpText if helpLink then helpText = ' (help)' else helpText = end -- Make the category text. local category if not title.isTalkPage and yesno(addTrackingCategory) ~= false then category = 'Hatnote templates with errors' category = string.format( '%s:%s', mw.site.namespaces[14].name, category ) else category = end return string.format( '%s', msg, helpText, category ) end

-- Format link -- -- Makes a wikilink from the given link and display values. Links are escaped -- with colons if necessary, and links to sections are detected and displayed -- with " § " as a separator rather than the standard MediaWiki "#". Used in -- the template.

function p._formatLink(link, display) -- Find whether we need to use the colon trick or not. We need to use the -- colon trick for categories and files, as otherwise category links -- categorise the page and file links display the file. checkType('_formatLink', 1, link, 'string') checkType('_formatLink', 2, display, 'string', true) link = removeInitialColon(link) local namespace = p.findNamespaceId(link, false) local colon if namespace == 6 or namespace == 14 then colon = ':' else colon = end -- Find whether a faux display value has been added with the | magic -- word. if not display then local prePipe, postPipe = link:match('^(.-)|(.*)$') link = prePipe or link display = postPipe end -- Find the display value. if not display then local page, section = link:match('^(.-)#(.*)$') if page then display = page .. ' § ' .. section end end -- Assemble the link. if display then return string.format('%s', colon, link, display) else return string.format('%s%s', colon, link) end end

-- Hatnote -- -- Produces standard hatnote text. Implements the template.

function p.hatnote(frame) local args = getArgs(frame) local s = args[1] local options = {} if not s then return p.makeWikitextError( 'no text specified', 'Template:Hatnote#Errors', args.category ) end options.extraclasses = args.extraclasses options.selfref = args.selfref return p._hatnote(s, options) end

function p._hatnote(s, options) checkType('_hatnote', 1, s, 'string') checkType('_hatnote', 2, options, 'table', true) local classes = {'hatnote'} local extraclasses = options.extraclasses local selfref = options.selfref if type(extraclasses) == 'string' then classes[#classes + 1] = extraclasses end if selfref then classes[#classes + 1] = 'selfref' end return string.format( '
%s
', table.concat(classes, ' '), s )

end

return p
1. ^ Adjunction is seldom mentioned in the literature. Exceptions are Burgess (2005) passim, and QIII in Tarski and Givant (1987: 223).
2. ^ The Null Set axiom in STZ is redundant, because the existence of the null set is derivable from the axiom schema of Specification.
3. ^ Called S' in Tarski et al. (1953: 34).
4. ^ Burgess (2005), 2.2, p. 91.
5. ^ Tarski et al. (1953), p. 34.

## References

• George Boolos (1998) Logic, Logic, and Logic. Harvard Univ. Press.
• Burgess, John, 2005. Fixing Frege. Princeton Univ. Press.
• Richard Montague (1961) "Semantical closure and non-finite axiomatizability" in Infinistic Methods. Warsaw: 45-69.
• Alfred Tarski, Andrzej Mostowski, and Raphael Robinson (1953) Undecidable Theories. North Holland.
• Tarski, A., and Givant, Steven (1987) A Formalization of Set Theory without Variables. Providence RI: AMS Colloquium Publications, v. 41.