Mixing
is first-order logic with constants equally expressive as first-order logic without constants?
Clash Royale CLAN TAG#URR8PPP
up vote
4
down vote
favorite
I define a logic as a set of formulas $mathcalL$ (formulated in some given signature) with a consequence relation $vDash$. Say a logic $L_1$ is at least as expressive as $L_2$ if there is a conservative translation from $L_1$ to $L_2$, i.e.~there is $t: mathcalL_1rightarrowmathcalL_2$ such that $GammavDash_1varphi$ iff $t(Gamma)vDash_2t(varphi)$. Consider $mathcalL_con$, the language of first-order logic with denumerably many constants, and $mathcalL$, the language of first-order logic with no constants. I suspect that these two languages are equally expressive. In particular, we can translate any formula with constants in $mathcalL_con$ to a formula with only variables in $mathcalL$, with the restriction that different constants are mapped to different variables. So for instance, $F(c_1,c_2)mapsto F(x_1,x_2)$. Is this right?
I guess a more fundamental question is that I do not have a firm grasp of how to prove properties of translations. I suppose that, given the soundness and completeness of first-order logic, one could induct on the complexity of proofs. But this seems rather tedious and does not extend to logics that are known to be incomplete. Is there a canonical way of proving equal expressiveness (or equivalently, the existence of a conservative translation) between any two logics?
logic first-order-logic model-theory
edited Jul 24 at 4:30
Taroccoesbrocco
3,48941431
asked Jul 23 at 18:51
discretizer
1077
add a comment |Â
up vote
4
down vote
favorite
I define a logic as a set of formulas $mathcalL$ (formulated in some given signature) with a consequence relation $vDash$. Say a logic $L_1$ is at least as expressive as $L_2$ if there is a conservative translation from $L_1$ to $L_2$, i.e.~there is $t: mathcalL_1rightarrowmathcalL_2$ such that $GammavDash_1varphi$ iff $t(Gamma)vDash_2t(varphi)$. Consider $mathcalL_con$, the language of first-order logic with denumerably many constants, and $mathcalL$, the language of first-order logic with no constants. I suspect that these two languages are equally expressive. In particular, we can translate any formula with constants in $mathcalL_con$ to a formula with only variables in $mathcalL$, with the restriction that different constants are mapped to different variables. So for instance, $F(c_1,c_2)mapsto F(x_1,x_2)$. Is this right?
I guess a more fundamental question is that I do not have a firm grasp of how to prove properties of translations. I suppose that, given the soundness and completeness of first-order logic, one could induct on the complexity of proofs. But this seems rather tedious and does not extend to logics that are known to be incomplete. Is there a canonical way of proving equal expressiveness (or equivalently, the existence of a conservative translation) between any two logics?
logic first-order-logic model-theory
edited Jul 24 at 4:30
Taroccoesbrocco
3,48941431
asked Jul 23 at 18:51
discretizer
1077
add a comment |Â
up vote
4
down vote
favorite
up vote
4
down vote
favorite
I define a logic as a set of formulas $mathcalL$ (formulated in some given signature) with a consequence relation $vDash$. Say a logic $L_1$ is at least as expressive as $L_2$ if there is a conservative translation from $L_1$ to $L_2$, i.e.~there is $t: mathcalL_1rightarrowmathcalL_2$ such that $GammavDash_1varphi$ iff $t(Gamma)vDash_2t(varphi)$. Consider $mathcalL_con$, the language of first-order logic with denumerably many constants, and $mathcalL$, the language of first-order logic with no constants. I suspect that these two languages are equally expressive. In particular, we can translate any formula with constants in $mathcalL_con$ to a formula with only variables in $mathcalL$, with the restriction that different constants are mapped to different variables. So for instance, $F(c_1,c_2)mapsto F(x_1,x_2)$. Is this right?
I guess a more fundamental question is that I do not have a firm grasp of how to prove properties of translations. I suppose that, given the soundness and completeness of first-order logic, one could induct on the complexity of proofs. But this seems rather tedious and does not extend to logics that are known to be incomplete. Is there a canonical way of proving equal expressiveness (or equivalently, the existence of a conservative translation) between any two logics?
logic first-order-logic model-theory
edited Jul 24 at 4:30
Taroccoesbrocco
3,48941431
asked Jul 23 at 18:51
discretizer
1077
I define a logic as a set of formulas $mathcalL$ (formulated in some given signature) with a consequence relation $vDash$. Say a logic $L_1$ is at least as expressive as $L_2$ if there is a conservative translation from $L_1$ to $L_2$, i.e.~there is $t: mathcalL_1rightarrowmathcalL_2$ such that $GammavDash_1varphi$ iff $t(Gamma)vDash_2t(varphi)$. Consider $mathcalL_con$, the language of first-order logic with denumerably many constants, and $mathcalL$, the language of first-order logic with no constants. I suspect that these two languages are equally expressive. In particular, we can translate any formula with constants in $mathcalL_con$ to a formula with only variables in $mathcalL$, with the restriction that different constants are mapped to different variables. So for instance, $F(c_1,c_2)mapsto F(x_1,x_2)$. Is this right?
I guess a more fundamental question is that I do not have a firm grasp of how to prove properties of translations. I suppose that, given the soundness and completeness of first-order logic, one could induct on the complexity of proofs. But this seems rather tedious and does not extend to logics that are known to be incomplete. Is there a canonical way of proving equal expressiveness (or equivalently, the existence of a conservative translation) between any two logics?
logic first-order-logic model-theory
edited Jul 24 at 4:30
Taroccoesbrocco
3,48941431
asked Jul 23 at 18:51
discretizer
1077
edited Jul 24 at 4:30
Taroccoesbrocco
3,48941431
edited Jul 24 at 4:30
Taroccoesbrocco
3,48941431
edited Jul 24 at 4:30
Taroccoesbrocco
3,48941431
3,48941431
asked Jul 23 at 18:51
discretizer
1077
asked Jul 23 at 18:51
discretizer
1077
asked Jul 23 at 18:51
discretizer
1077
1077
add a comment |Â
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
3
down vote
accepted
Translating constant symbols to variables does not work well, because in most logics where you contemplate formulas with free variables, the intended semantics is that of their universal closure. In those systems you have, for example
$$ p(x) vDash p(y) qquadtextbut notqquad p(c_0) vDash p(c_1) $$
because the models that satisfy $p(x)$ are exactly those where $p$ holds for every individual, which are the same models that satisfy $p(y)$.
You can, however, simulate constants using new function and predicate symbols. Construct a new language by adding a fresh variable letter $0$, a single new unary predicate symbol $Z$, and countably many new symbol functions $f_n$, and then translate
- each constant $c_n$ as $f_n(0)$;
- all other parts of terms remain unchanged;
- each atomic formula $p(t_1, ldots, t_n)$ as
$$ neg exists 0Bigl (Z(0) land forall x(Z(x)to x=0) land neg p(t[t_1],ldots,t[t_n]Bigr); $$ - and all connectives and quantifiers remain themselves
I hope this qualifies for your concept of a translation $mathcal L_1tomathcal L_2$. If you want to be completely rigid about it, you could "make room" for the new $0,Z,f_n$ symbols by selecting existing symbols for them and shifting the existing symbols out of the way with the Hilbert's-hotel map as part of the translation, but I'm not going to complicate my notation by making that explicit.
Suppose that for some $Gamma$, $varphi$ we have that $t(Gamma) vDash_2 t(varphi)$ and for some model $mathfrak M$ we have $mathfrak MvDash_1 Gamma$. Then we can construct a new $mathfrak M_2$ by selecting a single of $mathfrak M$'s elements to have the $Z$ property, and letting $(f_n)^mathfrak M_2$ map everything to $(c_n)^mathfrak M$ for each $n$.
Then $mathfrak M_2vDash_2 t(psi)$ exactly if $mathfrak MvDash_1 psi$. Now since $mathfrak MvDash_1 Gamma$ we have $mathfrak M_2vDash_2 t(Gamma)$ and then by assumption $mathfrak M_2 vDash_2 t(varphi)$ and then $mathfrak MvDash_1 varphi$.
Conversely, suppose $Gamma vDash_1 varphi$ and we have some $mathfrak M vDash_2 t(Gamma)$. Then,
either there is a unique $m_0inmathfrak M$ that satisfies $Z(m_0)$, and in that case we can construct an $mathfrak M_1$ by the reverse of the above procedure -- namely, let $(c_n)^mathfrak M_1$ be $f^mathfrak M(m_0)$ -- such that $mathfrak M_1vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
or there is no such element, in which case the translation of every atomic formula is true in $mathfrak M$ for all values of the variables. In that case let $mathfrak M_0$ be the model with a single element where all predicates are true; then $mathfrak M_0vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
(The negations in the translation of atomic formulas are there to allow $mathfrak M_0$ to work when $p$ is the equality predicate $=$, which we're not allowed to make "always false" when constructing a model -- but we can make it "always true" by selecting a model with a single element).
answered Jul 24 at 2:01
Henning Makholm
225k16290516
Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)notvDash p(c_j)$ for $ineq j$ comes out true)?
– discretizer
Jul 25 at 13:55
@discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity.
– Henning Makholm
Jul 25 at 14:51
ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again.
– discretizer
Jul 25 at 15:21
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
3
down vote
accepted
Translating constant symbols to variables does not work well, because in most logics where you contemplate formulas with free variables, the intended semantics is that of their universal closure. In those systems you have, for example
$$ p(x) vDash p(y) qquadtextbut notqquad p(c_0) vDash p(c_1) $$
because the models that satisfy $p(x)$ are exactly those where $p$ holds for every individual, which are the same models that satisfy $p(y)$.
You can, however, simulate constants using new function and predicate symbols. Construct a new language by adding a fresh variable letter $0$, a single new unary predicate symbol $Z$, and countably many new symbol functions $f_n$, and then translate
- each constant $c_n$ as $f_n(0)$;
- all other parts of terms remain unchanged;
- each atomic formula $p(t_1, ldots, t_n)$ as
$$ neg exists 0Bigl (Z(0) land forall x(Z(x)to x=0) land neg p(t[t_1],ldots,t[t_n]Bigr); $$ - and all connectives and quantifiers remain themselves
I hope this qualifies for your concept of a translation $mathcal L_1tomathcal L_2$. If you want to be completely rigid about it, you could "make room" for the new $0,Z,f_n$ symbols by selecting existing symbols for them and shifting the existing symbols out of the way with the Hilbert's-hotel map as part of the translation, but I'm not going to complicate my notation by making that explicit.
Suppose that for some $Gamma$, $varphi$ we have that $t(Gamma) vDash_2 t(varphi)$ and for some model $mathfrak M$ we have $mathfrak MvDash_1 Gamma$. Then we can construct a new $mathfrak M_2$ by selecting a single of $mathfrak M$'s elements to have the $Z$ property, and letting $(f_n)^mathfrak M_2$ map everything to $(c_n)^mathfrak M$ for each $n$.
Then $mathfrak M_2vDash_2 t(psi)$ exactly if $mathfrak MvDash_1 psi$. Now since $mathfrak MvDash_1 Gamma$ we have $mathfrak M_2vDash_2 t(Gamma)$ and then by assumption $mathfrak M_2 vDash_2 t(varphi)$ and then $mathfrak MvDash_1 varphi$.
Conversely, suppose $Gamma vDash_1 varphi$ and we have some $mathfrak M vDash_2 t(Gamma)$. Then,
either there is a unique $m_0inmathfrak M$ that satisfies $Z(m_0)$, and in that case we can construct an $mathfrak M_1$ by the reverse of the above procedure -- namely, let $(c_n)^mathfrak M_1$ be $f^mathfrak M(m_0)$ -- such that $mathfrak M_1vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
or there is no such element, in which case the translation of every atomic formula is true in $mathfrak M$ for all values of the variables. In that case let $mathfrak M_0$ be the model with a single element where all predicates are true; then $mathfrak M_0vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
(The negations in the translation of atomic formulas are there to allow $mathfrak M_0$ to work when $p$ is the equality predicate $=$, which we're not allowed to make "always false" when constructing a model -- but we can make it "always true" by selecting a model with a single element).
answered Jul 24 at 2:01
Henning Makholm
225k16290516
Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)notvDash p(c_j)$ for $ineq j$ comes out true)?
– discretizer
Jul 25 at 13:55
@discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity.
– Henning Makholm
Jul 25 at 14:51
ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again.
– discretizer
Jul 25 at 15:21
add a comment |Â
up vote
3
down vote
accepted
Translating constant symbols to variables does not work well, because in most logics where you contemplate formulas with free variables, the intended semantics is that of their universal closure. In those systems you have, for example
$$ p(x) vDash p(y) qquadtextbut notqquad p(c_0) vDash p(c_1) $$
because the models that satisfy $p(x)$ are exactly those where $p$ holds for every individual, which are the same models that satisfy $p(y)$.
You can, however, simulate constants using new function and predicate symbols. Construct a new language by adding a fresh variable letter $0$, a single new unary predicate symbol $Z$, and countably many new symbol functions $f_n$, and then translate
- each constant $c_n$ as $f_n(0)$;
- all other parts of terms remain unchanged;
- each atomic formula $p(t_1, ldots, t_n)$ as
$$ neg exists 0Bigl (Z(0) land forall x(Z(x)to x=0) land neg p(t[t_1],ldots,t[t_n]Bigr); $$ - and all connectives and quantifiers remain themselves
I hope this qualifies for your concept of a translation $mathcal L_1tomathcal L_2$. If you want to be completely rigid about it, you could "make room" for the new $0,Z,f_n$ symbols by selecting existing symbols for them and shifting the existing symbols out of the way with the Hilbert's-hotel map as part of the translation, but I'm not going to complicate my notation by making that explicit.
Suppose that for some $Gamma$, $varphi$ we have that $t(Gamma) vDash_2 t(varphi)$ and for some model $mathfrak M$ we have $mathfrak MvDash_1 Gamma$. Then we can construct a new $mathfrak M_2$ by selecting a single of $mathfrak M$'s elements to have the $Z$ property, and letting $(f_n)^mathfrak M_2$ map everything to $(c_n)^mathfrak M$ for each $n$.
Then $mathfrak M_2vDash_2 t(psi)$ exactly if $mathfrak MvDash_1 psi$. Now since $mathfrak MvDash_1 Gamma$ we have $mathfrak M_2vDash_2 t(Gamma)$ and then by assumption $mathfrak M_2 vDash_2 t(varphi)$ and then $mathfrak MvDash_1 varphi$.
Conversely, suppose $Gamma vDash_1 varphi$ and we have some $mathfrak M vDash_2 t(Gamma)$. Then,
either there is a unique $m_0inmathfrak M$ that satisfies $Z(m_0)$, and in that case we can construct an $mathfrak M_1$ by the reverse of the above procedure -- namely, let $(c_n)^mathfrak M_1$ be $f^mathfrak M(m_0)$ -- such that $mathfrak M_1vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
or there is no such element, in which case the translation of every atomic formula is true in $mathfrak M$ for all values of the variables. In that case let $mathfrak M_0$ be the model with a single element where all predicates are true; then $mathfrak M_0vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
(The negations in the translation of atomic formulas are there to allow $mathfrak M_0$ to work when $p$ is the equality predicate $=$, which we're not allowed to make "always false" when constructing a model -- but we can make it "always true" by selecting a model with a single element).
answered Jul 24 at 2:01
Henning Makholm
225k16290516
Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)notvDash p(c_j)$ for $ineq j$ comes out true)?
– discretizer
Jul 25 at 13:55
@discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity.
– Henning Makholm
Jul 25 at 14:51
ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again.
– discretizer
Jul 25 at 15:21
add a comment |Â
up vote
3
down vote
accepted
up vote
3
down vote
accepted
Translating constant symbols to variables does not work well, because in most logics where you contemplate formulas with free variables, the intended semantics is that of their universal closure. In those systems you have, for example
$$ p(x) vDash p(y) qquadtextbut notqquad p(c_0) vDash p(c_1) $$
because the models that satisfy $p(x)$ are exactly those where $p$ holds for every individual, which are the same models that satisfy $p(y)$.
You can, however, simulate constants using new function and predicate symbols. Construct a new language by adding a fresh variable letter $0$, a single new unary predicate symbol $Z$, and countably many new symbol functions $f_n$, and then translate
- each constant $c_n$ as $f_n(0)$;
- all other parts of terms remain unchanged;
- each atomic formula $p(t_1, ldots, t_n)$ as
$$ neg exists 0Bigl (Z(0) land forall x(Z(x)to x=0) land neg p(t[t_1],ldots,t[t_n]Bigr); $$ - and all connectives and quantifiers remain themselves
I hope this qualifies for your concept of a translation $mathcal L_1tomathcal L_2$. If you want to be completely rigid about it, you could "make room" for the new $0,Z,f_n$ symbols by selecting existing symbols for them and shifting the existing symbols out of the way with the Hilbert's-hotel map as part of the translation, but I'm not going to complicate my notation by making that explicit.
Suppose that for some $Gamma$, $varphi$ we have that $t(Gamma) vDash_2 t(varphi)$ and for some model $mathfrak M$ we have $mathfrak MvDash_1 Gamma$. Then we can construct a new $mathfrak M_2$ by selecting a single of $mathfrak M$'s elements to have the $Z$ property, and letting $(f_n)^mathfrak M_2$ map everything to $(c_n)^mathfrak M$ for each $n$.
Then $mathfrak M_2vDash_2 t(psi)$ exactly if $mathfrak MvDash_1 psi$. Now since $mathfrak MvDash_1 Gamma$ we have $mathfrak M_2vDash_2 t(Gamma)$ and then by assumption $mathfrak M_2 vDash_2 t(varphi)$ and then $mathfrak MvDash_1 varphi$.
Conversely, suppose $Gamma vDash_1 varphi$ and we have some $mathfrak M vDash_2 t(Gamma)$. Then,
either there is a unique $m_0inmathfrak M$ that satisfies $Z(m_0)$, and in that case we can construct an $mathfrak M_1$ by the reverse of the above procedure -- namely, let $(c_n)^mathfrak M_1$ be $f^mathfrak M(m_0)$ -- such that $mathfrak M_1vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
or there is no such element, in which case the translation of every atomic formula is true in $mathfrak M$ for all values of the variables. In that case let $mathfrak M_0$ be the model with a single element where all predicates are true; then $mathfrak M_0vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
(The negations in the translation of atomic formulas are there to allow $mathfrak M_0$ to work when $p$ is the equality predicate $=$, which we're not allowed to make "always false" when constructing a model -- but we can make it "always true" by selecting a model with a single element).
answered Jul 24 at 2:01
Henning Makholm
225k16290516
Translating constant symbols to variables does not work well, because in most logics where you contemplate formulas with free variables, the intended semantics is that of their universal closure. In those systems you have, for example
$$ p(x) vDash p(y) qquadtextbut notqquad p(c_0) vDash p(c_1) $$
because the models that satisfy $p(x)$ are exactly those where $p$ holds for every individual, which are the same models that satisfy $p(y)$.
You can, however, simulate constants using new function and predicate symbols. Construct a new language by adding a fresh variable letter $0$, a single new unary predicate symbol $Z$, and countably many new symbol functions $f_n$, and then translate
- each constant $c_n$ as $f_n(0)$;
- all other parts of terms remain unchanged;
- each atomic formula $p(t_1, ldots, t_n)$ as
$$ neg exists 0Bigl (Z(0) land forall x(Z(x)to x=0) land neg p(t[t_1],ldots,t[t_n]Bigr); $$ - and all connectives and quantifiers remain themselves
I hope this qualifies for your concept of a translation $mathcal L_1tomathcal L_2$. If you want to be completely rigid about it, you could "make room" for the new $0,Z,f_n$ symbols by selecting existing symbols for them and shifting the existing symbols out of the way with the Hilbert's-hotel map as part of the translation, but I'm not going to complicate my notation by making that explicit.
Suppose that for some $Gamma$, $varphi$ we have that $t(Gamma) vDash_2 t(varphi)$ and for some model $mathfrak M$ we have $mathfrak MvDash_1 Gamma$. Then we can construct a new $mathfrak M_2$ by selecting a single of $mathfrak M$'s elements to have the $Z$ property, and letting $(f_n)^mathfrak M_2$ map everything to $(c_n)^mathfrak M$ for each $n$.
Then $mathfrak M_2vDash_2 t(psi)$ exactly if $mathfrak MvDash_1 psi$. Now since $mathfrak MvDash_1 Gamma$ we have $mathfrak M_2vDash_2 t(Gamma)$ and then by assumption $mathfrak M_2 vDash_2 t(varphi)$ and then $mathfrak MvDash_1 varphi$.
Conversely, suppose $Gamma vDash_1 varphi$ and we have some $mathfrak M vDash_2 t(Gamma)$. Then,
either there is a unique $m_0inmathfrak M$ that satisfies $Z(m_0)$, and in that case we can construct an $mathfrak M_1$ by the reverse of the above procedure -- namely, let $(c_n)^mathfrak M_1$ be $f^mathfrak M(m_0)$ -- such that $mathfrak M_1vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
or there is no such element, in which case the translation of every atomic formula is true in $mathfrak M$ for all values of the variables. In that case let $mathfrak M_0$ be the model with a single element where all predicates are true; then $mathfrak M_0vDash_1 psi$ iff $mathfrak MvDash_2 t(psi)$.
(The negations in the translation of atomic formulas are there to allow $mathfrak M_0$ to work when $p$ is the equality predicate $=$, which we're not allowed to make "always false" when constructing a model -- but we can make it "always true" by selecting a model with a single element).
answered Jul 24 at 2:01
Henning Makholm
225k16290516
edited Jul 24 at 2:13
answered Jul 24 at 2:01
Henning Makholm
225k16290516
answered Jul 24 at 2:01
Henning Makholm
225k16290516
answered Jul 24 at 2:01
Henning Makholm
225k16290516
225k16290516
Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)notvDash p(c_j)$ for $ineq j$ comes out true)?
– discretizer
Jul 25 at 13:55
@discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity.
– Henning Makholm
Jul 25 at 14:51
ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again.
– discretizer
Jul 25 at 15:21
add a comment |Â
Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)notvDash p(c_j)$ for $ineq j$ comes out true)?
– discretizer
Jul 25 at 13:55
@discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity.
– Henning Makholm
Jul 25 at 14:51
ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again.
– discretizer
Jul 25 at 15:21
Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)notvDash p(c_j)$ for $ineq j$ comes out true)?
– discretizer
Jul 25 at 13:55
Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)notvDash p(c_j)$ for $ineq j$ comes out true)?
– discretizer
Jul 25 at 13:55
@discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity.
– Henning Makholm
Jul 25 at 14:51
@discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity.
– Henning Makholm
Jul 25 at 14:51
ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again.
– discretizer
Jul 25 at 15:21
ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again.
– discretizer
Jul 25 at 15:21
add a comment |Â
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2860666%2fis-first-order-logic-with-constants-equally-expressive-as-first-order-logic-with%23new-answer', 'question_page');
);
Post as a guest
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
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
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