Hi guys I need to prove a Finite Support Theorem which states that $K$ is finitely definable iff $K$ has finite support. Unfortunately I succeeded in proving only the first part of if and only if.

$Introduction:$ We say that $S\subseteq \{p_i : i\in\mathbb{N}\}$ is a support for a set of assignments $K$, if for every two assignments $v$ and $v'$ that agree on all propositional variables in $S$ $\Rightarrow$ $v$$\in$$K$$\iff$$v'$$\in$$K$

$K$ is finitely definable if there exists a finite number of formulas in $\Sigma$ s.t. $Ass(\Sigma) = K$

$Proof \ attempt:$

Let $K$ be a set of truth assignments.

$\Rightarrow$ Suppose $K$ is finitely definable, I can just go over all the formulas in $\Sigma$ because it is finite and construct a finite set $S$ from a propositional variables in $\Sigma$, with some formality it's not a problem to prove that $S$ is a finite support for $K$.

$\Leftarrow$ Suppose $S$ is a finite support of $K$. I need to show that $K$ is finitely definable. In this direction I'm struggling to find a formal proof. Maybe I need somehow to construct $\Sigma$ from the a finite support I have, but I don't know how to use the given property of assignments... Anyway I'm a little lost here. Would be thankful for some help.

  • $\begingroup$ What are you trying to prove? What seems to be the theorem also seems to be the definition of "finitely definable", and then that says "if" and not "iff". Further, in that line, you say "... if there exists a finite number of formulas in $\Sigma$ s.t. ..." — do you mean, "if there exists a finite set of formulas $\Sigma s.t. ..."? $\endgroup$ – BrianO Dec 9 '15 at 12:40
  • $\begingroup$ @BrianO I just gave as an introduction the meanings of finite definability and finite support as I know them from propositional calculus because it may vary in different theories I guess. What I try to prove is that if S is a finite support of K as I described than K is finitely definable. $\endgroup$ – Evgeny A. Dec 9 '15 at 12:50

$\Leftarrow$: Suppose $K$ has finite support, for some finite $S\subseteq \{p_i\mid i\in \Bbb N\}$ such that for all assignments $v,v'$, if $v|S = v'|S$ then $v\in K\iff v'\in K$. (Note, abuse of notation: strictly speaking, $v|S$ should really be $v\,|\,\{i\mid p_i\in S\}$.)

Assume that assignments are functions $v\colon \Bbb N\to 2 = \{0,1\}$.

Let $K|S = \{v|S\mid v\in K\}$, the set of all restrictions of assignments in $K$ to $S$, so $K|S$ is finite. (Note, another abuse of notation: of course $K$ isn't a function, so don't take $K|S$ literally.)

For each partial assignment $s\in K|S$ and each $p_i\in S$, let $$ p_i^{(s)} = \begin{cases} p_i &\text{if $s_i = 1$},\\ \neg\, p_i &\text{if $s_i = 0$.}\\ \end{cases}$$

For each $s\in K|S$, let $\phi^{(s)}$ be the formula $$ \phi^{(s)} = \bigwedge_{p\in S} p^{(s)}, $$ so $\phi^{(s)}$ is true under any assignment $v\supseteq s$.

Finally, define the formula $\phi$ by $$ \phi = \bigvee_{s\in K|S} \phi^{(s)}. $$

We claim that $K = Assign(\{\phi\})$. Clearly, every $v\in K$ satisfies $\phi$, as $v$ satisfies $\phi^{(v|S)}$. For the reverse inclusion, suppose $v$ is an assignment satisfying $\phi$. Then for some $s\in K|S$, $v$ satisfies $\phi^{(s)}$. By definition of $K|S$, there is $v'\in K$ such that $s= v'|S$. By definition of $\phi^{(s)}$ and the fact that $v$ satisfies it, we must have $v|S = v'|S$. Hence, because $K$ has finite support with respect to $S$ and $v'\in K$, we must have $v\in K$. So $K$ is finitely definable.

| cite | improve this answer | |
  • $\begingroup$ Thank you very much for a detailed proof. Though it took me some time to understand it. $\endgroup$ – Evgeny A. Dec 9 '15 at 13:58
  • $\begingroup$ Just a little correction, I think you meant: $\phi = \bigvee_{s\in K|S} \phi^{(s)}$ $\endgroup$ – Evgeny A. Dec 9 '15 at 14:18
  • $\begingroup$ Yes I do mean that, thanks for catching it... Fixed. $\endgroup$ – BrianO Dec 9 '15 at 14:25
  • $\begingroup$ After I wrote it up I thought, hmm this answer doesn't explain what's going on at all, I hope it's not too formal. So I'm not surprised it took a while (sorry!). I'm glad you figured out what's going on :) $\endgroup$ – BrianO Dec 9 '15 at 14:30
  • $\begingroup$ It's just what I needed :). Actually I don't know if it's accurate to say that the definition of $v$ is as you mentioned. I mean maybe $v\colon \{p_i\mid i\in \Bbb N\}\to \{T,F\}$. And $p_i^{(s)} = \begin{cases} p_i &\text{if $s(p_i) = T$},\\ \neg\, p_i &\text{if $s(p_i) = F$.}\\ \end{cases}$ $\endgroup$ – Evgeny A. Dec 9 '15 at 14:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.