Does “every” first-order theory have a finitely axiomatizable conservative extension?Can every first order theory have a finitely axiomatizable conservative extension in this sense?Finite axiomatizability and $mathrmPA^top$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?
Can every first order theory have a finitely axiomatizable conservative extension in this sense?Finite axiomatizability and $mathrmPA^top$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 Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
$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 Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
$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
Mar 27 at 11:28
$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
Mar 27 at 11:31
$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♦
Mar 27 at 12:13
$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♦
Mar 27 at 12:16
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
Mar 27 at 15:25
|
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 Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
$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 Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
asked Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
edited Mar 27 at 11:53
Oscar Cunningham
asked Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
asked Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
asked Mar 27 at 11:09
Oscar CunninghamOscar Cunningham
923616
923616
$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
Mar 27 at 11:28
$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
Mar 27 at 11:31
$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♦
Mar 27 at 12:13
$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♦
Mar 27 at 12:16
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
Mar 27 at 15:25
|
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
Mar 27 at 11:28
$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
Mar 27 at 11:31
$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♦
Mar 27 at 12:13
$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♦
Mar 27 at 12:16
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
Mar 27 at 15:25
$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
Mar 27 at 11:28
$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
Mar 27 at 11:28
$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
Mar 27 at 11:31
$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
Mar 27 at 11:31
$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♦
Mar 27 at 12:13
$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♦
Mar 27 at 12:13
$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♦
Mar 27 at 12:16
$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♦
Mar 27 at 12:16
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
Mar 27 at 15:25
$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
Mar 27 at 15:25
|
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, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.$^+$”, and condition 2 “s.f.a.$^+$”):
Theorem. For any theory $T$ in a finite language, the following are equivalent:
$T$ has a finitely axiomatized conservative extension.
- There exists a finitely axiomatized extension $T'supseteq T$ such that every model of $T$ expands to a model of $T'$.
$T$ is equivalent to a $Sigma^1_1$ second-order sentence.
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Theorem. For any theory $T$ in a finite language, 1 implies 2:
$T$ has a finitely axiomatized conservative extension.
$T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Indeed, the truth of a fixed $Sigma^1_1$ sentence in finite models can be checked in NP.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
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.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
$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
Mar 27 at 16:15
$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
Mar 27 at 16:45
$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
Mar 27 at 17:07
$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
Mar 27 at 17:09
1
$begingroup$
It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4).
$endgroup$
– Fedor Pakhomov
Mar 29 at 5:51
|
show 5 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: "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, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.$^+$”, and condition 2 “s.f.a.$^+$”):
Theorem. For any theory $T$ in a finite language, the following are equivalent:
$T$ has a finitely axiomatized conservative extension.
- There exists a finitely axiomatized extension $T'supseteq T$ such that every model of $T$ expands to a model of $T'$.
$T$ is equivalent to a $Sigma^1_1$ second-order sentence.
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Theorem. For any theory $T$ in a finite language, 1 implies 2:
$T$ has a finitely axiomatized conservative extension.
$T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Indeed, the truth of a fixed $Sigma^1_1$ sentence in finite models can be checked in NP.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
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.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
$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
Mar 27 at 16:15
$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
Mar 27 at 16:45
$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
Mar 27 at 17:07
$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
Mar 27 at 17:09
1
$begingroup$
It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4).
$endgroup$
– Fedor Pakhomov
Mar 29 at 5:51
|
show 5 more comments
$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, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.$^+$”, and condition 2 “s.f.a.$^+$”):
Theorem. For any theory $T$ in a finite language, the following are equivalent:
$T$ has a finitely axiomatized conservative extension.
- There exists a finitely axiomatized extension $T'supseteq T$ such that every model of $T$ expands to a model of $T'$.
$T$ is equivalent to a $Sigma^1_1$ second-order sentence.
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Theorem. For any theory $T$ in a finite language, 1 implies 2:
$T$ has a finitely axiomatized conservative extension.
$T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Indeed, the truth of a fixed $Sigma^1_1$ sentence in finite models can be checked in NP.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
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.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
$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
Mar 27 at 16:15
$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
Mar 27 at 16:45
$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
Mar 27 at 17:07
$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
Mar 27 at 17:09
1
$begingroup$
It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4).
$endgroup$
– Fedor Pakhomov
Mar 29 at 5:51
|
show 5 more comments
$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, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.$^+$”, and condition 2 “s.f.a.$^+$”):
Theorem. For any theory $T$ in a finite language, the following are equivalent:
$T$ has a finitely axiomatized conservative extension.
- There exists a finitely axiomatized extension $T'supseteq T$ such that every model of $T$ expands to a model of $T'$.
$T$ is equivalent to a $Sigma^1_1$ second-order sentence.
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Theorem. For any theory $T$ in a finite language, 1 implies 2:
$T$ has a finitely axiomatized conservative extension.
$T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Indeed, the truth of a fixed $Sigma^1_1$ sentence in finite models can be checked in NP.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
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.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
$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, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.$^+$”, and condition 2 “s.f.a.$^+$”):
Theorem. For any theory $T$ in a finite language, the following are equivalent:
$T$ has a finitely axiomatized conservative extension.
- There exists a finitely axiomatized extension $T'supseteq T$ such that every model of $T$ expands to a model of $T'$.
$T$ is equivalent to a $Sigma^1_1$ second-order sentence.
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Theorem. For any theory $T$ in a finite language, 1 implies 2:
$T$ has a finitely axiomatized conservative extension.
$T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Indeed, the truth of a fixed $Sigma^1_1$ sentence in finite models can be checked in NP.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
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.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
edited Mar 29 at 15:04
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
answered Mar 27 at 14:58
Emil JeřábekEmil Jeřábek
30.3k389142
30.3k389142
$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
Mar 27 at 16:15
$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
Mar 27 at 16:45
$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
Mar 27 at 17:07
$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
Mar 27 at 17:09
1
$begingroup$
It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4).
$endgroup$
– Fedor Pakhomov
Mar 29 at 5:51
|
show 5 more comments
$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
Mar 27 at 16:15
$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
Mar 27 at 16:45
$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
Mar 27 at 17:07
$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
Mar 27 at 17:09
1
$begingroup$
It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4).
$endgroup$
– Fedor Pakhomov
Mar 29 at 5:51
$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
Mar 27 at 16:15
$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
Mar 27 at 16:15
$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
Mar 27 at 16:45
$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
Mar 27 at 16:45
$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
Mar 27 at 17:07
$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
Mar 27 at 17:07
$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
Mar 27 at 17:09
$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
Mar 27 at 17:09
1
1
$begingroup$
It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4).
$endgroup$
– Fedor Pakhomov
Mar 29 at 5:51
$begingroup$
It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4).
$endgroup$
– Fedor Pakhomov
Mar 29 at 5:51
|
show 5 more comments
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
-computability-theory, lo.logic, set-theory
$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
Mar 27 at 11:28
$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
Mar 27 at 11:31
$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♦
Mar 27 at 12:13
$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♦
Mar 27 at 12:16
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
Mar 27 at 15:25