{"id":143,"date":"2017-09-22T03:01:02","date_gmt":"2017-09-22T10:01:02","guid":{"rendered":"http:\/\/alexmennen.com\/?p=143"},"modified":"2022-01-28T19:45:06","modified_gmt":"2022-01-29T03:45:06","slug":"metamathematics-and-probability","status":"publish","type":"post","link":"http:\/\/alexmennen.com\/index.php\/2017\/09\/22\/metamathematics-and-probability\/","title":{"rendered":"Metamathematics and probability"},"content":{"rendered":"\n

<\/p>\n\n\n

Content warning: mathematical logic.<\/p>\n

Note: This write-up consists mainly of open questions rather than results, but may contain errors anyway.<\/p>\n

Setup<\/h3>\n

I’d like to describe a logic for talking about probabilities of logical sentences. Fix some first-order language \"{\cal L}\". This logic deals with pairs \"\left(\varphi,p\right)\", which I’m calling assertions, where \"\varphi\in{\cal L}\" is a formula and \"p\in\left[0,1\right]\". Such a pair is to be interpreted as a claim that \"\varphi\" has probability at least \"p\".<\/p>\n

A theory consists of a set of assertions. A model of a theory \"T\" consists of a probability space \"\left(X,P\right)\" whose points are \"{\cal L}\"-structures, such that for every assertion \"\left(\varphi,p\right)\in T\", \"P_{*}\left(\left\{ {\cal M}\in X\mid{\cal M}\models\varphi\right\} \right)\geq p\", where \"P_{*}\" is inner probability. I’ll write \"T\vdash_{p}\varphi\" for \"\left(\varphi,p\right)\" can be proved from \"T\", and \"T\models_{p}\varphi\" for all models of \"T\" are also models of \"\left\{ \left(\varphi,p\right)\right\}\".<\/p>\n

The rules of inference are all rules \"\Gamma\vdash_{p}\varphi\" where \"\Gamma\" is a finite set of assertions, and \"\left(\varphi,p\right)\" is an assertion such that \"P_{*}\left(\left\{ {\cal M}\in X\mid{\cal M}\models\varphi\right\} \right)\geq p\" in all models of \"\Gamma\". Can we make an explicit finite list of inference rules that generate this logic? If not, is the set of inference rules at least recursively enumerable? (For recursive enumerability to make sense here, we need to restrict attention to probabilities in some countable dense subset of \"\left[0,1\right]\" that has a natural explicit bijection with \"\mathbb{N}\", such as \"\mathbb{Q}\cap\left[0,1\right]\".) I’m going to assume later that the set of inference rules is recursively enumerable; if it isn’t, everything should still work if we use some recursively enumerable subset of the inference rules that includes all of the ones that I use.<\/p>\n

Note that the compactness theorem fails for this logic; for example, \"\left\{ \left(\varphi,p\right)\mid p<1\right\} \models_{1}\varphi\", but no finite subset of \"\left\{ \left(\varphi,p\right)\mid p<1\right\}\" implies \"\left(\varphi,1\right)\", and hence \"\left\{ \left(\varphi,p\right)\mid p<1\right\} \nvdash_{1}\varphi\".<\/p>\n

Any classical first-order theory \"T\" can be converted into a theory in this logic as \"\left\{ \left(\varphi,1\right)\mid T\vdash\varphi\right\}\".<\/p>\n

L\u00f6b’s Theorem<\/h3>\n

Let \"T\" be a consistent, recursively axiomatizable extension of Peano Arithmetic. By the usual sort of construction, there is a \"\Sigma_{1}^{0}\" binary predicate \"\square_{y}\left(x\right)\" such that \"T\vdash_{p}\varphi\iff\mathbb{N}\models\square_{p}\left(\ulcorner\varphi\urcorner\right)\" for any sentence \"\varphi\" and \"p\in\left[0,1\right]\cap\mathbb{Q}\", where \"\ulcorner\urcorner\" is a coding of sentences with natural numbers. We have a probabilistic analog of L\u00f6b’s theorem: if \"T\vdash_{p}\square_{p}\left(\ulcorner\varphi\urcorner\right)\rightarrow\varphi\", then \"T\vdash_{p}\varphi\". Peano arithmetic can prove this theorem, in the sense that \"PA\vdash_{1}\square_{p}\left(\ulcorner\square_{p}\left(\ulcorner\varphi\urcorner\right)\rightarrow\varphi\urcorner\right)\rightarrow\square_{p}\left(\ulcorner\varphi\urcorner\right)\".<\/p>\n

Proof: Assume \"T\vdash_{p}\square_{p}\left(\ulcorner\varphi\urcorner\right)\rightarrow\varphi\". By the diagonal lemma, there is a sentence \"\psi\" such that \"T\vdash_{1}\psi\leftrightarrow\left(\square_{p}\left(\ulcorner\psi\urcorner\right)\rightarrow\varphi\right)\". If \"\square_{p}\left(\ulcorner\psi\urcorner\right)\", then \"\square_{1}\left(\ulcorner\square_{p}\left(\ulcorner\psi\urcorner\right)\urcorner\right)\" and \"\square_{p}\left(\ulcorner\square_{p}\left(\ulcorner\psi\urcorner\right)\rightarrow\varphi\urcorner\right)\", so \"\square_{p}\left(\ulcorner\varphi\urcorner\right)\". This shows that \"T\cup\left\{ \left(\square_{p}\left(\ulcorner\psi\urcorner\right),1\right)\right\} \vdash_{1}\square_{p}\left(\ulcorner\varphi\urcorner\right)\". By the assumption that \"T\vdash_{p}\square_{p}\left(\ulcorner\varphi\urcorner\right)\rightarrow\varphi\", this implies that \"T\cup\left\{ \left(\square_{p}\left(\ulcorner\psi\urcorner\right),1\right)\right\} \vdash_{p}\varphi\". By a probabilistic version of the deduction theorem, \"T\vdash_{p}\square_{p}\left(\ulcorner\psi\urcorner\right)\rightarrow\varphi\". That is, \"T\vdash_{p}\psi\". Going back around through all that again, we get \"T\vdash_{p}\varphi\".<\/p>\n

If we change the assumption to be that \"T\vdash_{q}\square_{p}\left(\ulcorner\varphi\urcorner\right)\rightarrow\varphi\" for some \"q<p\", then the above proof does not go through (if \"q>p\", then it does, because \"\left(\theta,q\right)\vdash_{p}\theta\"). Is there a consistent theory extending Peano Arithmetic that proves a soundness schema about itself, \"\left\{ \left(\square_{p}\left(\ulcorner\varphi\urcorner\right)\rightarrow\varphi,q\right)\mid q<p\right\}\", or can this be used to derive a contradiction some other way? If there is no such consistent theory, then can the soundness schema be modified so that it is consistent, while still being nontrivial? If there is such a consistent theory with a soundness schema, can the theory also be sound? That is actually several questions, because there are multiple things I could mean by “sound”. The possible syntactic things “sound” could mean, in decreasing order of strictness, are: 1) The theory does not assert a positive probability to any sentence that is false in \"\mathbb{N}\". 2) There is an upper bound below \"1\" for all probabilities asserted of sentences that are false in \"\mathbb{N}\". 3) The theory does not assert probability \"1\" to any sentence that is false in \"\mathbb{N}\".<\/p>\n

There are also semantic versions of the above questions, which are at least as strict as their syntactic analogs, but probably aren’t equivalent to them, since the compactness theorem does not hold. The semantic version of asking if the soundness schema is consistent is asking if it has a model. The first two soundness notions also have semantic analogs. 1′) \"\left\{ \mathbb{N}\right\}\" is a model of the theory. 2′) There is a model of the theory that assigns positive probability to \"\mathbb{N}\". I don’t have a semantic version of 3, but metaphorically speaking, a semantic version of 3 should mean that there is a model that assigns nonzero probability density at \"\mathbb{N}\", even though it might not have a point mass at \"\mathbb{N}\".<\/p>\n

Motivation<\/h3>\n

This is somewhat similar to Definability of Truth in Probabilistic Logic<\/a>. But in place of adding a probability predicate to the language, I’m only changing the metalanguage to refer to probabilities, and using this to express statements about probability in the language through conventional metamathematics. An advantage of this approach is that it’s constructive. Theories with the properties described by the Christiano et al paper are unsound, so if some reasonably strong notion of soundness applies to an extension of Peano Arithmetic with the soundness schema I described, that would be another advantage of my approach.<\/p>\n

A type of situation that this might be useful for is that when an agent is reasoning about what actions it will take in the future, it should be able to trust its future self’s reasoning. An agent with the soundness schema can assume that its future self’s beliefs are accurate, up to arbitrarily small loss in precision. A related type of situation is if an agent reaches some conclusion, and then writes it to external storage instead of its own memory, and later reads the claim it had written to external storage. With the soundness schema, if the agent has reason to believe that the external storage hasn’t been tampered with, it can reason that since its past self had derived the claim, the claim is to be trusted arbitrarily close to as much as it would have been if the agent had remembered it internally.<\/p>\n

First Incompleteness Theorem<\/h3>\n

For a consistent theory \"T\", say that a sentence \"\varphi\" is \"T\"-measurable if there is some \"p\in\left[0,1\right]\" such that \"T\vdash_{q}\varphi\" for every \"q<p\" and \"T\vdash_{q}\neg\varphi\" for every \"q<1-p\". So \"T\"-measurability essentially means that \"T\" pins down the probability of the sentence. If \"\varphi\" is not \"T\"-measurable, then you could say that \"T\" has Knightian uncertainty about \"\varphi\". Say that \"T\" is complete if every sentence is \"T\"-measurable. Essentially, complete theories assign a probability to every sentence, while incomplete theories have Knightian uncertainty.<\/p>\n

The first incompleteness theorem (that no recursively axiomatizable extension of PA is consistent and complete) holds in this setting. In fact, for every consistent recursively axiomatizable extension of PA, there must be sentences that are given neither a nontrivial upper bound nor a nontrivial lower bound on their probability. Otherwise, we would be able to recursively separate the theorems of PA from the negations of theorems of PA, by picking some recursive enumeration of assertions of the theory, and sorting sentences by whether they are first given a nontrivial lower bound or first given a nontrivial upper bound; theorems of PA will only be given a nontrivial lower bound, and their negations will only be given a nontrivial upper bound. [Thanks to Sam Eisenstat for pointing this out; I had somehow managed not to notice this on my own.]<\/p>\n

For an explicit example of a sentence for which no nontrivial bounds on its probability can be established, use the diagonal lemma to construct a sentence \"\varphi\" which is provably equivalent to “for every proof of \"\left(\varphi,p\right)\" for any \"p>0\", there is a proof of \"\left(\neg\varphi,q\right)\" for some \"q>0\" with smaller G\u00f6del number.”<\/p>\n

Thus a considerable amount of Knightian uncertainty is inevitable in this framework. Dogmatic Bayesians such as myself might find this unsatisfying, but I suspect that any attempt to unify probability and first-order arithmetic will suffer similar problems.<\/p>\n

A side note on model theory and compactness<\/h3>\n

I’m a bit unnerved about the compactness theorem failing. It occurred to me that it might be possible to fix this by letting models use hyperreal probabilities. Problem is, the hyperreals aren’t complete, so the countable additivity axiom for probability measures doesn’t mean anything, and it’s unclear what a hyperreal-valued probability measure is. One possible solution is to drop countable additivity, and allow finitely-additive hyperreal-valued probability measures, but I’m worried that the logic might not even be sound for such models.<\/p>\n

A different possible solution to this is to take a countably complete ultrafilter \"U\" on a set \"\kappa\", and use probabilities valued in the ultrapower \"\mathbb{R}^{\kappa}/U\". Despite \"\mathbb{R}^{\kappa}/U\" not being Cauchy complete, it inherits a notion of convergence of sequences from \"\mathbb{R}\", since a sequence \"\left\{ \left[x_{i,j}\mid i\in\kappa\right]\mid j\in\omega\right\}\" can be said to converge to \"\left[\lim_{j\rightarrow\infty}x_{i,j}\mid i\in\kappa\right]\", and this is well-defined (if \"\lim_{j\rightarrow\infty}x_{i,j}\" is for a \"U\"-large set of indices \"i\") by countable completeness. Thus the countable additivity axiom makes sense for \"\mathbb{R}^{\kappa}/U\"-valued probability measures. Allowing models to use \"\mathbb{R}^{\kappa}/U\"-valued probability measures might make the compactness theorem work. [Edit: This doesn’t work, because \"\mathbb{R}^{\kappa}/U\cong\mathbb{R}\". To see this, it is enough to show that \"\mathbb{R}^{\kappa}/U\" is Archimedean, since \"\mathbb{R}\" has no proper Archimedean extensions.\u00a0Given \"\left[x_i\mid i\in\kappa\right]\in\mathbb{R}^{\kappa}/U\", let \"A_n:=\{i\in\kappa\mid| x_i|<n\}\" for \"n\in\mathbb{N}\". \"\bigcup_{n\in\mathbb{N}}A_n = \kappa\", so by countable completeness of \"U\", there is some \"n\in\mathbb{N}\" such that \"A_n\in U\", and thus\u00a0\"\left[x_i\mid i\in\kappa\right]<n\".]<\/p>","protected":false},"excerpt":{"rendered":"

Content warning: mathematical logic. Note: This write-up consists mainly of open questions rather than results, but may contain errors anyway. Setup I’d like to describe a logic for talking about probabilities of logical sentences. Fix some first-order language . This logic deals with pairs , which I’m calling assertions, where is a formula and . … Continue reading Metamathematics and probability<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[7],"tags":[],"class_list":["post-143","post","type-post","status-publish","format-standard","hentry","category-math"],"post_mailing_queue_ids":[],"_links":{"self":[{"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/posts\/143","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/comments?post=143"}],"version-history":[{"count":12,"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/posts\/143\/revisions"}],"predecessor-version":[{"id":316,"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/posts\/143\/revisions\/316"}],"wp:attachment":[{"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/media?parent=143"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/categories?post=143"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/alexmennen.com\/index.php\/wp-json\/wp\/v2\/tags?post=143"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}