Foundation of Formal Logic

Question

All the books that I’ve read about formal logic either starts assuming the existence of set theory (they talk of countable sets of symbols and define formulae as sequences of symbols), or follow an axiomatic approach that assumes known the meaning of words like symbol, formula, substitution etc. Is there a way to formalize these concepts (with no reference to set theory, I consider set theory a product of formal logic)?

We could assume as primitive the notion of symbol, but could the concepts of string, formula, composition of formulae be rendered in more precise way that don’t rely on intuition? A book or paper reference on this matter would be appreciated.

Answer 1

Regarding the issue with defining strings and such, the most formal published discussions I know of are those I indicated in my answer to Highly Rigorous Logic Book.

In general, you might try googling metalanguage + logic.

I used to struggle with metalogic issues a lot myself, many years ago, and I still struggle a little now when reading some about some foundational topic that makes heavy use of mathematics in the metalanguage (for an example, see my answer to this question).

Here is a silly discussion that might help in thinking about the distinction between metalanguage and object language:

You are reading a formal logic book. Near the beginning of the book the author writes the following: "Recall the example we gave 3 sentences earlier $\ldots$" Since this occurs well before any construction or definition of the natural numbers, how would you suggest the sentence be rewritten? Maybe the author could say "Recall the most recent example we gave $\ldots$". However, this assumes certain aspects of the notion of an order, such as the idea of "before" and "after".

Or, suppose later in the book, the author cites a certain result, saying that it "can be found on page 235". Now the author is also using properties of decimal numerals, such as 235 = 200 + 30 + 5, this also well before the natural numbers are defined in some way, such as $\;0 = \emptyset,$ $\;1 = \{\emptyset\},\;$ $\;2=\{\emptyset, \{\emptyset\}\},$ $\ldots,$ which in turn is well before decimal numeral representations for the natural numbers are defined.

(ADDED A MONTH LATER) I recently came across a book review I have (photocopied about 12 years ago from a library journal volume) of Introduction to Mathematical Logic by Alonzo Church that gives a useful discussion of these logic and metalogic issues. The review is by Martin David Davis and the review appears on pp. 84-86 of Scripta Mathematica 24 (1959). What follows is approximately the first 2/3 of the review, on pp. 84-85.

Although nothing here actually answers the question Alex123 asked, it does provide more context for the question. I suspect the question more properly belongs to philosophy than to mathematics, and I suspect it is discussed in one or more philosophy papers somewhere, but I don't have any specific references to offer at this time.

This book is a comprehensive introduction to modern logic. Although no previous knowledge of mathematical logic is presumed, the reader is expected to have considerable mathematical maturity. (Roughly speaking, the text is suitable for first year graduate students.)

Unlike many works in this field, this book does not limit itself to the development of one definite system of logic. Rather, a series of such systems is studied. The key technique employed is what Church calls "the logistic method."

Mathematical logic is principally concerned with formal reasoning. However, any attempt to develop this subject matter as a deductive system---in the sense of, say, Euclidean geometry---comes up against a seemingly insurmountable obstacle. Namely, the usual technique of beginning with suitable axioms and then employing logic to derive theorems, i.e., logical consequences of the axioms, is clearly inappropriate when the subject matter itself is logic. Put otherwise, any attempt to develop logic as the study of the logical consequences of certain axioms is circular in that the laws of logic are used in obtaining the laws of logic. The logistic method provides a means for overcoming this difficulty. One begins by rigorously specifying exactly which symbols will be employed in the development. This specification must be complete and unambiguous. E.g., punctuation marks such as commas and parentheses must be included if they are going to be used; only those letters of the alphabet which are listed may be used. Among the various finite sequences that can be formed from these symbols, certain ones are distinguished as well-formed formulas. It is the well-formed formulas that are to be thought of as being "meaningful." The criterion for a finite sequence of symbols being a well-formed formula must be effective in the sense that there must be a purely mechanical procedure for determining whether or not a given finite sequence of symbols is a well-formed formula. Next, certain of the well-formed formulas are set aside as axioms. Again, it is demanded that there be an effective criterion for determining whether or not a well-formed formula is an axiom. (This last requirement is automatically satisfied in case the number of axioms is finite; often it is convenient, or even necessary, to work with an infinite number of axioms.) Finally rules of inference are specified. It is these rules of inference which enable one to derive theorems from the given axioms. The circularity referred to above is avoided because the rules of inference refer only to the symbols of which well-formed formulas are constructed, and not at all to any "meaning" which might be attributed to the well-formed formulas. Thus, a system of logic (or logistic system) whose primitive symbols include (among others) $[\;\;] \;\; \supset$ might well have the following rule of inference:

If A and B are well-formed formulas then one may infer B from A and [A $\supset$ B].

Here it is understood that [A $\supset$ B] is the well-formed formula which begins with [, followed by the symbols which make up A, followed by $\supset,$ followed by the symbols which make up B, followed by ]. The rules of inference of a logistic system are also required to be effective. That is, there must be available a mechanical procedure for determining whether or not a given well-formed formula can be inferred from other given well-formed formulas by means of the rules of inference.

