Logic Notes

Published on the

Introduction

Propositional Logic

Logical Consequence

Hilbert Calculus

Proposition: \[\{\neg \neg B\} \vdash_H B\] Proof: \[ \begin{align} \text{(1) } \ & (\neg \neg B) \to (\neg \neg \neg \neg B \to \neg \neg B) & \text{Ax 1} \\ \text{(2) } \ & \neg \neg B & \text{Ass}\\ \text{(3) } \ & (\neg \neg \neg \neg B \to \neg \neg B) & \text{MP 1,2}\\ \text{(4) } \ & (\neg \neg \neg \neg B \to \neg \neg B) \to (\neg B \to \neg \neg \neg B) & \text{Ax 3}\\ \text{(5) } \ & (\neg B \to \neg \neg \neg B) & \text{MP 4,3}\\ \text{(6) } \ & (\neg B \to \neg \neg \neg B) \to (\neg \neg B \to B) & \text{Ax 3}\\ \text{(7) } \ & (\neg \neg B \to B) & \text{MP 5,6}\\ \text{(8) } \ & B & \text{MP 2,7}\\ \end{align} \]

First-order Logic

Properties of Formal Systems

Proofs

Proposition: If \(\phi \vdash_H \psi\), then \(\phi \models \psi\).

Proof: We shall use induction on the length of the derivation. The base case will be for the first line of the derivation. We shall refer to the propositions on each line of the derivation as \(\psi_1, \psi_2... \psi_n\).

Base Case: The first line of our derivation, can either arise as an axiom or an assumption. All axioms are tautologies so must be true, so if \(\psi_1\) is an application of an axiom, the \(\phi \models \psi_1\). Similarly, if it is an assumption then \(\psi_1 \in \phi\), so \(\phi \models \psi_1\).

Inductive Case: Assume \(\phi \models \psi_1 ... \psi_{i-1}\). If \(\psi_i\) is an axiom then, it is a tautology, so \(\phi \models \psi_i\). if is an assumption then \(\psi_i \in \phi\) so \(\phi \models \psi_i\). Finally if \(\psi_i\) is an application of the modus ponens inference rule, then there must be some \(k\), such that \(k < i\) and that \((\psi_k \to \psi_i)\) and \(\psi_k\) appear in the derivation previously. If \(\psi_k\) appears in the derivation then \(\psi_k\) must be true. Since \(\psi_k \to \psi_i\) appears in the derivation, then that must also be true. Because of the truth table for implication, \(\psi_i\) must also be true, so \(\phi \models \psi_i\).

Conclusion: If \(\phi \models \psi_{i-1}\) then \(\phi \models \psi_i\). Since \(\phi \models \psi_1\), \(\phi \models \phi_k\), where \(1 \le k \le n\). Since \(\psi\) must appear in its derivation, if \(\phi \vdash_H \psi\), then \(\phi \models \psi\).

Proposition: The first-order theory of Peano arithmetic is negation incomplete.

Proof: We shall show this by introduce the notion of Gödel numbering. We shall assign a distinct numeric value to every symbol in our first-order language. Then we shall show that any statement in our first-order language consisting of \(n\) symbols can be encoded as a natural number, by matching them with the first \(n\) prime numbers. The product of each prime number raised to the power of the numeric value of its respective symbol, is a unique representation of the string as a natural number. This is because the result can be prime factorised, to get the symbols in their original positions. For instance, the first symbol will the exponent of 2 (as a numeric value), in the prime factorisation of the result. This is what is meant by Gödel numbering, every statement in our first-order language is a natural number; or to put it another way, every proof in our first order language can be expressed a natural number.

Note to represent quantified variables, e.g. \(\exists x\) and \(\forall y\) a unary notation can be used to represent different variables. E.g. \(x_1\), \(x_{11}\), \(x_{111}\). This can be extended to represent as many quantified variables as needed, with a finite number of symbols.

