Anima Ex Machina

Both the philosopher Charles Sanders Peirce in 1880 and the American logician H. M. Sheffer in 1913 realized that the truth-functions of elementary logic could all be defined from a single operation. The Sheffer stroke, also known as the Nand operation, is a logical operator with the following meaning: p Nand q is true if and only if not both p and q are true. It is named for Henry M. Sheffer, who proved that all the usual operators of Boolean algebra (Not, And, Or, Implies) could be expressed in terms of Nand. There is another logical operator which is able to express all the others: Nor [A set of five independent postulates for Boolean algebras, with application to logical constants. Transactions of the American Mathematical Soc. 14 (1913), pp. 481-488]. In 1933, Edward Huntington proposed an alternative set of axioms for Boolean algebra, consisting of associativity and commutativity plus Huntington’s axiom:

!( !x [Or] y) [Or] ( !( !x [Or] !y ) = x

Huntington showed that the three axioms together imply the axioms of Boolean algebra. Sometime after, Herbert Ellis Robbins also found a single axiom:

!( !( x [Or] y) [Or] ( y [Or] !x )) = x

that he conjectured (when taken  together with associativity and commutativity) implied that of Huntington, so that Robbins algebras are equivalent to Boolean algebras. The proof was finally delivered in 1996 by William McCune, using his theorem prover EQP. See:

Gina Kolata, Computer Math Proof Shows Reasoning Power, The New York Times, 1996.

Tutorial on Automatic Reasoning and Theorem Proving related to the course MAT 504, Topics in Logic, for the Spring term of 1997 from prof. Edward Nelson

As a result of an exhaustive and systematic computer exploration undertaken by Stephen Wolfram looking for the shortest single axiom equivalent to the axioms of Boolean algebra. Wolfram found among 288684 a single formula (up to other equivalent of the same size) with Nands and 3 variables. It then turns out that Wolfram’s axiom:

(((x [Nand] y) [Nand] z) [Nand] (x [Nand] ((x [Nand] z) [Nand] x))) = z

is equivalent to the axioms of Boolean algebra and the shortest (in the number of operators and variables) single axiom equivalent to Boolean algebra (Wolfram 2002, pp. 808-811 and 1174).

In the NKS notes at the end of the book there is an account that around 1949 Carew Meredith found the axiom system (NKS page 1173):

f[f[a, f[b, c]], f[a, f[b, c]]] = f[f[f[c, a], a],f[f[b, a], a]]f[f[a, a], f[b, a]] ==a

And in 1967 George Spencer Brown found:

f[f[a, a], f[f[b, b], b]] ==af[a, f[b, c]] = f[f[f[f[c, c], a], f[f[b, b], a]], f[f[f[c, c], a], f[f[b, b], a]]]

and again Meredith in 1969:

f[a, f[b, f[a, c]]] = f[a, f[b, f[b, c]]]f[f[a, a], f[b, a]] = af[a, b] == f[b, a]

Carew Meredith spent a long time studying somewhat similar forms. Meredith’s interest in short axioms came originally from Lukasiewicz.

More references:

• - NKS explanation on the use of axioms.
• - Simple Axiom Systems for Boolean Algebra.
• - A Summary of New Results in Mathematics Obtained with Argonne’s Automated Deduction Software.- Group Theory Single Axioms Survey.
• - Axiomatizations of Some Sentential Logics.

More bibliographical references (Meredith and Prior 1968 and Meredith 1969b are the main ones on equational logic, and Meredith 1951 contains the six-character single axiom that Prior described as ‘sensational’):

• - Meredith, C.A. 1951. ‘On an Extended System of the Propositional Calculus’. Proceedings of the Royal Irish Academy, vol. 54 Sect. A, 37-47.
• - Meredith, C.A. 1953a. ‘Single Axioms for the Systems (C,N), (C, 0), and (A, N) of the Two-Valued Propositional Calculus’. Journal of Computing Systems, vol. 1, 155-164.
• - Meredith, C.A. 1953b. ‘A Single Axiom of Positive Logic’. Journal of Computing Systems, vol. 1, 169-170.
• - Meredith, C.A. 1958. ‘The Dependence of an Axiom of Lukasiewicz’. Transactions of the American Mathematical Society, vol. 87, 54.
• - Meredith, C.A. 1966. ‘Postulates for Implicational Calculi’. Journal of Symbolic Logic, vol. 31, 7-9.
• - Meredith, C.A. 1969b. ‘Equational Postulates for the Sheffer Stroke’. Notre Dame Journal of Formal Logic, vol. 10, 266-270.
• - Meredith, C.A., Prior, A.N. 1963. ‘Notes on the Axiomatics of the Propositional Calculus’. Notre Dame Journal of Formal Logic, vol. 4, 171-187.
• - Meredith, C.A., Prior, A.N. 1968. ‘Equational Logic’. Notre Dame Journal of Formal Logic, vol. 9, 212-226.

Kurt Godel workshop for studying his legacy and writings. Lille, France, May 19-21, 2006

My thoughts, ideas, references, comments and informal notes:

- The wheel machine, a machine for real computation which I am proposing -as a thought experiment- in a forthcoming paper  on the Church-Turing thesis -Yes, one more paper on the CT thesis!- with comments on Wilfried Sieg’s paper entitled “Church Without Dogma: Axioms for Computability”

- “In case Cantor’s continuum problem should turn out to be undecidable from the accepted axioms of set theory, the question of its truth would loose its meaning, exactly as the question of the truth of Euclid’s fifth postulate in Euclidian geometry did”. Godel replies: “It has meaning anyway, as Euclid’s fifth postulate gave rise to other now accepted mathematical fields.”

- Godel Gibbs Lecture and his dicotomy on absolutely undecidable propositions and the computational power of the human mind (Turing did great work… but he was wrong when he proposed his formal theory as a model of human thought…)

- New contacts and references: Olivier Souan, Rudy Rucker, Karl Svozil

Mark van Atten’s “On Godel’s awareness of Skolem’s lecture”.
Rick Tieszen

- Herbrand on general recursive functions, letter to Godel.

- Leibniz’ influence on Godel’s arithmetization?

- Sources: Godel Editorial Project. Firestone Library, Princeton University. I.A.S. Marcia Tucker, librarian for Godel papers.

- Godel’s concept of finite procedure as the most satisfactory definition of computation. “A machine with a finite number of parts as Turing did” or “finite combinatorial procedure” as a definition of an algorithm, mechanical or computational procedure.

- Computation’s main constraints: boundness and locality (paper from Hernandez-Quiroz and Raymundo Morado).

- Aphorisms and autoreference (Gabriel Sandu and Hinttika)

- Feferman on Turing

- Is Sieg’s paper and the question of “finite machine=effective procedure” a tautology? In fact such an approach seems to be one of the most strict versions of the Turing Thesis, and even though both Church and Turing probably did propose it in such a strict sense, extensive versions of the thesis have traditionaly covered more content, but even when it is strictly stated that there is still space for a thesis, it is neither proved nor provable from my point of view, and most authors would concur, though some clearly would not. I will comment on this more extensively later, since this was one of my Master’s topics and merits a post by itself.

- Putnam’s thought experiment on cutting all sensorial inputs. Solution: It is impossible in practice. However, machines are an example in a sense, and that is why we do not recognize intelligence in them – they are deprived of  sensorial capabilities.

Yes, Godel found an inconsistency in the U.S. constitution. My answer: One? Certainly a bunch. That’s why we need lawyers, who make them even worse.

Metamathematics is to mathematics what metaphysics is to philosophy. It is about stepping outside the discipline and attempting to grasp it as a single entity/ object of study; it is an investigation into the foundations of mathematics. (For an elucidation of  Foundations of Mathematics see http://www.math.psu.edu/simpson/hierarchy.html)

Some mathematicians have begun to practice  a quasi-empirical brand of mathematics and insist on results for which there is experimental evidence. This development has been facilitated by the fact that massive calculations are possible nowadays.  This new brand of mathematics is related to experimental mathematics in being a type of mathematical research in which computation is used to investigate mathematical structures and identify their fundamental properties and patterns.

A few researchers have devoted themselves to what we could call experimental metamathematics, doing methamatematical research with the help of today’s vast computational resources, which were unavailable not too long ago. Among such researchers are Stephen Wolfram and Gregory Chaitin, both of whom have formulated rich questions and made remarkable discoveries and contributions to the field (NKS on Math sample video lecture by Wolfram  available here.)

Such efforts have made it possible to explore and arrive at important results regarding particular spaces of possible programs, including precise results which are perfectly consonant with traditional mathematics. For instance, Wolfram arrived at an axiom using only NAND and NOR equivalent to the set of all axioms of Boolean Algebra by considering the space of all propositional logic expressions up to six NANDs and two variables. He found that none of the 16896 possible axiom systems of this kind explored by him worked even up to 3-value operators. But with 6 NANDS and 3 variables, he found that 296 of the 288684 possible axiom systems worked up to 3-value operators, and 100 worked up to 4-value operators (NKS Book, Wolfram 2002, p. 809). He then found the smallest, proving that there were no smaller and formulating the following axiom: (((x \[Nand] y) \[Nand] z) \[Nand] (x \[Nand] ((x \[Nand] z) \[Nand] x))) == z.

Similar research on first-order logic would be worth undertaking, considering that it is powerful enough to express most or all of our mathematical theories.

The image below is a graph of what I call the universe of mathematical theories (or axiom systems, since they are not interpreted under any particular structure and have no semantic content). Each column represents a formula generated under an enumeration which eventually goes through all possible first-order formulas. Each cell on the matrix has a color,  gray if the formula of the column is false in the axiom system of the row,  white if it is true. Some cells are black and they represent formulas that are neither false nor true. In other words they are syntactically underivable within the axiom system in question. The project was  developed in a pre-release Mathematica Version 6 using Waldmeister, an automatic theorem prover embedded in the new Mathematica– a theorem prover based on the Bendix-Knuth resolution. Some patterns in the image can be explained by the chosen enumeration of the formulas and the axiom systems (which are subsets of the same formulas). However the question is whether or not a pattern can always be explained, and whether patterns are formed only by syntactical facts or whether they can shed light on the general properties of classes of axiom systems. I have explored these issues through to the beginning of the mathematical universe of length 5 and 6, but the process is clearly intractable, so I am beginning to generate samples of universes of higher degree, and to perform translations of mathematical theories into pure syntactical axioms and axioms systems into theories under arbitrary interpretations. One way or another this procedure will touch one of our current mathematical theories. The question is which number will it be  and how many times could it be repeated under different interpretations.

 the The image above shows a sample with the first proofs for all the 161 raw formulas of length 4 (involving 4 bound variables) and the first 1000 axiom systems (which come from the subset operation applied to the  161 raw formulas of length 4). Since the size (total number of axiom systems) in the universe of length 4 is 2.9×10^48, this is only the very first part of it, with the first 161000 proofs obtained using the automated theorem prover. The problem is evidently intractable but a sampling method can be conceived in order to explore higher universes, to mix formulas between universes and find possible unrecognized (not easily syntactically explained) structures.

All equational axiom systems can be represented with two binary operators f and p, where p is a pairing function and we specify a constant using an axiom of the form
ForAll[a,ForAll[b,f[a, a] == f[b, b]]], and then the ith constant is c[i]=Nest[p[f[a,a],#]&,f[a,a],i]. We can then use f[c[i],p[c[1],x]], as the ith function of x. Note that x may be a list built from pairs. Of course, this assumes that there are an infinite number of  individuals in the most general case.

All axioms can be given in Skolemized form, hence there is no need to use existential quantifiers in axioms.

The mathematical universes created by this method were checked for consistency (proving that a==b in inconsistency systems for any a and b, in other words that in them it is possible to prove that anything equals anything) and internal independence (the minimal set of axioms, in other words that an axiom ai in S cannot be derived from another axiom aj or a subset of {a1,..,an} in the system S, where n is the length –number of axioms– of the system S). Some interesting results (to be published in the Journal of Complex Systems) have been obtained, like the proportion of  consistent to inconsistent axiom systems in such an enumeration –which is not precisely arbitrary but lexicographically–, or of internal independence to dependency. The purpose of the project is to shed some light on questions like the following:

- Euclid described axioms as self-evident truths. From the perspective of modern mathematics it is quite evident that it would be very difficult to  find axioms that are self-evident truths, and even  more difficult to claim that one’s axiom of choice or the continuum hypothesis are self-evident truths. So the problem is: Where do we get axioms from?
- What is evident is that math theories begin from something that is assumed to be true,  a starting point adopted for pragmatical reasons rather than because of its intrinsic truth value.
- How special are our mathematics (Are we being “mathcentric” in the Copernican sense)?
- How far along are  current mathematical theories in the enumeration of all possible axiom systems (they are enumerable)?
- Given an enumeration, how arbitrary is it and what role will it have in placing our current mathematics?
- Is there a shorter axiom system (in terms of number of axioms or their length) defining current mathematical theories? (My claim: There may be several copies of mathematical theories through the whole enumeration, but I wonder whether they get syntactically simpler while becoming semanticaly more complicated. For example, the same operations may have more complicated interpretations in order to capture an equivalent theory in fewer or shorter axioms. S. Wolfram was surprised at how close the axiom systems for propositional logic were when he enumerated non-quantified systems for his NKS book.  Could the same be true  for arbitrary mathematical theories, and if so what would that mean?)
- Is there a single type of math? In other words, could  an hypothetical alien civilization have a different mathematics? It seems that there is a single physics since, presumably, we live in a single universe. However we have several models of that universe, not all of which are mutually compatible, and a priori their are known as approximations. So the question could be split into two: perhaps there is a single physics but we are not able to access it assuming real numbers, i.e. by traditional methods. However, it seems unclear how we might argue that there is a single type of mathematics.
- Is there a minimum set of mathematics shared by all possible hypothetical civilizations, probably at least  arithmetic theory, those theories closer to physical reality?.
- Assuming a discrete universe and the role of mathematics and physics for determining what we call “real”, the enumeration of possible universes would be feasible. What would it mean if our universe is very close to the beginning of the enumeration of all possible universes? Of course that is very dependent on the chosen enumeration, but could it be in some way independent or less arbitrary? In what degree?