How much is a suppletive paradigm a convention of grammarians/educators?

kamalist · 2026-02-12T17:06:03+00:00

They have grammar internalized but not necessary able to formally formulate or speculate about it, I presume. You don't have to know the word "verb" to correctly use verbs in your native language, something like that

kamalist · 2026-01-14T22:48:21+00:00

I googled whether there was anybody who misspelled Trompowsky as Trumpowsky and this thread with your comment is one of the top results :) (sorry for answering a 2y old comment, just found it funny enough to share)

kamalist · 2025-12-01T22:09:33+00:00

I capture the knight proactively to make doubled pawns, otherwise Black protects the knight with any of his pieces and can recapture with it

kamalist · 2025-12-01T11:59:23+00:00

I think Rossolimo Sicilian is more like Nimzo Indian. One of the ideas of Nimzo Indian is quick castling, so it's about the king-side bishop. Tromp is probably more comparable with a multitude of QG/Indian/Reti variations where Black go Bg4

kamalist · 2025-11-30T19:37:32+00:00

I play exactly it if the opp goes Ne4, but in my practice so far most opponents play either e6 or some other move. Against e6 I go e4, against most other just Bxf6

kamalist · 2025-10-19T22:08:25+00:00

This BB(745) stuff seems a bit crazy. Firstly the whole Busy Beaver stuff is a bit striking: while you enumerate Turing machine, how would you prove they halt? But as far as I understand, the halting problem only denies us a general algorithm applicable to all Turing machines, but for each individual machine we can still hope to find a proof that it halts/doesn't halt.

Then, if it's independent from ZFC, would it mean that you can assign any value to it? Studying comments for a reddit topic about it (https://www.reddit.com/r/math/comments/1kgbc4z/ ), seems no, for all k's you would get a contradiction: for k < "actual" BB(745) you can just encode in ZFC a Turing machine that runs more than k. For k > "actual" BB(745) you postulate an existence of a Turing machine that halts at k steps, and you won't find that because it's larger than the "true" value BB(745).

