Foundation of Formal Logic

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.

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.)

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.