2 Predicate Logic

quantifier, predicate

2.1 The need for a richer language

Limitations of propositional logic:

• sentence components: not, and, or and if ...
• modifiers: exists..., all..., among... and only...

Reasoning about system:

• \(\vdash\): reason symbolically
• \(\vDash\): reason semantically

Soundness and completeness: The proof of the soundness and completeness of the predicate logic was done by K. Godel.

Functions: Each predicate symbol and each function symbol comes with an arity, the number of arguments it expects.

Vocabulary:

• A predicate vocabulary consists of three sets:
  • predicate symbols \(\mathcal{P}\)
  • function symbols \(\mathcal{F}\)
  • constant symbols \(\mathcal{C}\): nullary functions (functions without parameters)
  • Hence we can use only \(\mathcal{P}\) and \(\mathcal{F}\) to represent the vocabulary.

2.2 Preicate logic as a formal language

2.2.1 Terms

Terms: \(t ::= x | c | f(t_1, t_2, \dots, t_n)\)

2.2.2 Formulas

Formulas: define the set of formulas over \((\mathcal{F}, \mathcal{P})\)

\[\phi ::= P(t_1, t_2, \dots, t_n) | (\neg \phi) | (\phi \land \psi) | (\phi \lor \psi) | (\phi \to \psi) | (\forall x \phi) | (\exists x \phi)\]

2.2.3 Free and bound variables

Free and bound variables: To verify that \(\forall x Q(x)\) is true, we have to replace \(x\) with any possible concrete value and check whether \(Q\) holds for each of them.

An occurence of \(x\) in \(\phi\) is free if it is a leaf node in the parse tree of \(\phi\) such that there is no path upwards from the node \(x\) to a node \(\forall x\) or \(\exists x\).

2.2.4 Substitution

Definition

Given a variable \(x\), a term \(t\) and a formula \(\phi\), we define \(\phi[t/x]\) to be the formula obtained by replacing each free occurrence of variable x in \(\phi\) with \(t\).

Definition

Given a term \(t\), a variable \(x\) and a formula \(\phi\), we say that \(t\) is free for \(x\) in \(\phi\) if no free \(x\) leaf in \(\phi\) occurs in the scope of \(\forall y\) or \(\exists y\) for any variable \(y\) occurring in \(t\).

2.3 Proof theory of predicate logic

• Proof rules for equality
• Proof rules for universal quantification
• Proof rules for existential quantification
• Quantifier equivalences

2.4 Semantics of predicate logic

Deductive system VS. Semantics

• Both methods are used to verify whether we can make conclusions given premises.
• Deductive system: It is easier to answer questions like "Is \(\Gamma \vdash \psi\) valid?"
• Semantics: Is is easier to answer questions like "Is \(\Gamma \nvDash \psi\) valid?"

2.4.1 Models

2.4.2 Semantic entailment

Propositional logic: Each line of a truth table is a model. (finite models) Predicate logic: infinite models

"Example 1"

\(\forall x (P(x) \to Q(x)) \vDash \forall x P(x) \to \forall x Q(x)\) valid

\(\forall x P(x) \to \forall x Q(x) \vDash \forall x (P(x) \to Q(x))\) invalid

2.4.3 The semantics of equiality

2.5 Undecidability of predicate logic

Reference: Lecture 21: Undecidability, halting and diagonalization

"What to prove?"

Given a predicate logic formula \(\phi\), there is no algorithm to judge whether \(\phi\) is T or F.

"Validity"

A formula \(\phi\) is valid, if \(\vDash\) holds.

"How to define a problem?"

\(input \land inner behaviors \vdash output\)

\(\vdash (input \land inner behaviors \to output)\)

\(\vdash \phi_1 \land \phi_2 \to \phi_3\)

A. Turing machine

Finite Control = \(\{rules\}\)

B. The halting problem

\[A_{TM} = \{<M, w> | M \, is \, a \, TM \, and \, M \, accepts \, w\}\]

1. If \(M\) always stops and the result is accept for each possible \(w\), then \(M\) is decidable.
2. If for each possible \(w\), whenever \(M\) stops (\(M\) may not stops), it accepts \(w\), then \(w\) is recognized by \(M\). （dead loop: Turing recognizable）
3. Even \(M\) stops, the result is not accept, then \(M\) is not Turing recognizable.

"Example: Turing decidable"

int add(m, n) {
    return m + n;
}

"Example: Turing recognizable"

int add(m, n) {
    wait(message);
    return m + n;
}

"The halting problem"

Given a Turing Machine \(M\) and an input \(w\), please answer that whether \(M\) stops or not.

Solving \(A_{TM}\) to check whether \(<M, w> \in A_{TM}\).

"Diagonalization"

e.g., The set of real number is not countable.

Proof:

Suppose that there is a mapping, it maps each real number to a natural number, but we can always construct a real number that is not on the mapping table, so there is not exist such a mapping.

"Proof of halting problem¹"

Proof concept

Suppose that there exists a total computable funciton halts(f) that returns true if the subroutine f halfs and returns false otherwise. Now consider the following subroutine:

def g():
    if halts(g):
        loop_forever()

halts(g) must either return true or false, because halts() was assumed to be total. If halts(g) returns true, then g will call loop_forever() and never halt, which is a contradiction. If halts(g) returns false, then g will halt, this is alse a contradiction.

Overall, g does the opposite of what halts says g should do, so halts(g) can not return a truth value that is consistant with whether g halts. Therefore, the initial assumption that halts is a total computable function must be false.

Sketch of rigorous proof

Ref: https://en.wikipedia.org/wiki/Halting_problem#Sketch_of_rigorous_proof

C. The proof of undecidability of predicate logic

