SamEisenstat

Karma: 186

SamEisenstat 26 Nov 2025 8:16 UTC
1 point
0
in reply to: SamEisenstat’s comment on: Informality
I have a feeling that something is missing from the Łukasiewicz stuff you’ve been doing because I don’t think that assigning a quantitative degree of truth is all that vagueness really ought to be about. Vague sentences shift their meanings as the context changes. Vague statements can become crisp statements, and accordingly our language can gain more powerful synonymy. As a slogan perhaps, “vagueness wants to become ambiguity”.

SamEisenstat 26 Nov 2025 8:08 UTC
4 points
0
on: Informality
I want to use some notion of the power of logic/synonymy relation here. We can always have a vacuous synonymy relation—then all valid substitions preserve truth. Something like propositional logic would be more powerful, and quantificational logic more powerful yet.
Consider how much we can do in Peano arithmetic because of the power of the quantifier. We can use induction to deduce many things about divisibility, the solutions of Diophantine equations, and onward to large parts of mathematics.
For a less precise example, consider reasoning only in coordinates, or with the ability to perform a change of coordinates. A change of coordinates gives a synonymy relation, which we may find simplifies an argument significantly, or lets us “really understand” what’s happening. The picture that I have is that of a weaker and a stronger logical system—in the weaker system, we can’t express the notion of a change of coordinates, but in the stronger system we can. In fact, it’s doubtful whether there’s a reasonable language in which we can express many other thoughts, but not changes of coordinates, not even by some “coding trick”. So, we can take this example as a metaphor, or as a premonition of a generalization of the idea struggling to come into existence. I hope it is still able to shed light on what I mean by the power of a synonymy relation.
Anyway, here you want a normative direction pointing from vaguer languages to crisper languages. The crisper languages are better because they have synonymy. As you say “you don’t really understand something unless you can translate it into a transparent-context description”.
I want to construe this as about the power of synonymy relations. Crisp languages are better because we can use them to have interesting sequences of thoughts, because their synonymy does something for us. And so not just any synonymy relation are better—powerful ones are better.
I strongly doubt, as may be clear, the possibility of a “simple” definition that could measure power in terms of e.g. elementary syntactic criteria, but I think that we still have to admit that it’s what we want here.

SamEisenstat 26 Nov 2025 7:37 UTC
1 point
0
on: In Defense of Goodness
I worry that this equivocates between “we make our values in an ongoing way together” and simpler kinds of aggregation (analogous to voting, linear combinations, etc.). Well, strictly speaking you haven’t spelled out the former position—maybe I should just assert that it’s the only plausible way to interpret the creation of the individual out of “sub-self” entities, and that ultimately I’d like to describe what different individuals do together in this way also.
To explain somewhat further, I’ll assert that entities to which the concept of reinforcement learning is appropriate (say, Q-learners with function approximation, taking some sort of observation as the “state”)--and which I think I am right to construe as exemplifying the sort of sub-self entities that you’d like this discussion to describe—don’t have values. (The truth of that assertion probably depends on how I’m intending some of the words in ways that readers may not find obvious.) Most simply, they don’t really have beliefs; they don’t have anything we could call “world models” in a strong sense. To ask what they’d think of some possible world, we have to invent a way of presenting that world to their observation stream, opening the possibility of things like framing effects. If we find something that looks like incoherence, we don’t have a way of asking them to reflect on it. (We could try to invent ways to do such things, but if we equip them with such, then I want to say that they are no longer “mere” reinforcement learners.)
As such, they can’t vote, assign utilities, Nash bargain, etc. I think that there’s an interesting phenomenon of the arising of selves. I think that economics-flavored discussion of rational agent concepts can often distract from what’s most important, but in cases like this, can point in a productive direction. And here we see the disanalogy between the arising of selves and simple aggregation.
(Indeed, we see the limits of economic-flavored analysis is that fact that what is really missing from reinforcement learners is the space of possible worlds, which is classically taken as the precondition for analysis of rationality rather than something that can be evaluated as rational or irrational.)

