From New World Encyclopedia

Metalogic is a study of formal languages of logic from both syntactic and semantic perspectives. Formal languages consist of vocabulary (constants, variables, connectives, etc.) and formation rules (or grammar) of formulas in the language. Semantics concerns the interpretations of the elements of formal languages. Syntax provides deductive devices for formal languages on the top of their vocabulary and formation rules. Some of the most important properties that are frequently studied in metalogic are: soundness, completeness (in various sense), compactness, decidability, etc.

Formal Languages of Logic

Formal languages are artificial languages designed to clearly express statements in various areas of studies. There are varieties of formal languages and they are chosen depending on the subjects and the purposes of studies. A formal language consists of vocabulary and formation rules. Vocabulary postulates the linguistic symbols that are used to build the expressions. (To see the point, consider natural languages. Say, English provides "small," "tall" and etc. as a part of its vocabulary.) The formation rules define the ways to build the expressions from the vocabulary. (Again in the case of English, we can form a noun phrase "small dog" based on the grammar of English.)

One of the simplest (but also the most important) examples of formal languages is the language of propositional logic (let us denote this language as PL). The vocabulary of PL consists of:

  1. Propositional variables, p, q, r,…, (which are considered to stand for propositions)
  2. Propositional connectives , , , , , (interpreted as sentential connectives in natural language: not, and, or, if…then…, …if and only if…respectively in order)
  3. parentheses, "(," ")."

The formation rules of PL are given inductively and define the permissible formulas in PL, called well-formed formulas (abbreviated as wff). The definition of wffs is as follows:

  • a. A propositional variable is a wff.
  • b. If is a wff, then is a wff.
  • c. If and are both wffs, then , , , are all wffs.
  • d. Things built from a, b, c exhaust the wffs.

Observe that, say, “” is a wff by this inductive definition. Other frequently used formal languages are first-order logic, second-order language, languages of modal logic, etc.


(For a general explanation about Semantic in linguistics, see Semantics.)

Formal languages, as they are, just stipulate meaningless strings of symbols. Semantics takes care of the aspects about the meanings of the symbols in the language and defines the relevant important notions for linguistic expressions. An interpretation (also called a model, a structure, etc) of a given formal language determines various kinds of assignments to the symbols of the language. In our previous example, PL, an interpretation is a function that assigns one or zero (considered to be truth and falsity usually) to propositional variables. Likewise, interpretations for various kinds of languages are given in similar ways so that certain kinds of entities are assigned to the expressions of the languages.

The notion of truth is defined relative to an interpretation for all the wffs. For instance, in PL, the notion of truth is inductively defined as follows ( and are both wffs):

  • a. p is true under (with p a propositional variable) iff .
  • b. is true under iff is true under and is true under .
  • c. is true under iff is true under or is true under .
  • d. is true under iff is not true under or is true under .
  • e. is true under iff is true under and is true under , or is not true under and is true under .

(To see how the definition works, consider, say, “” under an interpretation that assigns zero to both p and q. First, a wff is true under since is false (). Thus, turns out to be true under .) We often put "" to be read as " is true under ." Also, given an interpretation , we call the theory of a set of wffs that are true under .

Another set of important semantic notions are the notions of satisfiability and validity. These notions are defined based on the notion of truth. A wff in a formal language L is satisfiable if and only if there is an interpretation such that that is true under . Similarly we call a set of wffs satisfiable if and only if there is an interpretation such that all the sentences in are true under . For example, consider the wff "" and "." The former is satisfiable since it is true under the interpretation such that and , while it is not difficult to see that the latter is not satisfiable. A wff is valid if and only if is true under all the interpretation for L. In PL, consider, say, the wff "." This wff turns out to be true no matter which value, zero or one, p gets assigned; therefore, the wff is valid.


(For a general explanation of Syntax in linguistics, see Syntax)

While the semantics of a formal language deals with the assignments of the meanings to the symbols and the relevant notions, truth, validity etc., the syntax of a formal language, in addition to the formation rules of wffs, deals with a transformation of wffs of distinguished forms based on the transformation rules. This transformational setting of a formal language is called a deductive system (based on the formal language).

Given a formal language, a deductive system is specified with the set of logical axioms and the rules of inferences. Logical axioms are given by wffs or forms of wffs, and the rules of inference determines the permissible ways of transforming given wffs. If a wff can be obtained as a result of transforming some of the logical axioms by the rules of inferences, is said to be provable or a theorem in the deductive system.