graph TD
    A[Halting problem is undecidable] --> B[Every halting problem can be transformed to a PCP problem];
    B --> C[PCP problem is undecidable];
    C --> D[Each PCP problem can be convert into a predicate logic problem];
    D --> E[Predicate logic is undecidable];

"Is this conversion correct?"

C has a solution iff \(\phi\) is valid.

1. If \(\phi\) is valid, then C has a solution.
   1. How to construct a solution for C?
   2. Idea: Construct a model for \(\phi\). Based on this model, \(\phi\) valuates to T, so we have a solution for C.
   3. The university of \(\mathcal{M}\) is the set of all binary strings, which is {0, 1}^*.
2. If C has a solution, then \(\phi\) is valid.
   1. We need to prove that, if \(\mathcal{M}'\) is any model, then \(\mathcal{M}' \vDash \phi\) holds.
   2. If \(\mathcal{M}' \nvDash \phi_1\) or \(\mathcal{M}' \nvDash \phi_2\), we are already done.
      1. PPT(68-69)
   3. Next, we need to verify whenever \(\mathcal{M}' \vDash \phi_1 \land \phi_2\) holds, \(\mathcal{M}' \vDash \phi_3\) holds as well.
      1. We do this trick by interpreting finite, binary string in the domain of value \(A'\) of the model \(\mathcal{M}'\).
      2. We use the intepret function to map strings from \(C\) to any universe \(A'\). We're gonna draw the conclusion of \(\phi_3\) in \(A'\) by using the knowledge in \(C\).
      3. PPT(70-73)

"Closure"

\(A^* = A^0 \cup A^1 \cup A^2 \cup \dots\)

\(A = \{0, 1\}\)

\(A^0 = \{\varepsilon\}\)

\(A^1 = \{0, 1\}\)

\(A^2 = \{00, 01, 10, 11\}\)

\(A^3\) = The set of a possible binary strings which have the length of 3.

2.6 Expressiveness of predicate logic

Soundess and Completeness

Expressiveness

Reachability

"Reachability"

Reachability is not expressible in predicate logic: there is no predicate-logic formula \(\phi\) with \(u\) and \(v\) as its free variables and \(R\) as its only predicate symbols such that \(\phi\) holds in directed graphs iff there is a path from \(u\) to \(v\).

"Proof"

Suppose there is a formula \(\phi\) expressing the existence of a path form the node associated to \(u\) to the node associated to \(v\). Let \(c\) and \(c'\) be constants. Let \(\phi_{n}\) be the formula expressing that there is a path of length \(n\) from \(c\) to \(c'\): we define \(\phi_{0}\) as \(c=c'\), \(\phi_1\) as \(R(c, c')\) and, for \(n > 1\),

\[\phi_n \overset{def}{=} \exists x_{n-1} (R(c, x_1) \land R(x_1, x_2) \land \dots \land R(x_{n-1}, c'))\]

Let \(\Delta = \{ \neg \phi_i | i \geq 0 \} \cup \{ \phi[c/u][c'/u] \}\). All formulas in \(\Delta\) sentences and \(\Delta\) is unsatisfiable, since the 'conjunction' of all sententces in \(\Delta\) says that there is no path of length 0, no path of length 1, etc. from the node denoted by \(c\) to the node denoted by \(c'\), but there is a finite path from \(c\) to \(c'\) as \(\phi[c/u][c'/u]\) is true.

However, every finite subset of \(\Delta\) is satisfiable since there are paths of any finite length. Therefore, by the Compactness Theorem, \(\Delta\) itself is satisfiable. This is a contradiction. Therefore, there cannot be such a formula \(\phi\).

Compactness Theorem

"Compactness Theorem"

Let \(\Gamma\) be a set of sentences of predicate logic. If all finite subsets of \(\Gamma\) are satisfiable, then so is \(\Gamma\).

Higher-order Logic

"higher-order logics"

In first order logic, you have quantifiers \(\forall\) (for all) and \(\exists\) (there exists) that allow you to make statements about your entire domain of discourse by involving variables that range over the objects you are discussing. You can talk about properties of these objects or relationships between them by using 1-place predicates or multiplace predicates, respectively. These predicates can be viewed as sets where their elements are those of the domain that satisfy some property or n-tuples that satisfy some relation.

In second order logic, you have the same quantifiers as before, but now you can use them to range over predicates. This essentially allows you to quantify sets. You can still use the quantifiers for elements of the sets, if you need to, just like you did in first order logic.

In third-order logic, once again the quantifiers are the same as before, what changes now is that you can quantify sets of sets.

In fact, that pattern holds for forth-, fifth-,…,n-order logic. With each step up you take, you use the quantifiers on sets of the things you previously quantified.

"What are the orders in mathematical logic, and what do they matter?"

Reference: https://qr.ae/pv39QS

"Higher-order logic"

• First-order logic quantifies only variables that range over individuals;
• Second-order logic, in addition, also quantifies over sets;
• Third-order logic also quantifies over sets of sets, and so on.
• The term "higher-order logic", abbreviated as HOL, is commonly used to mean higher order simple predicate logic. Here "simple" indicates that the underlying type theory is simple, not polymorphic or dependent
• higher-order logic are also undecidable.

2.6.1 Existential second-order logic

"Reachability"

R(x, y) means there is an edge (x, y). P(x, y) means that y is reachable from x.

2.6.2 Universal second-order predicate

"Reachability"

\(\forall P \exists x \exists y \exists z(\neg C_1 \lor \neg C_2 \lor \neg C_3 \lor \neg C_4)\)

"Conclusion"

1. Predicate logic is undecidable, since we cannot enumerate all models.
2. Given a specific model, it may be decidable.

---

1. https://en.wikipedia.org/wiki/Halting_problem#Formalization ↩