Mixing
Prove the theory of equality with a finite number of unary predicates is decidable
Clash Royale CLAN TAG#URR8PPP
up vote
0
down vote
favorite
Let the signature have $n$ unary predicate symbols $P_1, dots, P_n$ and a single binary predicate $=$. Consider the theory of equality with the following axioms:
- $forall x (x = x)$
- $forall x forall y (x = y rightarrow y = x)$
- $forall x forall y forall z (x = y land y = z rightarrow x = z)$
- For each $i$, $forall x forall y (x = y land P_i(x) rightarrow P_i(y))$.
Is the set of formulas of this theory decidable?
The solution is somewhat intuitive if the predicates are omitted. In this case it's fairly easy to show that
- all [normal] models with domains of the same power are equivalent, and,
- for a closed formula that is $k$ quantifiers deep, all models having more than $k$ elements are equivalent.
Given this, for a formula that is $k$ quantifiers deep it's sufficient to check some $k + 1$ normal models with domains of $1, dots, k + 1$ elements respectively. If the formula is true in all of those, then it's true in every model of the theory, then it's deducible, otherwise it's not. So, we got an algorithm, and thus the set in question is decidable!
But how to prove this considering the unary predicates?
logic first-order-logic decidability
asked Jul 21 at 15:30
0xd34df00d
387212
add a comment |Â
up vote
0
down vote
favorite
Let the signature have $n$ unary predicate symbols $P_1, dots, P_n$ and a single binary predicate $=$. Consider the theory of equality with the following axioms:
- $forall x (x = x)$
- $forall x forall y (x = y rightarrow y = x)$
- $forall x forall y forall z (x = y land y = z rightarrow x = z)$
- For each $i$, $forall x forall y (x = y land P_i(x) rightarrow P_i(y))$.
Is the set of formulas of this theory decidable?
The solution is somewhat intuitive if the predicates are omitted. In this case it's fairly easy to show that
- all [normal] models with domains of the same power are equivalent, and,
- for a closed formula that is $k$ quantifiers deep, all models having more than $k$ elements are equivalent.
Given this, for a formula that is $k$ quantifiers deep it's sufficient to check some $k + 1$ normal models with domains of $1, dots, k + 1$ elements respectively. If the formula is true in all of those, then it's true in every model of the theory, then it's deducible, otherwise it's not. So, we got an algorithm, and thus the set in question is decidable!
But how to prove this considering the unary predicates?
logic first-order-logic decidability
asked Jul 21 at 15:30
0xd34df00d
387212
So how do you decide $exists xexists y(x neq y)$?
– Rob Arthan
Jul 22 at 1:25
Its quantifier depth is 2, so I consider normal models with domains having 1, 2 and 3 elements (the last one is probably unnecessary, but it's easier to check it than prove the inequality is non-strict). 1-element model immediately shows this formula is false thus it's not a formula of this theory.
– 0xd34df00d
Jul 22 at 4:38
What is a "normal model?"
– Noah Schweber
Jul 22 at 17:48
add a comment |Â
up vote
0
down vote
favorite
up vote
0
down vote
favorite
Let the signature have $n$ unary predicate symbols $P_1, dots, P_n$ and a single binary predicate $=$. Consider the theory of equality with the following axioms:
- $forall x (x = x)$
- $forall x forall y (x = y rightarrow y = x)$
- $forall x forall y forall z (x = y land y = z rightarrow x = z)$
- For each $i$, $forall x forall y (x = y land P_i(x) rightarrow P_i(y))$.
Is the set of formulas of this theory decidable?
The solution is somewhat intuitive if the predicates are omitted. In this case it's fairly easy to show that
- all [normal] models with domains of the same power are equivalent, and,
- for a closed formula that is $k$ quantifiers deep, all models having more than $k$ elements are equivalent.
Given this, for a formula that is $k$ quantifiers deep it's sufficient to check some $k + 1$ normal models with domains of $1, dots, k + 1$ elements respectively. If the formula is true in all of those, then it's true in every model of the theory, then it's deducible, otherwise it's not. So, we got an algorithm, and thus the set in question is decidable!
But how to prove this considering the unary predicates?
logic first-order-logic decidability
asked Jul 21 at 15:30
0xd34df00d
387212
Let the signature have $n$ unary predicate symbols $P_1, dots, P_n$ and a single binary predicate $=$. Consider the theory of equality with the following axioms:
- $forall x (x = x)$
- $forall x forall y (x = y rightarrow y = x)$
- $forall x forall y forall z (x = y land y = z rightarrow x = z)$
- For each $i$, $forall x forall y (x = y land P_i(x) rightarrow P_i(y))$.
Is the set of formulas of this theory decidable?
The solution is somewhat intuitive if the predicates are omitted. In this case it's fairly easy to show that
- all [normal] models with domains of the same power are equivalent, and,
- for a closed formula that is $k$ quantifiers deep, all models having more than $k$ elements are equivalent.
Given this, for a formula that is $k$ quantifiers deep it's sufficient to check some $k + 1$ normal models with domains of $1, dots, k + 1$ elements respectively. If the formula is true in all of those, then it's true in every model of the theory, then it's deducible, otherwise it's not. So, we got an algorithm, and thus the set in question is decidable!
But how to prove this considering the unary predicates?
logic first-order-logic decidability
asked Jul 21 at 15:30
0xd34df00d
387212
asked Jul 21 at 15:30
0xd34df00d
387212
asked Jul 21 at 15:30
0xd34df00d
387212
asked Jul 21 at 15:30
0xd34df00d
387212
387212
So how do you decide $exists xexists y(x neq y)$?
– Rob Arthan
Jul 22 at 1:25
Its quantifier depth is 2, so I consider normal models with domains having 1, 2 and 3 elements (the last one is probably unnecessary, but it's easier to check it than prove the inequality is non-strict). 1-element model immediately shows this formula is false thus it's not a formula of this theory.
– 0xd34df00d
Jul 22 at 4:38
What is a "normal model?"
– Noah Schweber
Jul 22 at 17:48
add a comment |Â
So how do you decide $exists xexists y(x neq y)$?
– Rob Arthan
Jul 22 at 1:25
Its quantifier depth is 2, so I consider normal models with domains having 1, 2 and 3 elements (the last one is probably unnecessary, but it's easier to check it than prove the inequality is non-strict). 1-element model immediately shows this formula is false thus it's not a formula of this theory.
– 0xd34df00d
Jul 22 at 4:38
What is a "normal model?"
– Noah Schweber
Jul 22 at 17:48
So how do you decide $exists xexists y(x neq y)$?
– Rob Arthan
Jul 22 at 1:25
So how do you decide $exists xexists y(x neq y)$?
– Rob Arthan
Jul 22 at 1:25
Its quantifier depth is 2, so I consider normal models with domains having 1, 2 and 3 elements (the last one is probably unnecessary, but it's easier to check it than prove the inequality is non-strict). 1-element model immediately shows this formula is false thus it's not a formula of this theory.
– 0xd34df00d
Jul 22 at 4:38
Its quantifier depth is 2, so I consider normal models with domains having 1, 2 and 3 elements (the last one is probably unnecessary, but it's easier to check it than prove the inequality is non-strict). 1-element model immediately shows this formula is false thus it's not a formula of this theory.
– 0xd34df00d
Jul 22 at 4:38
What is a "normal model?"
– Noah Schweber
Jul 22 at 17:48
What is a "normal model?"
– Noah Schweber
Jul 22 at 17:48
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
This is a good example of a situation where Ehrenfeucht-Fraisse games are quite useful. I claim that in fact the general satisfiability problem for this language - that is, the problem of whether an arbitrary sentence in the language is satisfiable - is decidable; since your theory is finitely axiomatized, its decidability also follows since your theory proves a sentence $theta$ iff the sentence $psiwedgenegtheta$ is unsatisfiable where $psi$ is the conjunction of the axioms in your theory.
Note that if $mathcalM$ is a structure in your language, then $mathcalM$ is completely determined by $2^n$ numbers, namely how many elements satisfy each of the Boolean combinations of the $P_i$s. Put another way, an element $a$ of $mathcalM$ is determined up to "automorphism orbit" by $i: P^mathcalM_i(a)$, and there are only $2^n$ many possible such sets.
This suggests that something like your equality-only analysis might also work here: that since there are only a fixed number of "possible behaviors," for every sentence $sigma$ we can effectively find a number $n$ such that if $sigma$ is satisfiable then it has a model of cardinality $le n$. We can prove this with some syntactic work, or - much more slickly - via EF-games:
Let $Struc(m_1,..., m_2^n)$ denote the unique-up-to-isomorphism structure with $m_k$-many elements in the $k$th Boolean combination of the $P_i$s. (Here the $m_k$s are allowed to be infinite.) Note that every structure in your language is isomorphic to exactly one of this form.
Given a structure $mathcalM$ and a number $k$, let $mathcalM[n]=Struc(maxk, m_1, ..., maxk, m_2^n)$ where $mathcalM=Struc(m_1,..., m_2^n)$.
Now show that regardless of what $k$ is, Duplicator wins the game $EF_k(mathcalM,mathcalM[k])$.
Finally, show that the previous bulletpoint implies that any satisfiable $k$-quantifier sentence has a model of size at most $k2^n$.
answered Jul 22 at 18:01
Noah Schweber
111k9140261
That's indeed a great application of EF games, thanks! And I also noticed that the structure is defined by the behaviour on predicates, but in my vague and clumsy proof sketch it only worked for finite (or at most countable) $m_k$s, and this one overcomes it easily!
– 0xd34df00d
Jul 23 at 13:01
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
This is a good example of a situation where Ehrenfeucht-Fraisse games are quite useful. I claim that in fact the general satisfiability problem for this language - that is, the problem of whether an arbitrary sentence in the language is satisfiable - is decidable; since your theory is finitely axiomatized, its decidability also follows since your theory proves a sentence $theta$ iff the sentence $psiwedgenegtheta$ is unsatisfiable where $psi$ is the conjunction of the axioms in your theory.
Note that if $mathcalM$ is a structure in your language, then $mathcalM$ is completely determined by $2^n$ numbers, namely how many elements satisfy each of the Boolean combinations of the $P_i$s. Put another way, an element $a$ of $mathcalM$ is determined up to "automorphism orbit" by $i: P^mathcalM_i(a)$, and there are only $2^n$ many possible such sets.
This suggests that something like your equality-only analysis might also work here: that since there are only a fixed number of "possible behaviors," for every sentence $sigma$ we can effectively find a number $n$ such that if $sigma$ is satisfiable then it has a model of cardinality $le n$. We can prove this with some syntactic work, or - much more slickly - via EF-games:
Let $Struc(m_1,..., m_2^n)$ denote the unique-up-to-isomorphism structure with $m_k$-many elements in the $k$th Boolean combination of the $P_i$s. (Here the $m_k$s are allowed to be infinite.) Note that every structure in your language is isomorphic to exactly one of this form.
Given a structure $mathcalM$ and a number $k$, let $mathcalM[n]=Struc(maxk, m_1, ..., maxk, m_2^n)$ where $mathcalM=Struc(m_1,..., m_2^n)$.
Now show that regardless of what $k$ is, Duplicator wins the game $EF_k(mathcalM,mathcalM[k])$.
Finally, show that the previous bulletpoint implies that any satisfiable $k$-quantifier sentence has a model of size at most $k2^n$.
answered Jul 22 at 18:01
Noah Schweber
111k9140261
That's indeed a great application of EF games, thanks! And I also noticed that the structure is defined by the behaviour on predicates, but in my vague and clumsy proof sketch it only worked for finite (or at most countable) $m_k$s, and this one overcomes it easily!
– 0xd34df00d
Jul 23 at 13:01
add a comment |Â
up vote
1
down vote
accepted
This is a good example of a situation where Ehrenfeucht-Fraisse games are quite useful. I claim that in fact the general satisfiability problem for this language - that is, the problem of whether an arbitrary sentence in the language is satisfiable - is decidable; since your theory is finitely axiomatized, its decidability also follows since your theory proves a sentence $theta$ iff the sentence $psiwedgenegtheta$ is unsatisfiable where $psi$ is the conjunction of the axioms in your theory.
Note that if $mathcalM$ is a structure in your language, then $mathcalM$ is completely determined by $2^n$ numbers, namely how many elements satisfy each of the Boolean combinations of the $P_i$s. Put another way, an element $a$ of $mathcalM$ is determined up to "automorphism orbit" by $i: P^mathcalM_i(a)$, and there are only $2^n$ many possible such sets.
This suggests that something like your equality-only analysis might also work here: that since there are only a fixed number of "possible behaviors," for every sentence $sigma$ we can effectively find a number $n$ such that if $sigma$ is satisfiable then it has a model of cardinality $le n$. We can prove this with some syntactic work, or - much more slickly - via EF-games:
Let $Struc(m_1,..., m_2^n)$ denote the unique-up-to-isomorphism structure with $m_k$-many elements in the $k$th Boolean combination of the $P_i$s. (Here the $m_k$s are allowed to be infinite.) Note that every structure in your language is isomorphic to exactly one of this form.
Given a structure $mathcalM$ and a number $k$, let $mathcalM[n]=Struc(maxk, m_1, ..., maxk, m_2^n)$ where $mathcalM=Struc(m_1,..., m_2^n)$.
Now show that regardless of what $k$ is, Duplicator wins the game $EF_k(mathcalM,mathcalM[k])$.
Finally, show that the previous bulletpoint implies that any satisfiable $k$-quantifier sentence has a model of size at most $k2^n$.
answered Jul 22 at 18:01
Noah Schweber
111k9140261
That's indeed a great application of EF games, thanks! And I also noticed that the structure is defined by the behaviour on predicates, but in my vague and clumsy proof sketch it only worked for finite (or at most countable) $m_k$s, and this one overcomes it easily!
– 0xd34df00d
Jul 23 at 13:01
add a comment |Â
up vote
1
down vote
accepted
up vote
1
down vote
accepted
This is a good example of a situation where Ehrenfeucht-Fraisse games are quite useful. I claim that in fact the general satisfiability problem for this language - that is, the problem of whether an arbitrary sentence in the language is satisfiable - is decidable; since your theory is finitely axiomatized, its decidability also follows since your theory proves a sentence $theta$ iff the sentence $psiwedgenegtheta$ is unsatisfiable where $psi$ is the conjunction of the axioms in your theory.
Note that if $mathcalM$ is a structure in your language, then $mathcalM$ is completely determined by $2^n$ numbers, namely how many elements satisfy each of the Boolean combinations of the $P_i$s. Put another way, an element $a$ of $mathcalM$ is determined up to "automorphism orbit" by $i: P^mathcalM_i(a)$, and there are only $2^n$ many possible such sets.
This suggests that something like your equality-only analysis might also work here: that since there are only a fixed number of "possible behaviors," for every sentence $sigma$ we can effectively find a number $n$ such that if $sigma$ is satisfiable then it has a model of cardinality $le n$. We can prove this with some syntactic work, or - much more slickly - via EF-games:
Let $Struc(m_1,..., m_2^n)$ denote the unique-up-to-isomorphism structure with $m_k$-many elements in the $k$th Boolean combination of the $P_i$s. (Here the $m_k$s are allowed to be infinite.) Note that every structure in your language is isomorphic to exactly one of this form.
Given a structure $mathcalM$ and a number $k$, let $mathcalM[n]=Struc(maxk, m_1, ..., maxk, m_2^n)$ where $mathcalM=Struc(m_1,..., m_2^n)$.
Now show that regardless of what $k$ is, Duplicator wins the game $EF_k(mathcalM,mathcalM[k])$.
Finally, show that the previous bulletpoint implies that any satisfiable $k$-quantifier sentence has a model of size at most $k2^n$.
answered Jul 22 at 18:01
Noah Schweber
111k9140261
This is a good example of a situation where Ehrenfeucht-Fraisse games are quite useful. I claim that in fact the general satisfiability problem for this language - that is, the problem of whether an arbitrary sentence in the language is satisfiable - is decidable; since your theory is finitely axiomatized, its decidability also follows since your theory proves a sentence $theta$ iff the sentence $psiwedgenegtheta$ is unsatisfiable where $psi$ is the conjunction of the axioms in your theory.
Note that if $mathcalM$ is a structure in your language, then $mathcalM$ is completely determined by $2^n$ numbers, namely how many elements satisfy each of the Boolean combinations of the $P_i$s. Put another way, an element $a$ of $mathcalM$ is determined up to "automorphism orbit" by $i: P^mathcalM_i(a)$, and there are only $2^n$ many possible such sets.
This suggests that something like your equality-only analysis might also work here: that since there are only a fixed number of "possible behaviors," for every sentence $sigma$ we can effectively find a number $n$ such that if $sigma$ is satisfiable then it has a model of cardinality $le n$. We can prove this with some syntactic work, or - much more slickly - via EF-games:
Let $Struc(m_1,..., m_2^n)$ denote the unique-up-to-isomorphism structure with $m_k$-many elements in the $k$th Boolean combination of the $P_i$s. (Here the $m_k$s are allowed to be infinite.) Note that every structure in your language is isomorphic to exactly one of this form.
Given a structure $mathcalM$ and a number $k$, let $mathcalM[n]=Struc(maxk, m_1, ..., maxk, m_2^n)$ where $mathcalM=Struc(m_1,..., m_2^n)$.
Now show that regardless of what $k$ is, Duplicator wins the game $EF_k(mathcalM,mathcalM[k])$.
Finally, show that the previous bulletpoint implies that any satisfiable $k$-quantifier sentence has a model of size at most $k2^n$.
answered Jul 22 at 18:01
Noah Schweber
111k9140261
answered Jul 22 at 18:01
Noah Schweber
111k9140261
answered Jul 22 at 18:01
Noah Schweber
111k9140261
answered Jul 22 at 18:01
Noah Schweber
111k9140261
111k9140261
That's indeed a great application of EF games, thanks! And I also noticed that the structure is defined by the behaviour on predicates, but in my vague and clumsy proof sketch it only worked for finite (or at most countable) $m_k$s, and this one overcomes it easily!
– 0xd34df00d
Jul 23 at 13:01
add a comment |Â
That's indeed a great application of EF games, thanks! And I also noticed that the structure is defined by the behaviour on predicates, but in my vague and clumsy proof sketch it only worked for finite (or at most countable) $m_k$s, and this one overcomes it easily!
– 0xd34df00d
Jul 23 at 13:01
That's indeed a great application of EF games, thanks! And I also noticed that the structure is defined by the behaviour on predicates, but in my vague and clumsy proof sketch it only worked for finite (or at most countable) $m_k$s, and this one overcomes it easily!
– 0xd34df00d
Jul 23 at 13:01
That's indeed a great application of EF games, thanks! And I also noticed that the structure is defined by the behaviour on predicates, but in my vague and clumsy proof sketch it only worked for finite (or at most countable) $m_k$s, and this one overcomes it easily!
– 0xd34df00d
Jul 23 at 13:01
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%2f2858595%2fprove-the-theory-of-equality-with-a-finite-number-of-unary-predicates-is-decidab%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
So how do you decide $exists xexists y(x neq y)$?
– Rob Arthan
Jul 22 at 1:25
Its quantifier depth is 2, so I consider normal models with domains having 1, 2 and 3 elements (the last one is probably unnecessary, but it's easier to check it than prove the inequality is non-strict). 1-element model immediately shows this formula is false thus it's not a formula of this theory.
– 0xd34df00d
Jul 22 at 4:38
What is a "normal model?"
– Noah Schweber
Jul 22 at 17:48