The proof resets on a single predicate \(\mathsf{Proof(x, y, z)}\), however note that this predicate is not really a predicate (unless you want to it to be). This is because the predicate is really a short-hand for a very long expression in our first-order language. Optionally, you can say there exists a bi-implication in the form \(\mathsf{Proof(x, y, z)} \leftrightarrow \phi\), where \(\phi\) is a placeholder for this really long expression, in other words, \(\mathsf{Proof(x, y, z)}\) is not necessary. Either the way the predicate relies on a very important notion: all computable functions can be expressed solely with the Peano axioms (well provided the Church-Turing thesis holds). In any case, the predicate \(\mathsf{Proof(x, y, z)}\) holds if \(x\) is the Gödel-encoded proof of the Gödel-encoded statement \(y\) with integer \(z\) substituted in it. Now, we shall make a new short-hand predicate, \(\mathsf{Prf(y)} \leftrightarrow \neg\exists x\;\mathsf{Proof(x, y, y)}\), \(\mathsf{Prf(y)}\) holds when there doesn’t exist a proof of the Gödel-encoded statement \(y\) with \(y\) substituted in it. Now let \(g\) be the Gödel number of that predicate. Does \(\mathsf{Prf(g)}\) hold? If it does hold there isn’t a proof of \(\mathsf{Prf(g)}\). But if it does hold, there must be a proof of \(\mathsf{Prf(g)}\). Contradiction. If it doesn’t hold, then that means there is a proof of \(\mathsf{Prf(g)}\). But since it doesn’t hold, there can’t be. Contradiction. Both contradictions are due to the completeness of first-order logic, shown by Gödel previously. In other words there is neither a proof of \(\mathsf{Prf(g)}\) or \(\neg\mathsf{Prf(g)}\). Hence there are some statements, for which neither \(\phi\) nor \(\neg\phi\) hold in the first-order theory of arithmetic.

Proposition: There is no general procedure to verify whether a set of formulae in first-order logic are universally valid.

Proof: In order to prove the aforementioned proposition, we will show there are propositions \(\phi\) for which either \(\phi\) or \(\neg\phi\) must hold, and there does not exist a general procedure to determine whether \(\phi\) or \(\neg\phi\) are universally valid. To do this we shall show to how to axiomatise Turing machines, a first-order theory, I shall call \(\mathcal{T}\). The Turing machine we will axiomatise will be represented by the quintuple \((Q, \Sigma, B, \Gamma, \delta, q_0, F)\). Note that the Turing machine, for convenience will have a semi-infinite tape, however, this is equivalent to Turing machine with a two-way infinite tape. \(\mathcal{T}\) shall have the following functions:

  • A 0-ary constant, \(0\)
  • A 1-ary successor functions, \(s\)

\(\mathcal{T}\) shall have the following predicates:

  • \(\forall q \in Q, M_q(x, y)\) which holds when the Turing machine is in state \(q\) after \(x\) steps, and scanning the \(y\) square.
  • \(\forall \sigma \in \Sigma, N_\sigma(x, y)\) which holds when the Turing machine has symbol \(\sigma\) after \(x\) steps on the \(y\) square.
  • A 2-ary equals predicate

\(\mathcal{T}\) shall have the following basic axioms in addition to the axioms for equality:

  • \(\forall x\;\forall y\;(s(x) = s(y)) \to x = y)\) i.e. the successor function is injective
  • \(\neg \exists x\;s(x) = 0\) i.e. 0 does not have a successor
  • \(\forall x\;\neg(x = 0) \to \exists y\;s(y) = x\) i.e. all numbers other than 0 have predecessors

\(\mathcal{T}\) shall also have the following axioms for the Turing machine’s initial configuration:

  • \(M_{q_0}(0, 0)\)
  • Where \(\theta_1 ... \theta_n\) are the initial symbols on the Turing machine’s tape, \(N_{\theta_1}(0,0) ... N_{\theta_n}(0, n-1)\). Bearing in mind that \(n-1\) is to be written formally as the application \(s\) to 0, \(n-1\) times.
  • All other tape symbols are blank: \[\forall x\;(\bigwedge_{i \in \{1..n\}} \neg (x = i)) \to (N_B(0, x))\]

\(\mathcal{T}\) also needs axioms to represent state transitions in the form, \(\delta(q, \sigma) = (q', \sigma', L)\) or \(\delta(q, \sigma) = (q', \sigma', R)\).

  • To represent \(\delta(q, \sigma) = (q', \sigma', L)\):

\[\forall x\;\exists y\;(M_q(x, y) \wedge N_{\sigma}(x, y)) \to (M_{q'}(s(x), s(y)) \wedge N_{\sigma'}(s(x), y))\]

  • To represent \(\delta(q, \sigma) = (q', \sigma', R)\):

\[\forall x\;\exists y\;(M_q(x, s(y)) \wedge N_{\sigma}(x, s(y))) \to (M_{q'}(s(x), y) \wedge N_{\sigma'}(s(x), s(y)))\]

  • To represent non-changed tape symbols, for all \(\sigma \in \Sigma\):

\[\forall x\;\forall y\;(\neg M_{\sigma}(x, y) \to N_{\sigma}(s(x), y))\]

To represent whether the machine halts the following sentence can be used, where \(X\) represents pairs of \((q, \sigma)\) for which \(\delta\) is undefined:

\[\exists x\;\exists y\;(\bigvee_{(q, \sigma) \in X} (M_q(x, y) \wedge N_{\sigma}(x, y)))\]

Clearly, because the halting problem is unsolvable, there cannot be an algorithm to decide whether the above proposition holds for a Turing machine. However, clearly there must exist a truth value to the above proposition. Therefore, first-order logic is undecidable.

Bibliography