Can someone explain the connection between them? For example i have read about Hofstadter's MIU System and don't know how it relates to first order logic. What do formal systems and first order logic have in common? What is the difference between them?


"First-order logic" is a relatively well defined family of systems. Apart from minor differences, "first order logic" as described in one contemporary book is equivalent to "first-order logic" as defined in another.

"Formal system" is not very well defined. It is a general, informal term for various sorts of systems that are studied in logic, philosophy, and computer science. One thing that most of these have in common is a rigorously defined set of "sentences", "formulas", "expressions", or similar. After that, they differ wildly.

  • Some have inference rules, som do not. The inference rules can be very different.

  • Some have a notion of semantics or truth values, others don't. When they do have a notion of semantics, it can be extremely different from one system to another.

So the relationship is that first-order logic is one way of making the informal notion of "formal system" precise, but there are many other things called "formal systems" that are not first-order logic.

In some contexts, authors do give a more rigorous definition of "formal system" for their own purposes. But any definition like that will vary from one author to another, and should not be taken as a general definition that applies in all contexts.

One place that a more general notion of "formal system" or "abstract logic" is used is in Lindström's theorem, which characterizes first-order logic among a broader class of "abstract logics". The definitions are sketched in a paper "Lindström’s Theorem" by Jouko Väänänen (Universal Logic: An Anthology, Springer, 2012, 231-236). The definition of "abstract logic", though, still does not include everything that could be called a "formal system".

| cite | improve this answer | |
  • $\begingroup$ Why does the wikipedia article say that fo logic is a collection of formal systems? Isn't it just one formal system with semantics? Also, can you point out some examples of this collection of formal systems? $\endgroup$ – LearningMath Nov 11 '16 at 15:50
  • $\begingroup$ There are many different versions of first-order logic, which are basically equivalent but differ in details. Some people might even say that each different language for first-order logic gives a different formal system. @notorious $\endgroup$ – Carl Mummert Nov 11 '16 at 15:51
  • $\begingroup$ Can you point out some of the different versions of first order logics and their difference? Where can I find more information about this? Can you suggest an article or a book to read about this? $\endgroup$ – LearningMath Nov 11 '16 at 15:53
  • $\begingroup$ Well, some first-order logics use only the connectives $\{\lor, \lnot\}$, others use only $\{\to, \lnot\}$, and others use all the connectives. Some include a notion of equality, while others don't. The way parentheses are used in formulas can vary from one definition of first-order logic to another. There are many equivalent deductive systems. There are at least two ways of defining the truth function of a particular model. I don't think any book summarizes all the differences - each author works with their own system. But different authors give slightly different presentations. $\endgroup$ – Carl Mummert Nov 11 '16 at 15:57
  • 1
    $\begingroup$ There are also various other logics (intuitionistic logic, three-valued logic, various infinitary logics, logics with game quantifiers, etc.), which are all formal systems different from classical first-order logic. $\endgroup$ – Mitchell Spector Nov 11 '16 at 18:36

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.