Chapter 1:
Syntax and Informal Semantics of Predicate Logic

Why Syntax?

What Is Syntax?

However, whatever the concrete notation is, the syntactical structure of an expression in predicate logic (and other langauges) is defined by the answers to three questions:

\(\(∀ \+x\)\+\(x\^2 > a\)\((x > 
            b ∧ |1\/x| < ϵ)\)\)

Moreover, it should be seen, that the validity of the rules of mathematical logic is not restricted to mathematics. The rules of logic have developed over centuries and they only reflect what humans have observed in their every–day behavior. Therefore, it can also be of help in daily conversation to recognize the logic structure in statements such as “There is always …” or “If we … then … we will …” and to know what conclusions are allowed from these. It can often be observed, that wrong conclusions are drawn by wrong application of logical rules.

What is Semantics?

\(\(∀ \+x\)\+\(x\^2 > a\)\((x > 
            b ∧ |1\/x| < ϵ)\)\)

A Standard Syntax: Theorema

This loads Theorema during a Mathematica session. A valid license for Theorema is necessary.

Needs["Theorema`"]

To obtain the internal format of the above predicate logic expression, enter

•[  (Underscript[((Underscript[∀ , x])), (x^2) > a])(x > 
                b ∧ \[LeftBracketingBar](1/x)\[RightBracketingBar] < ϵ)   ] // InputForm

(Wrapping an expression into •[…] tells Mathematica to parse the expression as a Theorema expression, the suffix //InputForm shows the internal representation instead of the standard external form.)

The hierarchical inter–relation of language chunks left after lexical analysis is established by the “parsing” of the expression, i.e. the grammatical analysis of the expression. During parsing, the sequence of tokens `x', ` > ', and `b' is recognized as “the operation ` > ' applied to the arguments `x' and `b'”. This can be established since the token ` > ' is recognized as a symbol, which may occur between its subexpressions. It stands for the known head symbol ™Greater, thus “x > b” is parsed as ™Greater[x, b]. The result of parsing is best visualized in the so–called “parse tree” of the expression.

In Mathematica, the parse tree of an expression can be displayed using the command TreeForm.

•[  (Underscript[((Underscript[∀ , x])), (x^2) > a])(x > 
                b ∧ \[LeftBracketingBar](1/x)\[RightBracketingBar] < ϵ)   ] // TreeForm

The use of symbols starting with ™ as head symbols in Theorema has technical reasons. The same is true for head symbols starting with •, such as •var or •range.

The Standard Language Constructs of Predicate Logic

Example from Analysis 1: The Definition of `converges'

•[   (Underscript[∀ , f])(Underscript[∀ , a])(converges[f, 
                  a]   : ⇔(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[((Underscript[∃ , n])), n ∈ ℕ])(Underscript[((Underscript[∀ , m])), m ∈ ℕ ∧ m > n])\[LeftBracketingBar](Subscript[f, m]) - 
                              a\[RightBracketingBar] < ϵ)   ] // InputForm

™ForAll[
•range[•simpleRange[•var[
            f]]], 
True, 
™ForAll[
•range[•simpleRange[•var[
              a]]], 
True, 
™Iff[
converges[•var[
              f], •var[
              a]], 
™ForAll[
•range[•simpleRange[•var[ϵ]]], 
™And[™Element[•var[ϵ], ™ℝ], ™Greater[•var[ϵ], 
                0]], 
™Exists[
•range[•simpleRange[•var[
                    n]]], 
™Element[•var[
                  n], ™ℕ], 
™ForAll[
•range[•simpleRange[•var[
                      m]]], 
™And[™Element[•var[
                      m], ™ℕ], ™Greater[•var[m], •var[
                      n]]], 
™Less[
™BracketingBar[
™Minus[
™Subscript[•var[f], •var[
                          m]], 
•var[
                        a]]], 
•var[ϵ]]]]]]]]

\(new[v\_1, …, 
        v\_n]\ \  : \(\(⇔\)\(\ \)\(expression\_\(v\_1, …, 
            v\_n\)\)\)\)

new[(Subscript[v, 1]), …, (Subscript[v, n])]   :=  
      (Subscript[expression, (Subscript[v, 1]), …, (Subscript[v, n])])

The “wrappers” starting with • in the internal form of the expression are used for clarification of syntactical structure in the Theorema system. They are not part of predicate logic. For instance, •var is used to explicitely mark symbols to denote variables in order to be able to distinguish them from symbols denoting constants, see below.

Terms

Constants

Variables

Compound Terms

•[   a + b   ] // InputForm

•[   a + b + c   ] // InputForm

\(a + \(b!\)\ \ \(…\&?\)\ \ ™Factorial[™Plus[a, 
            b]]\)

\(a + \(b!\)\ \ \(…\&?\)\ \ ™Plus[
          a, ™Factorial[b]]\)

(a + 
            b)!  …  ™Factorial[™Plus[
          a, b]]

a + (b! ) …  ™Plus[
          a, ™Factorial[b]]

Formulae

Atomic Formulae

•[   a < b   ] // InputForm

•[   0 < n < M   ] // InputForm

Propositional Formulae

Quantifier Formulae

\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
            a| < ϵ\)

