[FOM] 629: Boolean Algebra/Simplicity

[Harvey Friedman]

Nice, again! Perhaps you know the most likely suspects who would be
interested in

i. Revisiting the BA case with multiple axioms as I discussed earlier.
ii. Taking on the HA case with multiple axioms in the spirit of
http://www.cs.nyu.edu/pipermail/fom/2012-March/016357.html

and send them links to this FOM thread?

I remember writing about lots of examples where studies of this kind
would be very interesting, and in very wide audiences. I thought it
was in

http://www.cs.nyu.edu/pipermail/fom/2012-March/016357.html

but was HORRIFIED to find that this is NOT the place where I had
discussed my systematic program along these lines. In fact, I haven't
been able to locate it, so I am going to restate it as I am older and
wiser now.

We measure the complexity of an axiomatization by a pair of numbers
(n,m). n is the number of axioms. m is the maximum complexity of the
axioms. The complexity is measured by counting the number of signs
excluding parentheses and commas. The signs are quantifiers,
variables, connectives, constants, relations, functions. You can
suppress outer universal quantifiers. (forall x) counts as 2, one for
the forall, and one for x. There is obvious flexibility in the
complexity measure, and variants should also be explored. The
primitives should be the usual ones everybody uses. There should be no
fixation on single axiom axiomatizations. One can incorporate Schemes,
which is not relevant for the examples discussed. Use free logic when
there are naturally undefined terms. Uparrows, downarrows,
wiggle-equal (both sides are undefined or both sides are defined and
equal), all count as 1.

1. Linear orderings. <,=.
2. Linear orderings. <=,=.
3. Boolean algebra. 0,1,and,or,not. Also Heyting algebra, with if then added.
4. Group. dot,=.
5. Group. dot,=,inverse.
6. Commutative Ring. +,-,x,=.
7. Field. +,-,x,=,reciprocal.
8. Ordered group. dot,=,<.
9. Ordered ring. +,-,x,=,<.
10. Ordered field. +,-,x,=,reciprocal,<.
11. Discrete 8,9,10.
12. Vector space. Two sorted logic. Field operations, group on
vectors, scalar multiplication.
13. Normed vector space. Vector space with norm function. Take norm
values in R, R for granted, with addition and 0.
14. Banach space. Take R and infinite sequences for granted.

A closely related kind of study is to let F:R into R, and look at the
complexity of definitions of properties of F. I leave it to the
researcher to set up the appropriate languages carefully, so you can
write epsilon/delta definitions naturally. It is fairly obvious what
you want to do.

i. F is pointwise continuous.
ii. F is Lipshitz.
iii. F is pointwise differentiable.
iv. F is continuously differentiable.
v. F is monotone.
vi. F is piecewise continuous.
etcetera.

Also take on F:C into C for complex variable theory.

It is also important to do this kind of study for second order logic.
E.g., questions like: how complicated is it to characterize the
(V(alpha),epsilon) up to isomorphism in second order logic with
epsilon,=?

Harvey Friedman

On Sun, Oct 4, 2015 at 7:34 AM, Matthew Szudzik <mszudzik at szudzik.com> wrote:
> On Sun, Oct 04, 2015 at 01:08:57AM -0400, Harvey Friedman wrote:
>>
>> In this particular case, I am more interested in the formulation
>> allowing multiple axioms, using 0,1,and,or,not,=. This Wolfram/Veroff
>> example involves a single axiom with an abbreviation for nand, which I
>> consider substantially less attractive for the spirit of
>
> Wolfram also considered equational axiomatizations for Boolean algebra
> with And, Or, and Not (but without 0 and 1).  Unfortunately, I don't
> think that computers were fast enough in 2000 to search for the shortest
> single axiom in that case.
>
> Nevertheless, Wolfram came up with the following interesting result:
>
>  http://wolframscience.com/nksonline/page-817
>
> If one lists the theorems of Boolean algebra in order of syntactic
> complexity (based on the height of the parse tree, number of leaves on
> the tree, number of distinct variable names, etc.), and if one picks out
> those theorems in the list that cannot be derived from earlier theorems,
> then those theorems are exactly the standard theorems that are given
> names in textbooks (with the exception of the second of the two
> distributive laws, which can be derived from theorems earlier in the
> list).  This provides a nice formalization for the intuitive notion of
> an 'interesting theorem of Boolean algebra'.
>
> Matthew Szudzik