1
$\begingroup$

From small cases to all of them. This is in the spirit of 15 theorem see https://en.wikipedia.org/wiki/15_and_290_theorems

EXAMPLE : Suppose you have the following problem: P(a)

For any fixed non negative integer $a$ define the relation $R_a :\mathbb{N}\times\mathbb{N}\rightarrow \{0,1\} $ as $ R_a(i,j)=1$ if $ i\leq Min(a,j)$ else $0$.

Do we have $ \forall (i,j,k) R_a(i,j).R_a(j,k) <= R_a(i,k)$ ?

You may of course show by hand that $R_a$ is transitive. You may also test it by computer for all quadruples $(a,i,j,k)$ in some TEST_SPACE like [0,10]x[1,1000]x[1,1000]x[1,1000].

If the test is positive I think most people are convinced that P(a) is true for any $a$. Mainly because we use 3 variables(i,j,k) and one parameter (a) , and addition(+) and compare (<=) and Min.

QUESTION: Are there any theorem saying that if the size of TEST_SPACE is at least above a bound function of the formula length,depth,number of variables(...) then truth on TEST_SPACE implies truth everywhere.

a) Assume there are only Min,Max , add , substract , comparison , small constants ,only integers (non negative?) , and a small number of variables ( says < 10).

NOTE1 : I guess some terribly high bound does exist BUT the theorem should be useful that is I don't want triple exponential bound ,( says one exponential at most )

Concrete answers or domain direction will be appreciated.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ You seem to be asking about the size of a minimal counterexample to a universal sentence of Presburger arithmetic, or equivalently, of a minimal solution of an integer linear program. These are known to have bit-length polynomial in the length of the formula. $\endgroup$
    – Emil Jeřábek
    Commented May 27 at 13:56
  • $\begingroup$ @Emil Jeřábek : Taking a quick look at Pressburger Arith : Is the degree of polynomial constructive, and I am not sure how to cover Min(i,j) or Max() ? $\endgroup$
    – Jérôme JEAN-CHARLES
    Commented May 27 at 20:14
  • $\begingroup$ $\min$ and $\max$ are quantifier-free definable from order: e.g., $\min(x,y)=z\iff(x\le y\land z=x)\lor(y\le x\land z=y)$. The bounds are explicit, and the exponent should be something small (2 or 3 or so), but I can’t search the literature now. $\endgroup$
    – Emil Jeřábek
    Commented May 27 at 21:28
  • $\begingroup$ @Emil Jeřábek : Very clear, thank you. $\endgroup$
    – Jérôme JEAN-CHARLES
    Commented May 28 at 8:25

0

Reset to default