\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
              a| < ϵ\)\)

\(\(∀ \+ϵ\)\+\(ϵ ∈ ℝ ∧ ϵ > 0\)\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
                a| < ϵ\)\)\)

\(∀ \+a\((converges[f, 
            a]\  ⇔ \(\(∀ \+ϵ\)\+\(ϵ ∈ ℝ ∧ ϵ > 0\)\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
                      a| < ϵ\)\)\))\)\)

\(\(\(\ \)\(∀ \+f\(∀ \+a\((converges[f, 
              a]\  ⇔ \(\(∀ \+ϵ\)\+\(ϵ ∈ ℝ ∧ ϵ > 0\)\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
                        a| < ϵ\)\)\))\)\)\)\)\)

\(∀ \((ϵ ∈ ℝ ∧ ϵ > 
                0)\)\ \ \ \(∃ n ∈ ℕ\ \ \ \(∀ \((m ∈ ℕ ∧ 
                      m > n)\)\)\) : \ \ |f\_m - 
            a| < \(\(ϵ\)\(\ \ \)\(.\)\)\)

… (Underscript[∀ , m > n])|(Subscript[f, m]) - 
              a| < ϵ

(Underscript[∀ , x])(Underscript[∀ , y])(Underscript[∀ , z]) A

(Underscript[∀ , x, y, z])A

¬(Underscript[∀ , x])A ⇔ (Underscript[∃ , x])¬ A

¬(Underscript[∃ , x])A ⇔ (Underscript[∀ , x])¬ A

Substitution and Replacement

Free and Bound Occurences of Variables

