875: Structural Proof Theory/7

Tue Mar 2 04:07:47 EST 2021

REGARDING DECISION PROCEDURES

1. OVER THE USUAL NUMBER SYSTEMS

I started a project some years back on TINY DIOPHANTINE EQUATIONS. The
idea is that we should have some software which decides whether tiny
polynomials with integer coefficients have a solution in nonnegative
integers, in integers, inrationals, and whether they have infinitely
many solutions over the integers, and also if finitely many solutions,
then either list them all or describe them.

I interacted with Andrej Bauer in this vein, and see the report
http://math.andrej.com/2006/11/04/are-small-sentences-of-peano-arithmetic-decidable/
and I think he may have written further pieces on this topic.

We can view this, more generally, as investigating sentences of the form

(there exists x1,...,xk in Z)(there exists y1,...,yn in Q)(there
exists z1,...,zm in R)(there exists w1,...,wr in C)(s1 = t1 and ...
and sp = tp)

with rational constants allowed. Hilbert's Tenth Problem is a special
case of this for n = m = s = 0 and p = 1. With integer parameters
allowed, there is a single instance where the choice of what
parameters we can use to make this true is not recursive. However, the
examples known of this are ENORMOUS either in degree or in the number
of variables. This leads naturally to the question of just what can be
done for TINY cases, where k,n,m,r,p are tiny and the degrees of the
s,t are TINY.

In here I mentioned a result of Tung:
http://cs.nyu.edu/pipermail/fom/2006-October/011050.html

Tung's result is that if we look at (for all n >= 0)(there exists m >=
0)(s = t), with constants from N allowed, then we get a decision
procedure. IF I RECALL, negative results move in quickly here with s,t
unrestricted. Does anybody here know where to look for Tung and its
follow ups?

2. EQUATIONAL THEORIES

Now we move to pure logic. An equational theory is a theory that
asserts that some given finite set of equations in variables holds
universally over the nonempty domain D. The equations are terms in
several functions of varying arity over D. A particularly famous
example of this is GROUPS, using constant e (identity) binary function
dot and unary function inverse (or ^-1). The axioms are a list of
familiar equations. So we allow function symbols and constant symbols
here.

NOTE: An equational theory always has a model - namely the unique
model where D is a singleton. I.e., |D| = 1.

The issues are: whether there is a model with |D| >= 2? Whether there
is a model with |D| infinite?

THEOREM. (well known) The following are equivalent for an equational
theory T. If T has a model with one given infinite domain, then it has
a model with any other given infinite domain. If T has finite models
of unlimited sized finite D, then T has models on any infinite D. But
T may have a model with an infinite domain yet have no model with
finite domain of cardinality at least 2.

OF COURSE, you know from logic that the above Theorem even holds for
all first order theories.

The following result is also well known.

THEOREM. The set of equational theories with a model with |D| >=2 is
complete Pi01. The set of equational theories with an infinite model
is also complete Pi01. The set of equational theories with finite
models of infinitely many different sizes is complete Pi02. The set of
equational theories with a finite model of cardinality >= 2 is
complete r.e. THe set of equational theories with models of every
finite cardinality is complete Pi01.

QUESTION. How can we tell whether a TINY equational theory has these
various properties in the above Theorem?

LITERATURE QUESTION. I think that the above Theorem has been
established even for equational theories with just ONE EQUATION.
Anybody familiar with this?

Things are quite straightforward if one uses only functions of arity
1. Things start to get serious with at least one binary operation.

case 1. Just one binary function and a tiny number of equations and a
tiny number of occurrences of variables.
case 2. A tiny number of constant, unary, and binary functions and a
tiny number of equations and a tiny number of occurrences of
variables.

##########################################

My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 875th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16  Jun 13 01:08:40
818: Beyond Perfectly Natural/17  6/13/18  4:16PM
819: Sugared ZFC Formalization/1  6/13/18  6:42PM
820: Sugared ZFC Formalization/2  6/14/18  6:45PM
821: Beyond Perfectly Natural/18  6/17/18  1:11AM
822: Tangible Incompleteness/1  7/14/18  10:56PM
823: Tangible Incompleteness/2  7/17/18  10:54PM
824: Tangible Incompleteness/3  7/18/18  11:13PM
825: Tangible Incompleteness/4  7/20/18  12:37AM
826: Tangible Incompleteness/5  7/26/18  11:37PM
827: Tangible Incompleteness Restarted/1  9/23/19  11:19PM
828: Tangible Incompleteness Restarted/2  9/23/19  11:19PM
829: Tangible Incompleteness Restarted/3  9/23/19  11:20PM
830: Tangible Incompleteness Restarted/4  9/26/19  1:17 PM
831: Tangible Incompleteness Restarted/5  9/29/19  2:54AM
832: Tangible Incompleteness Restarted/6  10/2/19  1:15PM
833: Tangible Incompleteness Restarted/7  10/5/19  2:34PM
834: Tangible Incompleteness Restarted/8  10/10/19  5:02PM
835: Tangible Incompleteness Restarted/9  10/13/19  4:50AM
836: Tangible Incompleteness Restarted/10  10/14/19  12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20  02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory  2/8/20  2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20  12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1:  5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1  5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1  6/19/20 1132PM :
860: Unary Regressive Growth/1  8/120  9:50PM
861: Simplified Axioms for Class Theory  9/16/20  9:17PM
862: Symmetric Semigroups  2/2/21  9:11 PM
863: Structural Mapping Theory/1  2/4/21  11:36PM
864: Structural Mapping Theory/2  2/7/21  1:07AM
865: Structural Mapping Theory/3  2/10/21  11:57PM
866: Structural Mapping Theory/4  2/13/21  12:47AM
867: Structural Mapping Theory/5  2/14/21  11:27PM
868: Structural Mapping Theory/6  2/15/21  9:45PM
869: Structural Proof Theory/1  2/24/21  12:10AM
870: Structural Proof Theory/2  2/28/21  1:18AM
871: Structural Proof Theory/3  2/28/21  9:27PM
872: Structural Proof Theory/4  2/28/21  10:38PM
873: Structural Proof Theory/5  3/1/21  12:58PM
874: Structural Proof Theory/6

Harvey Friedman