#separator:tab
#html:true
#notetype column:1
#deck column:2
#tags column:5
Basic Part III Notes::LogicAndComputability What do we mean by \(\Gamma \vdash \varphi\)? In the context \(\Gamma\), we have a proof of \(\rho\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What do we mean by \(\Gamma_1 A \vdash B\)? Adding A to the context \(\Gamma\), we have a proof of B. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\land\) - I) \[ \frac{\Gamma \vdash A \quad \Gamma\vdash B}{\Gamma \vdash A \land B } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\lor\) - I) \[ \frac{\Gamma \vdash A}{\Gamma \vdash A \lor B } \text{ and } \frac{\Gamma \vdash B}{\Gamma \vdash A \lor B} \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\land\) - E) \[ \frac{\Gamma \vdash A \land B}{\Gamma \vdash A} \text{ and } \frac{\Gamma \vdash A \land B}{\Gamma \vdash B} \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\lor\) - E) \[ \frac{ \Gamma \vdash A \lor B \quad \Gamma_1 A \vdash C \quad \Gamma_1 B \vdash C }{ \Gamma \vdash C } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\bot\) - E) For all \(A\), \[ \frac{ \Gamma \vdash \bot }{ \Gamma \vdash A } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\rightarrow\) - I) \[ \frac{ \Gamma_1 A \vdash B }{ \Gamma \vdash A \rightarrow B } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\rightarrow\) - E) \[ \frac{ \Gamma \vdash A \rightarrow B \quad \Gamma \vdash A }{ \Gamma \vdash B } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (?x) For all \(A\), \[ \frac{ \cdot }{ \Gamma_1 A \vdash A } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (LEM) For all \(A\), \[ \frac{ \cdot }{ \Gamma \vdash A \lor (A \rightarrow \bot) } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: IQC First-order intuitionistic logic. Includes the axioms for quantifiers (that's what the Q stands for) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What do we mean by \(\varphi [x := t]\) for some term t? Whatever \(\varphi\) is, with all instances of \(x\) replaced with \(t\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\exists\)-I) For all terms \(t\), \[ \frac{ \Gamma \vdash \varphi[x := t] }{ \Gamma \vdash \exists x. \varphi(x) } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\exists\)-E) \[ \frac{ \Gamma \vdash \exists x.\varphi \quad \Gamma_1\varphi \vdash \psi }{ \Gamma \vdash \psi } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\forall\)-I) For all \(x\) not free in \(\Gamma\), \[ \frac{ \Gamma \vdash \varphi }{ \Gamma \vdash \forall x.\varphi } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability (\(\forall\)-E) For all terms \(t\), \[ \frac{ \Gamma \vdash \forall x.\varphi }{ \Gamma \vdash \varphi [x := t] } \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What does \({\mathcal{U}}\) and \(V\) denote in the simply-typed \(\lambda\)-calculus? \({\mathcal{U}}\) is a countable set of primitive types.
\(V\) is an infinite set of variables. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What does \(\Pi\) represent in the simply-typed \(\lambda\)-calculus? Define its grammar \(\Pi\) is the set of types in \(\lambda\)-calculus, denoted \(\lambda_\Pi (\rightarrow)\): \[\begin{align*} \Pi :=&\,\,\, {\mathcal{U}}\\\\ &|\, \Pi \to \Pi \end{align*}\]
(also sometimes called the implicational fragment of \(\lambda_\Pi\)) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What does \(\lambda_\Pi\) represent in the simply-typed \(\lambda\)-calculus? Define its grammar and label it \(\lambda_\Pi\) is the set of terms in simply-typed \(\lambda\)-calculus: \[\begin{align*} \Pi :=&\,\,\, V\\\\ &|\, \lambda V : \Pi . \lambda_\Pi & (\lambda-\text{abstraction})\\\\ &|\, \lambda_\Pi \lambda_\Pi & (\lambda-\text{application}) \end{align*}\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability If we know \(\Gamma \vdash \varphi\), what do we know about \(\Gamma_1 \psi\) and \(\Gamma [p:= \psi]\)? By Lemma 1.1.4, we must have \(\Gamma_1 \psi \vdash \varphi\)
Furthermore, if we have a primitive proposition \(p\) and any proposition \(\psi\), then \(\Gamma [p:= \psi] \vdash \varphi[p:=\psi]\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Context (in the \(\lambda\)-calculus) A set of pairs of the form \(x : \sigma\)
(where \(x \in V\) is a variable and \(\sigma \in \Pi\) is a type)
Note that we write \(\Gamma_1 x : \sigma\) for \(\Gamma \cup \{x : \sigma\}\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Range of \(\Gamma\) Denoted \(|\Gamma|\), the set of all types that appear in \(\Gamma\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Typability Relation
(basic definition) \[\Vdash\, \subseteq C \times \lambda_\Pi \times \Pi\] where \(C\) is the set of all contexts. Links every term in a context to a type. Must fulfill three properties (recursing on any term in \(\lambda_\Pi\)).
This type system is denoted \(\lambda_\Pi (\to)\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: \(\alpha\)-equivalency Two \(\lambda\)-terms are \(\alpha\)-equivalent if they differ only in the name of the bound variables.
e.g. \(\lambda x : {\mathbb{Z}} . x^2 \equiv_\alpha \lambda y : {\mathbb{Z}}.y^2\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What does it mean for a \(\lambda\)-term to be closed? It has no free variables. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Typing Rule for Variables 1. Type of standalone variables: \[\Gamma_1 x : \tau \Vdash x : \tau\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Typing Rule for \(\lambda\)-abstractions 2. Type of \(\lambda\)-abstractions:
\[\Gamma_1 x: \sigma \Vdash M : \tau \implies \Gamma \Vdash (\lambda x : \sigma . M): \sigma \to \tau\]
(assuming \(x\) does not occur in \(\Gamma\), \(M \in \lambda_\Pi\))
LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Typing Rule for \(\lambda\)-applications 3. Type of \(\lambda\)-applications: \[(\Gamma \Vdash M : \sigma \to \tau)\land(\Gamma \Vdash N : \sigma) \implies \Gamma \Vdash (MN): \tau\] (\(M,N \in \lambda_\Pi\))
LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Substitution in \(\lambda_\Pi\)
(Inductive definition) Given \(\lambda\)-terms M, N and a variable \(x\), we define the substitution \(M[x := N]\) by pattern matching inductively:
Case 1: M is a variable equal to x: \[x[x:=N] := N\]
Case 2: M is a variable not equal to x: \[y[x := N] := y\]
Case 3: M is a \(\lambda\)-abstraction: \[(\lambda a:\sigma. A)[x := N] := (\lambda a: \sigma.A[x := N])\] (assuming \(x \neq y\) and \(y\) not free in N)
Case 4: M is a \(\lambda\)-application: \[(PQ)[x := N] := (P[x := N])(Q[x := N])\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: \(\beta\)-Reduction
(Name the two sides of the reduction) \[(\lambda x : \sigma.P)Q \rightarrow_\beta P[x:= Q]\]
The left side is called the \(\beta\)-redex and the right side is called the \(\beta\)-contraction.
We also write \(M \twoheadrightarrow_\beta N\) if M \(\beta\)-reduces to N after a finite number of reductions.
Note that this is preserved under \(\lambda\)-abstraction and \(\lambda\)-application: if \(P \to_\beta P'\), \[\lambda x : \sigma . P \to_\beta \lambda x : \sigma . P'\] \[PZ \to_\beta P'Z\] \[ZP \to_\beta ZP'\] (we can choose to evaluate in any order; we'll end up in the same place either way) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: \(\beta\)-Equivalence The smallest equivalence relation containing \(\to_\beta\), denoted \(\equiv_\beta\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: \(\eta\)-reduction Simplify pointless \(\lambda\)-abstractions: \[\lambda x:\sigma . (Px) \to_\eta P\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: \(\beta\)-Normal Form M is in \(\beta\)-NF if there is no N such that \(M \to_\beta N\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability When we write a \(\lambda\)-term like \(ABC\), what do we actually mean? \[(AB)C\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Free Variables Lemma
(Given \(\Gamma \Vdash M : \sigma\),) then we must have:
1. For all \(\Gamma \subseteq \Gamma'\), \(\Gamma' \Vdash M : \sigma\).
2. The free variables of M occur in \(\Gamma\)
3. There exists some \(\Gamma' \subseteq \Gamma\) consisting of exactly the free variables of M, preserving \(\Gamma' \Vdash M : \sigma\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Generation Lemma Just read each type inference rule in reverse:
1. If \(\Gamma \Vdash x:\sigma\), \[x : \sigma \in \Gamma\]
2. If \(\Gamma \Vdash (\lambda x : M) : \sigma\), then there exists types \(\tau, \rho \in \Pi\) such that \[\Gamma_1 x : \tau \Vdash M : \rho \quad \land \quad \sigma = (\tau \to \rho)\]
3. If \(\Gamma \Vdash (MN) : \sigma\), then there exists types \(\tau \in \Pi\) such that \[\Gamma \Vdash M : \tau \to \sigma\quad \land \quad \Gamma \Vdash N : \tau\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Substitution Lemma 1. If \(\Gamma \Vdash M : \sigma\) and \(\alpha\) is some type variable, then: \[\Gamma[\alpha := \tau] \Vdash M:\sigma[\alpha := \tau]\] (how substitution behaves for types in a context)
2. If \(\Gamma_1 x : \tau \Vdash M : \sigma\) and \(\Gamma \Vdash N : \tau\), then \[\Gamma \Vdash M[x := N] : \sigma\] (how substitution behaves for terms in a context) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Subject Reduction If \(\Gamma \Vdash M : \sigma\) and \(M \to_\beta N\), then \[\Gamma \Vdash N : \sigma\] (\(\beta\)-reduction preserves types)
Proven by induction with the generation and substitution lemmas. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Theorem: Church-Rosser Theorem for \(\lambda_\Pi\) Supposing \(\Gamma \Vdash M : \sigma\), if \(M \twoheadrightarrow_\beta N_1\) and \(M \twoheadrightarrow_\beta N_2\), then there exists some \(L \in \lambda_\Pi\) such that \[N_1 \twoheadrightarrow_\beta L \quad \land \quad N_2 \twoheadrightarrow_\beta L\] with \(\Gamma \Vdash L . \sigma\).
Also called the confluence property or the diamond property. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Corollary to the Church-Rosser Theorem for \(\lambda_\Pi\) If \(M \in \lambda_\Pi\) admits a \(\beta\)-NF, then it is unique. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Give an example of a \(\lambda\) term that is impossible to type \[\lambda x.xx\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: The height function A recursively defined map on types \(h: \Pi \to {\mathbb{N}}\) mapping:
1. \(v \in V\) to 0
2. \(\sigma \to \tau\) to \(1 + \max(h(\sigma), h(\tau))\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Theorem: The Weak Normalization Theorem for \(\lambda_\Pi(\to)\) Let \(\Gamma \Vdash M : \sigma\). There exists a finite reduction path \[M := M_0 \to_\beta M_1 \to_\beta ...\to_\beta M_n\] where \(M_n\) is a \(\beta\)-NF. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Theorem: The Strong Normalization Theorem for \(\lambda_\Pi(\to)\) Let \(\Gamma \Vdash M : \sigma\). There exists no infinite reduction chain \[M := M_0 \to_\beta M_1 \to_\beta ...\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Curry-Howard for IPC(\(\to\)) Let \(\Gamma\) be a context and \(\varphi\) be a proposition (type). Then:
1. If \(\Gamma \Vdash M : \varphi\), then \[|\Gamma| = \left\{ \tau \in \Pi : (x : \tau) \in \Gamma \text{ for some variable } x \right\} \vdash_{IPC} \varphi\]
2. If \(\Gamma \vdash_{IPC} \varphi\), then there exists some \(M \in \lambda_\Pi(\rightarrow)\) such that \[\left\{ (x_\psi : \psi) \,|\, \psi \in \Gamma \right\} \Vdash M : \varphi\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Binary Relation
(and when it is said to contain another relation) Given some set \(X\), \(X \times X\) is said to be a relation on \(X\). It contains another relation \(Y\) if for every \((a,b) \in Y\), \((a,b) \in X\).
It's an equivalence relation when it is reflexive, symmetric, and transitive.
Note that any intersection of equivalence relations always is an equivalence relation. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: The Three Laws of Lattices A lattice L is a set equipped with a a binary operators \(\wedge\) and \(\vee\) such that both operations obey:
- commutativity, and
- associativity
Plus together they must follow the absorption laws.
Note together these imply \(a \vee a = a\) and \(a \wedge a = a\) (this is called being idempotent) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Distributive Lattice A lattice that fulfills distributivity: \[a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)\] Note this is true iff \[a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c)\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Bounded Lattice A lattice where there exists \(\bot, \top \in L\) such that: \[a \vee \bot = a,\] \[a \wedge \top = a\] Note that these imply: \[a \wedge \bot = \bot\] \[a \vee \top = \top\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Complemented Lattice A bounded lattice such that, for all \(a \in L\), there exists some \(a^* \in L\) such that: \[a \wedge a^* = \bot,\] \[a \vee a^* = \top\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Boolean Lattice A lattice that is distributive, bounded, and complemented.
(Note that the structure this creates makes the complement function \(*\) equivalent to \(\lnot\) since we must have \(a \lor \lnot a = \top\) and \(a \land \lnot a = \bot\). This is also where \(\wedge\) and \(\vee\) come from! \(\lor\) prefers \(\top\) and \(\land\) prefers \(\bot\)) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Induced Order from a Lattice We say \(a \leq b\) when \(a \wedge b = a\) and equivalently \(a \vee b = b\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Induced Order of Bounded Lattices For any bounded lattice, for the induced order, we have: \[a \wedge b = \inf\{a, b\},\] \[a \vee b = \sup\{a, b\}\]
Conversely, for any partial order, finite meets and joins form a lattice as above.
Note then that for any total order, we have \(\wedge \equiv \min\) and \(\vee \equiv \max\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Draw the free distributive lattice on {x, y} \begin{tikzpicture}[ node/.style={circle, draw, fill=white, inner sep=2pt, minimum size=6pt}, label/.style={font=\small}, >=stealth ]
% Nodes \node[node] (bot) at (0, 0) {}; \node[node] (xay) at (0, 1.5) {}; \node[node] (x) at (-1.5, 3) {}; \node[node] (y) at (1.5, 3) {}; \node[node] (xvy) at (0, 4.5) {}; \node[node] (top) at (0, 6) {};
% Edges \draw (bot) -- (xay); \draw (xay) -- (x); \draw (xay) -- (y); \draw (x) -- (xvy); \draw (y) -- (xvy); \draw (xvy) -- (top);
% Labels \node[label, below] at (bot.south) {\(\bot\)}; \node[label, left] at (xay.west) {\(x \wedge y\)}; \node[label, left] at (x.west) {\(x\)}; \node[label, right] at (y.east) {\(y\)}; \node[label, left] at (xvy.west) {\(x \vee y\)}; \node[label, above] at (top.north) {\(\top\)};
\end{tikzpicture} LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Valuation A function \(v:L \to \{0, 1\}\) assigning truth values to statements in a consistent manner (respecting logical connectives) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Heyting Algebra A bounded lattice \(H\) equipped with an extra binary relation \(\Rightarrow: H \times H \to H\) such that \[a \wedge b \leq c \iff a \leq (b \Rightarrow c)\]
(So \(a \Rightarrow b\) can be thought of the weakest thing you can assume that, when combined with \(b\), gets you to \(c\)) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Heyting Homomorphism A function that preserves \(\wedge\), \(\vee\), and \(\Rightarrow\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Show that every Boolean algebra is a Heyting algebra We can construct our own \(\Rightarrow\) function: \[a \Rightarrow b := (\lnot a) \lor b\]
An example of this are the power sets of a set. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Show that every topology on a set X is a Heyting algebra We construct a \(\Rightarrow\) function: \[U \Rightarrow V := {\mathrm{Int}}(U^c \cup V)\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: H-Valuation Given some language \(L\) with a set of primitive propositions \(P\), an H-valuation \(v: P \to H\) is extended to \(L\) recursively by:
1. \(v(\bot) = \bot\)
2. \(v(A\land B) = v(A) \land v(B)\)
3. \(v(A\lor B) = v(A) \lor v(B)\)
4. \(v(A \to B) = v(A) \Rightarrow v(B)\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: H-Valid A proposition \(A \in L\) is H-valid if, for all H-valuations \(v\), \(v(A) = \top\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: H-Consequence A proposition \(A \in L\) is an H-consequence of a finite set of propositions \(\Gamma \subseteq L\) if, for all valuations \(v\), \(v(\bigwedge \Gamma) \leq v(A)\).
We denote this by \(\Gamma \vDash_H A\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Lemma: Soundness of Heyting Semantics If H is a Heyting algebra and v is an H-valuation, we always have: \[\Gamma \vdash_{IPC} A \implies \Gamma_{H,v} \vDash A\]
Proven over the structure of all IPC rules. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Example: Show that the LEM is not intuitionistically valid By the soundness of Heyting semantics, we need only to find an example of a Heyting algebra with a valuation where \(v(p \lor \lnot p) \neq \top\) for some \(p \in L\).
Consider the topology \(\{ \emptyset, \{ 1\}, \{1,2\} \}\) (called the Sierpinski space). Take some primitive proposition \(p\), and define our valuation so that \(v(p) = \{1\}\). Then we have
\[v(\lnot p) = v(p) \Rightarrow \emptyset = {\mathrm{Int}} (\{1,2\} \backslash \{ 1\}) = \emptyset\]
and thus
\[v(p \lor \lnot p) = v(p) \lor v(\lnot p) = \{ 1\} \neq \top = \{ 1, 2\}\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Pierce's Law \[((p \to q) \to p) \to p\] This is a tautology in classical logic, but not intuitionistically valid. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Example: Show that Pierce's Law is not intuitionistically valid. By the soundness of Heyting semantics, we need only to find an example of a Heyting algebra with a valuation where \(v(p \lor \lnot p) \neq \top\) for some \(p \in L\).
Take the usual topology on \({\mathbb{R}}^2\) with the valuation:
\[p \longmapsto {\mathbb{R}}^2 \backslash \{ 0, 0\}\] \[q \longmapsto \emptyset\]
Plugging in, you get \(((p \to q) \to p) \to p = {\mathbb{R}}^2 \backslash \{0,0\} \neq \top = {\mathbb{R}}^2\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Lindenbaum-Tarski Algebra A Lindenbaum-Tarski Algebra \(F^Q(T)\) over an L-theory T is an algebra over equivalence classes of propositions where \(\varphi \sim \psi\) \[T, \varphi \vdash_Q \psi \text{ and } T, \psi \vdash_Q \varphi\] (equivalence class over \(\varphi \iff \psi\))
If \(\bowtie\) is any logical connective in \(T\), we set \([\varphi] \bowtie [\psi]\) where \([\varphi \bowtie \psi]\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Show that the LT Algebra of any theory relative to IPC \(\backslash \to\) (IPC without implication) is a distributive lattice. Commutativity and associativity are trivial, just show the two absorption laws and a distributivity law by IPC rules: \[([A] \lor [B])\land [A] = [(A \lor B) \land A] = [A]\] \[([A] \land [B])\lor [A] = [(A \land B) \lor A] = [A]\] \[[A] \land ([B] \lor [C]) = [A \land (B \lor C)] = [(A \land B) \lor (A \land C)] = ([A] \land [B]) \lor ([A] \land [C]) \] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Lemma: Show that the LT algebra of any theory relative to IPC is a Heyting Algebra We showed that IPC \(\backslash \to\) is a distributive lattice, so we just need to show that IPC has \(\Rightarrow\) and is bounded. Use \(\to\) as \(\Rightarrow\), \(\bot\) as \(\bot\), and \(\bot \to \bot\) as \(\top\). So just show that:
Assuming \([A] \land [B] \leq [C]\), we have \([A] \leq ([B] \Rightarrow [C])\)
Assuming \([A] \leq ([B] \Rightarrow [C])\), we have \([A] \land [B] \leq C\)
Both directions needed to make \(\bot \leq A\) for all \(A\)
Both directions needed to make \(A \leq \top\) for all \(A\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Theorem: Completeness of Heyting semantics A formula is provable in IPC if it is H-valid for every Heyting algebra H (and only if by soundness) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Principal Up-set
(of some poset \(S\)) \[a\uparrow\, := \{s \in S: a \leq s\}\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Terminal Segment
(of a poset \(S\)) A subset \(U \subseteq S\) where \(a \uparrow\, \subseteq U\) for every \(a \in U\)
Note that this isn't the same as a filter: for any lattice with incomparable elements, we can escape the terminal segment with finite meets! LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: If \(S\) is a poset, \(T(S) := \{ U \subseteq S : U \text{ is a terminal segment} \}\) is a Heyting algebra Order by set inclusion, the fact that this is a bounded lattice and closed is taken as trivial. The key step is using \[U \Rightarrow V := \{ s \in S: (s \uparrow) \cap U \subseteq V \}\]
Must show that this is a terminal segment and both directions of the Heyting Algebra definition. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Kripke Model Let P be some set of primitive propositions. A triple \((S, \leq, \Vdash)\) where \((S, \leq)\) is a poset, with S called the set of worlds and \(\leq\) the accessibility relation; and \(\Vdash \subseteq S \times P\) is the forcing relation.
It must fulfill the Persistence Property.
Note that for \(X \subseteq S\) we say \(X \Vdash \varphi\) if all worlds in \(x \in X\) force \(\varphi\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Extended Forcing Relation of the Kripke Model When \(p\) is not a primitive proposition, we define the forcing relation inductively as follows:
1. There is no world that believes in \(\bot\): \(\not \exists s,\, s \Vdash \bot\)
2. We write \(s \Vdash \varphi \land \psi\) iff \(s \Vdash \varphi\) and \(s \Vdash \psi\)
3. We write \(s \Vdash \varphi \lor \psi\) iff \(s \Vdash \varphi\) or \(s \Vdash \psi\)
4. We write \(s \Vdash (\varphi \to \psi)\) iff, for every more knowledgeable world \(s \leq s'\), \(s' \Vdash \varphi\) implies \(s' \Vdash \psi\)
(worlds are humble: they believe only in things that they believe more knowledgeable worlds believe in)
LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What are the conditions for negation in a Kripke model? \[s \Vdash \lnot \varphi \iff \forall s' \geq s,\,\, s' \not \Vdash \varphi\] \(\lnot \varphi\) holds iff no more knowledgeable worlds believe in it LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What are the conditions for double negation in a Kripke model? \[s \Vdash \lnot \lnot \varphi \iff \forall s' \geq s,\,\, \exists s'' \geq s',\,\, s'' \Vdash \varphi\] In all more knowledgeable worlds, there exists some even more knowledgeable world that believes in \(\varphi\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Filter A filter \(F\) on a lattice \(L\) is a subset \(F \subseteq L\) with the following properties:
1. \(F \neq \emptyset\)
2. F is a terminal segment of \(L\): ie if \(x \leq y\) and \(x \in F\), then \(y \in F\).
3. \(F\) is closed under finite meets.
LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Prime Filter A filter is prime if \(x \vee y \in F \implies x \in F \text{ or } y \in F\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Absorption Laws of Lattices \[a \vee (a \wedge b) = a,\] \[a \wedge (a \vee b) = a\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Partial Recursive Function The smallest class of functions \({\mathbb{N}}^k \to {\mathbb{N}}\) that contains the three atomic functions, and is closed under composition, primitive recursion, and minimization.
For the class of primitive recursive functions, ignore minimization. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: The three atomic partial recursive function building blocks 1. Projections: Pick one number out of a list ( \[\Pi_i^k: {\mathbb{N}}^k \to {\mathbb{N}}\] \[\Pi_i^k: (n_1,...,n_k) \mapsto n_i\] 2. Successor: Add one \[S^+ : {\mathbb{N}} \to {\mathbb{N}}\] \[S^+: n \to n + 1\] 3. Zero: Any number to zero \[Z: {\mathbb{N}} \to {\mathbb{N}}\] \[Z : n \mapsto 0\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Partial Recursive Function Closure under Composition Given \(g: {\mathbb{N}}^k \to {\mathbb{N}}\), and for each \(i \in [k]\) we have a function \(h_i: {\mathbb{N}}^m \to {\mathbb{N}}\), then there exists a function \(f : {\mathbb{N}}^m \to {\mathbb{N}}\) given by
\[f(\bar n) := g(h_1(\bar n), ..., h_k(\bar n))\]
Note that \(\bar n\) refers to a tuple of natural numbers.
Sort of like a weird inverse map-reduce, except we're mapping over a list of functions by applying \(\bar n\) to all of them. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Partial Recursion Function Closure under Primitive Recursion Given a base function \(g: {\mathbb{N}}^m \to {\mathbb{N}}\) and step function \(h: {\mathbb{N}}^{m+2} \to {\mathbb{N}}\), there exists a function \(f: {\mathbb{N}}^{m+1} \to {\mathbb{N}}\) defined by: \[\begin{align*} f(0, \bar n) &:= g(\bar n)\\\\ f(k+1, \bar n) &:= h(f(k, \bar n), k, \bar n) \end{align*}\]
The first parameter is the fuel, the second is the surrounding context (constant through the process) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Partial Recursive Function Closure under Minimization Given \(g : {\mathbb{N}}^{m + 1} \to {\mathbb{N}}\), there exists a function \(f: {\mathbb{N}}^m \to {\mathbb{N}}\) that maps \(\bar n\) to the smallest \(k\) such that \(g(k, \bar n)=0\).
Note that it may not exist!
This is sometimes denoted \(f(\bar n) = \mu k. g(k,\bar n) = 0\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Total Recursive Function A partial recursive function for which every every input maps to some outputs.
This just means it always terminates: there's no input that will search forever. All primitive recursive functions are total. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Godel Numbering Let \(L\) be a language. A Godel Numbering is an injection \(L \hookrightarrow {\mathbb{N}}\) with three properties:
1. It's computable: there exists an algorithm you can follow to find the Godel number of any expression in finite time
2. Its image is a recursive subset of \({\mathbb{N}}\) (membership is decidable).
3. Its inverse (where defined) is also computable. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Recursively Enumerable Set \(X \subseteq {\mathbb{N}}\) is recursively enumerable (or recognizable, or semi-decidable) if any of the following are true:
1. \(X\) is the image of some partial recursive function \(f: {\mathbb{N}} \to {\mathbb{N}}\)
(dovetail computations and generate a big list)
2. \(X\) is the image of some total recursive function \(f: {\mathbb{N}} \to {\mathbb{N}}\)
(just run on all numbers sequentially)
3. \(X\) is the domain of some partial recursive function \(f: {\mathbb{N}} \to {\mathbb{N}}\)
(same as 1, but mark the input on the list, not the output) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Recursive Set A set \(X \subseteq {\mathbb{N}}\) is recursive if both \(X\) and its complement \({\mathbb{N}} \,\backslash\, X\) are recursively enumerable. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Recursive Language There exists an algorithm to check whether a string of symbols is an L-formula
(this is generally trivial: just checking if a statement makes sense) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Recursive L-Theory An L-Theory \(T\) is recursive if membership in \(T\) is decidable (we can check if a sentence is assumed or not) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Decidable L-Theory An L-Theory \(T\) is decidable if there is an algorithm for deciding \(T \Vdash \varphi\) for any \(\varphi\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Craig's Trick Every first-order theory with a recursively-enumerable set of axioms admits a recursive axiomatization
(if your list of axioms is recognizable, it can be reconfigured into a decidable one)
Proof:
There exists a totally recursive \(f\) with \(f(n) = \phi_i\) for \(n \in {\mathbb{N}}\).
Map each \(\phi_i\) to a logically equivalent \(\bigwedge_{j=1}^i \phi_i\).
The algorithm to check if a statement \(A\) is an axiom is thus:
First, check if \(A\) is equivalent to \(f(1)\) (can do this in finite time due to finite sentence length). If it is, return yes, otherwise continue.
Second, find any decompositions \(A = \bigwedge_j^i A_j\). Then just check axiom \(i\) for equivalence. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Notation for the Godel numbering of an expression \(\lceil x \rceil\) maps \(x\) to its Godel numbering
\(\lfloor x \rfloor\) maps a Godel numbering \(x\) to the statement in represents LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: The set of total recursive functions (or their respective Godel numberings) is not recursively enumerable Proof:
By definition, there exists some function \(f\) such that, for every total function \(h\), there exists some \(n \in {\mathbb{N}}\) such that \(h = \lfloor f(n) \rfloor\).
In particular, this includes \(g(x) = \lfloor f(x) \rfloor (x) + 1\).
Show a contradiction from there. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: The Language of Arithmetic \(\mathcal{L}_{PA}\) The first-order language with signature \((0, 1, +, \cdot, <)\) where \(0, 1\) are constants, \(+, \cdot \) are functions with arity two, and \(<\) is a relation with arity two. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: The Base Theory of Arithmetic \(PA^-\) An \(\mathcal{L}_{PA}\)-theory fulfilling:
1. \(+, \cdot\) are commutative and associative, and have identity elements 0 and 1.
(\(+, \cdot\) individually)
2. \(\cdot\) distributes over \(+\).
(distributivity)
3. \(<\) is a linear ordering compatible with \(+\) and \(\cdot\).
(\(<\) is a compatible linear ordering)
4. \(\forall x, y,\, (x < y \implies \exists z,\, x + z = y)\).
(Quantifier definition of \(<\))
5. \(0 < 1\) and \(\forall x,\, (x > 0 \implies x \geq 1)\).
(Zero is less than 1, \(\leq\) base definition)
6. \(\forall x,\, x \geq 0\).
(Everything is greater than or equal to zero) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: The Theory of Peano Arithmetic (PA) \(PA^-\) with the extra set of axioms, the scheme of induction:
For each \(\mathcal{L}_{PA}\)-formula \(\varphi(x, \bar y)\), we have the axiom \[I\varphi := \forall \bar y,\, (\varphi(0, \bar y) \land \forall x,\, (\varphi (x, \bar y) \to \varphi(x + 1, \bar y)) \to \forall x,\, \varphi(x, \bar y)\]
(proving the base case \(n = 0\) and proving the inductive case \(n \implies n+1\) is enough to prove something for all \(n \in {\mathbb{N}}\)) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Delta-0 Formula (\(\Delta_0\)) A formula whose quantifiers (\(\forall\), \(\exists\)) are bounded: for some fixed \(n \in {\mathbb{N}}\), either \[\forall x,\, x<n,\, \varphi(x)\] or \[\exists x,\, x<n,\, \varphi(x)\] for \(n\) not free in \(\varphi(x)\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Strict Order Axioms 1. Irreflexivity: \(\forall x,\, x \not < x\)
2. Asymmetry: \(\forall a,b,\, a < b \implies b \not < a\)
3. Transitivity: \(\forall a, b, c,\, (a < b) \land (b < c) \implies a < c\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Pi-1 Formula and Sigma-1 Formula (\(\Pi_1\), \(\Sigma_1\)) A formula \(\varphi(\bar x)\) is a \(\Sigma_1\)-formula if it is provably equivalent to a there-exists statement with a \(\Delta_0\)-formula body, ie, there exists a \(\Delta_0\) \(\psi(\bar x, \bar y)\) such that \[PA \vdash \left(\varphi(\bar x) \iff \exists \bar y.\, \psi(\bar x, \bar y) \right)\] Similarly \(\varphi(\bar x)\) is a \(\Pi_1\)-formula if it is provably equivalent to a for-all statement with a \(\Delta_0\)-formula body, ie, there exists a \(\Delta_0\) \(\psi(\bar x, \bar y)\) such that \[PA \vdash \left(\varphi(\bar x) \iff \forall \bar y.\, \psi(\bar x, \bar y) \right)\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability State a total recursive bijection from \({\mathbb{N}}^2 \to {\mathbb{N}}\), denoted \(\langle x, y \rangle\) \[ \langle x, y \rangle := \frac{(x+y)(x + y + 1)}{2} + y \] This is called the Cantor Pairing Function.
Intuition: it's just diagonalization. Count up the triangular number underneath the square we want the number of, then add how many squares into the next triangle we are. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Godel's Beta Function There exists a function \(\beta(x, y)\) derivable in PA such that for any sequence \(x\), there is a code \(u\) such that \(\beta(u, i)\) = \(x_i\).
(Decodes the sequence and gives us the \(i\)th element. This is the projection function...)
Note that with Cantor's pairing function, we can reduce this to just one coded number. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Godel's Lemma Let \(M \Vdash PA\), \(n \in {\mathbb{N}}\), and \(x_0,...,x_{n-1} \in M\).
Then there exists a \(u \in M\) such that \(M \Vdash ((u)_i = x_i)\) for all \(i < n\).
If M believes in PA, M can prove that Godel's beta function works as intended. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Let \(f: {\mathbb{N}}^k \to {\mathbb{N}}\) be a partial function.
\(f\) is (partial) recursive iff there is a \(\Sigma_1\)-formula \(\theta(\bar x, y)\) such that \[y = f(\bar x) \iff {\mathbb{N}} \Vdash \theta(\bar x, y)\]
(ie the graph of \(f\) is \(\Sigma_1\)-definable in \({\mathbb{N}}\)) First we show that if the graph of \(f\) is \(\Sigma_1\)-definable, then \(f\) must be partial recursive. We can just implement a minimization procedure then run the outer there-exists clause, checking every case exhaustively (computing results in \({\mathbb{N}}\) as normal).
Constructing a \(\Sigma_1\) statement from a partial recursive \(f\) is more complicated. The base functions are simple. For the rest:
Composition: show this is equivalent to a there-exists over each subfunction output, with \(f\) applied to all of them together making the required full output.
Primitive Recursion: absolutely requires Godel's beta-function so that you can get an existence statement over the sequence length (we don't know how many times we'll need to run through the loop).
A similar argument holds for minimization. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What is meant when we write \(T(S)\) where \(S\) is a poset? The set of terminal segments of \(S\): \[\{ U \subseteq S : U \text{ is a terminal segment} \}\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What is a simple way to make a Kripke model? Take a mapping ('valuation') \(v\) from the set of primitive propositions \(P\) to the set of terminal segments \(T(S)\) (known to be a Heyting algebra).
This induces a Kripke model by setting \[s \Vdash p \iff s \in v(p)\] for \(s \in S\), \(p \in P\).
It's clear to see that this fulfills the persistence property: \[s \Vdash p \implies s \in v(p) \implies (s\uparrow) \subseteq v(p) \implies s' \in v(p) \implies s' \Vdash p\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proper Filter A filter is called 'proper' when it isn't just the whole set \(X\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Extension of Filters If \(F\) is a proper filter and \(x \not \in F\), then there exists a prime filter extending \(F\) that still avoids containing \(x\) (by Zorn's Lemma) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Chinese Remainder Theorem Take integers a list of \(k\) integers \(n_1,...,n_k\), all greater than one. Assume they are pairwise coprime: no pair shares any divisor besides 1. no Let \(N\) be their product, \(n_1...n_k\). Specify a list of \(k\) possible remainders for each \(n_k\), \(0 \leq a_k < n_k\).
Then there exists only one possible solution \(0 \leq x < N\) such that the remainder of \(x\) with each \(n_i\) is \(a_i\).
Another way to state it: with the same assumptions above, the system \[\begin{align*} x \equiv a_1\mod n_1\\\\ ...\\\\ x \equiv a_k\mod n_k \end{align*}\] has only one solution \(x\) mod \(N\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability How do we encode numbers for use in Godel's Beta Function? Suppose we want to code the numbers \( x_0, ..., x_{n-1}\). Let \(m = \max (0, x_0, ..., x_{n-1})!\). Define pairwise coprime \(b_1 :=m + 1,\, b_2:= 2m + 1, ..., b_n:= nm + 1\). Then our tuple becomes coded as the unique \(x\) guaranteed by the Chinese Remainder Theorem such that the remainder by \(b_i\) is \(x_i\). Thus we have \(u = \langle a, m \rangle\)
LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: The Persistence Property for Kripke Models \[(s \Vdash p) \land (s \leq s') \implies s' \Vdash p\] Worlds are ordered by the knowledge they believe.
LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability How do we actually implement Godel's beta function given an encoded number? \[ \beta(u, i) := a \% (m(i+1) + 1) \] where \((a, m)\) are the unique numbers such that \(u = \langle a, m \rangle\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability \(PA \vdash \varphi\) versus \(PA\vDash\varphi\) versus \({\mathbb{N}} \vDash \varphi\) \(PA \vdash \varphi\) means that you can prove \(\varphi\) from axioms in \(PA\),
\(PA \vDash \varphi\) means that \(\varphi\) holds in every model of \(PA\) (even nonstandard ones),
\({\mathbb{N}} \vDash \varphi\) means that \(\varphi\) holds in the standard model specifically. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: \(\Sigma_1\)-definable Set A set \(A \subseteq {\mathbb{R}}^n\) is \(\Sigma_1\)-definable if there exists a \(\Sigma_1\)-formula \(\varphi\) such that \[\bar n \in A \iff {\mathbb{N}} \vDash \varphi(\bar n) \] We need to construct a \(\Sigma_1\) that is true if and only if \(\bar n \in A\).
For instance, \(A\) is the set of perfect squares, then we could use \(\varphi(n) = \exists x,\, (n = xx)\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Initial Segment A subset of a poset that is downward closed (the reverse of a terminal segment) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: \({\mathbb{N}}\) forms an initial segment of every model \(M\) of \(PA^-\) Map \(0 \in M\) to \(0 \in {\mathbb{N}}\), \(S(0) \in M\) to \(1 \in {\mathbb{N}}\), and onwards.
It's an initial segment because \[PA^- \vdash \forall x. (x \leq k \to x = 0 \lor x = 1 \lor ...\lor x = k)\] for all standard \(k \in {\mathbb{N}}\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Function Representation in a Theory Let \(f: {\mathbb{N}}^l \to {\mathbb{N}}\) be a total function with \(T\) being any \(L_{PA}\) theory extending \(PA^-\). \(f\) is represented in \(T\) if there exists an \(L_{PA}\) formula \(\theta(x_1,...,x_l,y)\) such that, for all \(\bar n \in {\mathbb{N}}^l\),
1) \[T \vdash \exists !y.\theta(\hat n, y)\] 2) \[k = f(\bar n) \implies T\vdash \theta(\bar n, k)\] If \(\theta\) can be made a \(\Sigma_1\), we say \(f\) is \(\Sigma_1\)-represented in \(T\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Subset Representation in a Theory A subset \(S \subseteq {\mathbb{N}}^l\) is represented in an \(L_{PA}\) theory extending \(PA^-\) if there exists an \(L_{PA}\) formula \(\theta(x_1,...,x_l)\) such that for all \(\bar n \in {\mathbb{N}}^l\):
1) \[\bar n \in S \implies T \vdash \theta(\bar n)\] 2) \[n \not \in S \implies T \vdash \neg \theta(\bar n)\] If \(\theta\) can be made a \(\Sigma_1\), we say \(S\) is \(\Sigma_1\)-represented in \(T\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Every total recursive function \(f: {\mathbb{N}}^m \to {\mathbb{N}}\) is \(\Sigma_1\)-represented in \(PA^-\) We apply the previous result for \({\mathbb{N}}\) to get a \(\Sigma_1\) \(\exists \bar z. \phi(\bar x, y, \bar z)\) and equivalently \(\exists z. \phi(\bar x, y, z)\) by coding.
By example sheet 4 question 2, any \(\Sigma_1\)-sentence true in \({\mathbb{N}}\) is true in any model of \(PA^-\). So we have the second part of the representation definition, but we need the first part. That's tricky because we don't yet have uniqueness for the \(\phi\) statement above (we could pick a \(z\) larger than the smallest minimizable).
So just write a predicate that forbids smaller solutions: \[\psi(\bar x, y, z) := \phi(\bar x, y, z) \land \forall u,\, u \leq (y + z). \forall v, v \leq (y + z). (u+v < y + z \to \neg \phi(\hat x, u, v))\]
Corollary:
Every recursive set \(A \subseteq {\mathbb{N}}^m\) is \(\Sigma_1\)-represented in \(PA^-\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability What do we call an \(L_{PA}\) formula with one free variable? An unary predicate LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: State the Diagonalization Lemma Let \(T\) be an \(L_{PA}\) theory in which every total recursive function is \(\Sigma_1\)-represented, and let \(\theta(x)\) be an \(L_{PA}\) formula with one free variable. Then there exists some sentence \(G\) of \(L_{PA}\) such that \[T \vdash (G \iff \theta(\lceil G \rceil))\]
(So for any numeric property, there's a sentence \(G\) that provably states that its own Godel number has that property) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Diag \(\mathrm{diag}(n):\)
If \(n = \lceil \sigma(x)\rceil\), return \(\lceil \forall y. (y = n \to \sigma(y)) \rceil\)
Else return 0.
We're just rewriting the sentence \(\sigma(x)\) coded by \(n\) to include \(n\) itself.
diag is the coded function that plugs a number into the conditional it represents (if possible). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Fixed Point Theorem There exists a closed \(\lambda\)-term \(Y\) such that for all \(F\), \[F(YF) \equiv_\beta YF\]
\(Y\) is called a fixed-point function. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Axiom of Extensionality Two sets are equal if they have the same elements. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Axiom of Separation We can define sets as we normally do: \[A = \{ x \in S : \varphi(x) \}\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Axiom of Pairing If you have two sets, there exists a set that contains those two sets: \[\{ A, B \}\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Axiom of Choice Suppose you have a set \(X\) of nonempty sets. Then there exists a function \(f\) that maps each \(x \in X\) to one of its elements. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Statement of Diaconescu's Theorem We can deduce the Law of Excluded Middle (\(\forall \varphi,\,\varphi \lor \neg \varphi \)) from the Axion of Choice in a minimal intuitionistic setting. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proposition: Diaconescu's Theorem Want to show \(\forall \varphi,\,\varphi \lor \neg \varphi \); fix \(\varphi\).
Use the axiom of seperation to get: \[A = \{ x \in \{ 0, 1 \} : \varphi \lor (x = 0) \}\] \[B = \{ x \in \{ 0, 1 \} : \varphi \lor (x = 1) \}\] Use the Axiom of Pairing to get \(\{ A, B \}\). Because \(0 \in A\) and \(1 \in B\), \(A\) and \(B\) are inhabited, so we have a choice function \[f: \{ A, B \} \to A \cup B\] with \(f(A) \in A\) and \(f(B) \in B\).
So we have a proof of \[(f(A) = 0 \lor \varphi) \land (f(B) = 1 \lor \varphi)\] By intuistic logic, we can split into four cases: \[f(A) =0,\, f(B) = 0\] \(f(B) = 0\) implies \(\varphi\) above. \[f(A) = 0,\, f(B) = 1\] Hard case, see below. \[f(A) = 1, f(B) = 0\] \(f(A) = 1\) implies \(\varphi\) above. \[f(A) = 1, f(B) = 1\] \(f(A) = 1\) implies \(\varphi\) above.
Hard case: \(f(A) = 0,\, f(B) = 1\). Prove \(\neg \varphi = \varphi \to \bot\) by the following:
Assume \(\varphi\).
By the Axiom of Extensionality, \(A = B\)
But \(f(A)\) and \(f(B)\) don't have the same value! \[0 = f(A) = f(B) = 1\] Contradiction, we have \(\neg \varphi\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: \(\beta\)-redex A term we can simplify into a \(\beta\)-contractum: \[(\lambda x: \sigma . p) Q \to_\beta P[x := Q]\] Read this as 'function application candidate' LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Weak Normalization Theorem \(m\) function \[m(M) := (0,0) \, \text{ if $M$ is in beta-normal form}\] \[m(M) := (h(M), \mathrm{redex}(M))\]
where \(h(M)\) is the greatest height of a redex in \(M\), and \(\mathrm{redex}(M)\) is the number of occurances of redexes in \(M\) of maximal height.
(the height of a redex is the height of the type of the function being applied) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Grammar of the Full Simply-Typed Lambda Calculus Types \[\begin{align*} \lambda_\Pi &:\, V & \text{Variable}\\\\ &|\, \lambda V: \Pi . \lambda_\Pi & \text{$\lambda$-Abstraction}\\\\ &|\, \lambda_\Pi\lambda_\Pi & \text{$\lambda$-Application}\\\\ &|\, \left< \Pi, \Pi \right> & \text{Product Constructor}\\\\ &|\, \Pi_1(\lambda_\Pi)\, | \, \Pi_2(\lambda_\Pi) & \text{Projection Types / Product Eliminators}\\\\ &|\, \iota_1(\lambda_\Pi)\, | \, \iota_2(\lambda_\Pi) & \text{Left and Right Coproduct Constructors}\\\\ &|\, \mathrm{Case}(\lambda_\Pi; V.\lambda_\Pi; V. \lambda_\Pi) & \text{Coproduct Eliminator}\\\\ &|\, * & \text{Terminal Type Constructor}\\\\ &|\, !_\Pi \lambda_\Pi & \text{Explosion Type} \end{align*}\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Explosion Typing Rule \[\frac{\Gamma \Vdash M : 0}{\Gamma \Vdash !_\varphi M : \varphi}\] for every type \(\varphi \in \Pi\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Case Beta-Reduction \[\mathrm{Case}(\iota_1(M); x.K; y.L) )\to_\beta K[x := M]\] \[\mathrm{Case}(\iota_2(M); x.K; y.L) )\to_\beta L[y := M]\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Extra BHK interpretation \(\eta\)-reductions \[\left< \pi_1 M, \pi_2 M \right> \to_\eta M\] Also if \(\Gamma \Vdash M : 1\) we have \(M \to_\eta *\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: G \[G := \forall y. (y = n \to \psi(y))\] where \[\psi (x) := \forall z. (\delta(x, z) \to \theta(z))\] (\(\delta(x, z)\) is the \(\Sigma_1\)-representation of diag)
and \(n = \lceil \psi (x)\rceil\)
LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Crude Incompleteness Let \(T\) be a recursive set of (Godel numbers of) \(L_{PA}\) sentences that is consistent (never contains both \(\phi\) and \(\neg \phi\)) and contains all the \(\Sigma_1\) and \(\Pi_1\) sentences provable in \(PA^-\).
Then there exists a \(\Pi_1\) sentence \(\tau\) such that \(\tau \not\in T\) and \(\neg \tau \not \in T\) (\(T\) can't prove \(\tau\) or its negation). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Godel-Rosser Theorem Let \(T\) be a consistent \(L_{PA}\) theory extending \(PA^-\) and admitting a recursively enumerable axiomatization.
Then \(T\) is \(\Pi_1\) incomplete: there exists a \(\Pi_1\) sentence \(\tau\) for which \(T \not \vdash \tau\) and \(T \not \vdash \neg \tau\)
Assume that \(T\) is complete to get a contradiction. Use Craig's trick to get a recursive axiomatization, do exhaustive proof search from axioms (paired with completeness) to show that \(S\) is recursive. But then we can apply Crude Incompleteness to get a contradiction. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Recursive (and countable) \(L_{PA}\)-structures A (countable) \(L_{PA}\)-structure \({\mathcal{M}}\) is recursive if and only if there exist recursive functions \(\oplus: {\mathbb{N}}^2 \to {\mathbb{N}}\), \(\otimes: {\mathbb{N}}^2 \to {\mathbb{N}}\), a binary recursive relation \(\preceq \subseteq {\mathbb{N}}^2\), and natural numbers \(n_0, n_1 \in {\mathbb{N}}\) such that \[ {\mathcal{M}} \cong ({\mathbb{N}}, \oplus, \otimes, \preceq, n_0, n_1)\] LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Prime Function The \(\Sigma_1\) formula \(\mathrm{pr}(x,y)\) is true only when \(y\) is the \(x\)th prime number. \[PA \vdash \forall x,\exists! y, \mathrm{pr}(x,y)\] So if \({\mathbb{N}}\) believes \(y\) is the \(x\)th prime number, all models of \(PA\) do.
We denote the \(k\)th prime \(\pi_k\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Overspill Lemma Let \({\mathcal{M}}\) be a nonstandard model of \(PA\), \(\phi(x,\bar y)\) be an \(L_{PA}\) formula, and \(\bar a \in {\mathcal{M}}\).
If \({\mathcal{M}} \vDash \phi(n, \bar a)\) for all standard natural numbers \(n\), then there exists a nonstandard \(e \in M\) such that \({\mathcal{M}} \vDash \forall x \leq e. \phi(x,\bar a)\) LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Proof of Overspill Suppose there exists some function \(\mathrm{st}(x,\bar a)\), that, given some helper data \(\bar a\), is true only when \(x\) is a standard natural number.
But clearly we can apply 'st' inductively from zero: \[M \vDash \mathrm{st}(0, \bar a) \land \forall x. \mathrm{st}(x, \bar a) \to \mathrm{st}(x+1,\bar a)\] and remember by the inductive axiom of \(PA\), we must then have \(\forall x, \mathrm{st}(x,\bar a)\)! But that defeats the whole point: every element of a nonstandard model can't be standard! LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Canonical Coding A subset \(S \subseteq {\mathbb{N}}\) is canonically coded in a model \({\mathcal{M}}\) of \(PA\) if there exists some element \(c \in {\mathcal{M}}\) such that \[S = \{ n \in {\mathbb{N}}: \exists y. (\pi_{n^*} \times y) = c \}\] where \(n^*\) is the standard natural number \(n\) in the model.
We proved in class that for any nonstandard model \({\mathcal{M}}\) of \(PA\), there exists a non-recursive set \(S\) which is canonically coded in \({\mathcal{M}}\). LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Recursive Inseparability Subsets \(A\), \(B\) of \({\mathbb{N}}\) are recursively inseparable if they are disjoint and there is no recursive subset \(C\) of \({\mathbb{N}}\) such that \(B \cap C = \emptyset\) and \(A \subseteq C\).
We proved in class that they must exist. LogicAndComputability PartIIINotes
Basic Part III Notes::LogicAndComputability Definition: Tennenbaum's Theorem Let \({\mathcal{M}} = (M, \oplus, \otimes, \preceq, n_0, n_1)\) be a countable nonstandard model of \(PA\). Then \(\oplus\) is not recursive. LogicAndComputability PartIIINotes