For instance, a deductive system in PL can be given as follows (for simplicity, the outermost parentheses of wffs are omitted below). First, we define formulas of the forms , , respectively as , , . Observe that, with this definition, we can always rewrite all the wffs in PL with only propositional variables, , and . Now, the logical axioms are given as the wffs of the forms that are specified in the following schemas:

  • A1
  • A2
  • A3

Also, the rule of inference of the deductive system is given as the following rule (generally called modus ponens and modus tollens):

  • MP If you have the wffs of the forms and , then obtain .

For example, observe that "" is an axiom by A1 and that "" is an axiom by A3. Then, we obtain "" as a theorem in this deductive system by MP.

There are other types of deductive systems in PL and also there are various deductive systems in other types of formal languages.

On the top of deductive systems, we often consider additional nonlogical axioms (specified wffs other than logical axioms) that characterize the main subjects in a given area of study. In such cases, we consider axiomatic systems, which are specified as the set of nonlogical axioms (of course, deductive systems are also axiomatic systems in the sense that the set of specified nonlogical axioms is empty). Given an axiomatic system A, we call a wff provable in A if it is obtainable from logical axioms and the nonlogical axioms in A based on the rules of inferences.

Basic Metalogical Properties

Metalogic is the study of formal languages from semantic and syntactic perspectives. Among the metalogical properties of formal languages, we will look at some of the most basic and important ones below to get the sense about what the metalogical properties are like. The list consists of soundness, completeness (in at least two important senses), compactness, and decidability.

Soundness and Completeness

The first set of metalogical notions that we look at are the soundness and completeness. These notions connect the semantic notion of validity and the syntactic notion of provability (or theoremhood) in the following way. A deductive system is called sound if, for every wff , the provability of implies the validity of . Also, a deductive system is called complete if, for every wff , the validity of implies the provability of .

Many formal languages are known with respect to which semantics S and deductive systems D are given so that D is both sound and complete with respect to S. In fact, in our example of PL, its semantics and its deductive system are one of sound and complete formal systems. Also, it is well known that we can have semantics and deductive systems on the first-order logic that are both sound and complete, and also on modal logic.

However, there are other languages on which there are no complete deductive systems. One famous example is the second-order logic.


The next metalogical property is compactness. This property mainly concerns the notion of satisfiablity. A language L is compact if, for every set of wffs in L, is satisfiable if every finite subset of wffs in is satisfiable.

PL and other formal languages such as first-order logic and many languages for modal logic are known to be compact. However, languages such as second-order language are known not to be compact.


Another important metalogical property is completeness in a different sense from the one above. An axiomatic system is complete if, for every wff , either itself or is provable in A.

There are many axiomatic systems that are known to be complete. One famous example is Presburger arithmetic (roughly speaking, it is a theory in the first-order logic for the arithmetric only with addition) etc. On the other hand, there are many axiomatic systems that are known to be incomplete. Famous examples are Peano arithmetic, which is an axiomatic system for a full arithmetic.


Decidability is also one of the important metalogical properties. One formulation of this property is as follows. A theory in a language L (for the definition of theory, see the paragraph above on the notion of truth in the semantics section) is said to be decidable if there is an effective procedure through which, for every wff in L, we can determine whether is in the theory or not.

There are various theories that are known to be decidable. For instance, Presburger arithmetic is one of them. On the other hand, Peano arithmetic is a famous example of the theories that are known to be undecidable.

ISBN links support NWE through referral fees

  • Barwise, Jon and John Etchemendy. 2002. Language, Proof and Logic. CSLI Publication. ISBN 157586374X
  • Boolos, George, John Burgess, and Richard Jeffrey. 2002. Computability and Logic, 4th ed. Cambridge University ISBN 0521809754
  • Enderton, Herbert. 2002. A Mathematical Introduction to Logic, 2nd ed. Academic Press. ISBN 0122384520
  • Hodges, Wilfred. 1997. A Shorter Model Theory. Cambridge University Press. ISBN 0521587131
  • Mendelson, Elliott. 1997. Introduction to Mathematical Logic, 4th ed. Champan & Hall. ISBN 0412808307
  • Troelstra A. S. and H. Schwichtenberg. 2000. Basic Proof Theory, 2nd. ed. Cambridge University Press. ISBN 0521779111

External links

All links retrieved November 9, 2022.

General Philosophy Sources


This article began as an original work prepared for New World Encyclopedia and is provided to the public according to the terms of the New World Encyclopedia:Creative Commons CC-by-sa 3.0 License (CC-by-sa), which may be used and disseminated with proper attribution. Any changes made to the original text since then create a derivative work which is also CC-by-sa licensed. To cite this article click here for a list of acceptable citing formats.

Note: Some restrictions may apply to use of individual images which are separately licensed.