Mixing
Two types of axiomatic theories in mathematics
Apart from the notion of formal theory, which formalises the idea of axiomatic system in first order logic, in mathematics people also consider another type of axiomatic systems, which can be described as extensions by definitions of the axiomatic set theory that a mathematician uses in his work. The examples of such systems are
axioms of general topology,
axioms of probability theory,
Hilbert's axioms of geometry,
etc. As far as I know these are not formal theories in first order logic, although, of course they can be presented as such theories, since they are extensions by definitions of ZFC; I think however that this will be too bulky, so I believe, there must be another notion of axiomatic theory in mathematics, which covers the theories from my list.
Is that true? Can anybody enlighten me if the second kind of axiomatic systems has a formal definition (different from the phrase "extension by definitions of ZFC", so that this indeed clarifies the picture)? Or, in other words,
is there a common scheme that describes the axiomatic systems of second type and explains the differences between them and the formal theories in first order logic?
For some time I thought that these are just axiomatic theories in second order logic, but now I got some doubts, and I would prefer to use first order language for describing the differences (I believe, this is possible).
logic axioms
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
|
show 5 more comments
Apart from the notion of formal theory, which formalises the idea of axiomatic system in first order logic, in mathematics people also consider another type of axiomatic systems, which can be described as extensions by definitions of the axiomatic set theory that a mathematician uses in his work. The examples of such systems are
axioms of general topology,
axioms of probability theory,
Hilbert's axioms of geometry,
etc. As far as I know these are not formal theories in first order logic, although, of course they can be presented as such theories, since they are extensions by definitions of ZFC; I think however that this will be too bulky, so I believe, there must be another notion of axiomatic theory in mathematics, which covers the theories from my list.
Is that true? Can anybody enlighten me if the second kind of axiomatic systems has a formal definition (different from the phrase "extension by definitions of ZFC", so that this indeed clarifies the picture)? Or, in other words,
is there a common scheme that describes the axiomatic systems of second type and explains the differences between them and the formal theories in first order logic?
For some time I thought that these are just axiomatic theories in second order logic, but now I got some doubts, and I would prefer to use first order language for describing the differences (I believe, this is possible).
logic axioms
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
"these are not formal theories in first order logic." If the axiom ssytem (like e.g.that of probability theory) is "written" in the language of $mathsf {ZF}$ set thoery (or similar) it is first-order.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:19
What define univocally "to be first-order" or not is the language: if quantification is allowed only on individual variables, then it is FO. $mathsf {ZF(C)}$ as well as $mathsf {NBG}$ are FO.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:20
Hilbert's axioms system is Second-Order: see "Axiom of completeness. To a system of points, straight lines, and planes, ..." there is a (universal) quantification on "system of points".
– Mauro ALLEGRANZA
Jun 15 '17 at 9:22
See Tarski's axioms (1959) for a system of axioms for elementary geometry that is formulated in first-order logic with identity, and requiring no set theory.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:24
Mauro, I know about Tarski, and I also (like you) think that it is possible to somehow translate everything into a first order language, but before this is done the picture looks differently (and besides this I don't believe that this translation will always be easy). So I wonder if this construction has a reasonable description inside set theory.
– Sergei Akbarov
Jun 15 '17 at 9:26
|
show 5 more comments
Apart from the notion of formal theory, which formalises the idea of axiomatic system in first order logic, in mathematics people also consider another type of axiomatic systems, which can be described as extensions by definitions of the axiomatic set theory that a mathematician uses in his work. The examples of such systems are
axioms of general topology,
axioms of probability theory,
Hilbert's axioms of geometry,
etc. As far as I know these are not formal theories in first order logic, although, of course they can be presented as such theories, since they are extensions by definitions of ZFC; I think however that this will be too bulky, so I believe, there must be another notion of axiomatic theory in mathematics, which covers the theories from my list.
Is that true? Can anybody enlighten me if the second kind of axiomatic systems has a formal definition (different from the phrase "extension by definitions of ZFC", so that this indeed clarifies the picture)? Or, in other words,
is there a common scheme that describes the axiomatic systems of second type and explains the differences between them and the formal theories in first order logic?
For some time I thought that these are just axiomatic theories in second order logic, but now I got some doubts, and I would prefer to use first order language for describing the differences (I believe, this is possible).
logic axioms
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
Apart from the notion of formal theory, which formalises the idea of axiomatic system in first order logic, in mathematics people also consider another type of axiomatic systems, which can be described as extensions by definitions of the axiomatic set theory that a mathematician uses in his work. The examples of such systems are
axioms of general topology,
axioms of probability theory,
Hilbert's axioms of geometry,
etc. As far as I know these are not formal theories in first order logic, although, of course they can be presented as such theories, since they are extensions by definitions of ZFC; I think however that this will be too bulky, so I believe, there must be another notion of axiomatic theory in mathematics, which covers the theories from my list.
Is that true? Can anybody enlighten me if the second kind of axiomatic systems has a formal definition (different from the phrase "extension by definitions of ZFC", so that this indeed clarifies the picture)? Or, in other words,
is there a common scheme that describes the axiomatic systems of second type and explains the differences between them and the formal theories in first order logic?
For some time I thought that these are just axiomatic theories in second order logic, but now I got some doubts, and I would prefer to use first order language for describing the differences (I believe, this is possible).
logic axioms
logic axioms
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
edited Jun 15 '17 at 17:17
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
asked Jun 15 '17 at 9:14
Sergei Akbarov
837516
837516
"these are not formal theories in first order logic." If the axiom ssytem (like e.g.that of probability theory) is "written" in the language of $mathsf {ZF}$ set thoery (or similar) it is first-order.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:19
What define univocally "to be first-order" or not is the language: if quantification is allowed only on individual variables, then it is FO. $mathsf {ZF(C)}$ as well as $mathsf {NBG}$ are FO.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:20
Hilbert's axioms system is Second-Order: see "Axiom of completeness. To a system of points, straight lines, and planes, ..." there is a (universal) quantification on "system of points".
– Mauro ALLEGRANZA
Jun 15 '17 at 9:22
See Tarski's axioms (1959) for a system of axioms for elementary geometry that is formulated in first-order logic with identity, and requiring no set theory.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:24
Mauro, I know about Tarski, and I also (like you) think that it is possible to somehow translate everything into a first order language, but before this is done the picture looks differently (and besides this I don't believe that this translation will always be easy). So I wonder if this construction has a reasonable description inside set theory.
– Sergei Akbarov
Jun 15 '17 at 9:26
|
show 5 more comments
"these are not formal theories in first order logic." If the axiom ssytem (like e.g.that of probability theory) is "written" in the language of $mathsf {ZF}$ set thoery (or similar) it is first-order.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:19
What define univocally "to be first-order" or not is the language: if quantification is allowed only on individual variables, then it is FO. $mathsf {ZF(C)}$ as well as $mathsf {NBG}$ are FO.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:20
Hilbert's axioms system is Second-Order: see "Axiom of completeness. To a system of points, straight lines, and planes, ..." there is a (universal) quantification on "system of points".
– Mauro ALLEGRANZA
Jun 15 '17 at 9:22
See Tarski's axioms (1959) for a system of axioms for elementary geometry that is formulated in first-order logic with identity, and requiring no set theory.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:24
Mauro, I know about Tarski, and I also (like you) think that it is possible to somehow translate everything into a first order language, but before this is done the picture looks differently (and besides this I don't believe that this translation will always be easy). So I wonder if this construction has a reasonable description inside set theory.
– Sergei Akbarov
Jun 15 '17 at 9:26
"these are not formal theories in first order logic." If the axiom ssytem (like e.g.that of probability theory) is "written" in the language of $mathsf {ZF}$ set thoery (or similar) it is first-order.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:19
"these are not formal theories in first order logic." If the axiom ssytem (like e.g.that of probability theory) is "written" in the language of $mathsf {ZF}$ set thoery (or similar) it is first-order.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:19
What define univocally "to be first-order" or not is the language: if quantification is allowed only on individual variables, then it is FO. $mathsf {ZF(C)}$ as well as $mathsf {NBG}$ are FO.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:20
What define univocally "to be first-order" or not is the language: if quantification is allowed only on individual variables, then it is FO. $mathsf {ZF(C)}$ as well as $mathsf {NBG}$ are FO.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:20
Hilbert's axioms system is Second-Order: see "Axiom of completeness. To a system of points, straight lines, and planes, ..." there is a (universal) quantification on "system of points".
– Mauro ALLEGRANZA
Jun 15 '17 at 9:22
Hilbert's axioms system is Second-Order: see "Axiom of completeness. To a system of points, straight lines, and planes, ..." there is a (universal) quantification on "system of points".
– Mauro ALLEGRANZA
Jun 15 '17 at 9:22
See Tarski's axioms (1959) for a system of axioms for elementary geometry that is formulated in first-order logic with identity, and requiring no set theory.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:24
See Tarski's axioms (1959) for a system of axioms for elementary geometry that is formulated in first-order logic with identity, and requiring no set theory.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:24
Mauro, I know about Tarski, and I also (like you) think that it is possible to somehow translate everything into a first order language, but before this is done the picture looks differently (and besides this I don't believe that this translation will always be easy). So I wonder if this construction has a reasonable description inside set theory.
– Sergei Akbarov
Jun 15 '17 at 9:26
Mauro, I know about Tarski, and I also (like you) think that it is possible to somehow translate everything into a first order language, but before this is done the picture looks differently (and besides this I don't believe that this translation will always be easy). So I wonder if this construction has a reasonable description inside set theory.
– Sergei Akbarov
Jun 15 '17 at 9:26
|
show 5 more comments
2 Answers
2
active
oldest
votes
EDIT: Based on the comments, I think this more accurately answers the OP's question:
The axioms for rings are actually first-order - and we say they constitute a first-order theory! Basically, I can write down the ring axioms as first-order sentences in the language ${+, times,0, 1}$, and then rings are the same as models of this set of axioms. These models, of course, are sets, and so we can only talk about them directly in general inside a theory of sets; but the set of axioms itself is first-order. (And note that we can still talk about the theory of rings, and deductions from that theory, in a theory without sets like PA.)
The same is true for groups, fields, etc. The same is also essentially true, incidentally, for "weak topological spaces" (I don't know what these are actually called): say a weak topological space is a set $X$ together with a family $tau$ of subsets of $X$ containing $X$ and $emptyset$ and closed under finite unions and finite intersections. Then consider the language ${E, P, S}$, with a single binary relation $E$ and two unary relations $P, S$. Intuitively, $P$ refers to points, $S$ refers to sets (of points), and $E$ refers to membership. Now consider the following set of first-order sentences:
$forall x((P(x)vee S(x))wedgeneg(P(x)wedge S(x)))$. The only things in our structure are points or sets, and these are disjoint from each other.
$forall x, y(E(x, y)implies P(x), S(y))$. Membership is a relation between points and sets, only.
$forall x, y(S(x), S(y), forall z(E(z, x)iff E(z, y))implies x=y)$. Sets with the same elements are the same.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)wedge E(w, y)))).$ Intersection of two sets (hence finitely many sets is a set.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)vee E(w, y)))).$ Finite unions.
A model of these axioms isn't necessarily literally a weak topological space - the $S$-elements might not actually be sets of $P$-elements - but they can be canonically identified with weak topological spaces: given a model $mathcal{M}=(M; P^M, S^M, E^M)$, we can assign it a weak topological space $T_mathcal{M}$ with underlying set ${min M: mathcal{M}models P^M}$ and "open sets" exactly those of the form ${min M: mathcal{M}models E(m, s)}$ for some $sin{min M: mathcal{M}models S(m)}$. Conversely, each weak topological space can be viewed as a model of the theory above in the obvious way. So we have a dichotomy:
Literally being a weak topological space isn't the same as satisfying some set of first-order axioms (whereas being a ring is the same as being a structure which satisfies the set of first-order ring axioms), but
There is a set of first-order axioms, the class of whose models is equivalent to the class of weak topological spaces in a precise sense (there is a definable function between the two classes which is appropriately surjective and injective-up-to-isomorphism).
Finally, full topological spaces aren't even morally first-order: this is because of the infinite unions bit, which is fundamentally second-order. Instead, there is a set of second-order sentences such that the topological spaces are appropriately equivalent to the models of this set of sentences. Note, however, that in order to talk about satisfaction of second-order sentences we need to work in a more set-theoretic context than if we just care about satisfaction of first-order sentences, and set-theoretic issues are more relevant: for example, (your favorite set theory proves that) there is a second-order sentence which is true in every structure iff the continuum hypothesis holds!
EDIT: The key idea below is that definitions in an extension by definitions are essentially definitions in the original language already. Specifically, you can easily write a computer program that will convert a formula in a extension-by-definitions $L'$ of $L$ into a corresponding formula in $L$. So really, this all boils down to why the language of set theory has enough expansions-by-definitions, and this is provided pretty quickly by playing with the language (e.g. discover how to express "function," "sequence," "relation," "Cartesian product").
I'll do two examples (topological spaces and groups), and hopefully this will indicate why this stuff isn't usually done explicitly - it's very straightforward and quite tedious.
Topological spaces.
Usual definition: A topological space is an ordered pair $(X, tau)$ where $X$ is a set, $tau$ is a set of subsets of $X$, and $tau$ is closed under finite intersections, arbitrary unions, and contains $X$ and $emptyset$.
Formal definition in the language of set theory: $varphi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$bsubseteqmathcal{P}(a)$;
$forall ssubseteq bexists cin b(c=bigcup s)$;
$forall ssubseteq_{finite} bexists cin bforall y(yin ciff forall z(zin simplies yin z))$;
$ain b, emptysetin b$].
I've used symbols not explicitly in the language of set theory above - namely, $langlecdot,cdot rangle$, $subseteq$, $bigcup$, $subseteq_{finite}$, $emptyset$. But it's an easy exercise to get rid of these, and get a formula using only "$in$." But given that the translation is completely straightforward, I'm not sure what value this provides.
Groups.
Usual definition: A set with a binary operation satisfying [stuff].
Formal definition in the language of set theory: $psi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$b$ is a binary function on $a$
[stuff].
Remember that functions, and Cartesian products, are elementary to define in the language of set theory; and so everything here is easy to write down.
One of the values of set theory is that concepts in mathematics translate without effort into the language of set theory. That said, they also translate tediously, so an argument can be made that we should use something other than ZFC; but this is why you don't see these kinds of definitions written out in full.
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right?
– Sergei Akbarov
Jun 15 '17 at 16:16
1
@SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd)
– Noah Schweber
Jun 15 '17 at 16:28
It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $Msubseteq N$ such that $N$ thinks $M$ is transitive but there is some set $rin M$ such that $M$ thinks $r$ is a topological space (that is, $Mmodelsvarphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd)
– Noah Schweber
Jun 15 '17 at 16:31
Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $Msubseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology.
– Noah Schweber
Jun 15 '17 at 16:32
Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"?
– Sergei Akbarov
Jun 15 '17 at 17:04
|
show 1 more comment
Generally mathematicians when doing mathematics (like topology, probability or geometry) do that in the framework of set theory.
This means that they introduce some definitions (topology, $sigma$-algebras, points etc) in terms of sets and provide proofs of facts about these objects using properties of sets.
Formally what mathematicians do is take ZFC theory add new symbols to the language (for instance predicates like "is a topology", "is a topological space", "is a continuous function" and so on) and then axiomatically define these predicates in terms of formulas in the language of ZFC, that is they add some axioms of the form
$$x text{ is a topology} iff varphi(x)$$
$$x text{ is a topological space} iff varphi'(x)$$
$$dots$$
where the formulas $varphi(x)$, $varphi'(x)$ etc are ZFC formulas.
In this way they can reduce any proof about the new introduced objects (toplogical spaces, geometric figures etc) to a proof about sets, that is a proof that ultimately relies on the axioms of ZFC+the definitional axioms for the new predicates.
On the other hand in principle one could try to look at the formal systems you listed as some logical systems on their own.
For instance Hilber's system for euclidean geometry can be easily seen as a first-order theory, as it is basically shown in the wikipedia link you gave.
The other systems you listed could be seen as formal systems for an higher-order logic, but you have to go at least third order because in these systems you would need to quantify over families of subsets (that is over families of predicates, or predicates of predicates).
If you like I could add the details, at least for one of the systems.
Let me know if you need any additional clarification.
Hope this helps.
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
1
Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory.
– Sergei Akbarov
Jun 15 '17 at 15:24
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2323458%2ftwo-types-of-axiomatic-theories-in-mathematics%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
EDIT: Based on the comments, I think this more accurately answers the OP's question:
The axioms for rings are actually first-order - and we say they constitute a first-order theory! Basically, I can write down the ring axioms as first-order sentences in the language ${+, times,0, 1}$, and then rings are the same as models of this set of axioms. These models, of course, are sets, and so we can only talk about them directly in general inside a theory of sets; but the set of axioms itself is first-order. (And note that we can still talk about the theory of rings, and deductions from that theory, in a theory without sets like PA.)
The same is true for groups, fields, etc. The same is also essentially true, incidentally, for "weak topological spaces" (I don't know what these are actually called): say a weak topological space is a set $X$ together with a family $tau$ of subsets of $X$ containing $X$ and $emptyset$ and closed under finite unions and finite intersections. Then consider the language ${E, P, S}$, with a single binary relation $E$ and two unary relations $P, S$. Intuitively, $P$ refers to points, $S$ refers to sets (of points), and $E$ refers to membership. Now consider the following set of first-order sentences:
$forall x((P(x)vee S(x))wedgeneg(P(x)wedge S(x)))$. The only things in our structure are points or sets, and these are disjoint from each other.
$forall x, y(E(x, y)implies P(x), S(y))$. Membership is a relation between points and sets, only.
$forall x, y(S(x), S(y), forall z(E(z, x)iff E(z, y))implies x=y)$. Sets with the same elements are the same.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)wedge E(w, y)))).$ Intersection of two sets (hence finitely many sets is a set.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)vee E(w, y)))).$ Finite unions.
A model of these axioms isn't necessarily literally a weak topological space - the $S$-elements might not actually be sets of $P$-elements - but they can be canonically identified with weak topological spaces: given a model $mathcal{M}=(M; P^M, S^M, E^M)$, we can assign it a weak topological space $T_mathcal{M}$ with underlying set ${min M: mathcal{M}models P^M}$ and "open sets" exactly those of the form ${min M: mathcal{M}models E(m, s)}$ for some $sin{min M: mathcal{M}models S(m)}$. Conversely, each weak topological space can be viewed as a model of the theory above in the obvious way. So we have a dichotomy:
Literally being a weak topological space isn't the same as satisfying some set of first-order axioms (whereas being a ring is the same as being a structure which satisfies the set of first-order ring axioms), but
There is a set of first-order axioms, the class of whose models is equivalent to the class of weak topological spaces in a precise sense (there is a definable function between the two classes which is appropriately surjective and injective-up-to-isomorphism).
Finally, full topological spaces aren't even morally first-order: this is because of the infinite unions bit, which is fundamentally second-order. Instead, there is a set of second-order sentences such that the topological spaces are appropriately equivalent to the models of this set of sentences. Note, however, that in order to talk about satisfaction of second-order sentences we need to work in a more set-theoretic context than if we just care about satisfaction of first-order sentences, and set-theoretic issues are more relevant: for example, (your favorite set theory proves that) there is a second-order sentence which is true in every structure iff the continuum hypothesis holds!
EDIT: The key idea below is that definitions in an extension by definitions are essentially definitions in the original language already. Specifically, you can easily write a computer program that will convert a formula in a extension-by-definitions $L'$ of $L$ into a corresponding formula in $L$. So really, this all boils down to why the language of set theory has enough expansions-by-definitions, and this is provided pretty quickly by playing with the language (e.g. discover how to express "function," "sequence," "relation," "Cartesian product").
I'll do two examples (topological spaces and groups), and hopefully this will indicate why this stuff isn't usually done explicitly - it's very straightforward and quite tedious.
Topological spaces.
Usual definition: A topological space is an ordered pair $(X, tau)$ where $X$ is a set, $tau$ is a set of subsets of $X$, and $tau$ is closed under finite intersections, arbitrary unions, and contains $X$ and $emptyset$.
Formal definition in the language of set theory: $varphi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$bsubseteqmathcal{P}(a)$;
$forall ssubseteq bexists cin b(c=bigcup s)$;
$forall ssubseteq_{finite} bexists cin bforall y(yin ciff forall z(zin simplies yin z))$;
$ain b, emptysetin b$].
I've used symbols not explicitly in the language of set theory above - namely, $langlecdot,cdot rangle$, $subseteq$, $bigcup$, $subseteq_{finite}$, $emptyset$. But it's an easy exercise to get rid of these, and get a formula using only "$in$." But given that the translation is completely straightforward, I'm not sure what value this provides.
Groups.
Usual definition: A set with a binary operation satisfying [stuff].
Formal definition in the language of set theory: $psi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$b$ is a binary function on $a$
[stuff].
Remember that functions, and Cartesian products, are elementary to define in the language of set theory; and so everything here is easy to write down.
One of the values of set theory is that concepts in mathematics translate without effort into the language of set theory. That said, they also translate tediously, so an argument can be made that we should use something other than ZFC; but this is why you don't see these kinds of definitions written out in full.
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right?
– Sergei Akbarov
Jun 15 '17 at 16:16
1
@SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd)
– Noah Schweber
Jun 15 '17 at 16:28
It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $Msubseteq N$ such that $N$ thinks $M$ is transitive but there is some set $rin M$ such that $M$ thinks $r$ is a topological space (that is, $Mmodelsvarphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd)
– Noah Schweber
Jun 15 '17 at 16:31
Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $Msubseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology.
– Noah Schweber
Jun 15 '17 at 16:32
Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"?
– Sergei Akbarov
Jun 15 '17 at 17:04
|
show 1 more comment
EDIT: Based on the comments, I think this more accurately answers the OP's question:
The axioms for rings are actually first-order - and we say they constitute a first-order theory! Basically, I can write down the ring axioms as first-order sentences in the language ${+, times,0, 1}$, and then rings are the same as models of this set of axioms. These models, of course, are sets, and so we can only talk about them directly in general inside a theory of sets; but the set of axioms itself is first-order. (And note that we can still talk about the theory of rings, and deductions from that theory, in a theory without sets like PA.)
The same is true for groups, fields, etc. The same is also essentially true, incidentally, for "weak topological spaces" (I don't know what these are actually called): say a weak topological space is a set $X$ together with a family $tau$ of subsets of $X$ containing $X$ and $emptyset$ and closed under finite unions and finite intersections. Then consider the language ${E, P, S}$, with a single binary relation $E$ and two unary relations $P, S$. Intuitively, $P$ refers to points, $S$ refers to sets (of points), and $E$ refers to membership. Now consider the following set of first-order sentences:
$forall x((P(x)vee S(x))wedgeneg(P(x)wedge S(x)))$. The only things in our structure are points or sets, and these are disjoint from each other.
$forall x, y(E(x, y)implies P(x), S(y))$. Membership is a relation between points and sets, only.
$forall x, y(S(x), S(y), forall z(E(z, x)iff E(z, y))implies x=y)$. Sets with the same elements are the same.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)wedge E(w, y)))).$ Intersection of two sets (hence finitely many sets is a set.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)vee E(w, y)))).$ Finite unions.
A model of these axioms isn't necessarily literally a weak topological space - the $S$-elements might not actually be sets of $P$-elements - but they can be canonically identified with weak topological spaces: given a model $mathcal{M}=(M; P^M, S^M, E^M)$, we can assign it a weak topological space $T_mathcal{M}$ with underlying set ${min M: mathcal{M}models P^M}$ and "open sets" exactly those of the form ${min M: mathcal{M}models E(m, s)}$ for some $sin{min M: mathcal{M}models S(m)}$. Conversely, each weak topological space can be viewed as a model of the theory above in the obvious way. So we have a dichotomy:
Literally being a weak topological space isn't the same as satisfying some set of first-order axioms (whereas being a ring is the same as being a structure which satisfies the set of first-order ring axioms), but
There is a set of first-order axioms, the class of whose models is equivalent to the class of weak topological spaces in a precise sense (there is a definable function between the two classes which is appropriately surjective and injective-up-to-isomorphism).
Finally, full topological spaces aren't even morally first-order: this is because of the infinite unions bit, which is fundamentally second-order. Instead, there is a set of second-order sentences such that the topological spaces are appropriately equivalent to the models of this set of sentences. Note, however, that in order to talk about satisfaction of second-order sentences we need to work in a more set-theoretic context than if we just care about satisfaction of first-order sentences, and set-theoretic issues are more relevant: for example, (your favorite set theory proves that) there is a second-order sentence which is true in every structure iff the continuum hypothesis holds!
EDIT: The key idea below is that definitions in an extension by definitions are essentially definitions in the original language already. Specifically, you can easily write a computer program that will convert a formula in a extension-by-definitions $L'$ of $L$ into a corresponding formula in $L$. So really, this all boils down to why the language of set theory has enough expansions-by-definitions, and this is provided pretty quickly by playing with the language (e.g. discover how to express "function," "sequence," "relation," "Cartesian product").
I'll do two examples (topological spaces and groups), and hopefully this will indicate why this stuff isn't usually done explicitly - it's very straightforward and quite tedious.
Topological spaces.
Usual definition: A topological space is an ordered pair $(X, tau)$ where $X$ is a set, $tau$ is a set of subsets of $X$, and $tau$ is closed under finite intersections, arbitrary unions, and contains $X$ and $emptyset$.
Formal definition in the language of set theory: $varphi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$bsubseteqmathcal{P}(a)$;
$forall ssubseteq bexists cin b(c=bigcup s)$;
$forall ssubseteq_{finite} bexists cin bforall y(yin ciff forall z(zin simplies yin z))$;
$ain b, emptysetin b$].
I've used symbols not explicitly in the language of set theory above - namely, $langlecdot,cdot rangle$, $subseteq$, $bigcup$, $subseteq_{finite}$, $emptyset$. But it's an easy exercise to get rid of these, and get a formula using only "$in$." But given that the translation is completely straightforward, I'm not sure what value this provides.
Groups.
Usual definition: A set with a binary operation satisfying [stuff].
Formal definition in the language of set theory: $psi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$b$ is a binary function on $a$
[stuff].
Remember that functions, and Cartesian products, are elementary to define in the language of set theory; and so everything here is easy to write down.
One of the values of set theory is that concepts in mathematics translate without effort into the language of set theory. That said, they also translate tediously, so an argument can be made that we should use something other than ZFC; but this is why you don't see these kinds of definitions written out in full.
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right?
– Sergei Akbarov
Jun 15 '17 at 16:16
1
@SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd)
– Noah Schweber
Jun 15 '17 at 16:28
It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $Msubseteq N$ such that $N$ thinks $M$ is transitive but there is some set $rin M$ such that $M$ thinks $r$ is a topological space (that is, $Mmodelsvarphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd)
– Noah Schweber
Jun 15 '17 at 16:31
Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $Msubseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology.
– Noah Schweber
Jun 15 '17 at 16:32
Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"?
– Sergei Akbarov
Jun 15 '17 at 17:04
|
show 1 more comment
EDIT: Based on the comments, I think this more accurately answers the OP's question:
The axioms for rings are actually first-order - and we say they constitute a first-order theory! Basically, I can write down the ring axioms as first-order sentences in the language ${+, times,0, 1}$, and then rings are the same as models of this set of axioms. These models, of course, are sets, and so we can only talk about them directly in general inside a theory of sets; but the set of axioms itself is first-order. (And note that we can still talk about the theory of rings, and deductions from that theory, in a theory without sets like PA.)
The same is true for groups, fields, etc. The same is also essentially true, incidentally, for "weak topological spaces" (I don't know what these are actually called): say a weak topological space is a set $X$ together with a family $tau$ of subsets of $X$ containing $X$ and $emptyset$ and closed under finite unions and finite intersections. Then consider the language ${E, P, S}$, with a single binary relation $E$ and two unary relations $P, S$. Intuitively, $P$ refers to points, $S$ refers to sets (of points), and $E$ refers to membership. Now consider the following set of first-order sentences:
$forall x((P(x)vee S(x))wedgeneg(P(x)wedge S(x)))$. The only things in our structure are points or sets, and these are disjoint from each other.
$forall x, y(E(x, y)implies P(x), S(y))$. Membership is a relation between points and sets, only.
$forall x, y(S(x), S(y), forall z(E(z, x)iff E(z, y))implies x=y)$. Sets with the same elements are the same.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)wedge E(w, y)))).$ Intersection of two sets (hence finitely many sets is a set.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)vee E(w, y)))).$ Finite unions.
A model of these axioms isn't necessarily literally a weak topological space - the $S$-elements might not actually be sets of $P$-elements - but they can be canonically identified with weak topological spaces: given a model $mathcal{M}=(M; P^M, S^M, E^M)$, we can assign it a weak topological space $T_mathcal{M}$ with underlying set ${min M: mathcal{M}models P^M}$ and "open sets" exactly those of the form ${min M: mathcal{M}models E(m, s)}$ for some $sin{min M: mathcal{M}models S(m)}$. Conversely, each weak topological space can be viewed as a model of the theory above in the obvious way. So we have a dichotomy:
Literally being a weak topological space isn't the same as satisfying some set of first-order axioms (whereas being a ring is the same as being a structure which satisfies the set of first-order ring axioms), but
There is a set of first-order axioms, the class of whose models is equivalent to the class of weak topological spaces in a precise sense (there is a definable function between the two classes which is appropriately surjective and injective-up-to-isomorphism).
Finally, full topological spaces aren't even morally first-order: this is because of the infinite unions bit, which is fundamentally second-order. Instead, there is a set of second-order sentences such that the topological spaces are appropriately equivalent to the models of this set of sentences. Note, however, that in order to talk about satisfaction of second-order sentences we need to work in a more set-theoretic context than if we just care about satisfaction of first-order sentences, and set-theoretic issues are more relevant: for example, (your favorite set theory proves that) there is a second-order sentence which is true in every structure iff the continuum hypothesis holds!
EDIT: The key idea below is that definitions in an extension by definitions are essentially definitions in the original language already. Specifically, you can easily write a computer program that will convert a formula in a extension-by-definitions $L'$ of $L$ into a corresponding formula in $L$. So really, this all boils down to why the language of set theory has enough expansions-by-definitions, and this is provided pretty quickly by playing with the language (e.g. discover how to express "function," "sequence," "relation," "Cartesian product").
I'll do two examples (topological spaces and groups), and hopefully this will indicate why this stuff isn't usually done explicitly - it's very straightforward and quite tedious.
Topological spaces.
Usual definition: A topological space is an ordered pair $(X, tau)$ where $X$ is a set, $tau$ is a set of subsets of $X$, and $tau$ is closed under finite intersections, arbitrary unions, and contains $X$ and $emptyset$.
Formal definition in the language of set theory: $varphi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$bsubseteqmathcal{P}(a)$;
$forall ssubseteq bexists cin b(c=bigcup s)$;
$forall ssubseteq_{finite} bexists cin bforall y(yin ciff forall z(zin simplies yin z))$;
$ain b, emptysetin b$].
I've used symbols not explicitly in the language of set theory above - namely, $langlecdot,cdot rangle$, $subseteq$, $bigcup$, $subseteq_{finite}$, $emptyset$. But it's an easy exercise to get rid of these, and get a formula using only "$in$." But given that the translation is completely straightforward, I'm not sure what value this provides.
Groups.
Usual definition: A set with a binary operation satisfying [stuff].
Formal definition in the language of set theory: $psi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$b$ is a binary function on $a$
[stuff].
Remember that functions, and Cartesian products, are elementary to define in the language of set theory; and so everything here is easy to write down.
One of the values of set theory is that concepts in mathematics translate without effort into the language of set theory. That said, they also translate tediously, so an argument can be made that we should use something other than ZFC; but this is why you don't see these kinds of definitions written out in full.
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
EDIT: Based on the comments, I think this more accurately answers the OP's question:
The axioms for rings are actually first-order - and we say they constitute a first-order theory! Basically, I can write down the ring axioms as first-order sentences in the language ${+, times,0, 1}$, and then rings are the same as models of this set of axioms. These models, of course, are sets, and so we can only talk about them directly in general inside a theory of sets; but the set of axioms itself is first-order. (And note that we can still talk about the theory of rings, and deductions from that theory, in a theory without sets like PA.)
The same is true for groups, fields, etc. The same is also essentially true, incidentally, for "weak topological spaces" (I don't know what these are actually called): say a weak topological space is a set $X$ together with a family $tau$ of subsets of $X$ containing $X$ and $emptyset$ and closed under finite unions and finite intersections. Then consider the language ${E, P, S}$, with a single binary relation $E$ and two unary relations $P, S$. Intuitively, $P$ refers to points, $S$ refers to sets (of points), and $E$ refers to membership. Now consider the following set of first-order sentences:
$forall x((P(x)vee S(x))wedgeneg(P(x)wedge S(x)))$. The only things in our structure are points or sets, and these are disjoint from each other.
$forall x, y(E(x, y)implies P(x), S(y))$. Membership is a relation between points and sets, only.
$forall x, y(S(x), S(y), forall z(E(z, x)iff E(z, y))implies x=y)$. Sets with the same elements are the same.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)wedge E(w, y)))).$ Intersection of two sets (hence finitely many sets is a set.
$forall x, y(S(x), S(y)implies exists z(S(z)wedgeforall w(E(w, z)iff E(w, x)vee E(w, y)))).$ Finite unions.
A model of these axioms isn't necessarily literally a weak topological space - the $S$-elements might not actually be sets of $P$-elements - but they can be canonically identified with weak topological spaces: given a model $mathcal{M}=(M; P^M, S^M, E^M)$, we can assign it a weak topological space $T_mathcal{M}$ with underlying set ${min M: mathcal{M}models P^M}$ and "open sets" exactly those of the form ${min M: mathcal{M}models E(m, s)}$ for some $sin{min M: mathcal{M}models S(m)}$. Conversely, each weak topological space can be viewed as a model of the theory above in the obvious way. So we have a dichotomy:
Literally being a weak topological space isn't the same as satisfying some set of first-order axioms (whereas being a ring is the same as being a structure which satisfies the set of first-order ring axioms), but
There is a set of first-order axioms, the class of whose models is equivalent to the class of weak topological spaces in a precise sense (there is a definable function between the two classes which is appropriately surjective and injective-up-to-isomorphism).
Finally, full topological spaces aren't even morally first-order: this is because of the infinite unions bit, which is fundamentally second-order. Instead, there is a set of second-order sentences such that the topological spaces are appropriately equivalent to the models of this set of sentences. Note, however, that in order to talk about satisfaction of second-order sentences we need to work in a more set-theoretic context than if we just care about satisfaction of first-order sentences, and set-theoretic issues are more relevant: for example, (your favorite set theory proves that) there is a second-order sentence which is true in every structure iff the continuum hypothesis holds!
EDIT: The key idea below is that definitions in an extension by definitions are essentially definitions in the original language already. Specifically, you can easily write a computer program that will convert a formula in a extension-by-definitions $L'$ of $L$ into a corresponding formula in $L$. So really, this all boils down to why the language of set theory has enough expansions-by-definitions, and this is provided pretty quickly by playing with the language (e.g. discover how to express "function," "sequence," "relation," "Cartesian product").
I'll do two examples (topological spaces and groups), and hopefully this will indicate why this stuff isn't usually done explicitly - it's very straightforward and quite tedious.
Topological spaces.
Usual definition: A topological space is an ordered pair $(X, tau)$ where $X$ is a set, $tau$ is a set of subsets of $X$, and $tau$ is closed under finite intersections, arbitrary unions, and contains $X$ and $emptyset$.
Formal definition in the language of set theory: $varphi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$bsubseteqmathcal{P}(a)$;
$forall ssubseteq bexists cin b(c=bigcup s)$;
$forall ssubseteq_{finite} bexists cin bforall y(yin ciff forall z(zin simplies yin z))$;
$ain b, emptysetin b$].
I've used symbols not explicitly in the language of set theory above - namely, $langlecdot,cdot rangle$, $subseteq$, $bigcup$, $subseteq_{finite}$, $emptyset$. But it's an easy exercise to get rid of these, and get a formula using only "$in$." But given that the translation is completely straightforward, I'm not sure what value this provides.
Groups.
Usual definition: A set with a binary operation satisfying [stuff].
Formal definition in the language of set theory: $psi(x)$ is the formula, in the language of set theory, expressing:
$exists a, b[x=langle a, brangle$ and
$b$ is a binary function on $a$
[stuff].
Remember that functions, and Cartesian products, are elementary to define in the language of set theory; and so everything here is easy to write down.
One of the values of set theory is that concepts in mathematics translate without effort into the language of set theory. That said, they also translate tediously, so an argument can be made that we should use something other than ZFC; but this is why you don't see these kinds of definitions written out in full.
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
edited Jun 15 '17 at 18:53
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
answered Jun 15 '17 at 16:06
Noah Schweber
122k10148284
122k10148284
Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right?
– Sergei Akbarov
Jun 15 '17 at 16:16
1
@SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd)
– Noah Schweber
Jun 15 '17 at 16:28
It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $Msubseteq N$ such that $N$ thinks $M$ is transitive but there is some set $rin M$ such that $M$ thinks $r$ is a topological space (that is, $Mmodelsvarphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd)
– Noah Schweber
Jun 15 '17 at 16:31
Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $Msubseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology.
– Noah Schweber
Jun 15 '17 at 16:32
Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"?
– Sergei Akbarov
Jun 15 '17 at 17:04
|
show 1 more comment
Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right?
– Sergei Akbarov
Jun 15 '17 at 16:16
1
@SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd)
– Noah Schweber
Jun 15 '17 at 16:28
It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $Msubseteq N$ such that $N$ thinks $M$ is transitive but there is some set $rin M$ such that $M$ thinks $r$ is a topological space (that is, $Mmodelsvarphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd)
– Noah Schweber
Jun 15 '17 at 16:31
Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $Msubseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology.
– Noah Schweber
Jun 15 '17 at 16:32
Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"?
– Sergei Akbarov
Jun 15 '17 at 17:04
Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right?
– Sergei Akbarov
Jun 15 '17 at 16:16
Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right?
– Sergei Akbarov
Jun 15 '17 at 16:16
1
1
@SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd)
– Noah Schweber
Jun 15 '17 at 16:28
@SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd)
– Noah Schweber
Jun 15 '17 at 16:28
It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $Msubseteq N$ such that $N$ thinks $M$ is transitive but there is some set $rin M$ such that $M$ thinks $r$ is a topological space (that is, $Mmodelsvarphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd)
– Noah Schweber
Jun 15 '17 at 16:31
It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $Msubseteq N$ such that $N$ thinks $M$ is transitive but there is some set $rin M$ such that $M$ thinks $r$ is a topological space (that is, $Mmodelsvarphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd)
– Noah Schweber
Jun 15 '17 at 16:31
Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $Msubseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology.
– Noah Schweber
Jun 15 '17 at 16:32
Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $Msubseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology.
– Noah Schweber
Jun 15 '17 at 16:32
Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"?
– Sergei Akbarov
Jun 15 '17 at 17:04
Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"?
– Sergei Akbarov
Jun 15 '17 at 17:04
|
show 1 more comment
Generally mathematicians when doing mathematics (like topology, probability or geometry) do that in the framework of set theory.
This means that they introduce some definitions (topology, $sigma$-algebras, points etc) in terms of sets and provide proofs of facts about these objects using properties of sets.
Formally what mathematicians do is take ZFC theory add new symbols to the language (for instance predicates like "is a topology", "is a topological space", "is a continuous function" and so on) and then axiomatically define these predicates in terms of formulas in the language of ZFC, that is they add some axioms of the form
$$x text{ is a topology} iff varphi(x)$$
$$x text{ is a topological space} iff varphi'(x)$$
$$dots$$
where the formulas $varphi(x)$, $varphi'(x)$ etc are ZFC formulas.
In this way they can reduce any proof about the new introduced objects (toplogical spaces, geometric figures etc) to a proof about sets, that is a proof that ultimately relies on the axioms of ZFC+the definitional axioms for the new predicates.
On the other hand in principle one could try to look at the formal systems you listed as some logical systems on their own.
For instance Hilber's system for euclidean geometry can be easily seen as a first-order theory, as it is basically shown in the wikipedia link you gave.
The other systems you listed could be seen as formal systems for an higher-order logic, but you have to go at least third order because in these systems you would need to quantify over families of subsets (that is over families of predicates, or predicates of predicates).
If you like I could add the details, at least for one of the systems.
Let me know if you need any additional clarification.
Hope this helps.
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
1
Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory.
– Sergei Akbarov
Jun 15 '17 at 15:24
add a comment |
Generally mathematicians when doing mathematics (like topology, probability or geometry) do that in the framework of set theory.
This means that they introduce some definitions (topology, $sigma$-algebras, points etc) in terms of sets and provide proofs of facts about these objects using properties of sets.
Formally what mathematicians do is take ZFC theory add new symbols to the language (for instance predicates like "is a topology", "is a topological space", "is a continuous function" and so on) and then axiomatically define these predicates in terms of formulas in the language of ZFC, that is they add some axioms of the form
$$x text{ is a topology} iff varphi(x)$$
$$x text{ is a topological space} iff varphi'(x)$$
$$dots$$
where the formulas $varphi(x)$, $varphi'(x)$ etc are ZFC formulas.
In this way they can reduce any proof about the new introduced objects (toplogical spaces, geometric figures etc) to a proof about sets, that is a proof that ultimately relies on the axioms of ZFC+the definitional axioms for the new predicates.
On the other hand in principle one could try to look at the formal systems you listed as some logical systems on their own.
For instance Hilber's system for euclidean geometry can be easily seen as a first-order theory, as it is basically shown in the wikipedia link you gave.
The other systems you listed could be seen as formal systems for an higher-order logic, but you have to go at least third order because in these systems you would need to quantify over families of subsets (that is over families of predicates, or predicates of predicates).
If you like I could add the details, at least for one of the systems.
Let me know if you need any additional clarification.
Hope this helps.
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
1
Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory.
– Sergei Akbarov
Jun 15 '17 at 15:24
add a comment |
Generally mathematicians when doing mathematics (like topology, probability or geometry) do that in the framework of set theory.
This means that they introduce some definitions (topology, $sigma$-algebras, points etc) in terms of sets and provide proofs of facts about these objects using properties of sets.
Formally what mathematicians do is take ZFC theory add new symbols to the language (for instance predicates like "is a topology", "is a topological space", "is a continuous function" and so on) and then axiomatically define these predicates in terms of formulas in the language of ZFC, that is they add some axioms of the form
$$x text{ is a topology} iff varphi(x)$$
$$x text{ is a topological space} iff varphi'(x)$$
$$dots$$
where the formulas $varphi(x)$, $varphi'(x)$ etc are ZFC formulas.
In this way they can reduce any proof about the new introduced objects (toplogical spaces, geometric figures etc) to a proof about sets, that is a proof that ultimately relies on the axioms of ZFC+the definitional axioms for the new predicates.
On the other hand in principle one could try to look at the formal systems you listed as some logical systems on their own.
For instance Hilber's system for euclidean geometry can be easily seen as a first-order theory, as it is basically shown in the wikipedia link you gave.
The other systems you listed could be seen as formal systems for an higher-order logic, but you have to go at least third order because in these systems you would need to quantify over families of subsets (that is over families of predicates, or predicates of predicates).
If you like I could add the details, at least for one of the systems.
Let me know if you need any additional clarification.
Hope this helps.
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
Generally mathematicians when doing mathematics (like topology, probability or geometry) do that in the framework of set theory.
This means that they introduce some definitions (topology, $sigma$-algebras, points etc) in terms of sets and provide proofs of facts about these objects using properties of sets.
Formally what mathematicians do is take ZFC theory add new symbols to the language (for instance predicates like "is a topology", "is a topological space", "is a continuous function" and so on) and then axiomatically define these predicates in terms of formulas in the language of ZFC, that is they add some axioms of the form
$$x text{ is a topology} iff varphi(x)$$
$$x text{ is a topological space} iff varphi'(x)$$
$$dots$$
where the formulas $varphi(x)$, $varphi'(x)$ etc are ZFC formulas.
In this way they can reduce any proof about the new introduced objects (toplogical spaces, geometric figures etc) to a proof about sets, that is a proof that ultimately relies on the axioms of ZFC+the definitional axioms for the new predicates.
On the other hand in principle one could try to look at the formal systems you listed as some logical systems on their own.
For instance Hilber's system for euclidean geometry can be easily seen as a first-order theory, as it is basically shown in the wikipedia link you gave.
The other systems you listed could be seen as formal systems for an higher-order logic, but you have to go at least third order because in these systems you would need to quantify over families of subsets (that is over families of predicates, or predicates of predicates).
If you like I could add the details, at least for one of the systems.
Let me know if you need any additional clarification.
Hope this helps.
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
edited Nov 21 '18 at 10:34
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
answered Jun 15 '17 at 10:32
Giorgio Mossa
13.9k11749
13.9k11749
1
Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory.
– Sergei Akbarov
Jun 15 '17 at 15:24
add a comment |
1
Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory.
– Sergei Akbarov
Jun 15 '17 at 15:24
1
1
Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory.
– Sergei Akbarov
Jun 15 '17 at 15:24
Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory.
– Sergei Akbarov
Jun 15 '17 at 15:24
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2323458%2ftwo-types-of-axiomatic-theories-in-mathematics%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
"these are not formal theories in first order logic." If the axiom ssytem (like e.g.that of probability theory) is "written" in the language of $mathsf {ZF}$ set thoery (or similar) it is first-order.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:19
What define univocally "to be first-order" or not is the language: if quantification is allowed only on individual variables, then it is FO. $mathsf {ZF(C)}$ as well as $mathsf {NBG}$ are FO.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:20
Hilbert's axioms system is Second-Order: see "Axiom of completeness. To a system of points, straight lines, and planes, ..." there is a (universal) quantification on "system of points".
– Mauro ALLEGRANZA
Jun 15 '17 at 9:22
See Tarski's axioms (1959) for a system of axioms for elementary geometry that is formulated in first-order logic with identity, and requiring no set theory.
– Mauro ALLEGRANZA
Jun 15 '17 at 9:24
Mauro, I know about Tarski, and I also (like you) think that it is possible to somehow translate everything into a first order language, but before this is done the picture looks differently (and besides this I don't believe that this translation will always be easy). So I wonder if this construction has a reasonable description inside set theory.
– Sergei Akbarov
Jun 15 '17 at 9:26