Does “every” first-order theory have a finitely axiomatizable conservative extension?first-order definability transitive closure operatorIs theory with domain of interpretation in second order objects a First Order Theory?Is non-connectedness of graphs first order axiomatizable?Can ZFC → NBG be iterated?Is Robinson Arithmetic biinterpretable with some theory in LST?Are there any complete, first-order and unstable theories which have non-categorical second-order formulations?Theorems on sets provable in KM but not in ZFC set theoryCan we have more malleable proper classes without sacrificing conservativity?Question about the consistency of assuming (via axiom) that $kappa < nu$ for certain pairs of cardinal numbers provably satisfying $kappa leq nu$Do the analogies between metamathematics of set theory and arithmetic have some deeper meaning?
Does “every” first-order theory have a finitely axiomatizable conservative extension?
first-order definability transitive closure operatorIs theory with domain of interpretation in second order objects a First Order Theory?Is non-connectedness of graphs first order axiomatizable?Can ZFC → NBG be iterated?Is Robinson Arithmetic biinterpretable with some theory in LST?Are there any complete, first-order and unstable theories which have non-categorical second-order formulations?Theorems on sets provable in KM but not in ZFC set theoryCan we have more malleable proper classes without sacrificing conservativity?Question about the consistency of assuming (via axiom) that $kappa < nu$ for certain pairs of cardinal numbers provably satisfying $kappa leq nu$Do the analogies between metamathematics of set theory and arithmetic have some deeper meaning?
$begingroup$
I originally asked this question on math.stackexchange.com here.
There's a famous theorem (due to Montague) that states that if $sf ZFC$ is consistent then it cannot be finitely axiomatized. However $sf NBG$ set theory is a conservative extension of $sf ZFC$ that can be finitely axiomatized.
Similarly, if $sf PA$ is consistent then it is not finitely axiomatizable (Ryll-Nardzewski) but it has a conservative extension, $sf ACA_0$, which is finitely axiomatizable. (Usually $sf ACA_0$ is considered a second-order theory, but my understanding is that there isn't really a difference between first and second-order from the syntactic point of view.)
I'm wondering if this happens in general. At first I thought it might be that every theory had a finitely axiomatizable conservative extension. But then I realised that every theory with a finitely axiomatized conservative extension must be effectively axiomatizable. So we shouldn't hope for theories to have finitely axiomatizable conservative extensions unless they're already effectively axiomatizable. Similarly if we add countably many logical constants to the language and demand that they're all true then that's effectively axiomatizable but doesn't have a finitely axiomatizable conservative extension, so we should restrict our attention to finite languages.
Does every effectively axiomatizable first-order theory over a finite language have a finitely axiomatizable conservative extension?
set-theory lo.logic computability-theory
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
$endgroup$
|
show 3 more comments
$begingroup$
I originally asked this question on math.stackexchange.com here.
There's a famous theorem (due to Montague) that states that if $sf ZFC$ is consistent then it cannot be finitely axiomatized. However $sf NBG$ set theory is a conservative extension of $sf ZFC$ that can be finitely axiomatized.
Similarly, if $sf PA$ is consistent then it is not finitely axiomatizable (Ryll-Nardzewski) but it has a conservative extension, $sf ACA_0$, which is finitely axiomatizable. (Usually $sf ACA_0$ is considered a second-order theory, but my understanding is that there isn't really a difference between first and second-order from the syntactic point of view.)
I'm wondering if this happens in general. At first I thought it might be that every theory had a finitely axiomatizable conservative extension. But then I realised that every theory with a finitely axiomatized conservative extension must be effectively axiomatizable. So we shouldn't hope for theories to have finitely axiomatizable conservative extensions unless they're already effectively axiomatizable. Similarly if we add countably many logical constants to the language and demand that they're all true then that's effectively axiomatizable but doesn't have a finitely axiomatizable conservative extension, so we should restrict our attention to finite languages.
Does every effectively axiomatizable first-order theory over a finite language have a finitely axiomatizable conservative extension?
set-theory lo.logic computability-theory
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
$endgroup$
$begingroup$
I suspect the answer is yes via some modified form of $sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $sf NGB$ to get a finitely axiomatizable theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
@JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M vDash T$ where $vDash$ and $T$ are interpreted in their natural way in the larger theory. [...]
$endgroup$
– François G. Dorais♦
10 hours ago
$begingroup$
[...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $operatornameCon(T)$ there is no reason for $M vDash operatornameCon(T)$ to be true. This is probably not what Oscar really wants...
$endgroup$
– François G. Dorais♦
10 hours ago
1
$begingroup$
@OscarCunningham It's perfectly possible to write down a sentence in, say, $sf ZFC$ that means $M models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$.
$endgroup$
– James Hanson
7 hours ago
|
show 3 more comments
$begingroup$
I originally asked this question on math.stackexchange.com here.
There's a famous theorem (due to Montague) that states that if $sf ZFC$ is consistent then it cannot be finitely axiomatized. However $sf NBG$ set theory is a conservative extension of $sf ZFC$ that can be finitely axiomatized.
Similarly, if $sf PA$ is consistent then it is not finitely axiomatizable (Ryll-Nardzewski) but it has a conservative extension, $sf ACA_0$, which is finitely axiomatizable. (Usually $sf ACA_0$ is considered a second-order theory, but my understanding is that there isn't really a difference between first and second-order from the syntactic point of view.)
I'm wondering if this happens in general. At first I thought it might be that every theory had a finitely axiomatizable conservative extension. But then I realised that every theory with a finitely axiomatized conservative extension must be effectively axiomatizable. So we shouldn't hope for theories to have finitely axiomatizable conservative extensions unless they're already effectively axiomatizable. Similarly if we add countably many logical constants to the language and demand that they're all true then that's effectively axiomatizable but doesn't have a finitely axiomatizable conservative extension, so we should restrict our attention to finite languages.
Does every effectively axiomatizable first-order theory over a finite language have a finitely axiomatizable conservative extension?
set-theory lo.logic computability-theory
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
$endgroup$
I originally asked this question on math.stackexchange.com here.
There's a famous theorem (due to Montague) that states that if $sf ZFC$ is consistent then it cannot be finitely axiomatized. However $sf NBG$ set theory is a conservative extension of $sf ZFC$ that can be finitely axiomatized.
Similarly, if $sf PA$ is consistent then it is not finitely axiomatizable (Ryll-Nardzewski) but it has a conservative extension, $sf ACA_0$, which is finitely axiomatizable. (Usually $sf ACA_0$ is considered a second-order theory, but my understanding is that there isn't really a difference between first and second-order from the syntactic point of view.)
I'm wondering if this happens in general. At first I thought it might be that every theory had a finitely axiomatizable conservative extension. But then I realised that every theory with a finitely axiomatized conservative extension must be effectively axiomatizable. So we shouldn't hope for theories to have finitely axiomatizable conservative extensions unless they're already effectively axiomatizable. Similarly if we add countably many logical constants to the language and demand that they're all true then that's effectively axiomatizable but doesn't have a finitely axiomatizable conservative extension, so we should restrict our attention to finite languages.
Does every effectively axiomatizable first-order theory over a finite language have a finitely axiomatizable conservative extension?
set-theory lo.logic computability-theory
set-theory lo.logic computability-theory
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
edited 11 hours ago
Oscar Cunningham
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
asked 11 hours ago
Oscar CunninghamOscar Cunningham
888616
888616
$begingroup$
I suspect the answer is yes via some modified form of $sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $sf NGB$ to get a finitely axiomatizable theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
@JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M vDash T$ where $vDash$ and $T$ are interpreted in their natural way in the larger theory. [...]
$endgroup$
– François G. Dorais♦
10 hours ago
$begingroup$
[...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $operatornameCon(T)$ there is no reason for $M vDash operatornameCon(T)$ to be true. This is probably not what Oscar really wants...
$endgroup$
– François G. Dorais♦
10 hours ago
1
$begingroup$
@OscarCunningham It's perfectly possible to write down a sentence in, say, $sf ZFC$ that means $M models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$.
$endgroup$
– James Hanson
7 hours ago
|
show 3 more comments
$begingroup$
I suspect the answer is yes via some modified form of $sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $sf NGB$ to get a finitely axiomatizable theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
@JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M vDash T$ where $vDash$ and $T$ are interpreted in their natural way in the larger theory. [...]
$endgroup$
– François G. Dorais♦
10 hours ago
$begingroup$
[...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $operatornameCon(T)$ there is no reason for $M vDash operatornameCon(T)$ to be true. This is probably not what Oscar really wants...
$endgroup$
– François G. Dorais♦
10 hours ago
1
$begingroup$
@OscarCunningham It's perfectly possible to write down a sentence in, say, $sf ZFC$ that means $M models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$.
$endgroup$
– James Hanson
7 hours ago
$begingroup$
I suspect the answer is yes via some modified form of $sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
I suspect the answer is yes via some modified form of $sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $sf NGB$ to get a finitely axiomatizable theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $sf NGB$ to get a finitely axiomatizable theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
@JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M vDash T$ where $vDash$ and $T$ are interpreted in their natural way in the larger theory. [...]
$endgroup$
– François G. Dorais♦
10 hours ago
$begingroup$
@JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M vDash T$ where $vDash$ and $T$ are interpreted in their natural way in the larger theory. [...]
$endgroup$
– François G. Dorais♦
10 hours ago
$begingroup$
[...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $operatornameCon(T)$ there is no reason for $M vDash operatornameCon(T)$ to be true. This is probably not what Oscar really wants...
$endgroup$
– François G. Dorais♦
10 hours ago
$begingroup$
[...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $operatornameCon(T)$ there is no reason for $M vDash operatornameCon(T)$ to be true. This is probably not what Oscar really wants...
$endgroup$
– François G. Dorais♦
10 hours ago
1
1
$begingroup$
@OscarCunningham It's perfectly possible to write down a sentence in, say, $sf ZFC$ that means $M models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$.
$endgroup$
– James Hanson
7 hours ago
$begingroup$
@OscarCunningham It's perfectly possible to write down a sentence in, say, $sf ZFC$ that means $M models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$.
$endgroup$
– James Hanson
7 hours ago
|
show 3 more comments
1 Answer
1
active
oldest
votes
$begingroup$
Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, and Richard Zach’s summary.
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
$endgroup$
$begingroup$
@DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it.
$endgroup$
– Emil Jeřábek
6 hours ago
$begingroup$
Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types.
$endgroup$
– Dmytro Taranovsky
6 hours ago
$begingroup$
Yes, for finite models, being in NP is the same as being $Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $Sigma^1_1$ sentence $Phi$ such that $Mmodels Tiff MmodelsPhi$ for finite models $M$. By the results above, there is also a $Sigma^1_1$ sentence $Psi$ such that $Mmodels Tiff MmodelsPsi$ for infinite models $M$. We may actually assume that $Psi$ has no finite models, as infiniteness is $Sigma^1_1$. However, finiteness is not $Sigma^1_1$, hence we have no information ...
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
... about infinite models of $Phi$, and it is not clear to me that we can combine $Phi$ and $Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $Phi$ or $Psi$, but this is not a priori obvious.
$endgroup$
– Emil Jeřábek
5 hours ago
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: "504"
;
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%2fmathoverflow.net%2fquestions%2f326470%2fdoes-every-first-order-theory-have-a-finitely-axiomatizable-conservative-exten%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, and Richard Zach’s summary.
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
$endgroup$
$begingroup$
@DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it.
$endgroup$
– Emil Jeřábek
6 hours ago
$begingroup$
Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types.
$endgroup$
– Dmytro Taranovsky
6 hours ago
$begingroup$
Yes, for finite models, being in NP is the same as being $Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $Sigma^1_1$ sentence $Phi$ such that $Mmodels Tiff MmodelsPhi$ for finite models $M$. By the results above, there is also a $Sigma^1_1$ sentence $Psi$ such that $Mmodels Tiff MmodelsPsi$ for infinite models $M$. We may actually assume that $Psi$ has no finite models, as infiniteness is $Sigma^1_1$. However, finiteness is not $Sigma^1_1$, hence we have no information ...
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
... about infinite models of $Phi$, and it is not clear to me that we can combine $Phi$ and $Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $Phi$ or $Psi$, but this is not a priori obvious.
$endgroup$
– Emil Jeřábek
5 hours ago
add a comment |
$begingroup$
Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, and Richard Zach’s summary.
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
$endgroup$
$begingroup$
@DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it.
$endgroup$
– Emil Jeřábek
6 hours ago
$begingroup$
Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types.
$endgroup$
– Dmytro Taranovsky
6 hours ago
$begingroup$
Yes, for finite models, being in NP is the same as being $Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $Sigma^1_1$ sentence $Phi$ such that $Mmodels Tiff MmodelsPhi$ for finite models $M$. By the results above, there is also a $Sigma^1_1$ sentence $Psi$ such that $Mmodels Tiff MmodelsPsi$ for infinite models $M$. We may actually assume that $Psi$ has no finite models, as infiniteness is $Sigma^1_1$. However, finiteness is not $Sigma^1_1$, hence we have no information ...
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
... about infinite models of $Phi$, and it is not clear to me that we can combine $Phi$ and $Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $Phi$ or $Psi$, but this is not a priori obvious.
$endgroup$
– Emil Jeřábek
5 hours ago
add a comment |
$begingroup$
Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, and Richard Zach’s summary.
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
$endgroup$
Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, and Richard Zach’s summary.
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
answered 7 hours ago
Emil JeřábekEmil Jeřábek
30.2k388142
30.2k388142
$begingroup$
@DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it.
$endgroup$
– Emil Jeřábek
6 hours ago
$begingroup$
Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types.
$endgroup$
– Dmytro Taranovsky
6 hours ago
$begingroup$
Yes, for finite models, being in NP is the same as being $Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $Sigma^1_1$ sentence $Phi$ such that $Mmodels Tiff MmodelsPhi$ for finite models $M$. By the results above, there is also a $Sigma^1_1$ sentence $Psi$ such that $Mmodels Tiff MmodelsPsi$ for infinite models $M$. We may actually assume that $Psi$ has no finite models, as infiniteness is $Sigma^1_1$. However, finiteness is not $Sigma^1_1$, hence we have no information ...
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
... about infinite models of $Phi$, and it is not clear to me that we can combine $Phi$ and $Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $Phi$ or $Psi$, but this is not a priori obvious.
$endgroup$
– Emil Jeřábek
5 hours ago
add a comment |
$begingroup$
@DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it.
$endgroup$
– Emil Jeřábek
6 hours ago
$begingroup$
Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types.
$endgroup$
– Dmytro Taranovsky
6 hours ago
$begingroup$
Yes, for finite models, being in NP is the same as being $Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $Sigma^1_1$ sentence $Phi$ such that $Mmodels Tiff MmodelsPhi$ for finite models $M$. By the results above, there is also a $Sigma^1_1$ sentence $Psi$ such that $Mmodels Tiff MmodelsPsi$ for infinite models $M$. We may actually assume that $Psi$ has no finite models, as infiniteness is $Sigma^1_1$. However, finiteness is not $Sigma^1_1$, hence we have no information ...
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
... about infinite models of $Phi$, and it is not clear to me that we can combine $Phi$ and $Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $Phi$ or $Psi$, but this is not a priori obvious.
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
@DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it.
$endgroup$
– Emil Jeřábek
6 hours ago
$begingroup$
@DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it.
$endgroup$
– Emil Jeřábek
6 hours ago
$begingroup$
Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types.
$endgroup$
– Dmytro Taranovsky
6 hours ago
$begingroup$
Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types.
$endgroup$
– Dmytro Taranovsky
6 hours ago
$begingroup$
Yes, for finite models, being in NP is the same as being $Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $Sigma^1_1$ sentence $Phi$ such that $Mmodels Tiff MmodelsPhi$ for finite models $M$. By the results above, there is also a $Sigma^1_1$ sentence $Psi$ such that $Mmodels Tiff MmodelsPsi$ for infinite models $M$. We may actually assume that $Psi$ has no finite models, as infiniteness is $Sigma^1_1$. However, finiteness is not $Sigma^1_1$, hence we have no information ...
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
Yes, for finite models, being in NP is the same as being $Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $Sigma^1_1$ sentence $Phi$ such that $Mmodels Tiff MmodelsPhi$ for finite models $M$. By the results above, there is also a $Sigma^1_1$ sentence $Psi$ such that $Mmodels Tiff MmodelsPsi$ for infinite models $M$. We may actually assume that $Psi$ has no finite models, as infiniteness is $Sigma^1_1$. However, finiteness is not $Sigma^1_1$, hence we have no information ...
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
... about infinite models of $Phi$, and it is not clear to me that we can combine $Phi$ and $Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $Phi$ or $Psi$, but this is not a priori obvious.
$endgroup$
– Emil Jeřábek
5 hours ago
$begingroup$
... about infinite models of $Phi$, and it is not clear to me that we can combine $Phi$ and $Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $Phi$ or $Psi$, but this is not a priori obvious.
$endgroup$
– Emil Jeřábek
5 hours ago
add a comment |
Thanks for contributing an answer to MathOverflow!
- 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.
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%2fmathoverflow.net%2fquestions%2f326470%2fdoes-every-first-order-theory-have-a-finitely-axiomatizable-conservative-exten%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
$begingroup$
I suspect the answer is yes via some modified form of $sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $sf NGB$ to get a finitely axiomatizable theory.
$endgroup$
– James Hanson
11 hours ago
$begingroup$
@JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M vDash T$ where $vDash$ and $T$ are interpreted in their natural way in the larger theory. [...]
$endgroup$
– François G. Dorais♦
10 hours ago
$begingroup$
[...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $operatornameCon(T)$ there is no reason for $M vDash operatornameCon(T)$ to be true. This is probably not what Oscar really wants...
$endgroup$
– François G. Dorais♦
10 hours ago
1
$begingroup$
@OscarCunningham It's perfectly possible to write down a sentence in, say, $sf ZFC$ that means $M models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$.
$endgroup$
– James Hanson
7 hours ago