[FOM] 657: Definitional Complexity Theory 1

Mon Feb 15 00:39:06 EST 2016

Here I want to focus on one of the theories discussed in
http://www.cs.nyu.edu/pipermail/fom/2016-February/019499.html

In Definitional Complexity Theory, we look for exact calculations and
estimates concerning the least complexity of a definition of a
relation. Here we are referring to relations R on the set theoretic
universe V, and first order definitions of R over (V,epsilon,=).

Obviously there is a much more general such theory, where we are
referring to relations R on a domain D, and first order definitions of
R over a structure M = (D,...).

Obviously, we need a or various notions of complexity here. Formulas
will be unsugared, and use the two quantifiers and the usual five
connectives.

As in http://www.cs.nyu.edu/pipermail/fom/2016-February/019499.html we use

i. variable complexity. The total number of occurrences of variables.
ii. quantifier complexity. The total number of occurrences of quantifiers.
iii. alternating quantifier complexity, with existential or universal
lead. Defined in the usual inductive way.
iv. It makes sense to further use prefix classes like AAAEEAAAE.

In this posting, I will get exact calculations for just two toy
examples. If we go a little bit further, we expect  that we can also
get exact calculations, but probably needing the help of a computer.
If we go yet further, we will not be able to get exact calculations,
but only get estimates, where the upper bound is morally certain to be
exact, and the lower bound is obtained with the help of a computer.

The two toy examples considered here are: the binary inclusion
relation, and "being transitive".

x containedin y if and only if (forall z)(z in x implies z in y). This
has variable complexity 5, quantifier complexity 1, and no existential
definition.

We first show that inclusion has no existential definition. This may
be known(??). Jack Schwartz had some students who work on logic of
rudimentary set theory. Also there is work of some Italian logicians
which appeared some time ago on the FOM, including Policriti, Cantone,
Omodeo.

DEFINITION 1. We use 0 for the empty set. x_1,...,x_k and y_1,...,y_k
are isomorphic if and only if for all 1 = i,j <= k, x_i in x_j iff y_i
in y_j, and x_i = x_j iff y_i = y_j. x,y are incomparable if and only
if x not y and x notin y and y notin x.

LEMMA 1. Let k >= 1. and A be given. Suppose there is no epsilon chain
0 in a_1 in a_2 in ... in a_k in A. Then every 0,A,x_1,...,x_k is
isomorphic to some 0',A,x_1',...,x_k' with 0' of higher rank than A.

Proof: Look at the union K of the epsilon chains in 0,A,x_1,...,x_k
that start with 0. We can move K isomorphically, way out of sight and
leave the rest of 0,A,x_1,...,x_k alone. 0 will be moved, but A will
not be moved. The result will be isomorphic to 0,A,x_1,...,x_k, with 0
moved. QED

THEOREM 2. Set inclusion cannot be existentially defined.

Proof: Suppose x containedin y iff (there exists z_1,...,z_k)(phi),
where phi is quantifier free. We can assume that phi =
phi(x,y,z_1,...,z_k), where x,y,z_1,...,z_k are distinct variables, by
elimination of like variables, and change of variables, . Choose A so
that there is no epsilon chain 0 in a_1 in a_2 in ... in a_k in A. Let
phi(0,A,z_1,...,z_k). Let phi(0',A,z_1',...,z_k') according to Lemma
1. Then 0' is not a subset of A, contradiction. QED

THEOREM 3. Set inclusion has variable complexity 5.

Proof: Syntactically, the only formulas of complexity <= 4 are
i. quantifier free.
ii. (forall z)(phi), where phi is a literal.
iii. not(forall z)(phi), where phi is a literal.

By change of variable, we can assume z is not x,y. These are easily
eliminated by inspection. QED

We now come to transitivity.

THEOREM 4. Transitivity cannot be defined by (there exists
x_1,...,x_n)(for all y)(there exists
z_1,...,z_m)(phi(A,x_1,...,x_n,y,z_1,...,z_m)), phi quantifier free.

Actually, this is proving to be trickier than I thought, and so in the
interest of efficiency, I should defer to those names I mentioned
earlier to see if they have done this or know how to do this.

Also, one should have

THEOREM 5. The variable complexity of transitivity is 8.

**********************************************************
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 657th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM
640: Progress in Pi01 Incompleteness 3  10/30/15  2:30PM
641: Progress in Pi01 Incompleteness 4  10/31/15  8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1  11/3/15  11:57PM
644: Fixed Point Selectors 1  11/16/15  8:38AM
645: Fixed Point Minimizers #1  11/22/15  7:46PM
646: Philosophy of Incompleteness 1  Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1  11/30/15  6:52PM
648: Necessary Irrelevance 1  12/21/15  4:01AM
649: Necessary Irrelevance 2  12/21/15  8:53PM
650: Necessary Irrelevance 3  12/24/15  2:42AM
651: Pi01 Incompleteness Update  2/2/16  7:58AM
652: Pi01 Incompleteness Update/2  2/7/16  10:06PM
653: Pi01 Incompleteness/SRP,HUGE  2/8/16  3:20PM
654: Theory Inspired by Automated Proving 1  2/11/16  2:55AM
655: Pi01 Incompleteness/SRP,HUGE/2  2/12/16  11:40PM
656: Pi01 Incompleteness/SRP,HUGE/3  2/13/16  1:21PM

Harvey Friedman