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.

  • $\begingroup$ I don't know how you expect such a thing to be possible. Even correct application of formal rules is ultimately grounded in intuition. Can you give an argument for a formal deduction rule, say modus ponens, that isn't circular or ultimately just an appeal to our sense of what feels right? $\endgroup$ – Christian Sykes Feb 22 '18 at 9:47
  • 1
    $\begingroup$ Besides, Gödel's completeness theorem justifies the connection between semantics and syntax in as ironclad a manner as could be hoped for. $\endgroup$ – Christian Sykes Feb 22 '18 at 9:51
  • 1
    $\begingroup$ By the regress argument, if you always require whatever notion you use to be justified in terms of prior concepts, then you can never be satisfied. $\endgroup$ – Hurkyl Feb 22 '18 at 15:51
  • 1
    $\begingroup$ @Mark Even if I was willing to accept “formula” as a primitive notion, that wouldn’t be enough. Because given a formula and a “rule” (i.e. another formula) you should always be able to decide if it matches or not. You need the concept of “matching” and some form of structural induction, which usually implies knowledge of naturals numbers. $\endgroup$ – Alex123 Feb 23 '18 at 6:08
  • 1
    $\begingroup$ @Hurkyl That’s not what I want to do, I just want the primitive notions to be clearly identified and explained as best as we could in natural language. I was wondering if a lot of the things that are usually assumed as primitive could be explained in terms of more primitive concepts (i.e. concepts that are easier to explain in natural language). $\endgroup$ – Alex123 Feb 23 '18 at 6:32

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.


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.


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


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.

  • $\begingroup$ "Hillbert proposed a program to formally and very carefully work out all the details of mathematical foundations. Russell and Whitehead took on this (huge) task, resulting in the Principia Mathematica." I believe Hilbert's foundation/logic program did not develop until several years AFTER the Russell and Whitehead book appeared. $\endgroup$ – Dave L. Renfro Feb 22 '18 at 20:23
  • $\begingroup$ @DaveL.Renfro Yes, of course, thanks for pointing that out. I clarified that section a bit. $\endgroup$ – Burnsba Feb 22 '18 at 21:05
  • $\begingroup$ For what it's worth, neither of us have really answered the question, which incidentally I just upvoted (something I should have done earlier, when I realized it wasn't another metalanguage question). When I originally read it, I wasn't paying that close attention and just figured it was another question about metalanguage stuff (e.g. why is it not circular to use set theory notions when developing logic, which in turn is used to develop set theory notions), and when I realized this after posting my answer I went back and slightly modified it (but still not really answering the question). $\endgroup$ – Dave L. Renfro Feb 22 '18 at 21:18
  • $\begingroup$ I know that in today “application focused” world, wondering about foundational topics is usually considered not worth of the effort. But sometime I can’t help to think that we rely too much on intuition to define formal concepts. Is like the dust under the carpet, no one is going to see it, but it still bugs you. @DaveL.Renfro Thanks for the Kleene reference, I will look that up. $\endgroup$ – Alex123 Feb 23 '18 at 6:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.