Substituting the variable y for x in \(TraditionalForm\`∀ \+\(x ∈ ℕ\)\((x = 0)\)\) does not change the meaning of the formula, whereas substituting y for x in x = 0 might change the meaning. It depends on the assignments for x and y, whether x = 0 and y = 0 have the same meaning. 
Note that there is no possibility to decide whether an occurrence of a symbol in a formula is a free occurrence of a variable or a constant without knowing the context of the formula. For example, just looking at

\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
              a| < ϵ\)\)

We will discuss this subtle point in more detail later. In fact, wrapping symbols by •var[…] in the internal Theorema representation is done in order to be able to distinguish the usage of symbols as free variables and as constants. Alternatively, one would have to declare, once and for all, which symbols will be used as variables and which symbols will be used as constants. However, this is not attractive for practical purposes because it may well be that, for example, `π' in some texts is used as a constant and in some other text is used as a variable.
On the meta level—when we speak about expressions—we will often indicate free variables of an expression as subscripts of the expression, i.e. (Subscript[A, x]) should indicate that x occurs free in A. We do not fix in general, whether (Subscript[A, x]) should mean that x is among the free variables of A or whether x is the only free variable in A. On the object level, however, subscripting is often used as a hidden function symbol like in the example of (Subscript[f, m]) above. In other situations subscripting is used to distinguish between constants or variables of similar nature, e.g. if two constants for polynomials are required one often likes to name them (Subscript[p, 1]) and (Subscript[p, 2]). The meaning of subscripting must be understood from the context. The same is true for similar notations.

More Quantifiers

\(∑\+\(k = 1\)\%∞ b\_k = ∑\+\(k = 1\)\%∞ a\_k\)

Substitution

SUBSTITUTED[e, x, t]

We have already discussed an other operation that can be applied to expressions containing variables, namely “quantification”. Quantifiers “bind” variables. Variables bound by quantifiers are not any more free to the outside. More precisely, the operation of substitution does not substitute terms for bound variables. 
The interaction of quantification and substitution has one more subtle aspect: If a free variable x occurs inside the scope of a quantifier that quantifies variable y then, by substituting for x a term t containing a free variable y, the free variable y in t would be “caught”, i.e. turned into a bound variable! This must be avoided because it would drastically change the meaning of the expression. Hence, in such a case, before the actual substitution is carried out the bound variable y must be “renamed”. As we discussed above, it is a characteristic feature of bound variables that renaming them does not affect the meaning of the expression. This renaming of bound variables as a part of the substitution process should be well understood. It is an aspect of substitution that is less known.

f = SUBSTITUTED[e, x, t]

SUBSTITUTED[(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[((Underscript[∃ , n])), n ∈ ℕ])(Underscript[((Underscript[∀ , m])), m ∈ ℕ ∧ m > n])\[LeftBracketingBar](Subscript[f, m]) - 
                  a\[RightBracketingBar] < ϵ, a, 5]

SUBSTITUTED[(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[((Underscript[∃ , n])), n ∈ ℕ])(Underscript[((Underscript[∀ , m])), m ∈ ℕ ∧ m > n])\[LeftBracketingBar](Subscript[f, m]) - 
                  a\[RightBracketingBar] < ϵ, 
      a, (((u + v))^2)]

\(\(∀ \+ϵ\)\+\(ϵ ∈ ℝ ∧ ϵ > 0\)\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
                a| < ϵ\)\)\)

\(\(∀ \+ϵ\)\+\(ϵ ∈ ℝ ∧ ϵ > 0\)\)(Underscript[(Underscript[∃, n]), n∈ℕ])(Underscript[(Underscript[∀ , m]), m ∈ ℕ∧m>n])|(Subscript[f, m])-n|<ϵ

\(\(∀ \+ϵ\)\+\(ϵ ∈ ℝ ∧ ϵ > 0\)\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
                a| < ϵ\)\)\)

\(\(∀ \+ϵ\)\+\(ϵ ∈ ℝ ∧ ϵ > 0\)\(\(∃ \+n\)\+\(n ∈ ℕ\)\(\(∀ \+m\)\+\(m ∈ ℕ ∧ m > n\)|f\_m - 
                n| < ϵ\)\)\)

SUBSTITUTED[(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[((Underscript[∃ , n])), n ∈ ℕ])(Underscript[((Underscript[∀ , m])), m ∈ ℕ ∧ m > n])\[LeftBracketingBar](Subscript[f, m]) - 
                  a\[RightBracketingBar] < ϵ, a, n]

(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[(Underscript[∃, N]), N∈ℕ])(Underscript[(Underscript[∀ , m]), m ∈ ℕ∧m>N])\[LeftBracketingBar](Subscript[f, m]) - 
                n\[RightBracketingBar] < ϵ

SUBSTITUTED[(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[((Underscript[∃ , n])), n ∈ ℕ])(Underscript[((Underscript[∀ , m])), m ∈ ℕ ∧ m > n])\[LeftBracketingBar](Subscript[f, m]) - 
                  a\[RightBracketingBar] < ϵ, f, a + b, a, 
      f[a] + f[b]]

