Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

When was the idea of a well-formed formula first stated or can get inferred as such under another name?

share|cite|improve this question
at they give links to translations. I cannot be positive it was Frege, of course. – Will Jagy Sep 27 '12 at 1:33

That's an interesting historical question. The answer, I think, must be "rather later than you might imagine". The idea isn't in Frege. Frege's Begriffsschrift, his 'concept-script', is apparatus added to mathematical German for the purpose of rigorously expressing logical relations; he didn't think of it as a stand-alone formal language with a closed set of syntactic rules in the modern sense. The idea of a (well-formed) formula certainly isn't sharply defined in the famously careless Principia.

The idea is, however, explicitly there in Hilbert and Ackermann's Grundzüge der Theoretischen Logik of 1928. You will find the now familiar kind of recursive definition for the wffs of a predicate calculus at p. 66 of the English translation. I wouldn't at all be surprised to learn that Hilbert in his lectures earlier in the 1920s gave the first really clear statement.

It really is difficult to exaggerate the historical significance of Hilbert and Ackermann's book (and hence of Hilbert's earlier lectures on which it is based). The first recognisably 'modern' logic book, it is still very worth reading.

share|cite|improve this answer
Can you elaborate on "famously careless Principia"? – Michael Greinecker Sep 27 '12 at 10:00
@MichaelGreinecker I was being unnecessarily rude, and perhaps "careless" isn't quite the right word. But Principia does fall short of modern standards of explicit formal rigour. For example, as Randall Holmes has noted, "The type theory of PM is not formalized at all: in fact, no notation for types is presented anywhere in PM." So writing a type-checker for PM is a non-trivial task. – Peter Smith Sep 27 '12 at 10:16
That's quite interesting. I always thought that it was this überformalist project. I haven't read it of course. – Michael Greinecker Sep 27 '12 at 10:18
I think the "famously careless Principia" comment fair in a sense. Godel pointed that out. Also, the Wikipedia page points out that it did have this definition: ✸3.02. p ⊃ q ⊃ r .=. p ⊃ q . q ⊃ r Df. But, p ⊃ q ⊃ r is ambiguous. – Doug Spoonwood Sep 28 '12 at 2:39

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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