What's the difference between a logic, an internal logic (language) of a category, an internal logic of a...
maybe this question doesn't make sense at all. I don't know exactly the meaning of all these concepts, except the internal language of a topos (and searching on the literature is not helping at all).
However, vaguely speaking by a logic I mean a pair $(Sigma, vdash)$ where $Sigma$ is a signature (it has the types, functionals and relational symbols) and a consequence operator $vdash$.
By an internal logic in a category I mean viewing each object as a type and each morphism as a term.
So what's the difference between a logic, an internal logic (language) of a category, an internal logic (language) of a topos and a type theory? Furthermore why the interchanging in the literature between the word "logic" and "language" when dealing with the internal properties of a category? Moreover, how higher order logic, modal logic and fuzzy logic suit in these concepts stated above?
Thanks in advance.
logic category-theory formal-languages topos-theory categorical-logic
add a comment |
maybe this question doesn't make sense at all. I don't know exactly the meaning of all these concepts, except the internal language of a topos (and searching on the literature is not helping at all).
However, vaguely speaking by a logic I mean a pair $(Sigma, vdash)$ where $Sigma$ is a signature (it has the types, functionals and relational symbols) and a consequence operator $vdash$.
By an internal logic in a category I mean viewing each object as a type and each morphism as a term.
So what's the difference between a logic, an internal logic (language) of a category, an internal logic (language) of a topos and a type theory? Furthermore why the interchanging in the literature between the word "logic" and "language" when dealing with the internal properties of a category? Moreover, how higher order logic, modal logic and fuzzy logic suit in these concepts stated above?
Thanks in advance.
logic category-theory formal-languages topos-theory categorical-logic
add a comment |
maybe this question doesn't make sense at all. I don't know exactly the meaning of all these concepts, except the internal language of a topos (and searching on the literature is not helping at all).
However, vaguely speaking by a logic I mean a pair $(Sigma, vdash)$ where $Sigma$ is a signature (it has the types, functionals and relational symbols) and a consequence operator $vdash$.
By an internal logic in a category I mean viewing each object as a type and each morphism as a term.
So what's the difference between a logic, an internal logic (language) of a category, an internal logic (language) of a topos and a type theory? Furthermore why the interchanging in the literature between the word "logic" and "language" when dealing with the internal properties of a category? Moreover, how higher order logic, modal logic and fuzzy logic suit in these concepts stated above?
Thanks in advance.
logic category-theory formal-languages topos-theory categorical-logic
maybe this question doesn't make sense at all. I don't know exactly the meaning of all these concepts, except the internal language of a topos (and searching on the literature is not helping at all).
However, vaguely speaking by a logic I mean a pair $(Sigma, vdash)$ where $Sigma$ is a signature (it has the types, functionals and relational symbols) and a consequence operator $vdash$.
By an internal logic in a category I mean viewing each object as a type and each morphism as a term.
So what's the difference between a logic, an internal logic (language) of a category, an internal logic (language) of a topos and a type theory? Furthermore why the interchanging in the literature between the word "logic" and "language" when dealing with the internal properties of a category? Moreover, how higher order logic, modal logic and fuzzy logic suit in these concepts stated above?
Thanks in advance.
logic category-theory formal-languages topos-theory categorical-logic
logic category-theory formal-languages topos-theory categorical-logic
edited Dec 19 '16 at 20:22
Hanul Jeon
17.4k42780
17.4k42780
asked Aug 15 '14 at 7:48
user40276
2,3561130
2,3561130
add a comment |
add a comment |
2 Answers
2
active
oldest
votes
The internal logic of a topos is an instance of the internal logic of a category (since toposes are special kinds of categories). The internal logic of toposes (instead of an arbitrary category) can also be interpreted with the Kripke-Joyal semantics. For more on this, check part D of Johnstone's Elephant and chapter VI of Mac Lane's and Moerdijk's Sheaves in Geometry and Logic, lecture notes by Thomas Streicher, and of course the nLab articles on these matters.
I don't know the term "internal logic of a type theory". But check the (very accessible) introduction of the HoTT book on how type theory and logic are related.
The terms "internal logic" and "internal language" are often used synonymously. Personally, I prefer "internal language", since this stresses that one can use it not only to reason internally, but also to construct objects and morphisms internally.
The internal language of a topos $mathcal{E}$ is higher-order in the sense that, because of the existence of a subobject classifier, every object $X in mathcal{E}$ has an associated power object $mathcal{P}(X) in mathcal{E}$ which one can quantify over in the internal language. (In the special case $mathcal{E} = mathrm{Set}$, the internal language is really the same as the usual mathematical language and $mathcal{P}(X)$ is simply the power set of $X$.) In an arbitrary category, power objects need not exist, such that their internal language is (at best) first-order. Generally, richer categorical properties allow you to interpret greater fragments of first-order logic, this is neatly explained in Johnstone's part D.
Any Lawvere-Tierney topology in a topos gives rise to a modal operator in its associated internal language. (These operators can have concrete geometric meanings, for instance "on a dense open set it holds that" or "on an open neighbourhood of a point $x$ it holds that".)
I don't know of a direct relationship between fuzzy logic and the internal language of toposes, see an older question here.
On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure).
– Andreas Blass
Aug 15 '14 at 21:55
Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories.
– user40276
Aug 16 '14 at 1:30
@user40276: I'm not quite sure whether I understand you correctly. Let $mathcal{C}$ be a category. Then the signature induced by $mathcal{C}$ has all objects of $mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course.
– Ingo Blechschmidt
Aug 21 '14 at 11:05
1
Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic?
– user40276
Aug 21 '14 at 12:49
1
Yes, you are right that a predicate symbol would be a subobject.
– Ingo Blechschmidt
Nov 3 '14 at 14:28
|
show 1 more comment
Your definition of logic is pretty much correct. A logic contains both the language which the signature $Sigma$ generates and the deductive system defined by $vdash$.
A type theory is a logic with different sorts of individuals (called "types") and constructions that generate new types from existing ones, like product and arrow types.
An internal logic is a type theory derived from a category and the internal language is the language part of that logic. Specifically, the atomic sorts of the internal language are the objects of the category. Since a topos is a specific category of categories, the internal logic of a topos is the derived type theory.
The modalities of modal logic can sometimes be related to operators on subobjects in a category, but only if they preserve logical equivalence: $alphaiffbeta$ should imply $Boxalpha iff Box beta$. Otherwise, the induced function of subobjects is not well-defined.
Fuzzy logic is misnamed. It is more like a model theory than a logic.
Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $forall$ and $exists$ as adjoint functors.
– user40276
Aug 22 '14 at 16:55
1
Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much.
– Malice Vidrine
Aug 23 '14 at 0:46
2
Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products.
– Wouter Stekelenburg
Aug 23 '14 at 7:41
So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature.
– user40276
Aug 26 '14 at 17:14
1
@user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $Lto C$ that reflects equivalences of categories.
– Wouter Stekelenburg
Aug 28 '14 at 8:32
|
show 2 more comments
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%2f898062%2fwhats-the-difference-between-a-logic-an-internal-logic-language-of-a-categor%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
The internal logic of a topos is an instance of the internal logic of a category (since toposes are special kinds of categories). The internal logic of toposes (instead of an arbitrary category) can also be interpreted with the Kripke-Joyal semantics. For more on this, check part D of Johnstone's Elephant and chapter VI of Mac Lane's and Moerdijk's Sheaves in Geometry and Logic, lecture notes by Thomas Streicher, and of course the nLab articles on these matters.
I don't know the term "internal logic of a type theory". But check the (very accessible) introduction of the HoTT book on how type theory and logic are related.
The terms "internal logic" and "internal language" are often used synonymously. Personally, I prefer "internal language", since this stresses that one can use it not only to reason internally, but also to construct objects and morphisms internally.
The internal language of a topos $mathcal{E}$ is higher-order in the sense that, because of the existence of a subobject classifier, every object $X in mathcal{E}$ has an associated power object $mathcal{P}(X) in mathcal{E}$ which one can quantify over in the internal language. (In the special case $mathcal{E} = mathrm{Set}$, the internal language is really the same as the usual mathematical language and $mathcal{P}(X)$ is simply the power set of $X$.) In an arbitrary category, power objects need not exist, such that their internal language is (at best) first-order. Generally, richer categorical properties allow you to interpret greater fragments of first-order logic, this is neatly explained in Johnstone's part D.
Any Lawvere-Tierney topology in a topos gives rise to a modal operator in its associated internal language. (These operators can have concrete geometric meanings, for instance "on a dense open set it holds that" or "on an open neighbourhood of a point $x$ it holds that".)
I don't know of a direct relationship between fuzzy logic and the internal language of toposes, see an older question here.
On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure).
– Andreas Blass
Aug 15 '14 at 21:55
Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories.
– user40276
Aug 16 '14 at 1:30
@user40276: I'm not quite sure whether I understand you correctly. Let $mathcal{C}$ be a category. Then the signature induced by $mathcal{C}$ has all objects of $mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course.
– Ingo Blechschmidt
Aug 21 '14 at 11:05
1
Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic?
– user40276
Aug 21 '14 at 12:49
1
Yes, you are right that a predicate symbol would be a subobject.
– Ingo Blechschmidt
Nov 3 '14 at 14:28
|
show 1 more comment
The internal logic of a topos is an instance of the internal logic of a category (since toposes are special kinds of categories). The internal logic of toposes (instead of an arbitrary category) can also be interpreted with the Kripke-Joyal semantics. For more on this, check part D of Johnstone's Elephant and chapter VI of Mac Lane's and Moerdijk's Sheaves in Geometry and Logic, lecture notes by Thomas Streicher, and of course the nLab articles on these matters.
I don't know the term "internal logic of a type theory". But check the (very accessible) introduction of the HoTT book on how type theory and logic are related.
The terms "internal logic" and "internal language" are often used synonymously. Personally, I prefer "internal language", since this stresses that one can use it not only to reason internally, but also to construct objects and morphisms internally.
The internal language of a topos $mathcal{E}$ is higher-order in the sense that, because of the existence of a subobject classifier, every object $X in mathcal{E}$ has an associated power object $mathcal{P}(X) in mathcal{E}$ which one can quantify over in the internal language. (In the special case $mathcal{E} = mathrm{Set}$, the internal language is really the same as the usual mathematical language and $mathcal{P}(X)$ is simply the power set of $X$.) In an arbitrary category, power objects need not exist, such that their internal language is (at best) first-order. Generally, richer categorical properties allow you to interpret greater fragments of first-order logic, this is neatly explained in Johnstone's part D.
Any Lawvere-Tierney topology in a topos gives rise to a modal operator in its associated internal language. (These operators can have concrete geometric meanings, for instance "on a dense open set it holds that" or "on an open neighbourhood of a point $x$ it holds that".)
I don't know of a direct relationship between fuzzy logic and the internal language of toposes, see an older question here.
On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure).
– Andreas Blass
Aug 15 '14 at 21:55
Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories.
– user40276
Aug 16 '14 at 1:30
@user40276: I'm not quite sure whether I understand you correctly. Let $mathcal{C}$ be a category. Then the signature induced by $mathcal{C}$ has all objects of $mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course.
– Ingo Blechschmidt
Aug 21 '14 at 11:05
1
Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic?
– user40276
Aug 21 '14 at 12:49
1
Yes, you are right that a predicate symbol would be a subobject.
– Ingo Blechschmidt
Nov 3 '14 at 14:28
|
show 1 more comment
The internal logic of a topos is an instance of the internal logic of a category (since toposes are special kinds of categories). The internal logic of toposes (instead of an arbitrary category) can also be interpreted with the Kripke-Joyal semantics. For more on this, check part D of Johnstone's Elephant and chapter VI of Mac Lane's and Moerdijk's Sheaves in Geometry and Logic, lecture notes by Thomas Streicher, and of course the nLab articles on these matters.
I don't know the term "internal logic of a type theory". But check the (very accessible) introduction of the HoTT book on how type theory and logic are related.
The terms "internal logic" and "internal language" are often used synonymously. Personally, I prefer "internal language", since this stresses that one can use it not only to reason internally, but also to construct objects and morphisms internally.
The internal language of a topos $mathcal{E}$ is higher-order in the sense that, because of the existence of a subobject classifier, every object $X in mathcal{E}$ has an associated power object $mathcal{P}(X) in mathcal{E}$ which one can quantify over in the internal language. (In the special case $mathcal{E} = mathrm{Set}$, the internal language is really the same as the usual mathematical language and $mathcal{P}(X)$ is simply the power set of $X$.) In an arbitrary category, power objects need not exist, such that their internal language is (at best) first-order. Generally, richer categorical properties allow you to interpret greater fragments of first-order logic, this is neatly explained in Johnstone's part D.
Any Lawvere-Tierney topology in a topos gives rise to a modal operator in its associated internal language. (These operators can have concrete geometric meanings, for instance "on a dense open set it holds that" or "on an open neighbourhood of a point $x$ it holds that".)
I don't know of a direct relationship between fuzzy logic and the internal language of toposes, see an older question here.
The internal logic of a topos is an instance of the internal logic of a category (since toposes are special kinds of categories). The internal logic of toposes (instead of an arbitrary category) can also be interpreted with the Kripke-Joyal semantics. For more on this, check part D of Johnstone's Elephant and chapter VI of Mac Lane's and Moerdijk's Sheaves in Geometry and Logic, lecture notes by Thomas Streicher, and of course the nLab articles on these matters.
I don't know the term "internal logic of a type theory". But check the (very accessible) introduction of the HoTT book on how type theory and logic are related.
The terms "internal logic" and "internal language" are often used synonymously. Personally, I prefer "internal language", since this stresses that one can use it not only to reason internally, but also to construct objects and morphisms internally.
The internal language of a topos $mathcal{E}$ is higher-order in the sense that, because of the existence of a subobject classifier, every object $X in mathcal{E}$ has an associated power object $mathcal{P}(X) in mathcal{E}$ which one can quantify over in the internal language. (In the special case $mathcal{E} = mathrm{Set}$, the internal language is really the same as the usual mathematical language and $mathcal{P}(X)$ is simply the power set of $X$.) In an arbitrary category, power objects need not exist, such that their internal language is (at best) first-order. Generally, richer categorical properties allow you to interpret greater fragments of first-order logic, this is neatly explained in Johnstone's part D.
Any Lawvere-Tierney topology in a topos gives rise to a modal operator in its associated internal language. (These operators can have concrete geometric meanings, for instance "on a dense open set it holds that" or "on an open neighbourhood of a point $x$ it holds that".)
I don't know of a direct relationship between fuzzy logic and the internal language of toposes, see an older question here.
edited Apr 13 '17 at 12:21
Community♦
1
1
answered Aug 15 '14 at 17:56
Ingo Blechschmidt
1,325715
1,325715
On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure).
– Andreas Blass
Aug 15 '14 at 21:55
Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories.
– user40276
Aug 16 '14 at 1:30
@user40276: I'm not quite sure whether I understand you correctly. Let $mathcal{C}$ be a category. Then the signature induced by $mathcal{C}$ has all objects of $mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course.
– Ingo Blechschmidt
Aug 21 '14 at 11:05
1
Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic?
– user40276
Aug 21 '14 at 12:49
1
Yes, you are right that a predicate symbol would be a subobject.
– Ingo Blechschmidt
Nov 3 '14 at 14:28
|
show 1 more comment
On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure).
– Andreas Blass
Aug 15 '14 at 21:55
Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories.
– user40276
Aug 16 '14 at 1:30
@user40276: I'm not quite sure whether I understand you correctly. Let $mathcal{C}$ be a category. Then the signature induced by $mathcal{C}$ has all objects of $mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course.
– Ingo Blechschmidt
Aug 21 '14 at 11:05
1
Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic?
– user40276
Aug 21 '14 at 12:49
1
Yes, you are right that a predicate symbol would be a subobject.
– Ingo Blechschmidt
Nov 3 '14 at 14:28
On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure).
– Andreas Blass
Aug 15 '14 at 21:55
On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure).
– Andreas Blass
Aug 15 '14 at 21:55
Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories.
– user40276
Aug 16 '14 at 1:30
Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories.
– user40276
Aug 16 '14 at 1:30
@user40276: I'm not quite sure whether I understand you correctly. Let $mathcal{C}$ be a category. Then the signature induced by $mathcal{C}$ has all objects of $mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course.
– Ingo Blechschmidt
Aug 21 '14 at 11:05
@user40276: I'm not quite sure whether I understand you correctly. Let $mathcal{C}$ be a category. Then the signature induced by $mathcal{C}$ has all objects of $mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course.
– Ingo Blechschmidt
Aug 21 '14 at 11:05
1
1
Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic?
– user40276
Aug 21 '14 at 12:49
Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic?
– user40276
Aug 21 '14 at 12:49
1
1
Yes, you are right that a predicate symbol would be a subobject.
– Ingo Blechschmidt
Nov 3 '14 at 14:28
Yes, you are right that a predicate symbol would be a subobject.
– Ingo Blechschmidt
Nov 3 '14 at 14:28
|
show 1 more comment
Your definition of logic is pretty much correct. A logic contains both the language which the signature $Sigma$ generates and the deductive system defined by $vdash$.
A type theory is a logic with different sorts of individuals (called "types") and constructions that generate new types from existing ones, like product and arrow types.
An internal logic is a type theory derived from a category and the internal language is the language part of that logic. Specifically, the atomic sorts of the internal language are the objects of the category. Since a topos is a specific category of categories, the internal logic of a topos is the derived type theory.
The modalities of modal logic can sometimes be related to operators on subobjects in a category, but only if they preserve logical equivalence: $alphaiffbeta$ should imply $Boxalpha iff Box beta$. Otherwise, the induced function of subobjects is not well-defined.
Fuzzy logic is misnamed. It is more like a model theory than a logic.
Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $forall$ and $exists$ as adjoint functors.
– user40276
Aug 22 '14 at 16:55
1
Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much.
– Malice Vidrine
Aug 23 '14 at 0:46
2
Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products.
– Wouter Stekelenburg
Aug 23 '14 at 7:41
So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature.
– user40276
Aug 26 '14 at 17:14
1
@user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $Lto C$ that reflects equivalences of categories.
– Wouter Stekelenburg
Aug 28 '14 at 8:32
|
show 2 more comments
Your definition of logic is pretty much correct. A logic contains both the language which the signature $Sigma$ generates and the deductive system defined by $vdash$.
A type theory is a logic with different sorts of individuals (called "types") and constructions that generate new types from existing ones, like product and arrow types.
An internal logic is a type theory derived from a category and the internal language is the language part of that logic. Specifically, the atomic sorts of the internal language are the objects of the category. Since a topos is a specific category of categories, the internal logic of a topos is the derived type theory.
The modalities of modal logic can sometimes be related to operators on subobjects in a category, but only if they preserve logical equivalence: $alphaiffbeta$ should imply $Boxalpha iff Box beta$. Otherwise, the induced function of subobjects is not well-defined.
Fuzzy logic is misnamed. It is more like a model theory than a logic.
Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $forall$ and $exists$ as adjoint functors.
– user40276
Aug 22 '14 at 16:55
1
Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much.
– Malice Vidrine
Aug 23 '14 at 0:46
2
Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products.
– Wouter Stekelenburg
Aug 23 '14 at 7:41
So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature.
– user40276
Aug 26 '14 at 17:14
1
@user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $Lto C$ that reflects equivalences of categories.
– Wouter Stekelenburg
Aug 28 '14 at 8:32
|
show 2 more comments
Your definition of logic is pretty much correct. A logic contains both the language which the signature $Sigma$ generates and the deductive system defined by $vdash$.
A type theory is a logic with different sorts of individuals (called "types") and constructions that generate new types from existing ones, like product and arrow types.
An internal logic is a type theory derived from a category and the internal language is the language part of that logic. Specifically, the atomic sorts of the internal language are the objects of the category. Since a topos is a specific category of categories, the internal logic of a topos is the derived type theory.
The modalities of modal logic can sometimes be related to operators on subobjects in a category, but only if they preserve logical equivalence: $alphaiffbeta$ should imply $Boxalpha iff Box beta$. Otherwise, the induced function of subobjects is not well-defined.
Fuzzy logic is misnamed. It is more like a model theory than a logic.
Your definition of logic is pretty much correct. A logic contains both the language which the signature $Sigma$ generates and the deductive system defined by $vdash$.
A type theory is a logic with different sorts of individuals (called "types") and constructions that generate new types from existing ones, like product and arrow types.
An internal logic is a type theory derived from a category and the internal language is the language part of that logic. Specifically, the atomic sorts of the internal language are the objects of the category. Since a topos is a specific category of categories, the internal logic of a topos is the derived type theory.
The modalities of modal logic can sometimes be related to operators on subobjects in a category, but only if they preserve logical equivalence: $alphaiffbeta$ should imply $Boxalpha iff Box beta$. Otherwise, the induced function of subobjects is not well-defined.
Fuzzy logic is misnamed. It is more like a model theory than a logic.
edited Nov 25 at 18:35
answered Aug 22 '14 at 15:12
Wouter Stekelenburg
1,016612
1,016612
Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $forall$ and $exists$ as adjoint functors.
– user40276
Aug 22 '14 at 16:55
1
Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much.
– Malice Vidrine
Aug 23 '14 at 0:46
2
Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products.
– Wouter Stekelenburg
Aug 23 '14 at 7:41
So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature.
– user40276
Aug 26 '14 at 17:14
1
@user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $Lto C$ that reflects equivalences of categories.
– Wouter Stekelenburg
Aug 28 '14 at 8:32
|
show 2 more comments
Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $forall$ and $exists$ as adjoint functors.
– user40276
Aug 22 '14 at 16:55
1
Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much.
– Malice Vidrine
Aug 23 '14 at 0:46
2
Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products.
– Wouter Stekelenburg
Aug 23 '14 at 7:41
So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature.
– user40276
Aug 26 '14 at 17:14
1
@user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $Lto C$ that reflects equivalences of categories.
– Wouter Stekelenburg
Aug 28 '14 at 8:32
Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $forall$ and $exists$ as adjoint functors.
– user40276
Aug 22 '14 at 16:55
Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $forall$ and $exists$ as adjoint functors.
– user40276
Aug 22 '14 at 16:55
1
1
Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much.
– Malice Vidrine
Aug 23 '14 at 0:46
Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much.
– Malice Vidrine
Aug 23 '14 at 0:46
2
2
Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products.
– Wouter Stekelenburg
Aug 23 '14 at 7:41
Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products.
– Wouter Stekelenburg
Aug 23 '14 at 7:41
So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature.
– user40276
Aug 26 '14 at 17:14
So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature.
– user40276
Aug 26 '14 at 17:14
1
1
@user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $Lto C$ that reflects equivalences of categories.
– Wouter Stekelenburg
Aug 28 '14 at 8:32
@user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $Lto C$ that reflects equivalences of categories.
– Wouter Stekelenburg
Aug 28 '14 at 8:32
|
show 2 more comments
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%2f898062%2fwhats-the-difference-between-a-logic-an-internal-logic-language-of-a-categor%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