SUBSTITUTED[
      SUBSTITUTED[(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[((Underscript[∃ , n])), n ∈ ℕ])(Underscript[((Underscript[∀ , m])), m ∈ ℕ ∧ m > n])\[LeftBracketingBar](Subscript[f, m]) - 
                    a\[RightBracketingBar] < ϵ, f, a + b], a, 
      f[a] + f[b]]

SUBSTITUTED[
      SUBSTITUTED[(Underscript[((Underscript[∀ , ϵ])), ϵ ∈ ℝ ∧ ϵ > 0])(Underscript[((Underscript[∃ , n])), n ∈ ℕ])(Underscript[((Underscript[∀ , m])), m ∈ ℕ ∧ m > n])\[LeftBracketingBar](Subscript[f, m]) - 
                    a\[RightBracketingBar] < ϵ, a, f[a] + f[b]], 
      f, a + b]

A Notation for Substitution

(Subscript[e, x, y, z  ->  s, t, u])

SUBSTITUTED[e, x, s, y, t, z, u].

(Subscript[e, x, y  ->  s, t])

(Subscript[(((Subscript[e, x  ->  s]))), y  ->  t])

(Subscript[(((Subscript[e, y  ->  t]))), x  ->  
            s])  .

Declaration of (Free) Variables

x∘ (y∘ z) = (x∘ 
            y)∘ z

1∘ x = x

x∘ (x^(-1)) = 1

Alternatively, instead of considering formulae with free variables, we may just consider the formulae with all free variables quantified by a universal quantifier. This is particularly appropriate for formulae in “knowledge bases”, see below. Formulae without free variables are called “closed”. For example, the above axioms could also be written in the form

(Underscript[∀ , x, y, z]) 
        x∘ (y∘ z) = (x∘ 
            y)∘ z

(Underscript[∀ , x]) 1∘ x = x

(Underscript[∀ , x]) x∘ (x^(-1)) = 1

Replacement

REPLACED[e, p, f]

Note that, in replacement, f is replacing just one occurrence of a subexpression of e, namely the subexpression of e at one particular position p and that the subexpression at position p need not be a variable but may be an arbitrary expression. This is in sharp contrast to the operation of “substitution”, which we discussed in Section ...
Again one must be careful with replacing subexpression by expressions in expressions that contain quantifiers. We assume that the replacement operation takes care of the necessary renaming of bound variables if name clashes occur during replacement.

Positions

(x + y)*(x + y) = (x^2) + 2*x*y + (y^2)

x + y

•[   (x + y)*(x + y) = (x^2) + 2*x*y + (y^2)   ] // 
      InputForm

We will rarely use this explicit description of positions in this practical introduction to predicate logic. Most times it will suffice to say something like “the first occurrence” or the “third occurrence” of a subexpression.

