2.1.4: Unique Readability

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

The way we defined formulas guarantees that every formula has a unique reading, i.e., there is essentially only one way of constructing it according to our formation rules for formulas and only one way of “interpreting” it. If this were not so, we would have ambiguous formulas, i.e., formulas that have more than one reading or intepretation—and that is clearly something we want to avoid. But more importantly, without this property, most of the definitions and proofs we are going to give will not go through.

Perhaps the best way to make this clear is to see what would happen if we had given bad rules for forming formulas that would not guarantee unique readability. For instance, we could have forgotten the parentheses in the formation rules for connectives, e.g., we might have allowed this:

If \(A\) and \(B\) are formulas, then so is \(A \lif B\).

Starting from an atomic formula \(D\), this would allow us to form \(D \lif D\). From this, together with \(D\), we would get \(D \lif D \lif D\). But there are two ways to do this:

1. We take \(D\) to be \(A\) and \(D \lif D\) to be \(B\).
2. We take \(A\) to be \(D \lif D\) and \(B\) is \(D\).

Correspondingly, there are two ways to “read” the formula \(D \lif D \lif D\). It is of the form \(B \lif C\) where \(B\) is \(D\) and \(C\) is \(D \lif D\), but it is also of the form \(B \lif C\) with \(B\) being \(D \lif D\) and \(C\) being \(D\).

If this happens, our definitions will not always work. For instance, when we define the main operator of a formula, we say: in a formula of the form \(B \lif C\), the main operator is the indicated occurrence of \(\lif\). But if we can match the formula \(D \lif D \lif D\) with \(B \lif C\) in the two different ways mentioned above, then in one case we get the first occurrence of \(\lif\) as the main operator, and in the second case the second occurrence. But we intend the main operator to be a function of the formula, i.e., every formula must have exactly one main operator occurrence.

Lemma \(\PageIndex{1}\)

The number of left and right parentheses in a formula \(A\) are equal.

Proof. We prove this by induction on the way \(A\) is constructed. This requires two things: (a) We have to prove first that all atomic formulas have the property in question (the induction basis). (b) Then we have to prove that when we construct new formulas out of given formulas, the new formulas have the property provided the old ones do.

Let \(l(A)\) be the number of left parentheses, and \(r(A)\) the number of right parentheses in \(A\), and \(l(t)\) and \(r(t)\) similarly the number of left and right parentheses in a term \(t\). We leave the proof that for any term \(t\), \(l(t) = r(t)\) as an exercise.

1. \(\indcase{A}{\lfalse}\) \(\indfrm\) has 0 left and 0 right parentheses.
2. \(\indcase{A}{\Atom{R}{t_1,\dots,t_n}}\) \(l(\indfrm) = 1 + l(t_1) + \dots + l(t_n) = 1 + r(t_1) + \dots + r(t_n) = r(\indfrm)\). Here we make use of the fact, left as an exercise, that \(l(t) = r(t)\) for any term \(t\).
3. \(\indcase{A}{\eq[t_1][t_2]}\) \(l(\indfrm) = l(t_1) + l(t_2) = r(t_1) + r(t_2) = r(\indfrm)\).
4. \(\indcase{A}{\lnot B}\) By induction hypothesis, \(l(B) = r(B)\). Thus \(l(\indfrm) = l(B) = r(B) = r(\indfrm)\).
5. \(\indcase{A}{(B \ast C)}\) By induction hypothesis, \(l(B) = r(B)\) and \(l(C) = r(C)\). Thus \(l(\indfrm) = 1 + l(B) + l(C) = 1 + r(B) + r(C) = r(\indfrm)\).
6. \(\indcase{A}{\lforall{x}{B}}\) By induction hypothesis, \(l(B) = r(B)\). Thus, \(l(\indfrm) = l(B) = r(B) = r(\indfrm)\).
7. \(\indcase{A}{\lexists{x}{B}}\) Similarly.

◻

Definition \(\PageIndex{1}\): Proper prefix

A string of symbols \(B\) is a proper prefix of a string of symbols \(A\) if concatenating \(B\) and a non-empty string of symbols yields \(A\).

Lemma \(\PageIndex{2}\)

If \(A\) is a formula, and \(B\) is a proper prefix of \(A\), then \(B\) is not a formula.

Proof. Exercise. ◻

Problem \(\PageIndex{1}\)

Prove Lemma \(\PageIndex{2}\).

Proposition \(\PageIndex{1}\)

If \(A\) is an atomic formula, then it satisfies one, and only one of the following conditions.

1. \(A \ident \lfalse\).
2. \(A \ident \Atom{R}{t_1,\dots,t_n}\) where \(R\) is an \(n\)-place predicate symbol, \(t_1\), …, \(t_n\) are terms, and each of \(R\), \(t_1\), …, \(t_n\) is uniquely determined.
3. \(A \ident \eq[t_1][t_2]\) where \(t_1\) and \(t_2\) are uniquely determined terms.

Proof. Exercise. ◻

Problem \(\PageIndex{2}\)

Prove Proposition \(\PageIndex{1}\) (Hint: Formulate and prove a version of Lemma \(\PageIndex{2}\) for terms.)

Proposition \(\PageIndex{2}\): Unique Readability

Every formula satisfies one, and only one of the following conditions.

1. \(A\) is atomic.
2. \(A\) is of the form \(\lnot B\).
3. \(A\) is of the form \((B \land C)\).
4. \(A\) is of the form \((B \lor C)\).
5. \(A\) is of the form \((B \lif C)\).
6. \(A\) is of the form \(\lforall{x}{B}\).
7. \(A\) is of the form \(\lexists{x}{B}\).

Moreover, in each case \(B\), or \(B\) and \(C\), are uniquely determined. This means that, e.g., there are no different pairs \(B\), \(C\) and \(B'\), \(C'\) so that \(A\) is both of the form \((B \lif C)\) and \((B' \lif C')\).

Proof. The formation rules require that if a formula is not atomic, it must start with an opening parenthesis (, \(\lnot\), or with a quantifier. On the other hand, every formula that start with one of the following symbols must be atomic: a predicate symbol, a function symbol, a constant symbol, \(\lfalse\).

So we really only have to show that if \(A\) is of the form \((B \ast C)\) and also of the form \((B' \mathbin{\ast'} C')\), then \(B \ident B'\), \(C \ident C'\), and \(\ast = {\ast'}\).

So suppose both \(A \ident (B \ast C)\) and \(A \ident (B' \mathbin{\ast'} C')\). Then either \(B \ident B'\) or not. If it is, clearly \(\ast = {\ast'}\) and \(C \ident C'\), since they then are substrings of \(A\) that begin in the same place and are of the same length. The other case is \(B \not\ident B'\). Since \(B\) and \(B'\) are both substrings of \(A\) that begin at the same place, one must be a proper prefix of the other. But this is impossible by Lemma \(\PageIndex{2}\). ◻