User:IssaRice/Computability and logic/Diagonalization lemma (Yanofsky method): Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
This page is just a rewritten version of the [https://arxiv.org/pdf/math/0305282.pdf#section.5 proof of the diagonalization lemma from Yanofsky's paper]. There are some parts I found difficult to understand/gaps that I thought should be filled, so this version will hopefully be much more complete. | This page is just a rewritten version of the [https://arxiv.org/pdf/math/0305282.pdf#section.5 proof of the diagonalization lemma from Yanofsky's paper]. There are some parts I found difficult to understand/gaps that I thought should be filled, so this version will hopefully be much more complete. | ||
'''Theorem (Diagonalization lemma).''' Let <math>T</math> be some nice theory (I don't remember the exact conditions, but Peano Arithmetic or Robinson Arithmetic would work). For any single-place formula <math>\mathcal E(x)</math> with <math>x</math> as its only free variable, there exists a sentence (closed formula) <math>\mathcal C</math> such that <math>T \vdash \mathcal C \leftrightarrow \mathcal E(\ulcorner \mathcal C \urcorner)</math> | '''Theorem (Diagonalization lemma).''' Let <math>T</math> be some nice theory (I don't remember the exact conditions, but Peano Arithmetic or Robinson Arithmetic would work). For any single-place formula <math>\mathcal E(x)</math> with <math>x</math> as its only free variable, there exists a sentence (closed formula) <math>\mathcal C</math> such that <math>T \vdash \mathcal C \leftrightarrow \mathcal E(\ulcorner \mathcal C \urcorner)</math>. | ||
''Proof.'' We will use what's called the [[wikipedia:Lindenbaum–Tarski algebra]] in our proof, which the Yanofsky paper just calls Lindenbaum classes. The idea is to define an equivalence an equivalence relation on formulas, so that <math>A \sim B</math> iff our theory <math>T</math> can prove that <math>A</math> and <math>B</math> are logically equivalent. In other words, we define <math>A \sim B</math> iff <math>T \vdash A \leftrightarrow B</math>. This is easily verified to be an equivalence relation. One twist is that it doesn't make sense to compare two formulas with differing arity. For instance, what does it even mean to say "2+2=5" and "x+5=7" are or are not provably equivalent? For this reason, we make a separate equivalence relation for each arity, and so we end up with separate quotients for each arity. For <math>i=0,1,2,\ldots</math>, we let <math>\mathit{Lind}^i</math> be the set of Lindenbaum classes of formulas with <math>i</math> free variables. | |||
Acknowledgments: Thanks to Rupert McCallum for helping me work through the proof. | Acknowledgments: Thanks to Rupert McCallum for helping me work through the proof. | ||
Revision as of 20:35, 27 July 2021
This page is just a rewritten version of the proof of the diagonalization lemma from Yanofsky's paper. There are some parts I found difficult to understand/gaps that I thought should be filled, so this version will hopefully be much more complete.
Theorem (Diagonalization lemma). Let be some nice theory (I don't remember the exact conditions, but Peano Arithmetic or Robinson Arithmetic would work). For any single-place formula with as its only free variable, there exists a sentence (closed formula) such that .
Proof. We will use what's called the wikipedia:Lindenbaum–Tarski algebra in our proof, which the Yanofsky paper just calls Lindenbaum classes. The idea is to define an equivalence an equivalence relation on formulas, so that iff our theory can prove that and are logically equivalent. In other words, we define iff . This is easily verified to be an equivalence relation. One twist is that it doesn't make sense to compare two formulas with differing arity. For instance, what does it even mean to say "2+2=5" and "x+5=7" are or are not provably equivalent? For this reason, we make a separate equivalence relation for each arity, and so we end up with separate quotients for each arity. For , we let be the set of Lindenbaum classes of formulas with free variables.
Acknowledgments: Thanks to Rupert McCallum for helping me work through the proof.