SamEisenstat 1 Mar 2025 23:01 UTC
1 point
0
in reply to: Cole Wyeth’s comment on: Reflective oracles as a solution to the converse Lawvere problem
Yeah, it’s a bit weird to call this particular problem the converse Lawvere problem. The name suggests that there is a converse Lawvere problem for any concrete category and any base object $Y$--namely, to find an object $X$ and a map $f: X \to Y^X$ such that every morphism $X \to Y$ has the form $f(x)$ for some $x \in X$. But, among a small group of researchers, we ended up using the name for the case where $Y$ is the unit interval and the category is that of topological spaces, or alternatively a reasonable topological-like category. In this post, I play with that problem a bit, since I pass to considering functions with computability properties, rather than a topological definition. (I also don’t exactly define a category here...) I agree that what’s going on here is a UTM property.
I think this context of considering different categories is interesting. There’s an interplay between diagonal-lemma-type fixed-point theorems and topological fixed-point theorems going on in work like probabilistic truth predicates, reflective oracles, and logical induction. For more on analogies between fixed-point theorems, you can see e.g. A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points and Scott Garrabrant’s fixed point sequence.

SamEisenstat 24 Dec 2024 9:34 UTC
21 points
5
in reply to: Cleo Nardo’s comment on: strawberry calm’s Shortform
I think a lot of this is factual knowledge. There are five publicly available questions from the FrontierMath dataset. Look at the last of these, which is supposed to be the easiest. The solution given is basically “apply the Weil conjectures”. These were long-standing conjectures, a focal point of lots of research in algebraic geometry in the 20th century. I couldn’t have solved the problem this way, since I wouldn’t have recalled the statement. Many grad students would immediately know what to do, and there are many books discussing this, but there are also many mathematicians in other areas who just don’t know this.
In order to apply the Weil conjectures, you have to recognize that they are relevant, know what they say, and do some routine calculation. As I suggested, the Weil conjectures are a very natural subject to have a problem about. If you know anything about the Weil conjectures, you know that they are about counting points of varieties over a finite field, which is straightforwardly what the problems asks. Further, this is the simplest case, that of a curve, which is e.g. what you’d see as an example in an introduction to the subject.
Regarding the calculation, parts of it are easier if you can run some code, but basically at this point you’ve following a routine pattern. There are definitely many examples of someone working out what the Weil conjectures say for some curve in the training set.
Further, asking Claude a bit, it looks like $5^{18} \pm 6 \cdot 5^{9} + 1$ are particularly common cases here. So, if you skip some of the calculation and guess, or if you make a mistake, you have a decent chance of getting the right answer by luck. You still need the sign on the middle term, but that’s just one bit of information. I don’t understand this well enough to know if there’s a shortcut here without guessing.

Overall, I feel that the benchmark has been misrepresented. If this problem is representative, it seems to test broad factual knowledge of advanced mathematics more than problem-solving ability. Of course, this question is marked as the easiest of the listed ones. Daniel Litt says something like this about some other problems as well, but I don’t really understand how routine he’s saying that they are, are I haven’t tried to understand the solutions myself.

