5.2: First-Order Languages

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

Expressions of first-order logic are built up from a basic vocabulary containing variables, constant symbols, predicate symbols and sometimes function symbols. From them, together with logical connectives, quantifiers, and punctuation symbols such as parentheses and commas, terms and formulas are formed.

Informally, predicate symbols are names for properties and relations, constant symbols are names for individual objects, and function symbols are names for mappings. These, except for the identity predicate \(\eq[][]\), are the non-logical symbols and together make up a language. Any first-order language \(\Lang L\) is determined by its non-logical symbols. In the most general case, \(\Lang L\) contains infinitely many symbols of each kind.

In the general case, we make use of the following symbols in first-order logic:

1. Logical symbols

   1. Logical connectives: \(\lnot\) (negation), \(\land\) (conjunction), \(\lor\) (disjunction), \(\lif\) (conditional), \(\lforall{}{}\) (universal quantifier), \(\lexists{}{}\) (existential quantifier).

   2. The propositional constant for falsity \(\lfalse\).

   3. The two-place identity predicate \(\eq[][]\).

   4. A countably infinite set of variables: \(\Obj v_0\), \(\Obj v_1\), \(\Obj v_2\), …

2. Non-logical symbols, making up the standard language of first-order logic

   1. A countably infinite set of \(n\)-place predicate symbols for each \(n>0\): \(\Obj A^n_0\), \(\Obj A^n_1\), \(\Obj A^n_2\), …

   2. A countably infinite set of constant symbols: \(\Obj c_0\), \(\Obj c_1\), \(\Obj c_2\), ….

   3. A countably infinite set of \(n\)-place function symbols for each \(n>0\): \(\Obj f^n_0\), \(\Obj f^n_1\), \(\Obj f^n_2\), …

3. Punctuation marks: (, ), and the comma.

Most of our definitions and results will be formulated for the full standard language of first-order logic. However, depending on the application, we may also restrict the language to only a few predicate symbols, constant symbols, and function symbols.

Example \(\PageIndex{1}\)

The language \(\Lang L_A\) of arithmetic contains a single two-place predicate symbol \(<\), a single constant symbol \(\Obj 0\), one one-place function symbol \(\prime\), and two two-place function symbols \(+\) and \(\times\).

Example \(\PageIndex{2}\)

The language of set theory \(\Lang L_Z\) contains only the single two-place predicate symbol \(\in\).

Example \(\PageIndex{3}\)

The language of orders \(\Lang L_\le\) contains only the two-place predicate symbol \(\le\).

Again, these are conventions: officially, these are just aliases, e.g., \(<\), \(\in\), and \(\le\) are aliases for \(\Obj A^2_0\), \(\Obj 0\) for \(\Obj c_0\), \(\prime\) for \(\Obj f^1_0\), \(+\) for \(\Obj f^2_0\), \(\times\) for \(\Obj f^2_1\).

In addition to the primitive connectives and quantifiers introduced above, we also use the following defined symbols: \(\liff\) (biconditional), truth \(\ltrue\).

A defined symbol is not officially part of the language, but is introduced as an informal abbreviation: it allows us to abbreviate formulas which would, if we only used primitive symbols, get quite long. This is obviously an advantage. The bigger advantage, however, is that proofs become shorter. If a symbol is primitive, it has to be treated separately in proofs. The more primitive symbols, therefore, the longer our proofs.

You may be familiar with different terminology and symbols than the ones we use above. Logic texts (and teachers) commonly use either \(\sim\), \(\neg\), and ! for “negation”, \(\wedge\), \(\cdot\), and \(\&\) for “conjunction”. Commonly used symbols for the “conditional” or “implication” are \(\rightarrow\), \(\Rightarrow\), and \(\supset\). Symbols for “biconditional,” “bi-implication,” or “(material) equivalence” are \(\leftrightarrow\), \(\Leftrightarrow\), and \(\equiv\). The \(\lfalse\) symbol is variously called “falsity,” “falsum,” “absurdity,” or “bottom.” The \(\ltrue\) symbol is variously called “truth,” “verum,” or “top.”

It is conventional to use lower case letters (e.g., \(a\), \(b\), \(c\)) from the beginning of the Latin alphabet for constant symbols (sometimes called names), and lower case letters from the end (e.g., \(x\), \(y\), \(z\)) for variables. Quantifiers combine with variables, e.g., \(x\); notational variations include \(\forall x\), \((\forall x)\), \((x)\), \(\Pi x\), \(\bigwedge_x\) for the universal quantifier and \(\exists x\), \((\exists x)\), \((Ex)\), \(\Sigma x\), \(\bigvee_x\) for the existential quantifier.

We might treat all the propositional operators and both quantifiers as primitive symbols of the language. We might instead choose a smaller stock of primitive symbols and treat the other logical operators as defined. “Truth functionally complete” sets of Boolean operators include \(\{ \lnot, \lor \}\), \(\{ \lnot, \land \}\), and \(\{ \lnot, \lif\}\)—these can be combined with either quantifier for an expressively complete first-order language.

You may be familiar with two other logical operators: the Sheffer stroke \(|\) (named after Henry Sheffer), and Peirce’s arrow \(\downarrow\), also known as Quine’s dagger. When given their usual readings of “nand” and “nor” (respectively), these operators are truth functionally complete by themselves.