Data on AI 2024-06-20T06:31:57.216Z

Epoch is hiring an ML Distributed Systems Senior Researcher 2023-11-24T22:33:53.860Z

Announcing Epoch's newly expanded Parameters, Compute and Data Trends in Machine Learning database 2023-10-25T02:55:07.440Z

Comment by Jaime Sevilla Molina (jaime-sevilla-molina) on A Sketch of Good Communication · 2018-04-01T18:10:10.840Z · LW · GW

I appreciate that in the example it just so happens that the person assigning a lower probability ends up assigning a higher probability that the other person at the beginning, because it is not intuitive that this can happen but actually very reasonable. Good post!

Comment by Jaime Sevilla Molina (jaime-sevilla-molina) on Toward a New Technical Explanation of Technical Explanation · 2018-02-19T17:51:24.179Z · LW · GW

This is rather random, but I really appreciate the work made by the moderators when explaining their reasons for curating an article. Keep this up please!

Comment by Jaime Sevilla Molina (jaime-sevilla-molina) on A primer on provability logic · 2016-07-27T13:12:20.000Z · LW · GW

Generalized fixed point theorem:

Suppose that $A_i(p_1,...,p_n)$ are $n$ modal sentences such that $A_i$ is modalized in $p_n$ (possibly containing sentence letters other than $p_{j}s$).

Then there exists $H_1,...,H_n$ in which no $p_j$ appears such that $GL⊢{\wedge }_{i\le n}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow {\wedge }_{i\le n}\{⊡(p_i\leftrightarrow H_i)\}$.

---

We will prove it by induction.

For the base step, we know by the fixed point theorem that there is $H$ such that $GL⊢⊡(p_1\leftrightarrow A_i(p_1,...,p_n\left)\right)\leftrightarrow ⊡(p_1\leftrightarrow H(p_2,...,p_n\left)\right)$

Now suppose that for $j$ we have $H_1,...,H_j$ such that $GL⊢{\wedge }_{i\le j}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow {\wedge }_{i\le j}\{⊡(p_i\leftrightarrow H_i(p_{j+1},...,p_n\left)\right)\}$.

By the second substitution theorem, $GL⊢⊡(A\leftrightarrow B)\to \left[F\right(A)\leftrightarrow F(B\left)\right]$. Therefore we have that $GL⊢⊡(p_i\leftrightarrow H_i(p_{j+1},...,p_n)\to [⊡(p_{j+1}\leftrightarrow A_{j+1}(p_1,...,p_n\left)\right)\leftrightarrow ⊡(p_{j+1}\leftrightarrow A_{j+1}(p_1,...,p_{i-1},H_i(p_{j+1},...,p_n),p_{i+1},...,p_n\left)\right)]$.

If we iterate the replacements, we finally end up with $GL⊢{\wedge }_{i\le j}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\to ⊡(p_{j+1}\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n))$.

Again by the fixed point theorem, there is $H_{j+1}^{\prime }$ such that $GL⊢⊡(p_{j+1}\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n\left)\right)\leftrightarrow ⊡[p_{j+1}\leftrightarrow H_{j+1}^{\prime }(p_{j+2},...,p_n\left)\right]$.

But as before, by the second substitution theorem, $GL⊢⊡[p_{j+1}\leftrightarrow H_{j+1}^{\prime }(p_{j+2},...,p_n\left)\right]\to [⊡(p_i\leftrightarrow H_i(p_{j+1},...,p_n))\leftrightarrow ⊡(p_i\leftrightarrow H_i(H_{j+1}^{\prime },...,p_n))$.

Let $H_i^{\prime }$ stand for $H_i(H_{j+1}^{\prime },...,p_n)$, and by combining the previous lines we find that $GL⊢{\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\to {\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow H_i^{\prime }(p_{j+2},...,p_n\left)\right)\}$.

By Goldfarb's lemma, we do not need to check the other direction, so $GL⊢{\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow {\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow H_i^{\prime }(p_{j+2},...,p_n\left)\right)\}$ and the proof is finished $\square$

---

An immediate consequence of the theorem is that for those fixed points $H_i$ and every $A_i$, $GL⊢H_i\leftrightarrow A_i(H_1,...,H_n)$.

Indeed, since $GL$ is closed under substitution, we can make the change $p_i$ for $H_i$ in the theorem to get that $GL⊢{\wedge }_{i\le n}\{⊡(H_i\leftrightarrow A_i(H_1,...,H_n)\}\leftrightarrow {\wedge }_{i\le n}\{⊡(H_i\leftrightarrow H_i)\}$.

Since the righthand side is trivially a theorem of $GL$, we get the desired result.

---

One remark: the proof is wholly constructive. You can iterate the construction of fixed point following the procedure implied by the construction of the $H_i^{\prime }$ to compute fixed points.

Comment by Jaime Sevilla Molina (jaime-sevilla-molina) on A primer on provability logic · 2016-07-21T11:30:41.000Z · LW · GW

Uniqueness of arithmetic fixed points:

Notation: $⊡A=\square A\wedge A$

Let $H$ be a fixed point on $p$ of $\varphi \left(p\right)$; that is, $GL⊢⊡(p\leftrightarrow \varphi (p\left)\right)\leftrightarrow (p\leftrightarrow H)$.

Suppose $I$ is such that $GL⊢H\leftrightarrow I$. Then by the first substitution theorem, $GL⊢F\left(I\right)\leftrightarrow F\left(H\right)$ for every formula $F\left(q\right)$. If $F\left(q\right)=⊡(p\leftrightarrow q)$, then $GL⊢⊡(p\leftrightarrow H)\leftrightarrow ⊡(p\leftrightarrow I)$, from which it follows that $GL⊢⊡(p\leftrightarrow \varphi (p\left)\right)\leftrightarrow (p\leftrightarrow I)$.

Conversely, if $H$ and $I$ are fixed points, then $GL⊢⊡(p\leftrightarrow H)\leftrightarrow ⊡(p\leftrightarrow I)$, so since $GL$ is closed under substitution, $GL⊢⊡(H\leftrightarrow H)\leftrightarrow ⊡(H\leftrightarrow I)$. Since $GL⊢⊡(H\leftrightarrow H)$, it follows that $GL⊢(H\leftrightarrow I)$.

(Taken from The Logic of Provability, by G. Boolos.)