SamEisenstat 20 May 2024 18:17 UTC
1 point
0
in reply to: Terence Coelho’s comment on: The consistent guessing problem is easier than the halting problem
Well, I guess describing a model of a computably enumerable theory, like PA or ZFC counts. We could also ask for a model of PA that’s nonstandard in a particular way that we want, e.g. by asking for a model of $P A + \neg C o n (P A)$ , and that works the same way. Describing a reflective oracle has low solutions too, though this is pretty similar to the consistent guessing problem. Another one, which is really just a restatement of the low basis theorem, but perhaps a more evocative one, is as follows. Suppose some oracle machine $T$ has the property that there is some oracle that would cause it to run forever starting from an empty tape. Then, there is a low such oracle.
(Technically, these aren’t decision problems, since they don’t tell us what the right decision is, but just give us conditions that whatever decisions we make have to satisfy. I don’t know what to say instead; this is more general then e.g. promise problems. Maybe I’d use something like decision-class problems?)
All these have a somewhat similar flavour by the nature of the low basis theorem. We can enumerate a set of constraints, but we can’t necessarily compute a single object satisfying all the constraints. But the theorem tells us that there’s a low such object.
I don’t know what the situation is for subsets of the digits of Chaitin’s constant. Can it be as hard as the halting problem? You might try to refute this using some sort of incompressibility idea. Can it be low? I’d expect not, at least for computable subsets of indices of positive density. Plausibly computability theorists know about this stuff. They do like constructing posets of Turing degrees of various shapes, and they know about which shapes can be realized between $0$ and the halting degree $0^{'}$ . (E.g. this paper.)

SamEisenstat 20 May 2024 17:50 UTC
3 points
0
in reply to: jessicata’s comment on: The consistent guessing problem is easier than the halting problem
Yeah, there’s a sort of trick here. The natural question is uniform—we want a single reduction that can work from any consistent guessing oracle, and we think it would be cheating to do different things with different oracles. But this doesn’t matter for the solution, since we produce a single consistent guessing oracle that can’t be reduced to the halting problem.
This reminds me of the theory of enumeration degrees, a generalization of Turing degrees allowing open-set-flavoured behaviour like we see in partial recursive functions; if the answer to an oracle query is positive, the oracle must eventually tell you, but if the answer is negative it keeps you waiting indefinitely. I find the theory of enumeration degrees to be underemphasized in discussion of computability theory, but e.g. Odifreddi has a chapter on it all the way at the end of Classical Recursion Theory Volume II.
The consistent guessing problem isn’t a problem about enumeration degrees. It’s using a stronger kind of uniformity—we want to be uniform over oracles that differently guess consistently, not over a set of ways to give the same answers, but to present them differently. But there is again a kind of strangeness in the behaviour of uniformity, in that we get equivalent notions if we do or do not ask that a reduction between sets $A$ , $B$ be a single function that uniformly enumerates $A$ from enumerations of $B$ , so there might be some common idea here. More generally, enumeration degrees feel like they let us express more naturally things that are a bit awkward to say in terms of Turing degrees—it’s natural to think about the set of computations that are enumerable/ $Σ_{1}$ in a set—so it might be a useful keyword.

SamEisenstat 20 May 2024 9:23 UTC
19 points
2
on: The consistent guessing problem is easier than the halting problem
Note that Andy Drucker is not claiming to have discovered this; the paper you link is expository.
Since Drucker doesn’t say this in the link, I’ll mention that the objects you’re discussing are conventionally know as PA degrees. The PA here stands for Peano arithmetic; a Turing degree solves the consistent guessing problem iff it computes some model of PA. This name may be a little misleading, in that PA isn’t really special here. A Turing degree computes some model of PA iff it computes some model of ZFC, or more generally any $Σ_{1}$ theory capable of expressing arithmetic.
Drucker also doesn’t mention the name of the theorem that this result is a special case of: the low basis theorem. “Low” here suggests low computability strength. Explicitly, a Turing degree $A$ is low if solving the halting problem for machines with an oracle for $A$ is equivalent (in the sense of reductions) to solving the halting problem for Turing machines without any oracle. The low basis theorem says that every computable binary tree has a low path. We are able to apply the theorem to this problem, concluding that there is a consistent guessing oracle $C$ which is low. So, we cannot use this oracle to solve the halting problem; if we could, then an oracle machine with access to $C$ would be at least as strong as an oracle machine with access to the halting set, but we know that the halting set suffices to compute the halting problem for such a machine, which is a contradiction.
Various other things are known about PA degrees, though I’m not sure what might be of interest to you or others here. This stuff is discussed in books on computability theory, like Robert Soare’s Computability Theory and Applications. Though, I thought I learned about PA degrees from his earlier book, but now I don’t see them in there, so maybe I just learned about PA degrees around the same time, possibly following my interest in your and others’ work on reflective oracles. The basics of computability theory—Turing degrees, the Turing jump, and the arithmetic hierarchy in the computability sense—may be of interest to the extent there is anything there that you’re not already familiar with. With regard to PA degrees, in particular people like to talk about diagonally nonrecursive functions. This works as follows. Let $φ_{n}$ denote the $n$ th partial computable function according to some Goedel numbering. The PA degrees are exactly the Turing degrees that compute functions $f : N \to 2$ such that $f (n) \neq φ_{n} (n)$ for all numbers $n$ at which the right-hand side is defined. This is suggestive of the ideas around reflective oracles, the Lawvere fixed-point theorem, etc. But I wouldn’t say that when I think about these things, I think of them in terms of diagonally nonrecursive functions; plausibly that’s not an interesting direction to point people in.

SamEisenstat 28 Jul 2023 3:09 UTC
1 point
0
in reply to: Jesse Richardson’s comment on: [Error communicating with LW2 server]
I haven’t read too closely, but it looks like the equivalence relation that you’re talking about in the post sets elements that are scalar multiples of each other in equivalence. This isn’t the point of my equivalence; the stuff I wrote is all in terms of vectors, not directions. My other top-level comment discusses this.

SamEisenstat 28 Jul 2023 3:05 UTC
1 point
0
in reply to: Jesse Richardson’s comment on: [Error communicating with LW2 server]
Yeah, this could be clearer. The point is that 1/(c(v+ + w−))*(v+ + w−) and 1/(c(v+ + w−))*(v- + w+) are formal sums of elements of L. These formal sums have positive coefficients which sum to 1, so they represent convex combinations. But their not equal as formal sums, only the results of applying the convex combination operation of L are equal.

SamEisenstat 25 Jul 2023 16:21 UTC
1 point
0
on: [Error communicating with LW2 server]
We can then quotient $L^{2}$ by this relation to get a vector space $V$
I think you’re confusing two different parts here. There’s a quotient of a vector space to get a vector space, which is done to embed $\mathcal{L}$ in a vector space. There’s also something sort of like a projectivization, which does not produce a vector space. In the method I prefer, there isn’t an explicit quotient, but instead just functions on the vector space that satisfy certain properties. (I could see being convinced to prefer the other version if it did improve the presentation.)

SamEisenstat 25 Jul 2023 16:10 UTC
1 point
0
on: [Error communicating with LW2 server]
$L^{2}$ of differences of lotteries
Is this supposed to be the square of the space of lotteries? The square would correspond to formal differences, but actual differences would be a different space.
The point of my construction with formal differences is that differences of lotteries are not defined a priori. If we embed $\mathcal{L}$ in a vector space then we have already done what my construction is for. This is all in https://link.springer.com/article/10.1007/BF02413910 in some form, and many other places.
Happy to talk more about this.

SamEisenstat 24 Apr 2023 22:23 UTC
LW: 3 AF: 1
0
AF
on: Concave Utility Question
Q5 is true if (as you assumed), the space of lotteries is the space of distributions over a finite set. (For a general convex set, you can get long-line phenomena.)
First, without proof, I’ll state the following generalization.
Theorem 1. Let $⪯$ be a relation on a convex space $L$ satisfying axioms A1, A2, A3, and the following additional continuity axiom. For all $A, B_{1}, B_{2}, C \in L$ , the set
${p \in [0, 1] ∣ A ≺ p B_{1} + (1 - p) B_{2} ≺ C}$
is open in $[0, 1]$ . Then, there exists a function $u$ from $L$ to the long line such that $u (A) \leq u (B)$ iff $A ⪯ B$ .
The proof is not too different, but simpler, if we also assume A4. In particular, we no longer need the extra continuity axiom, and we get a stronger conclusion. Nate sketched part of the proof of this already, but I want to be clearer about what is stated and skip fewer steps. In particular, I’m not sure how Nate’s hypotheses rule out examples that require long-line-valued functions—maybe he’s assuming that the domain of the preference relation is a finite-dimensional simplex like I am, but none of his arguments use this explicitly.
Theorem 2. Let $⪯$ be a relation on a finite-dimensional simplex $L = Δ Ω$ satisfying axioms A1-A4. Then, there is a quasiconcave function $u : L \to R$ such that $u (A) \leq u (B)$ iff $A ⪯ B$ .
First, I’ll set up some definitions and a lemma. For any lotteries $A$ , $B$ , let $[A, B]$ denote the line segment
${p A + (1 - p) B ∣ p \in [0, 1]} .$
We say that preferences are increasing along a line segment $[A, B]$ if whenever $p \leq q$ , we have
$(1 - p) A + p B ⪯ (1 - q) A + q B .$
We will also use open and half-open interval notation in the corresponding way.
Lemma. Let $⪯$ be a preference relation on a finite-dimensional simplex $L = Δ Ω$ satisfying axioms A1-A4. Then, there are $⪯$ -minimal and -maximal elements in $L$ .
Proof. First, we show that there is a minimal element. Axiom A4 states that for any mixture $C = p A + (1 - p) B$ , either $C ⪰ A$ or $C ⪰ B$ . By induction, it follows more generally that any convex combination C of finitely many elements ${(A_{i})}_{i \in I}$ satisfies $C ⪰ A_{i}$ for some $i \in I$ . But every element is a convex combination of the vertices of $L$ , so some vertex of $L$ is $⪯$ -minimal.
The proof that there is a maximal element is more complex. Consider the family of sets
$F = {{B \in L ∣ B ⪰ A} ∣ A \in L} .$
This is a prefilter, so since $L$ is compact ( $L$ here carries the Euclidean metric), it has a cluster point $B$ . Either $B$ will be a maximal element, or we will find some other maximal element. In particular, take any $A \in L$ . We are done if $A$ is a maximal element; otherwise, pick $A^{'} ≻ A$ . By the construction of $F$ , for every $n \in N$ , we can pick some $C_{n} ⪰ A^{'}$ within a distance of $\frac{1}{n}$ from B. Now, if we show that $B$ itself satisfies $B ⪰ A$ , it will follow that $B$ is maximal.
The idea is to pass from our sequence ${(C_{n})}_{n \in N}$ , with limit $B$ , to another sequence lying on a line segment with endpoint $B$ . We can use axiom A4, which is a kind of convexity, to control the preference relation on convex combinations of our points $C_{n}$ , so these are the points that we will construct along a line segment. Once we have this line segment, we can finish by using A3, which is a kind of continuity restricted to line segments, to control $B$ itself.
Let $S \subseteq L$ be the set of lotteries in the affine span of the set ${C_{n}}_{n \in N}$ . Then, if we take some index set $I \subseteq N$ such that ${(C_{n})}_{n \in I}$ is a maximal affinely independent tuple, it follows that ${C_{n}}_{n \in I}$ affinely generates $S$ . Hence, the convex combination
$D = \sum n \in I \frac{1}{| I |} C_{n},$
i.e. the barycenter of the simplex with vertices at ${(C_{n})}_{n \in I}$ , is in the interior of the convex hull of ${C_{n}}_{n \in I}$ relative to $S$ , so we can pick some $r > 0$ such that the $r$ -ball around $D$ relative to $S$ is contained in this simplex.
Now, we will see that every lottery $E$ in the set $(B, D]$ satisfies $E ⪰ A^{'}$ . For any $ε > 0$ , pick $k$ so that $C_{k}$ is in the $ε$ -ball around $B$ . Since the tangent vector $v = B - C_{k}$ has length less than $ε$ , the lottery
$F = D + \frac{r}{ε} (B - C_{k})$
is in the $r$ -ball around $D$ , and it is in $S$ , so it is in the simplex with vertices ${(C_{n})}_{n \in I}$ . Then, $F ⪰ A^{'}$ by A4, and $C_{k} ⪰ A^{'}$ by hypothesis. So, applying A4 again,
$A^{'} ⪯ \frac{r}{r + ε} C_{k} + \frac{ε}{r + ε} F = \frac{r}{r + ε} B + \frac{ε}{r + ε} D .$
Using A4 one more time, it follows that every lottery
$E \in [\frac{r}{r + ε} B + \frac{ε}{r + ε} D, D]$
satisfies $E ⪰ A^{'}$ , and hence every lottery $E \in (B, D]$ .
Now we can finish up. If $B ≺ A$ then, using A3 and the fact that $D ⪰ A^{'} ≻ A$ , there would have to be some lottery in $[B, D]$ that is $⪯$ -equivalent to A, but this would contradict what we just concluded. So, $B ⪰ A$ , and so B is $⪯$ -maximal. $□$
Proof of Theorem 2. Let $C$ be a $⪯$ -minimal and $D$ a $⪯$ -maximal element of $L$ . First, we will see that preferences are increasing on $[C, D]$ , and then we will use this fact to construct a function $L \to R$ and show that it has the desired properties. Suppose preferences we not increasing; then, there would be $A, B \in [C, D]$ such that $A$ is closer to $C$ while $B$ is closer to $D$ , and $A ≻ B$ . Then, $B$ would be a convex combination of $A$ and $D$ , but $B ≺ A ⪯ D$ by the maximality of $D$ , contradicting A4.
Now we can construct our utility function $u : L \to R$ using A3; for each $\sim$ -class $[A]$ , we have $C ⪯ A ⪯ D$ , so there is some^[1] $p \in [0, 1]$ such that
$(1 - p) C + p D \sim A .$
Then, let $u (A^{'}) = p$ for all $A^{'} \in [A]$ . Since preferences are increasing on $[C, D]$ , it is immediate that if $u (A) \leq u (B)$ , then $A ⪯ B$ . Conversely, if $A ⪯ B$ , we have two cases. If $A ≺ B$ , then $B ⋠ A$ , so $u (B) ≰ u (A)$ , and so $u (A) \leq u (B)$ . Finally, if $A \sim B$ , then $u (A) = u (B)$ by construction.
Finally, since for all $A, B \in L$ we have $u (A) \leq u (B)$ iff $A ⪯ B$ , it follows immediately that $u$ is quasiconcave by A4. $□$
1. ^
  Nate mentions using choice in his answer, but here at least the use of choice is removable. Since $⪯$ is monotone on $[C, D]$ , the intersection of the $\sim$ -class $[A]$ with $[C, D]$ is a subinterval of $[C, D]$ , so we can pick $p$ based on the midpoint of that interval

SamEisenstat 12 Feb 2023 21:55 UTC
LW: 9 AF: 7
0
AF
in reply to: James Payor’s comment on: Modal Fixpoint Cooperation without Löb’s Theorem
Nice, I like this proof also. Maybe there’s a clearer way to say thing, but your “unrolling one step” corresponds to my going from $u$ to $v$ . We somehow need to “look two possible worlds deep”.

SamEisenstat 10 Feb 2023 20:29 UTC
LW: 25 AF: 16
10
AF
on: Modal Fixpoint Cooperation without Löb’s Theorem
Here’s a simple Kripke frame proof of Payor’s lemma.
Let $⟨ W, R, ⊩ ⟩$ be a Kripke frame over our language, i.e. $W$ is a set of possible worlds, $R$ is an accessibility relation, and $⊩$ judges that a sentence holds in a world. Now, suppose for contradiction that $W ⊩ x \leftrightarrow □ (□ x \to x)$ but that $W ⊮ x$ , i.e. $x$ does not hold in some world $u \in W$ .
A bit of De Morganing tells us that the hypothesis on $x$ is equivalent to $\neg x \leftrightarrow ◊ (□ x \land \neg x)$ , so $u ⊩ ◊ (□ x \land \neg x)$ . So, there is some world $v$ with $u R v$ such that $v ⊩ □ x \land \neg x$ . But again looking at our equivalent form for $\neg x$ , we see that $W ⊩ \neg x \to ◊ \neg x$ , so $v ⊩ □ x \land ◊ \neg x$ , a contradiction. $□$
Both this proof and the proof in the post are very simple, but at least for me I feel like this proof tells me a bit more about what’s going on, or at least tells me something about what’s going on that the other doesn’t. Though in a broader sense there’s a lot I don’t know about what’s going on in modal fixed points.
Kripke frame-style semantics are helpful for thinking about lots of modal logic things. In particular, there are cool inductiony interpretations of the Gödel/Löb theorems. These are more complicated, but I’d be happy to talk about them sometime.

SamEisenstat 22 Jul 2020 2:06 UTC
LW: 10 AF: 5
0
AF
on: Alignment proposals and complexity classes
Theorem. Weak HCH (and similar proposals) contain EXP.
Proof sketch: I give a strategy that H can follow to determine whether some machine that runs in $O (2^{c n^{k}})$ time accepts. Basically, we need to answer questions of the form “Does cell $x$ have value $y$ at time $t$ .” and “Was the head in position $x$ at time $t$ ?”, where $x$ and $t$ are bounded by some function in $O (2^{c n^{k}})$ . Using place-system representations of $x$ and $t$ , these questions have length in $O (n^{k})$ , so they can be asked. Further, each question is a simple function of a constant number of other such questions about earlier times as long as $t > 0$ , and can be answered directly in the base case $t = 0$ .

SamEisenstat 21 Apr 2020 7:03 UTC
7 points
0
in reply to: jpulgarin’s comment on: The Cartoon Guide to Löb’s Theorem
*I* think that there’s a flaw in the argument.
I could elaborate, but maybe you want to think about this more, so for now I’ll just address your remark about $\neg □ C \to C$ , where $C$ is refutable. If we assume that $\neg □ C \to C$ , then, since $C$ is false, $\neg □ C$ must be false, so $□ C$ must be true. That is, you have proven that PA proves $□ C$ , that is, since $C$ is contradictory, PA proves its own inconsistency. You’re right that this is compatible with PA being consistent—PA may be consistent but prove its own inconsistency—but this should still be worrying.

SamEisenstat 25 Mar 2020 6:01 UTC
7 points
0
on: Adding Up To Normality
This reminds me of the Discourse on Method.
[T]here is seldom so much perfection in works composed of many separate parts, upon which different hands had been employed, as in those completed by a single master. Thus it is observable that the buildings which a single architect has planned and executed, are generally more elegant and commodious than those which several have attempted to improve, by making old walls serve for purposes for which they were not originally built. Thus also, those ancient cities which, from being at first only villages, have become, in course of time, large towns, are usually but ill laid out compared with the regularity constructed towns which a professional architect has freely planned on an open plain; so that although the several buildings of the former may often equal or surpass in beauty those of the latter, yet when one observes their indiscriminate juxtaposition, there a large one and here a small, and the consequent crookedness and irregularity of the streets, one is disposed to allege that chance rather than any human will guided by reason must have led to such an arrangement. And if we consider that nevertheless there have been at all times certain officers whose duty it was to see that private buildings contributed to public ornament, the difficulty of reaching high perfection with but the materials of others to operate on, will be readily acknowledged. In the same way I fancied that those nations which, starting from a semi-barbarous state and advancing to civilization by slow degrees, have had their laws successively determined, and, as it were, forced upon them simply by experience of the hurtfulness of particular crimes and disputes, would by this process come to be possessed of less perfect institutions than those which, from the commencement of their association as communities, have followed the appointments of some wise legislator. It is thus quite certain that the constitution of the true religion, the ordinances of which are derived from God, must be incomparably superior to that of every other. And, to speak of human affairs, I believe that the pre-eminence of Sparta was due not to the goodness of each of its laws in particular, for many of these were very strange, and even opposed to good morals, but to the circumstance that, originated by a single individual, they all tended to a single end. In the same way I thought that the sciences contained in books (such of them at least as are made up of probable reasonings, without demonstrations), composed as they are of the opinions of many different individuals massed together, are farther removed from truth than the simple inferences which a man of good sense using his natural and unprejudiced judgment draws respecting the matters of his experience. And because we have all to pass through a state of infancy to manhood, and have been of necessity, for a length of time, governed by our desires and preceptors (whose dictates were frequently conflicting, while neither perhaps always counseled us for the best), I farther concluded that it is almost impossible that our judgments can be so correct or solid as they would have been, had our reason been mature from the moment of our birth, and had we always been guided by it alone.
It is true, however, that it is not customary to pull down all the houses of a town with the single design of rebuilding them differently, and thereby rendering the streets more handsome; but it often happens that a private individual takes down his own with the view of erecting it anew, and that people are even sometimes constrained to this when their houses are in danger of falling from age, or when the foundations are insecure. With this before me by way of example, I was persuaded that it would indeed be preposterous for a private individual to think of reforming a state by fundamentally changing it throughout, and overturning it in order to set it up amended; and the same I thought was true of any similar project for reforming the body of the sciences, or the order of teaching them established in the schools: but as for the opinions which up to that time I had embraced, I thought that I could not do better than resolve at once to sweep them wholly away, that I might afterwards be in a position to admit either others more correct, or even perhaps the same when they had undergone the scrutiny of reason. I firmly believed that in this way I should much better succeed in the conduct of my life, than if I built only upon old foundations, and leaned upon principles which, in my youth, I had taken upon trust. For although I recognized various difficulties in this undertaking, these were not, however, without remedy, nor once to be compared with such as attend the slightest reformation in public affairs. Large bodies, if once overthrown, are with great difficulty set up again, or even kept erect when once seriously shaken, and the fall of such is always disastrous. Then if there are any imperfections in the constitutions of states (and that many such exist the diversity of constitutions is alone sufficient to assure us), custom has without doubt materially smoothed their inconveniences, and has even managed to steer altogether clear of, or insensibly corrected a number which sagacity could not have provided against with equal effect; and, in fine, the defects are almost always more tolerable than the change necessary for their removal; in the same manner that highways which wind among mountains, by being much frequented, become gradually so smooth and commodious, that it is much better to follow them than to seek a straighter path by climbing over the tops of rocks and descending to the bottoms of precipices.
...
And finally, as it is not enough, before commencing to rebuild the house in which we live, that it be pulled down, and materials and builders provided, or that we engage in the work ourselves, according to a plan which we have beforehand carefully drawn out, but as it is likewise necessary that we be furnished with some other house in which we may live commodiously during the operations, so that I might not remain irresolute in my actions, while my reason compelled me to suspend my judgement, and that I might not be prevented from living thenceforward in the greatest possible felicity, I formed a provisory code of morals, composed of three or four maxims, with which I am desirous to make you acquainted.
The first was to obey the laws and customs of my country, adhering firmly to the faith in which, by the grace of God, I had been educated from my childhood and regulating my conduct in every other matter according to the most moderate opinions, and the farthest removed from extremes, which should happen to be adopted in practice with general consent of the most judicious of those among whom I might be living. For as I had from that time begun to hold my own opinions for nought because I wished to subject them all to examination, I was convinced that I could not do better than follow in the meantime the opinions of the most judicious; and although there are some perhaps among the Persians and Chinese as judicious as among ourselves, expediency seemed to dictate that I should regulate my practice conformably to the opinions of those with whom I should have to live; and it appeared to me that, in order to ascertain the real opinions of such, I ought rather to take cognizance of what they practised than of what they said, not only because, in the corruption of our manners, there are few disposed to speak exactly as they believe, but also because very many are not aware of what it is that they really believe; for, as the act of mind by which a thing is believed is different from that by which we know that we believe it, the one act is often found without the other. Also, amid many opinions held in equal repute, I chose always the most moderate, as much for the reason that these are always the most convenient for practice, and probably the best (for all excess is generally vicious), as that, in the event of my falling into error, I might be at less distance from the truth than if, having chosen one of the extremes, it should turn out to be the other which I ought to have adopted. And I placed in the class of extremes especially all promises by which somewhat of our freedom is abridged; not that I disapproved of the laws which, to provide against the instability of men of feeble resolution, when what is sought to be accomplished is some good, permit engagements by vows and contracts binding the parties to persevere in it, or even, for the security of commerce, sanction similar engagements where the purpose sought to be realized is indifferent: but because I did not find anything on earth which was wholly superior to change, and because, for myself in particular, I hoped gradually to perfect my judgments, and not to suffer them to deteriorate, I would have deemed it a grave sin against good sense, if, for the reason that I approved of something at a particular time, I therefore bound myself to hold it for good at a subsequent time, when perhaps it had ceased to be so, or I had ceased to esteem it such.
My second maxim was to be as firm and resolute in my actions as I was able, and not to adhere less steadfastly to the most doubtful opinions, when once adopted, than if they had been highly certain; imitating in this the example of travelers who, when they have lost their way in a forest, ought not to wander from side to side, far less remain in one place, but proceed constantly towards the same side in as straight a line as possible, without changing their direction for slight reasons, although perhaps it might be chance alone which at first determined the selection; for in this way, if they do not exactly reach the point they desire, they will come at least in the end to some place that will probably be preferable to the middle of a forest. In the same way, since in action it frequently happens that no delay is permissible, it is very certain that, when it is not in our power to determine what is true, we ought to act according to what is most probable; and even although we should not remark a greater probability in one opinion than in another, we ought notwithstanding to choose one or the other, and afterwards consider it, in so far as it relates to practice, as no longer dubious, but manifestly true and certain, since the reason by which our choice has been determined is itself possessed of these qualities. This principle was sufficient thenceforward to rid me of all those repentings and pangs of remorse that usually disturb the consciences of such feeble and uncertain minds as, destitute of any clear and determinate principle of choice, allow themselves one day to adopt a course of action as the best, which they abandon the next, as the opposite.
(This is probably 5% of the text. There is more interesting stuff there, but it’s less relevant to this post.)

SamEisenstat 12 Jun 2018 8:47 UTC
LW: 1 AF: 1
0
AF
on: A Loophole for Self-Applicative Soundness
As you say, this isn’t a proof, but it wouldn’t be too surprising if this were consistent. There is some $k \in N$ such that $□_{n} ϕ \to ϕ$ has a proof of length $n^{k}$ by a result of Pavel Pudlák (On the length of proofs of finitistic consistency statements in first order theories). Here I’m making the dependence on $n$ explicit, but not the dependence on $ϕ$ . I haven’t looked at it closely, but the proof strategy in Theorems 5.4 and 5.5 suggests that $k$ will not depend on $ϕ$ , as long as we only ask for the weaker property that $□_{n} ϕ \to ϕ$ will only be provable in length $n^{k}$ for sentences $ϕ$ of length at most $k$ .

SamEisenstat 5 Jun 2018 20:46 UTC
0 points
0
AF
in reply to: Diffractor’s comment on: A Loophole for Self-Applicative Soundness
I misunderstood your proposal, but you don’t need to do this work to get what you want. You can just take each sentence $□_{n} ϕ \to ϕ$ as an axiom, but declare that this axiom takes $n$ symbols to invoke. This could be done by changing the notion of length of a proof, or by taking axioms $ψ_{ϕ, n} \to (□_{n} ϕ \to ϕ)$ and $ψ_{ϕ, n}$ with $ψ_{ϕ, n}$ very long.