|
|
| (216 intermediate revisions by more than 100 users not shown) |
| Line 1: |
Line 1: |
| '''S''' is an [[axiomatic set theory]] set out by [[George Boolos]] in his article, Boolos (1989). '''S''', a [[first order logic|first-order]] theory, is two-sorted because its [[ontology]] includes “stages” as well as [[set (mathematics)|sets]]. Boolos designed '''S''' to embody his understanding of the “iterative conception of set“ and the associated [[iterative hierarchy]]. '''S''' has the important property that all axioms of [[Zermelo set theory]] ''Z'', except the [[axiom of Extensionality]] and the [[axiom of Choice]], are theorems of '''S''' or a slight modification thereof. | | This is a preview for the new '''MathML rendering mode''' (with SVG fallback), which is availble in production for registered users. |
|
| |
|
| ==Ontology==
| | If you would like use the '''MathML''' rendering mode, you need a wikipedia user account that can be registered here [[https://en.wikipedia.org/wiki/Special:UserLogin/signup]] |
| Any grouping together of [[mathematical object|mathematical]], [[abstract object|abstract]], or concrete objects, however formed, is a ''collection'', a synonym for what other [[set theory|set theories]] refer to as a [[Class (set theory)|class]]. The things that make up a collection are called [[element (mathematics)|element]]s or members. A common instance of a collection is the [[domain of discourse]] of a [[first order theory]].
| | * Only registered users will be able to execute this rendering mode. |
| | * Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere. |
|
| |
|
| All sets are collections, but there are collections that are not sets. A synonym for collections that are not sets is [[proper class]]. An essential task of [[axiomatic set theory]] is to distinguish sets from proper classes, if only because mathematics is grounded in sets, with proper classes relegated to a purely descriptive role.
| | Registered users will be able to choose between the following three rendering modes: |
|
| |
|
| The [[Von Neumann universe]] implements the “iterative conception of set” by stratifying the universe of sets into a series of “stages,” with the sets at a given stage being possible members of the sets formed at all higher stages. The notion of stage goes as follows. Each stage is assigned an [[ordinal number]]. The lowest stage, stage 0, consists of all entities having no members. We assume that the only entity at stage 0 is the [[empty set]], although this stage would include any [[urelements]] we would choose to admit. Stage ''n'', ''n''>0, consists of all possible sets formed from elements to be found in any stage whose number is less than ''n''. Every set formed at stage ''n'' can also be formed at every stage greater than ''n''.<ref>Boolos (1998:88).</ref>
| | '''MathML''' |
| | :<math forcemathmode="mathml">E=mc^2</math> |
|
| |
|
| Hence the stages form a nested and [[well-ordered]] sequence, and would form a [[hierarchy (mathematics)|hierarchy]] if set membership were [[transitive relation|transitive]]. The iterative conception has gradually become more accepted, despite an imperfect understanding of its historical origins.
| | <!--'''PNG''' (currently default in production) |
| | :<math forcemathmode="png">E=mc^2</math> |
|
| |
|
| The iterative conception of set steers clear, in a well-motivated way, of the well-known [[paradox]]es of [[Russell's paradox|Russell]], [[Burali-Forti paradox|Burali-Forti]], and [[Cantor's paradox|Cantor]]. These paradoxes all result from the unrestricted use of the [[axiom of comprehension|principle of comprehension]] of [[naive set theory]]. Collections such as “the class of all sets” or “the class of all [[ordinal number|ordinals]]” include sets from all stages of the iterative hierarchy. Hence such collections cannot be formed at any given stage, and thus cannot be sets.
| | '''source''' |
| | :<math forcemathmode="source">E=mc^2</math> --> |
|
| |
|
| ==Primitive notions== | | <span style="color: red">Follow this [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering link] to change your Math rendering settings.</span> You can also add a [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering-skin Custom CSS] to force the MathML/SVG rendering or select different font families. See [https://www.mediawiki.org/wiki/Extension:Math#CSS_for_the_MathML_with_SVG_fallback_mode these examples]. |
| This section follows Boolos (1998: 91). The variables ''x'' and ''y'' range over sets, while ''r'', ''s'', and ''t'' range over stages. There are three [[primitive notion|primitive]] two-place [[Predicate (mathematical logic)|predicates]]:
| |
| * Set-set: ''x''∈''y'' denotes, as usual, that set ''x'' is a member of set ''y'';
| |
| * Set-stage: ''Fxr'' denotes that set ''x'' “is formed at” stage ''r'';
| |
| * Stage-stage: ''r''<''s'' denotes that stage ''r'' “is earlier than” stage ''s''.
| |
|
| |
|
| The axioms below include a defined two-place set-stage predicate, ''Bxr'', which abbreviates:
| | ==Demos== |
| :<math>\exist s[s<r \land Fxs].</math>
| |
| ''Bxr'' is read as “set ''x'' is formed before stage ''r''.”
| |
|
| |
|
| [[identity (mathematics)|Identity]], denoted by infix ‘=’, does not play the role in '''S''' it plays in other set theories, and Boolos does not make fully explicit whether the background [[first order logic|logic]] includes identity. '''S''' has no [[axiom of Extensionality]] and identity is absent from the other '''S''' axioms. Identity does appear in the axiom schema distinguishing '''S+''' from '''S''',<ref>Boolos (1998: 97).</ref> and in the derivation in '''S''' of the [[axiom of pairing|Pairing]], [[axiom of the empty set|Null set]], and [[axiom of infinity|Infinity]] axioms of ''[[Z]]''.<ref>Boolos (1998: 103–04).</ref> | | Here are some [https://commons.wikimedia.org/w/index.php?title=Special:ListFiles/Frederic.wang demos]: |
|
| |
|
| ==Axioms==
| |
| The symbolic axioms shown below are from Boolos (1998: 91), and govern how sets and stages behave and interact. The natural language versions of the axioms are intended to aid the intuition.
| |
| <!-- The symbolic axioms should not be changed without discussion on the talk page. Altering these axioms would constitute original research. However the English descriptions may be changed.-->
| |
|
| |
|
| The axioms come in two groups of three. The first group consists of axioms pertaining solely to stages and the stage-stage relation ‘<’.
| | * accessibility: |
| | ** Safari + VoiceOver: [https://commons.wikimedia.org/wiki/File:VoiceOver-Mac-Safari.ogv video only], [[File:Voiceover-mathml-example-1.wav|thumb|Voiceover-mathml-example-1]], [[File:Voiceover-mathml-example-2.wav|thumb|Voiceover-mathml-example-2]], [[File:Voiceover-mathml-example-3.wav|thumb|Voiceover-mathml-example-3]], [[File:Voiceover-mathml-example-4.wav|thumb|Voiceover-mathml-example-4]], [[File:Voiceover-mathml-example-5.wav|thumb|Voiceover-mathml-example-5]], [[File:Voiceover-mathml-example-6.wav|thumb|Voiceover-mathml-example-6]], [[File:Voiceover-mathml-example-7.wav|thumb|Voiceover-mathml-example-7]] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Audio-Windows7-InternetExplorer.ogg Internet Explorer + MathPlayer (audio)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-SynchronizedHighlighting-WIndows7-InternetExplorer.png Internet Explorer + MathPlayer (synchronized highlighting)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Braille-Windows7-InternetExplorer.png Internet Explorer + MathPlayer (braille)] |
| | ** NVDA+MathPlayer: [[File:Nvda-mathml-example-1.wav|thumb|Nvda-mathml-example-1]], [[File:Nvda-mathml-example-2.wav|thumb|Nvda-mathml-example-2]], [[File:Nvda-mathml-example-3.wav|thumb|Nvda-mathml-example-3]], [[File:Nvda-mathml-example-4.wav|thumb|Nvda-mathml-example-4]], [[File:Nvda-mathml-example-5.wav|thumb|Nvda-mathml-example-5]], [[File:Nvda-mathml-example-6.wav|thumb|Nvda-mathml-example-6]], [[File:Nvda-mathml-example-7.wav|thumb|Nvda-mathml-example-7]]. |
| | ** Orca: There is ongoing work, but no support at all at the moment [[File:Orca-mathml-example-1.wav|thumb|Orca-mathml-example-1]], [[File:Orca-mathml-example-2.wav|thumb|Orca-mathml-example-2]], [[File:Orca-mathml-example-3.wav|thumb|Orca-mathml-example-3]], [[File:Orca-mathml-example-4.wav|thumb|Orca-mathml-example-4]], [[File:Orca-mathml-example-5.wav|thumb|Orca-mathml-example-5]], [[File:Orca-mathml-example-6.wav|thumb|Orca-mathml-example-6]], [[File:Orca-mathml-example-7.wav|thumb|Orca-mathml-example-7]]. |
| | ** From our testing, ChromeVox and JAWS are not able to read the formulas generated by the MathML mode. |
|
| |
|
| '''Tra''': <math> \forall r \forall s \forall t[r<s \land s<t \rightarrow r<t] \,.</math>
| | ==Test pages == |
|
| |
|
| “Earlier than” is transitive.
| | To test the '''MathML''', '''PNG''', and '''source''' rendering modes, please go to one of the following test pages: |
| | *[[Displaystyle]] |
| | *[[MathAxisAlignment]] |
| | *[[Styling]] |
| | *[[Linebreaking]] |
| | *[[Unique Ids]] |
| | *[[Help:Formula]] |
|
| |
|
| '''Net''': <math> \forall s \forall t \exist r[t<r \land s<r] \,.</math>
| | *[[Inputtypes|Inputtypes (private Wikis only)]] |
| | | *[[Url2Image|Url2Image (private Wikis only)]] |
| A consequence of ''Net'' is that every stage is earlier than some stage.
| | ==Bug reporting== |
| | | If you find any bugs, please report them at [https://bugzilla.wikimedia.org/enter_bug.cgi?product=MediaWiki%20extensions&component=Math&version=master&short_desc=Math-preview%20rendering%20problem Bugzilla], or write an email to math_bugs (at) ckurs (dot) de . |
| '''Inf''': <math> \exist r \exist u [u<r \land \forall t[t<r \rightarrow \exist s[t<s \land s<r]]] \,.</math>
| |
| | |
| The sole purpose of ''Inf'' is to enable deriving in '''S''' the [[axiom of infinity]] of other set theories.
| |
| | |
| The second and final group of axioms involve both sets and stages, and the predicates other than '<':
| |
| | |
| '''All''': <math> \forall x \exist r Fxr \,.</math>
| |
| | |
| Every set is formed at some stage in the hierarchy.
| |
| | |
| '''When''': <math> \forall r \forall x [Fxr \leftrightarrow [\forall y (y \in x \rightarrow Byr) \and \lnot Bxr] ] \,.</math>
| |
| | |
| A set is formed at some stage [[iff]] its members are formed at earlier stages.
| |
| | |
| Let ''A''(''y'') be a formula of '''S''' where ''y'' is free but ''x'' is not. Then the following axiom schema holds:
| |
| | |
| '''Spec''': <math> \exist r \forall y[A(y) \rightarrow Byr] \rightarrow \exist x \forall y[y \in x \leftrightarrow A(y)] \,.</math>
| |
| | |
| If there exists a stage ''r'' such that all sets satisfying ''A''(''y'') are formed at a stage earlier than ''r'', then there exists a set ''x'' whose members are just those sets satisfying ''A''(''y''). The role of ''Spec'' in '''S''' is analogous to that of the [[axiom schema of specification]] of [[Z]].
| |
| | |
| ==Discussion== | |
| Boolos’s name for [[Zermelo set theory]] minus extensionality was ''Z-''. Boolos derived in '''S''' all axioms of ''Z-'' except the [[axiom of choice]].<ref>Boolos (1998: 95–96; 103–04).</ref> The purpose of this exercise was to show how most of conventional set theory can be derived from the iterative conception of set, assumed embodied in '''S'''. [[Extensionality]] does not follow from the iterative conception, and so is not a theorem of '''S'''. However, '''S''' + Extensionality is free of contradiction if '''S''' is free of contradiction.
| |
| | |
| Boolos then altered ''Spec'' to obtain a variant of '''S''' he called '''S+''', such that the [[axiom schema of replacement]] is derivable in '''S+''' + Extensionality. Hence '''S+''' + Extensionality has the power of [[Zermelo–Fraenkel set theory|ZF]]. Boolos also argued that the [[axiom of choice]] does not follow from the iterative conception, but did not address whether Choice could be added to '''S''' in some way.<ref>Boolos (1998: 97).</ref> Hence '''S+''' + Extensionality cannot prove those theorems of the industry-standard set theory [[ZFC]] whose proofs require Choice.
| |
| | |
| '''Inf''' guarantees the existence of stages ω, and of ω + ''n'' for finite ''n'', but not of stage ω + ω. Nevertheless, '''S''' yields enough of [[transfinite numbers|Cantor's paradise]] to ground almost all of contemporary mathematics.<ref>”…the overwhelming majority of 20th century mathematics is straightforwardly representable by sets of fairly low infinite ranks, certainly less than ω + 20.” (Potter 2004: 220). The exceptions to Potter's statement presumably include [[category theory]], which requires the weakly [[inaccessible cardinal]]s afforded by [[Tarski–Grothendieck set theory]], and the higher reaches of set theory itself.</ref>
| |
| | |
| Boolos compares '''S''' at some length to a variant of the system of [[Frege]]’s ''Grundgesetze'', in which [[Hume's principle]], taken as an axiom, replaces Frege’s Basic Law V, an [[Comprehension_axiom#Unrestricted_comprehension|unrestricted comprehension axiom]] which made Frege's system inconsistent; see [[Russell's paradox]].
| |
| | |
| ==References== | |
| * [[George Boolos]] (1989) “Iteration Again,” ''Philosophical Topics'' 17: 5–21. Reprinted in his (1998) ''Logic, Logic, and Logic''. Harvard Univ. Press: 88–104.
| |
| * [[Michael Potter]] (2004) ''Set Theory and Its Philosophy''. Oxford Univ. Press.
| |
| | |
| ==Footnotes==
| |
| {{Reflist}}
| |
| | |
| [[Category:Set theory]]
| |
| [[Category:Systems of set theory]]
| |
| [[Category:Z notation]]
| |
