What is the difference between a First Order Logic and a First Order Theory. Can anybody please describe what each one precisely (formally) is?

For a bit more elaboration on the question, I think that for a theory which is specified in a First order Logic, it might be possible to have it specified in another logic. So if a logic is independent of any theory, how we can characterize it? for example, how can we characterize First Order logic, introduce a new logic, and how can we translate between them?

Reference to a helpful book which clearly define above concepts is appreciated.

Update: Some people thought that I do not have basic knowledge of First-Order Logic! At least I practically used it in a specification of a small-scale system. I also somehow understand what the theory is! So by this question, I intended to dig down a bit more on each one's understanding and distinguish both clearly.


  • $\begingroup$ For a first introduction: en.wikipedia.org/wiki/First-order_logic. My book in Mathematical Logic course: Van Dalen, Logic and structure $\endgroup$
    – Manlio
    Jan 20, 2015 at 22:12
  • $\begingroup$ First order logic : First order theory :: Algebra : Fields $\endgroup$
    – user203787
    Jan 20, 2015 at 22:13
  • 2
    $\begingroup$ Your should try reading a book like Enderton's Mathematical logic. $\endgroup$
    – user203787
    Jan 20, 2015 at 22:17

2 Answers 2


First-order logic is the rules that determine which propositions follow from other propositions.

More rigorously we can say that "(classical) first-order logic" consists of (1) a set of rules for what well-formed formulas are, given a particular non-logical vocabulary, and (2) a transitive(ish) relation $\vdash$ between finite sets of wffs and wffs, intuitively denoting "this formula can be derived from these other formulas".

There are several different ways of defining the $\vdash$ relation of classical first-order logic, such as by a Hilbert system, or by natural deduction or sequent calculus (or for that matter we can define it to be identical to semantic entailment after developing some rudimentary model theory). These all define one and the same logic, at least according to one way of looking at it.

A first order theory is a particular set of axioms whose consequences (according to first-order logic) you're interested in.

In other words, a "first-order theory" consists of (a) a first-order vocabulary, from which the generic first-order logic rules derive a concept of "well-formed formula", and (b) a particular set of well-formed formulas over that vocabulary, which we we call the "axioms" of the theory.

Classical first-order logic shares its rules for how well-formed formulas look with some other logics, such as intuitionistic first-order logic. So if we have a first-order theory, we can -- at least in principle -- also consider which formulas can be derived from its axioms under the intuitionistic entailment rule. But in practice that rarely work well because when people design first-order theories to be used with the classical rules, they don't generally care to distinguish between formulations of the axioms that are classically equivalent but intuitionistically distinct. So the set of intuitionistic consequences of a theory that's made to be interpreted by classical logic can be somewhat random.

  • $\begingroup$ To a person who doesn't understand what first order logic/theory means, your answer could be quite hard to follow. $\endgroup$
    – user203787
    Jan 20, 2015 at 22:19
  • $\begingroup$ @OohAah: Perhaps, but I'm assuming that the OP has had some exposure to how FOL works and merely needs to have explained how the words match up with the technical definitions he has learned. $\endgroup$ Jan 20, 2015 at 22:25
  • $\begingroup$ Okay. On second reading, I understand your answer better now. $\endgroup$
    – user203787
    Jan 20, 2015 at 22:29
  • $\begingroup$ One of us should probably say something about the discrepancy between our answers... And I'm already in bed. :-P $\endgroup$
    – Asaf Karagila
    Jan 20, 2015 at 22:57

First-order logic is a term for a general framework, in which we have a basic language including some symbols for relations, constants, functions and free variables; as well basic propositional calculus and existential and universal quantifiers, and in this framework a quantifier is only allowed to bound a free variable (representing an element of the universe of discourse).

This framework also includes basic inference rules that allow us to prove sentences from other sentences and from the basic axioms of the logic. And it also includes semantics, namely translating from statements written in the language, to "actual objects". The semantic part requires some set theory foundations, and we can omit it if we choose to.

Note that there are several ways to write the axioms and definitions of first-order logic (we may choose some inference rules, but not others; some connectives or some quantifiers; etc. but all these ways are essentially equivalent).

We say that $T$ is a first-order theory if $T$ is a set of sentences written in some language using first-order logic.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .