What's wrong with a 20% tax? We who make a living from labor instead of capital pay more than that.
Paul tries to frame it as an increase of 20% in the tax rate, but in reality the increase is from 0% to 20%, and it's hard to see why that's unfair.
The reason I say it's currently 0% is of course that for the wealthy most of these 5% gains are unrealized (e.g. inflation in the value of their assets) and untaxed.
> most of these 5% gains are unrealized (e.g. inflation in the value of their assets) and untaxed.
The worst part is that even when they need to realize their profits, they have schemes that allow them to avoid taxes (guess how much taxes Musk paid for his $20B realized profits from his Tesla shares he sold to buy Twitter).
But strangely politicians generally aren't pushing for targeted corrections to reduce those loopholes-- e.g. impugning realizing gains when you take a loan on assets beyond certain thresholds just as currently happens when you create a constructive sale with options trades. When assets are encumbered by loans or as collateral one could force the tax realization of gains at some rate which then adjusts the cost basis. The distortionary effect of this policy would be greatly diminished by the fact that everyone could just choose to not use their assets in this way.
Instead, the are running straight for the full on land grab while distracting people with the details of technical loopholes of comparatively small consequence.
> But strangely politicians generally aren't pushing for targeted corrections to reduce those loopholes
You are just not paying attention enough. They do talk about loopholes, and push to close them during the legislative process.
They just don't talk about the loopholes details a lot because you don't get elected by talking about technical details in the tax code: “Force the tax realization of gains at some rate which then adjusts the cost basis when assets are encumbered by loans or as collateral” isn't a slogan that makes you win an election.
Your current understanding also seems a bit warped. The US government provides the source of a lot of research funding but historically exerts little "control". Generally grant applications are evaluated by panels of researchers who don't work for the federal government.
Also, this government funding supports fundamental innovations that private companies wouldn't fund because it's too general and too far from monetizable. But after those breakthroughs happen funded by public research, private industry benefits enormously. This includes most health and medical advances and the science underlying most technological advances. So government funding doesn't conflict with the work being necessary or important, on the contrary, it is possibly more important long-term.
Disclaimer? The government funds some of my research.
* There are axioms, there are models, and there are theorems.
* A model is a particular structure with objects and relationships. The "standard model of arithmetic" is just the natural numbers 0, 1, 2, ... with normal rules of addition and subtraction and so on. A different model could be the real numbers, or one that includes infinitesimally small numbers, or so on.
* A set of axioms are rules about how a model can work. For example, we can have an axiom for any set of objects called "numbers" with an operation called "addition" that the operation must be commutative (x+y = y+x). The standard model above is one model that satisfies this axiom.
* A theorem is a fact that can be true or false about a given model. For example, "the model has infinitely many objects." If we can prove a theorem from a set of axioms, then that theorem is true for every model that satisfies the axioms. However, there can also be theorems that are true for one model that satisfies the axioms but false for a different model.
Godel's completeness theorem says that if a theorem is true for every model that satisfies a set of axioms, then one can prove that theorem from the axioms.
Godel's first incompleteness theorem says that in any axiomatic system (sufficiently complex) there are theorems that are neither always true nor always false. In other words, there is a theorem that is true for some model of the axioms but false for some other model of the axioms.
Godel's completeness theorem can not be understood without bringing in first order logic, because it is a statement of the expressitivity of the language(relative to its semantics). Other more expressive languages, like second order logic (with its usual semantics) is not complete. Trying to explain Godel's completeness theorem without bringing in the language is a path to confusion.
And your explanation of the first incompleteness theorem is also at best confusing. I must preface this with the comment that your definition of a 'theorem' matches what is usually called a sentence or a statement, and a theorem is usually reserved for a sentence which is proven by a axiomatic system. If the axiomatic system is sound, all theorems will be true in all models. The question of completeness is whether or not all truths(aka sentences true in all models) can be proven(aka they are theorems). With this more common usage of the words, Gödel's incompleteness theorems show that every consistent theory containing the natural numbers has true statements on natural numbers that are not theorems of the theory (that is they cannot be proved inside the theory).
Your description of the first incompleteness theorem is also true for complete logics, even for propositional logic (with your definition of 'theorem' as actually meaning statement). It has statements which is true in some models and false in others. This does not make it incomplete.
Actually, I think your statement muddies the waters a bit and the parent gives a clearer picture for those looking for a simple statement of what's going on. The background is the fellow comment: https://news.ycombinator.com/item?id=48224739. Godel's simplest (and roughly original) statement is any system of axioms strong enough to encode arithmetic is either consistent or complete. You can "Or the set of axioms is not enumerable" (as in Second Order Logic and other systems). But when one says that, one has jumped from what would be normally recognized as logic (finite axioms and process) to a mathematical construct with some similarities to naive logic but which "my gran pappy" would not see as logic.
I mean, you can formally construct an axiom system defined to include (via axiom of choice) and assign a truth value to each of the independent propositions of first order arithmetic logic. There, you have consistent and complete system but not one that's a whit closer to being in usable by anyone.
I'm not even a finitist but I think being clear what's going on with these claims is important. It's like saying "the halting problem can't be solved by finite computers but my infinite-foo hypothetical computer can solve it, gotten mention that..."
That is interesting, I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so. But if it that is not the case and there always exist models where the theorem is true and false, that makes it sound to me, like the incompleteness theorem is not really about proving things. With that it sounds more like the inability of a sufficiently complex set of axioms to only admit isomorphic models, i.e. have all possible models agree on all expressible theorems. Makes the entire thing sound almost trivial, of course you can not prove what does not follow from the axioms.
> I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so.
As the GP points out, that's not what Godel's incompleteness theorem actually shows. Although it's a common misconception (one which unfortunately is propagated by many sources that should know better).
The key point of the incompleteness theorem is that it shows that (at least in first order logic, which is the logic in which the theorem holds) no set of axioms can ever pin down a single model. For example, no set of first-order axioms can ever pin down "the standard natural numbers" as the only model satisfying the axioms. There will always be other models that also satisfy them. So if you want to pin down a single model, you always have to go beyond just a set of first-order axioms.
Using the natural numbers as an example, consider a model that consists of two "chains" of numbers:
(0, 1, 2, 3, ....)
(..., -3a, -2a, -1a, 0a, 1a, 2a, 3a, ...)
The first chain is, of course, the standard natural numbers, but the second chain also satisfies the standard first-order axioms that we normally take to define natural numbers. So this model, as a whole, satisfies those axioms. And there is no way, within first-order logic, to say "I only want my model to include the first chain". That's what Godel's incompleteness theorem (or more precisely, his first incompleteness theorem combined with his completeness theorem) tells us.
I think you’re right that "true in all models but unprovable" is not accurate. By Godel’s completeness theorem if a FO sentence is true in every model of the axioms then it is provable from those axioms.
But I don’t think incompleteness is best described as saying "no first-order axioms can pin down a single model" That’s more about non-categoricity/compactness/Lowenheim–Skolem.
> I don’t think incompleteness is best described as saying "no first-order axioms can pin down a single model"
Well, it's an obvious implication of the two theorems (completeness and incompleteness) combined: if a FO sentence is not provable from a system of FO axioms, it can't be true in all models of those axioms. And if an FO sentence is not provable, its negation can't be either (since proving its negation true would prove the sentence itself false). So the negation also can't be true in all models. That means there must be at least one model in which the FO sentence is false, and at least one in which its negation is false (so the sentence itself is true). Which means there must be at least two models of that set of FO axioms--i.e., the axioms can't pin down a single model. And the incompleteness theorem proves that there is such a sentence in every system of FO axioms.
I agree that the Lowenheim-Skolem theorem has similar consequences, since it says there must be models with different infinite cardinalities.
> That’s more about non-categoricity/compactness/Lowenheim–Skolem.
As I understand it, the proof of the Lowenheim-Skolem theorem requires the axiom of choice, but the proof of the two Godel theorems does not. That would make a difference for people who are doubtful about the axiom of choice.
> The key point of the incompleteness theorem is that it shows that (at least in first order logic, which is the logic in which the theorem holds) no set of axioms can ever pin down a single model.
No, this was known before the incompleteness theorem, ref Löwenheim–Skolem theorem.
The Lowenheim Skolem theorem only applies to first-order axiom systems that have an infinite model. So it would apply to the axioms for the natural numbers, yes.
The Godel theorems apply to any first-order axiom system, regardless of whether it has an infinite model or not.
I don't understand what you mean by this. Gödels two incompleteness theorems are about theories of natural numbers, so their models are infinite. I don't understand what you could mean by them applying to finite models.
I stand by my claim. The key point of Gödels incompleteness is NOT that no single theory can pin down a single model, that was known before.
He's right, the Godel theorems have nothing to do with existence of models satisfying this-or-that. Such would be "semantic" truths. The reason Hilbert's program survived Löwenheim–Skolem is that Hilbert was a formalist concerned with "syntactic" truth, that is, whether there are statements P such that neither P nor not-P could be proven by the axiom system.
You might think LS would trivially demonstrate as much---"Just take P = our underlying model is countable!"---but this is not formalizable within the system itself.
My understanding is that for any system of axioms strong enough to encode arithmetic, you can have at most two of these three properties:
1. Complete (for any well formed statement, the axioms can be used to prove either it or its negation)
2. Consistent (can't arrive at contradictory statements ~ arriving at a both a statement and its negation )
3. The set of axioms is enumerable ~ you can write a program that lists them in a defined order (since the workaround for completeness can be just adding an axiom for the cases that are unproven in your original set)
If my understanding is correct, I believe your explanation is missing the third required property.
It's also important to point out that if we cant prove a statement or its negation (one of which must be true) then we know there are true statements that are unprovable. This is a much stronger of a finding than "Godel's first incompleteness theorem says that in any axiomatic system (sufficiently complex) there are theorems that are neither always true nor always false. "
I just want to be a bit pedantic here (but this is logic after all...), and point out that in point 1 above you are talking about syntactical completeness, and not semantical completeness, which is the kind of completes Gödel proves in his first completeness proof. I think people are often confused because of this overloading of the word. And it is about sentences(a formula withouth free variables), not any well formed formula.
The common denominator: the data needs to be owned by you, or at least made accessible. Companies love to create walled gardens where they own the content and control how you access it, making this kind of personalized interface impossible. Hopefully we can push back more now.
The ability to quickly make an API connection + custom UX means that companies with a sub par website / app but a good data API are more valuable to me than the world class fancy website with a locked down API.
At work I have a great brain dump + TODO list tracker via custom API + MCP into confluence, using confluence pages as the app state. The website is so bloated it takes like 20 seconds to go from "idea" to getting it written down. Im now able to avoid all of that and make ~ MY ~ perfect UX while still being a good corporate employee.
I mean, hold up, if that thought lights you up I'm happy, but I don't actually think that's the common denominator. I used Things.app to track projects for a long time and ultimately fell out of love with it. Things.app didn't own my data; it's a pure UI app.
But now it occurs to me: I know precisely how I work, I know what patterns are valuable to me, I know when and how I need to remind myself of things. I don't know why I haven't already started building my Things.app replacement. But I'd guess I have it to a place where I'm happy by this time Saturday.
Honestly, it's harder for me to think of daily-driver apps where this wouldn't be the case. I guess vector graphics editing? I'm not going to vibe up a vector editor. But I'll bet all the money in my pocket that 5 years from now, the real value in vector graphics tools will be their API/SDK, not the packaged application experience.
I'm not following your reasoning about the common denominator, not sure we're on the same wavelength about what I meant. I'm claiming that in order for an application to be "reclaimable", you have to be able to access and manipulate the data under the app. Some applications currently work that way now, lots of them don't.
For example, we can "reclaim" non-DRM ebook readers, audiobooks, and music players that play local files or use an open API. But a company-specific walled garden streaming DRM'd ecosystem will be almost impossible to build around.
You're talking about entire systems. That's something to be optimistic about too. But it's actually not the thing the comment you responded to was about. I'm not saying I'm excited to get out of the Apple Music ecosystem (I like Apple Music, the service, quite a lot). I'm excited to get out of Music.app, and into my own custom Apple Music player; one where playlists and play history are simple, sanely-schemaed sqlite databases.
I gotta be careful, I'm going to talk myself into staying up late tonight building that.
Ownership can have different forms. Slack.app that doesn't let me easily extract code snippets from a thread - owns me. Jira that forces me to use their imbecilic, quirky wysiwyg owns me. Note taking app that keeps the data in their db and not my files - ain't my friend. The friction is the ownership. When extraction requires effort, the tool has leverage over you. It's a subtler form than data lock-in - behavioral lock-in. You adapt your workflow to what the tool makes easy, and gradually the tool's affordances shape what you even think to do. information gets buried in threads, search is mediocre, export is hostile. The "solution" they offer is to stay in Slack/Jira/Dropbox/Evernote/Notion/etc. longer, search in Slack, link to Slack, screenshare in Slack, summarize with AI in Slack, don't ever leave Slack. The tool becomes the answer to the problems the tool creates.
Plain text, local files, standard formats - they don't fight you on extraction because there's nothing to protect. That's why investing in FOSS tools is almost always paying for your own liberation rather than your own imprisonment. Even when there isn't feature parity, even when the FOSS tool doesn't have a "polished UI" and it's "maintained by a teenager in Nebraska" - still a better choice.
Nice article. One small comment, it's very hard to conclude anything about accuracy over time because the comparisons may not be apples to apples. For example if there used to be lots of questions about if it will rain in Boston and now there are lots of questions about if it will rain in Phoenix, it will look like predictions are getting more accurate, but the questions are just getting easier.
Author here. Agree, and I wrote in that section "Absolute accuracy is hard to compare across markets on one platform, and across platforms, because different forecasting questions have different difficulties. I addressed this by tracking similar markets on a single platform over time."
Even doing this, it's not apples-to-apples. One thing is, in this article, I filter only to "interesting" markets, so that controls for the % that are "easy" as you describe.
Cool stuff. I think there have been projects recently that use LLMs to encode messages in plain text by manipulating the choices of output tokens. Someone with the same version of the LLM can decode. Note sure where to find these projects though.
I created something similar a long long time ago, but much simpler, using markov chains. Basically just encoding data via the choice of the next word tuple given the current word tuple. It generated gibberish mostly, but was fun 25 years ago
This is a really interesting space, and one that I've been playing with since the first GPTs landed. But it's even cooler than simply using completion choice to encode data. It has been mathematically proven that you can use LLMs to do stego that cannot be detected[0]. I'm more than positive that comments on social media are being used to build stego dead drops.
What I find really interesting about this approach is that it's one of the less obvious ways LLMs might be used by the general public to defend themselves against the LLM capabilities used by bad actors (like the more obvious LLMs making finding bugs easier is good for blackhats, but maybe better for whitehats), i.e semantic search.
The reasoning in my head being that it creates a statistical firewall that would preclude eaves-droppers with privileged access from being able to use cheap statistical methods to detect a hidden message (which is effectively what crypto _is_, ipso facto this is effectively undetectable crypto).
ETA, the abstract for a paper I've been working on related to this:
Mass surveillance systems have systematically eroded the practical security of private communication by eliminating channel entropy through universal collection and collapsing linguistic entropy through semantic indexing. We propose a protocol that reclaims these lost "bits of security" by using steganographic text generation as a transport layer for encrypted communication. Building on provably secure generative linguistic steganography (ADG), we introduce conversation context as implicit key material, per-message state ratcheting, and automated heartbeat exchanges to create a system where the security properties strengthen over time and legitimate users enjoy constant-cost communication while adversaries face costs that scale with the entire volume of global public text. We further describe how state-derived proofs can establish a novel form of Web of Trust where relationship depth is cryptographically verifiable. The result is a communication architecture that is structurally resistant to mass surveillance rather than merely computationally resistant.
If Claude code is written by Claude code, and AI outputs are not currently considered copyrightable, then how is Anthropic asserting copyright over the leak?
reply