ThinkArt Lab Animation:  A.T. Kelemen

Cloning the Ur-Logik

---

Not only in arithmetics with its natural numbers we are involved in the naturality of our basic terms of thinking but also in logic itself. All ways of thinking are founded in a single way of thinking, reducing all possible multitudes to a strict unizity, the famous Ur-Logik. In contrast to arithmetics logic has unfolded itself in a wide range of different logical systems. But there are good reasons to accept the strategy to reduce this plurality back to the singularity of the Ur-Logik.

Combinatory Logic as introduced by Moses Schönfinkel (1924 in Moscow) and independently later by Haskell Curry (1930) was often called Ur-Logik, Schönfinkel's main operator was therefore U. And it was believed that with this Ur-Logik the very fundamental problems of the foundations of logic and mathematics could be solved for ever.

Today combinatory logic plays an important role in the construction of functional programming languages like ML, Haskell, Miranda. Combinatory logic is also crucial for the definition and exploitation of parallelism of functional programs.

As the great logician and magician Raymond Smullyan pointed out in his famous book To Mock a Mocking Bird (1985), combinators are programs and everything a program can do can be done by combinators. This is an enormous statement if we contrast the radical simplicity of combinatory logic with the complexity of programs. Obviously, combinatory logic must have a special power. This power is based in its abstractness which is surpassing our normal attitude to logic and which is not fearing logical paradoxes. Combinatory logic is not founded in ordinary language and perception (Anschauung) but in formal and formalist thinking and scriptural construction.

And again, ...

As Natural as 0,1,2

Philip Wadler. Evans and Sutherland Distinguished Lecture, University of Utah, 20 November 2002.

"Whether a visitor comes from another place, another planet, or another plane of being we can be sure that he, she, or it will count just as we do: though their symbols vary, the numbers are universal. The history of logic and computing suggests a programming language that is equally natural. The language, called lambda calculus, is in exact correspondence with a formulation of the laws of reason, called natural deduction. Lambda calculus and natural deduction were devised, independently of each other, around 1930, just before the development of the first stored program computer. Yet the correspondence between them was not recognized until decades later, and not published until 1980. Today, languages based on lambda calculus have a few thousand users. Tomorrow, reliable use of the Internet may depend on languages with logical foundations. "

http://homepages.inf.ed.ac.uk/wadler/topics/history.html#drdobbs

1 Disseminations of Combinatory Logics

Following E. Engler, (1983) combinatory logic as a proof theoretical system is build by language, axioms and rules. Combinatory logic is a system, or more exactly an algebra A = (A, *, S, K), therefore we can disseminate this algebra in a way we have introduced before by means of the proemial relationship.

The algebra A consists of the formulas A, the application "*", and the combinators "S" and "K". The terms of the language are build by atomic terms, with variables x, y, z...and the constants S and K and the binary application "*" of the combinatory algebra. Formulas are equations between terms. The universe of combinatory logic is single-sorted or untyped. That is, in this term algebra there is no distinction between functions and their arguments-except that * interprets the first expression as a function and the second as the function´s argument (R.W. Stark)

Axioms are

t = t for atomic terms

Sxyz = (xz) (yz)

Kxy = x

The deduction rules are the rules of equality.

t1 = t2 ==> t1t3 = t2t3

t1 = t2 ==> t3t1 = t3t1

t1 = t2 ==> t2 = t1

t1 = t2, t2 = t3 ==> t1 = t3

Provability

Again, it maybe helpful to put the skeleton of combinatory logic together in a conceptual graph which visualize the conceptual dependencies of the main notions of the system of combinatory logic.

Diagramm 1

Conceptual Graph of CombLogic System

Equality: equations are formulas, Operator: application *, Constants: S and K.

The operational conceptual graph deals with the dependencies of operator and operand of combinatory operations (formulas).

Diagramm 2

Operational Conceptual