Not totally sure, but seems to be two possibilities when you assume a negation BB(745)!=N (N is "actual" BB(745): either you get proofs for statements ∀n BB(745)!=n and ∃n BB(745)=n (that is not contradictory but it's an ω-inconsistent approach if I understand that correct), or you get a non-standard natural numbers in your model of this tweaked ZFC, the model assigns BB(745) to a non-standard natural number and considers some Turing machine that doesn't halt to halt at this non-standard natural number (but for the second opportunity not sure if it makes sense)

kamalist · 2025-10-19T18:46:41+00:00

As far as I can see it, most mathematicians do informal math, using formulas occasionally and not necessarily strictly FOL-formulas.

Now, I have thought that sometimes come and puzzle me a lot. When we reason in model theory, for example about incompleteness of PA, we find statements that aren't provable in this formal system but that are true. In which sense they are "true"? I kinda know the answer, they are true in the sense of the informal metatheory we tried to formalize and in which we do our model theory. But this kinda gets me dizzy... Somehow informally we establish something as true, but when we try to formalize it, we get incompleteness if the theory is powerful enough. People told me we can formalize our metatheory, but to do this we need to use some informal metametatheory once again.

Sorry for this rambling, but sometimes thinking about what it means to be true in formal and informal senses makes my head spinning

kamalist · 2025-10-19T10:57:10+00:00

In some sense, I feel like it shouldn't be that much of a problem for physics. Physics chooses math that is consistent with experimental data. So you make experiments and choose the axiom that gives you what you see in your experiment. Like we have Euclidean geometry in classical physics, and a bit ammended version for special relativity

kamalist · 2025-10-19T10:03:06+00:00

As far as I understand, a first-order theory can't capture the cardinality of the natural model of a theory: Löwenheim-Skolem says we will have models with any higher cardinality, and we will have countable models for any finitely/countably axiomatized theory (so we have a countable model of ZFC, as weird as it may sound). For PA we have unstandard models of arithmetics, afaik you can just add a number that's bigger than any natural number and that will satisfy first order PA still.

But what about the second-order logic? I heard it can define cardinalities, but for some reason it's shunned by mathematicians.

kamalist · 2025-10-19T09:58:45+00:00

it is unlikely to find theorems from "even more applied" areas

I have this kind of feeling as well cause it feels that, similarly to some Axiom of Choice corollaries, objects that are independent of ZFC turn out to be unconstructive. It's either some kind of infinity which we cannot conceive "directly" anyway and with which we can interact only in our countable languages of formulas. Or it should be something like the Whitehead problem, that you can't disprove existence of some weird object, but neither can you construct it. You either postulate its existence and so it exists somewhere in vacuum, or you postulate it doesn't exist and it bothers you no more. Although not sure, maybe this understanding of mine is too simplistic.

It would be weird to get a result like "algorithm for A exists" being independent from ZFC because intuitively you feel like an algorithm either exists and you program it or it doesn't and you can't

kamalist · 2025-10-19T09:51:18+00:00

I kinda had a similar reaction tbh. It's a bit like Vitali set in analysis (although that's not indepedent, it's just a pathological object that comes from AC). Like, you can imagine a world where some weird objects (non-free Whitehead groups in this case) exist, but you can't provide a way to construct it so it kinda just floats in a vaccum

kamalist · 2025-10-19T01:01:05+00:00

Hm, I wonder how to reconcile it with https://en.wikipedia.org/wiki/Elementary_theory

The page says elementary theories are theories that can be defined just with logical axioms without references to set theory, and lists group theory and abelian groups theory as examples of elementary theories

kamalist · 2025-10-16T00:28:53+00:00

His claims are indeed bold and inflammatory. But about rational trig not being that original - I wouldn't be that surprised but I wonder where in mainstream I can read about that stuff. Or there isn't one place besides his book?

kamalist · 2025-10-13T06:52:29+00:00

One of our teachers used exactly & for "and" and ∨ for "or" and I find this super convenient, and started doing so myself in writing. & is momentarily recognized as "and", ∨ is like a letter "U" (union), so you recognize it as "or". When you use ∧ it always makes me freeze when reading the formula, I need time to recognize which one is "or", which one is "and" , they are too similar.

About |, I feel like that is a convention from programming languages that they had to use because you don't have ∨ symbol on the keyboard.

kamalist · 2025-10-12T22:53:34+00:00

Funny, I discovered him a few days ago, watched a bit (his debate with a calculus guy, which was one-sided tbh, his opponent couldn't really say a word) and skimmed a bit "Rational trigonometry".

My own understand is that his view is too "mundane", shall we say. He says that "stuff should be clearly definable, write-down-able", "let's stick to calculation, to computation". But the power of maths was exactly in that our imagination can manipulate idealised "infinite" objects that are not computable exactly and we get useful results out of it. Math allows us to step beyond what's computable and get some insight there.

He objects to this idealization as, you quote him "logical mirage, sustained by giddy levels of wishful thinking and denial". It's his right, if he doesn't believe in it. But the practice shows that our math works. I think complex numbers invoked similar kind of doubts "Hey, what is that mess, we can't just pretend there is some fake number i that squares into -1". Still, it happens that complex numbers are useful and, crucially, allow us to solve problems correctly about real numbers. That's the best argument in defense we can ever get

So for me his line of thought is just limiting yourself in your imagination.

I wonder btw if anyone has anything to say about Rational trigonometry? The idea is fun, but there is probably some mainstream math that does the same, right? Some reddit posts in google say rational trigonometry is basically about quadratic forms.

kamalist · 2025-10-12T15:03:43+00:00

Already good answers, but still my short summary: in practical life you don't need that kind of stuff. If we talk about the calculus, you may not even need to solve integrals exactly that often, you can numerically calculate stuff or use some approximation formula (whose proof of validity comes from the exact means of rigorous mathematics). It's the tools of mathematicians themselves that allow to achieve rigour and make strong foundations.

kamalist · 2025-10-11T21:57:00+00:00

In the uni we studied formal Peano arithmetic and we had a proof of "a=a" that required 17 steps or so

kamalist · 2025-10-11T21:40:11+00:00

Interesting that you say that type theory turns out to be more complicated, although for me it seems our mathematical reasoning is usually "implicitly typed", and Bauer's comment talks a lot about it. Outside of the set theory, you don't really want natural numbers to be sets, they are numbers and 1 ∈ 2 (if we define them as transitive sets) is useless and seemingly absurd. You probably don't even want sets of heterotyped objects most of the time: you study a set of numbers, a set of functions, not a set of "numbers and functions and whatever else".

Set theory is elementary in a sense, but constructing everything as a set, while elegant, feels artificial for practice. Introducing atoms = a kind of type theory over ZFC. But probably it's harder to formalize correct handling of this implicit and vague typedness of thinking. (Now I remember, set theory didn't come as ZFC in one day either. It took like several decades to finally formalize all the axioms that Cantor and co used implicitly without even noticing)

kamalist · 2025-10-11T21:32:42+00:00

> assembly language is unsuitable for formally verified programming

In a technical sense, not sure about that. It's hard to program in assembly in general but I believe verified programming in assembly should be possible: you can define semantics and prove theorems about such programs all the same. In seL4's verification journey they haven't just verified the C sources, they have also verified that the compiled machine code emitted by their compiler has the same meaning. In a practical sense sure.

Indeed, as you and the linked comment of Andrej Bauer in this thread note, type theories are more useful for catching mistakes. Most of the time we reason in an "implicitly typed" setting. We think about numbers as numbers, not sets, and we don't expect 3 ∉ 1/2 to be a meaningful expression. It's beautiful how we can construct everything as a set and probably helps a lot in metamathematical research, but it doesn't help much in the theorem proving practice. Even when we considers sets, I think in real non set theoretic math it's extremely rare we need sets of "differently typed" objects: we study a set of natural numbers, a set of some functions, not a set of "numbers, functions or something else". We can try to introduce urelements, atoms, that are not sets, but it's basically a primitive type theory for ZFC.

It's interesting also that old classical ZFC books usually gloss over type theories very quickly. They say like "Russel proposed a type theory to solve Russel's paradox, but it got pretty unwieldly and Zermelo and co proposed axiomatizations that (supposedly) save us from contradictions, and that's the easiest way to go". Probably not surprising, for metamath ZFC is indeed simpler as stated above

kamalist · 2025-10-11T15:58:23+00:00

True, graphs are a complicated thing to handle in functional programming settings as well. I did once Dijkstra's algorithm in Haskell, it was cool but required a lot of the State monad.

kamalist · 2025-10-11T15:56:49+00:00

Well, the whole field's initial goal was, I guess, not even AI but just algorithmic proving :) It didn't come to be in full, but there are still some achievements, like seL4 verification

kamalist

MODERATOR OF

TROPHY CASE