Editing First-order logic (section)

===Restricted languages===
First-order logic can be studied in languages with fewer logical symbols than were described above:
* Because <math>\exists x \varphi(x)</math> can be expressed as <math>\neg \forall x \neg \varphi(x)</math>, and <math>\forall x \varphi(x)</math> can be expressed as <math>\neg \exists x \neg \varphi(x)</math>, either of the two quantifiers <math>\exists</math> and <math>\forall</math> can be dropped.
* Since <math>\varphi \lor \psi</math> can be expressed as <math>\lnot (\lnot \varphi \land \lnot \psi)</math> and <math>\varphi \land \psi</math> can be expressed as <math>\lnot(\lnot \varphi \lor \lnot \psi)</math>, either <math>\vee</math> or <math>\wedge</math> can be dropped. In other words, it is sufficient to have <math>\neg</math> and <math>\vee</math>, or <math>\neg</math> and <math>\wedge</math>, as the only logical connectives.
* Similarly, it is sufficient to have only <math>\neg</math> and <math>\rightarrow</math> as logical connectives, or to have only the [[Sheffer stroke]] (NAND) or the [[Peirce arrow]] (NOR) operator.
* It is possible to entirely avoid function symbols and constant symbols, rewriting them via predicate symbols in an appropriate way. For example, instead of using a constant symbol <math> \; 0 </math>  one may use a predicate  <math> \; 0(x) </math>  (interpreted as <math> \; x=0 </math> ) and replace every predicate such as <math>\; P(0,y) </math> with <math> \forall x \;(0(x) \rightarrow P(x,y)) </math>. A function such as <math> f(x_1,x_2,...,x_n) </math> will similarly be replaced by a predicate  <math> F(x_1,x_2,...,x_n,y) </math> interpreted as <math> y = f(x_1,x_2,...,x_n) </math>. This change requires adding additional axioms to the theory at hand, so that interpretations of the predicate symbols used have the correct semantics.<ref>[[Left-total]]ity can be expressed by an axiom <math>\forall x_1,...,x_n. \exists y. F(x_1,...,x_n,y)</math>; [[right-unique]]ness by <math>\forall x_1,...,x_n,y,y'.</math> <math>F(x_1,...,x_n,y) \land F(x_1,...,x_n,y') \rightarrow y=y'</math>, provided the equality symbol is admitted. Both also apply to constant replacements (for <math>n=0</math>).</ref>

Restrictions such as these are useful as a technique to reduce the number of inference rules or axiom schemas in deductive systems, which leads to shorter proofs of metalogical results. The cost of the restrictions is that it becomes more difficult to express natural-language statements in the formal system at hand, because the logical connectives used in the natural language statements must be replaced by their (longer) definitions in terms of the restricted collection of logical connectives. Similarly, derivations in the limited systems may be longer than derivations in systems that include additional connectives. There is thus a trade-off between the ease of working within the formal system and the ease of proving results about the formal system.

It is also possible to restrict the arities of function symbols and predicate symbols, in sufficiently expressive theories. One can in principle dispense entirely with functions of arity greater than 2 and predicates of arity greater than 1 in theories that include a [[pairing function]]. This is a function of arity 2 that takes pairs of elements of the domain and returns an [[ordered pair]] containing them. It is also sufficient to have two predicate symbols of arity 2 that define projection functions from an ordered pair to its components. In either case it is necessary that the natural axioms for a pairing function and its projections are satisfied.