A logistic system, once set up, is itself a mathematical object concerning which many questions can be asked. The answers to such questions are sought using the methods of ordinary mathematics. No circularity is involved since these mathematical techniques are employed, not to develop the logistic system, but to obtain information about it from without.

The study of a logistic system in this way, as involving finite sequences of symbols without reference to meaning, is called the syntax of the logistic system, in contradistinction to the study of possible interpretations of the system, which is called the semantics of the system.

Answer 2

I think perhaps it might be helpful to get a brief summary of mathematical foundations from the early-mid 20th century.

Cantor had made some important contributions to set theory (e.g. there is no bijection between $\mathbb N$ and $\mathbb R$), but there were some outstanding issues with foundations at the time (does the set of all sets contain "the set that does not contain itself?"). Russell and Whitehead spent some time working out the details and formalizing foundations so as to avoid these kinds of paradoxes. The result was the Principia Mathematica. (Hillbert, who had contributed to foundation issues earlier in the 20th century, wanted a similar work, but at a deeper level, and this came to be known as Hillbert's program. )

I think that is the kind of book you are looking for (though I wouldn't recommend reading this). The purpose of the book is to cover all the ground work and preliminary details to explain foundations (what it sounds like you want) but also to give a foundation for all mathematical statements. The book goes into excruciating detail to cover necessary background. As wikipedia says:

PM has long been known for its typographical complexity. Famously, several hundred pages of PM precede the proof of the validity of the proposition 1+1=2.

That is, it's almost 400 pages of preliminary work before being able to show $1+1=2$.

However.

Not too long after PM was Godel's incompleteness theorem. One of the side effects of this was to show that Hillbert's program was not possible: no self-contained set of axioms can build a formal system that proves it's own validity. This doesn't mean PM is useless for describing a formal system, but it is useless in trying to build up some foundation so that all mathematical statements can be proven.

That was all before the middle of the 20th century. What that means is (now) there's rarely a good reason to spend a lot of time formally defining a concept when it's application doesn't depend on a precise formal definition, and when it does matter authors will note aspects of that as needed. (That is, authors assume familiarity with the subject and don't spend more than passing remarks on trivial matters)

---

Now, if instead of set theory foundations you are asking about formalizing theories of symbols and formulas then look into Type Theory, perhaps lambda calculus or Intuitionistic Type Theory.

Answer 3

Ah, the old egg-chicken problem: the math version.

Unfortunately I have no reference on the subject which I believe belong to the field of philosophy, nevertheless here are some personal considerations on the matter.

If I understand the question correctly you are asking if it is possible to do formal logic without any set theory.

In order to answer this question one would probably have to define what it means to approach formally something.

This notion has changed meaning through history and probably different people can give you different definitions.

Here is my personal definition. By formal I mean that we deal with objects which can be represented through expressions on which we can apply manipulations.

In this regard to give a formal theory of something one should just provide:

• a list of objects (the symbols of an alphabeth)

• rules that describe how to build formulas from the basic alphabeth's symbols

• rules that describe how to build proofs of formulas (the inference rules, or underlying logic of the theory).

So in order to deal with these stuff you need a concept of string (or something else capable of representing formulas and proofs) and the concept of operation on strings.

With these concepts one could present a language just as a list of operations:

• some constant operations (i.e. operations with no input) that build basic expressions of the language (the atoms or axioms of the language)
• some operations that take some input-expressions (already build recursively using some specific operations) and return new expressions.

With these data one can define a formula just as any string that is defined by the rules, i.e. that can build using the rules (operations) of the language.

Observe that we can regard proofs as formulas of a language: after all we can encode proofs as finite lists of formulas, which can be represented as strings, build through the application of some operations (the inference rules).

I hope this argument could be convincing on my claim that the primitive concept required should be those of string and string-operation.

Using this approach one can formally build a theory (i.e. build all its formulas and proofs), without any reference to sets.

Nevertheless once you want to start studying formally a theory you are usually faced with the problem of considering collections of formulas and proof, so in order to do that you need a theory having expressions that encode these collections.

Clearly you can do that by providing a theory (i.e. a set of rules as described above) whose expressions stand for these collections but that is basically introducing the notion of collection axiomatically, which is not really very different to using collections as a primitive notion.

I hope this very long answer may help.

Answer 4

Here is a possible approach. Consider the minimalist language Brainfuck. This extremely stripped-down language comprises only eight commands and an instruction pointer. The first step is to train yourself to be able to execute Brainfuck programs. This does require some amount of intuition; you need the ability to read and write, at least well enough to be able to read and understand a description of the Brainfuck language. You need to be able to recognize a Brainfuck program when you see one, parse the symbols, and remember how to execute the commands using whatever writing method you have mastered. But you don't have to understand what a "symbol" is in general or what a "rule" is in general. You just have to master a very specific set of symbols and rules.

If you get this far, then in principle you have more than enough power to reproduce any formal logical proof, since Brainfuck is Turing complete. Of course, someone still has to code up logical axioms and rules in Brainfuck, but that's their problem, not yours. If they do their part, you can do your part by executing their Brainfuck programs. In this way, you can formally reproduce all of logic and mathematics, with a minimal reliance on non-formal intuition. (You won't understand anything, of course, but that doesn't seem to be your question.)