Mathematica offers an operation ReplacePart, which does exactly what REPLACED does, i.e. we can implement REPLACED using basic Mathematica operations. The notion of “position”, which we introduced above, corresponds exactly to the notion of position in Mathematica, except that Mathematica uses braces `{' and `}' to denote tuples instead of angle brackets `⟨' and `⟩'.

Position[•[   (x + y)*(x + y) = 
          (x^2) + 2*x*y + (y^2)   ], •[   x + 
          y   ]]

REPLACED[e_, p_, f_] := 
      ReplacePart[e, f, p /. AngleBracket -> List]

REPLACED[•[  (x + y)*(x + y) = 
          (x^2) + 2*x*y + (y^2)   ], ⟨1, 
        1⟩, •[   (Sqrt[(u^2)])   ]]

REPLACED[•[   (x + y)*(x + y) = 
          (x^2) + 2*x*y + (y^2)   ], ⟨1, 
        2⟩, •[   (Sqrt[(u^2)])   ]]

REPLACED[•[   (x + y)*(x + y) = 
          (x^2) + 2  x*y + (y^2)   ], ⟨2, 
        1⟩, •[   (Sqrt[(u^2)])   ]]

A Notation for Replacement

(Subscript[e, p ⇥ f])

REPLACED[e, p, f]

\(e_\_\(p_ ⇥ f_\) := REPLACED[e, p, f]\)

(Subscript[(•[   (x + y)*(x + y) = (x^2) + 2  x*y + (y^2)   ]), ⟨2, 2⟩ ⇥ •[(Sqrt[(u^2)])]])

An Informal Semantics

Semantics for Terms

Semantics for Formulae

Note in particular, that quantifiers with finite ranges have the same meaning as ∧ and ∨, e.g.

(a)    ¬(Underscript[((Underscript[∀ , x])), C])A ⇔ (Underscript[(Underscript[∃ , x]), C])¬ A

(b)    ¬(Underscript[((Underscript[∃ , x])), C])A ⇔ (Underscript[(Underscript[∀ , x]), C])¬ A

How to Define New Symbols in Terms of Known Symbols

Explicit Definitions

Explicit Definition of Functions

f[(Subscript[x, 1]), …, 
        (Subscript[x, n])] := (Subscript[τ, (Subscript[x, 1]), …, (Subscript[x, n])])

(Underscript[∀ , (Subscript[x, 1]), …, (Subscript[x, n])])   f[(Subscript[x, 1]), …, 
          (Subscript[x, n])] = (Subscript[τ, (Subscript[x, 1]), …, (Subscript[x, n])])

Explicit Definition of Predicates

\(p[x\_1, …, 
        x\_n] : \(\(⇔\)\(φ\_\(x\_1, …, 
            x\_n\)\)\)\)

\(∀ \+\(x\_1, …, x\_n\)\ \ \ p[x\_1, …, 
          x\_n] ⇔ φ\_\(x\_1, …, x\_n\)\)

Implicit Function Definitions

\(\@x := \(the\ y ∈ \(ℝ\_0\%+\)\ such\ that\ y\^2 = \(\(x\)\(\ \ \)\(.\)\)\)\)

\(f[x\_1, …, 
        x\_n] := \(\(∍\)\(\)\(!\)\)\+y\ \ \(\(φ\_\(x\_1, …, x\_n, 
              y\)\)\(\ \ \ \)\(.\)\)\)

\(∀ \+\(x\_1, …, x\_n, y\)f[x\_1, …, x\_n] = 
      y\ ⟺\ \ φ\_\(x\_1, …, x\_n, y\)\)

\(∀ \+\(x\_1, …, x\_n\)\(∃ ! \)\+y\ \ \(\(φ\_\(x\_1, …, x\_n, 
              y\)\)\(\ \ \)\(.\)\)\)

\(\(\(∀ \+\(x\_1, …, x\_n, y\)f[x\_1, …, 
          x\_n] = \(y\ ⟺\ \ y = τ\_\(x\_1, …, x\_n\)\)\)\(\ \ \ \)\(,\)\)\)

(Underscript[∀ , (Subscript[x, 1]), …, (Subscript[x, n])])f[(Subscript[x, 1]), …, 
          (Subscript[x, n])] = (Subscript[τ, (Subscript[x, 1]), …, (Subscript[x, n])])   ,

Weaker Form of Implicit Definitions

higherPrime[x]:=such a  y with y is prime and y>x  .

\(f[x\_1, …, 
        x\_n] := \(\( ∍ \+y\)\(\ \ \)\(φ\_\(x\_1, …, x\_n, y\)\)\)\)

\(∀ \+\(x\_1, …, x\_n, y\)f[x\_1, …, x\_n] = 
      y\ ⟹\ \ φ\_\(x\_1, …, x\_n, y\)\)

\(∀ \+\(x\_1, …, x\_n\)\(∃ \+y\ \ \(\(φ\_\(x\_1, …, x\_n, 
              y\)\)\(\ \ \)\(.\)\)\)\)

\(is–bounded[A, 
        M] : \(\(⇔\)\(∃ \+\(c ∈ M\)\(∀ \+\(x ∈ A\)x ≤ c\)\)\)\)

upper–bound[A, 
        M] :=  (Underscript[∍ , c ∈ 
              M])(Underscript[∀ , x ∈ A])x ≤ 
            c

upper–bound[A, M] = 10 .

upper–bound[A, M] = 12 ,

10 = 12 .

\(upper–bound[A, M, 
        c] : \(\(⇔\)\(c\)\) ∈ 
          M ∧ ∀ \+\(x ∈ A\)x ≤ \(\(c\)\(\ \)\(.\)\)\)

\(is–bounded[A, 
        M] : \(\(⇔\)\(∃ \+c upper–bound[A, M, 
            c]\)\)\)

upper–bound[A, M, 10] .

upper–bound[A, M, 12] ,

((f[x] - f[a])/(x - a))

gradient–secant–between[f, a, 
        x] := ((f[x] - f[a])/(x - a))

gradient–at[f, a] := 
      (lim_(x -> a))  gradient–secant–between[f, a, 
          x]     (=(lim_(x -> a))((f[x] - 
                  f[a])/(x - a)))

\(derivative[
        f] := λ\+a\ \ gradient–at[f, 
          a]\ \ \ \ \(\((\(=\)\(\(λ\+a\) 
                  lim\+\(x -> a\)\ \ gradient–secant–between[
                    f, a, x]\  = \(λ\+a\) \(lim\+\(x -> 
                        a\)\) \(f[x] - f[a]\)\/\(x - a\)\))\)\(\ \)\(.\)\)\)

\(is–limit–of–at[f, a, 
        y] : \(\(⇔\)\(∀ \+\(ϵ > 0\)\(∃ \+\(δ > 0\)\(∀ \+\(x ∈ U\_δ[a]∖{a} ⋂ 𝒟[f]\)f[x] ∈ 
                U\_ϵ[
                    y]\ \ \ \ \ \ \ \((i . e . \ lim\+\(x -> a\) f[x] = 
                      y)\)\)\)\)\)\)

gradient–secant–between[f, a, 
        x] := ((f[x] - f[a])/(x - a))

\(gradient–between[f, a] := \(λ\+x\) 
        gradient–secant–between[f, a, 
          x]\ \ \ \ \ \((\(=\)\(\(λ\+x\) \(f[x] - f[a]\)\/\(x - a\)\))\)\)

\(converges–gradient–between–to[f, a, 
        y] : \(\(⇔\)\(is–limit–of–at[
          gradient–between[f, a], a, 
          y]\)\(\ \ \ \ \)\)\)

\(differentiable[f, 
        a] : \(\(⇔\)\(\(\(∃ ! \)\+y\)\(\ \)\(converges–gradient–between–to[f, a, 
            y]\)\(\ \ \ \ \)\)\)\)

\(derivative[f, 
        a] := \(\(\(\(∍\)\(\)\(!\)\)\+y\)\(\ \)\(converges–gradient–between–to[f, a, 
          y]\)\(\ \ \ \ \)\)\)

\(differentiable[
        f] : \(\(⇔\)\(\(∀ \+a\)\(\ \)\(differentiable[f, 
            a]\)\(\ \ \ \ \)\)\)\)

derivative[f] := (Underscript[λ, a]) derivative[f, a]

({{f', ∶, I, →, ℝ}, {, , x, ↦, f'[x]}})

({{derivative[f], ∶, I, →, ℝ}, {, , x, ↦, derivative[f, x]}})

derivative[f][
        x] = derivative[f, x]   .

™Plus[™Plus[x][y]][z]

™Plus[
        x] := (Underscript[λ, u]) 
          x + u   .