2.1.3: Terms and Formulas

\(\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} } }\)

Once a first-order language \(\Lang L\) is given, we can define expressions built up from the basic vocabulary of \(\Lang L\). These include in particular terms and formulas.

Definition \(\PageIndex{1}\): Terms

The set of terms \(\Trm[L]\) of \(\Lang L\) is defined inductively by:

1. Every variable is a term.
2. Every constant symbol of \(\Lang L\) is a term.
3. If \(f\) is an \(n\)-place function symbol and \(t_1\), …, \(t_n\) are terms, then \(\Atom{f}{t_1, \ldots, t_n}\) is a term.
4. Nothing else is a term.

A term containing no variables is a closed term.

The constant symbols appear in our specification of the language and the terms as a separate category of symbols, but they could instead have been included as zero-place function symbols. We could then do without the second clause in the definition of terms. We just have to understand \(\Atom{f}{t_1, \ldots, t_n}\) as just \(f\) by itself if \(n = 0\).

Definition \(\PageIndex{2}\): Formula

The set of formulas \(\Frm[L]\) of the language \(\Lang L\) is defined inductively as follows:

1. \(\lfalse\) is an atomic formula.
2. If \(R\) is an \(n\)-place predicate symbol of \(\Lang L\) and \(t_1\), …, \(t_n\) are terms of \(\Lang L\), then \(\Atom{R}{t_1,\ldots, t_n}\) is an atomic formula.
3. If \(t_1\) and \(t_2\) are terms of \(\Lang L\), then \(\Atom{\eq[][]}{t_1, t_2}\) is an atomic formula.
4. If \(A\) is a formula, then \(\lnot A\) is formula.
5. If \(A\) and \(B\) are formulas, then \((A \land B)\) is a formula.
6. If \(A\) and \(B\) are formulas, then \((A \lor B)\) is a formula.
7. If \(A\) and \(B\) are formulas, then \((A \lif B)\) is a formula.
8. If \(A\) is a formula and \(x\) is a variable, then \(\lforall{x}{A}\) is a formula.
9. If \(A\) is a formula and \(x\) is a variable, then \(\lexists{x}{A}\) is a formula.
10. Nothing else is a formula.

The definitions of the set of terms and that of formulas are inductive definitions. Essentially, we construct the set of formulas in infinitely many stages. In the initial stage, we pronounce all atomic formulas to be formulas; this corresponds to the first few cases of the definition, i.e., the cases for \(\lfalse\), \(\Atom{R}{t_1,\dots,t_n}\) and \(\Atom{\eq[][]}{t_1,t_2}\). “Atomic formula” thus means any formula of this form.

The other cases of the definition give rules for constructing new formulas out of formulas already constructed. At the second stage, we can use them to construct formulas out of atomic formulas. At the third stage, we construct new formulas from the atomic formulas and those obtained in the second stage, and so on. A formula is anything that is eventually constructed at such a stage, and nothing else.

By convention, we write \(\eq[][]\) between its arguments and leave out the parentheses: \(\eq[t_1][t_2]\) is an abbreviation for \(\Atom{\eq[][]}{t_1,t_2}\). Moreover, \(\lnot \Atom{\eq[][]}{t_1,t_2}\) is abbreviated as \(\eqN[t_1][t_2]\). When writing a formula \((B \ast C)\) constructed from \(B\), \(C\) using a two-place connective \(\ast\), we will often leave out the outermost pair of parentheses and write simply \(B \ast C\).

Some logic texts require that the variable \(x\) must occur in \(A\) in order for \(\lexists{x}{A}\) and \(\lforall{x}{A}\) to count as formulas. Nothing bad happens if you don’t require this, and it makes things easier.

Definition \(\PageIndex{3}\)

Formulas constructed using the defined operators are to be understood as follows:

1. \(\ltrue\) abbreviates \(\lnot\lfalse\).
2. \(A \liff B\) abbreviates \((A \lif B) \land (B \lif A)\).

If we work in a language for a specific application, we will often write two-place predicate symbols and function symbols between the respective terms, e.g., \(t_1 < t_2\) and \((t_1 + t_2)\) in the language of arithmetic and \(t_1 \in t_2\) in the language of set theory. The successor function in the language of arithmetic is even written conventionally after its argument: \(t'\). Officially, however, these are just conventional abbreviations for \(\Atom{\Obj A^2_0}{t_1, t_2}\), \(\Obj f^2_0(t_1, t_2)\), \(\Atom{\Obj A^2_0}{t_1, t_2}\) and \(f^1_0(t)\), respectively.

Definition \(\PageIndex{4}\): Syntactic identity

The symbol \(\ident\) expresses syntactic identity between strings of symbols, i.e., \(A \ident B\) iff \(A\) and \(B\) are strings of symbols of the same length and which contain the same symbol in each place.

The \(\ident\) symbol may be flanked by strings obtained by concatenation, e.g., \(A \ident (B \lor C)\) means: the string of symbols \(A\) is the same string as the one obtained by concatenating an opening parenthesis, the string \(B\), the \(\lor\) symbol, the string \(C\), and a closing parenthesis, in this order. If this is the case, then we know that the first symbol of \(A\) is an opening parenthesis, \(A\) contains \(B\) as a substring (starting at the second symbol), that substring is followed by \(\lor\), etc.