migrate this to this room or basic mathematics?

Hi there.

@Secret No need; it's more relevant here. Though the answer is simple. ZFC is strong enough to do what most mathematicians want to do, minus a few restrictions that usually can be circumvented. So it's true that almost all mathematics today can be proven in ZFC. That doesn't make it "so great", nor is it what we use to judge "everything".

It's as much a social and historical matter as a mathematical one.

Yeah, wasn't ZFC essentially the first published theory which turned out to be strong enough that nearly all of everyday mathematics can be done within it comfortably?

That is pretty great, I do admit.

@TannerSwett Right. It's currently the top contender for an elegant theory that can do what everyday mathematicians want to do. But nobody actually works in ZFC; they work in some conservative extension with some syntactic sugar.

Though elegance doesn't imply soundness, and I have reservations about that.

Right.

I guess my reservation about ZFC is I've never seen a compelling argument that it's arithmetically sound.

@TannerSwett Apparently, you're the first one I've met to voice exactly that opinion, which is exactly what I would say myself. I was just lazy to include the word "arithmetically" just now.

The best argument seems to be something like: "well, the von Neumann universe V exists, and it obeys all the axioms of ZFC."

And my response to that argument is: oh, it does, does it?

There are other logicians who also have doubts about ZFC, but they often refrain from talking about it.

I once spent just a couple of hours trying to prove various theorems while not using a base theory at all, and not making any assumptions whatsoever.

@TannerSwett You may be interested to know that Boolos had similar thoughts as I did on Replacement, and I only found out he did after searching for logicians who had actually thought properly about the philosophical assumptions.

Now, obviously, in (say) first-order logic, you can't prove much substantive without using any axioms. So I'm trying to remember what I actually did.

Ah, here's what I did. Instead of using one monolithic, fundamental theory of everything (similar to ZFC), I decided to study a variety of very small and specific theories.

I'm looking back at my notes.

I see that I managed to prove that addition of natural numbers is commutative, but I didn't explicitly write down which theory I proved that in.

Lol. Doesn't matter. I'm sure we can both agree that classical PA is a good starting point.

Looks like the theory I used is significantly weaker than that, actually. :D Although maybe not.

Actually, I'm not sure if my theory is strong enough to prove that 0 ≠ 1.

I think the theory I used consists of the axioms of a category with all finite products and a parameterized natural numbers object.

The category 1 is such a category, so sure enough, I can't prove that 0 ≠ 1. :D

Buuuut let me set that aside for now.

First-order Peano arithmetic definitely seems like a good starting point. And apparently there's a set theory, ALPO, which is a conservative extension of it.

Well, for logic itself to make sense we have to assume basic facts about finite strings. That's captured by TC. It turns out that TC is essentially incomplete, and that TC plus induction (the obvious schema) interprets PA. PA interprets TC by Godel's β-lemma. So can't escape PA... =)

So if you want to create a "weakest viable set theory", then ALPO seems to be a good starting point.

@TannerSwett Google doesn't find ALPO. Reference?

"A Strong Conservative Extension of Peano Arithmetic", Harvey Friedman.

Amazing; Google couldn't find that...

Anyway, I'll have to pursue what I was doing further—the idea of proving each theorem within a very small theory

I feel like the fundamental theorem of arithmetic seems like a good "test theorem". If you can prove that, then you can prove a lot.

Then again, I personally don't care much about conservativity over PA but rather (arithmetical) soundness. Assuming PA is sound, note that ACA0 is conservative over PA, so ACA0 is sound too. Now ACA is ACA0 plus full induction, which is strictly stronger than ACA0, but is sound as well because full induction is sound.

That's why I accept ACA (see this post).

Hmmmm, makes sense.

I should go to sleep, but I'd like to toss out one last thought.

Sure; I also need to go. Let's talk again next time! Preferably next week, as I'm very busy this week. =)

Sounds good :D

My last thought is: I'd like to try to take broad theorems of algebra, such as "groups form a category", and "translate" those into arithmetic statements. That particular statement would become something like "The axioms of a group 'fulfill' the axioms of a category, in a particular way".

Obviously, I'm going to have to define what it means for one set of axioms to "fulfill" another set of axioms.

The intended meaning is something like "the collection of all models of the first theory, is a model of the second theory".

@TannerSwett By the way, unique factorization (expressed via Godel coding) is trivially provable in PA.

If you haven't heard of Reverse Mathematics you should take a look. Most mathematics (outside of set theory and related areas) can be done in ACA, and only a handful require ATR0 or beyond.

And this answer implies that the other FTA (algebraic closure of the complex numbers) is provable in ACA0, but as one might expect it's not a simple question. Note that this FTA can't technically be stated in PA, since complex numbers cannot be coded as natural numbers, so one really has to go to at least second-order arithmetic.

@user21820 Sorry for the late response, but the main application I have in mind is in creating a programming language leveraging it to ensure formal soundness and completeness while prohibiting infinite loops, making memory leaks much harder, and the like, all common areas of program bugs. Infinities exist in mathematics, but they don't really exist in computing without assuming infinite time and/or memory, two things that obviously don't concretely exist.

So even though these theories are much weaker than what modern mathematics are based upon, the little I've seen still make it seem potentially useful in enforcing invariants preventing various bugs in practical programs. (It's worth noting that two's complement arithmetic in machines is implemented as an operation from two tuples of booleans to a single tuple of booleans, usually all of the same size. Floating point is also similar.)

So the use cases might not seem immediately obvious from a pure mathematics or logic standpoint, but I'm coming at this from an engineering standpoint where something like this could potentially set the stage to fix a lot of problems within the industry.

@IsiahMeadows Perhaps you're unaware that this has been done before. Prolog, Coq, and so on. Also, it sounds like you don't understand the incompleteness theorems. You cannot prohibit infinite loops without severely restricting the possible programs you can write to a very small part. Furthermore, there are useful programs that are supposed to run indefinitely, such as those on internet servers.

For a concrete example, prove that Ackermann's function is total. It appears widely in algorithm analysis.

@user21820 I'm aware of what's done before, and I'm aware of the incompleteness theorems. And I'm aware what the restrictions mean. BTW, infinite work on infinite input is okay. My concern is with finite input causing indefinite work, and also, I'm questioning the utility of things like Ackermann's function in practice - this is aimed not at highly theoretical stuff but at more practical things like reacting to UI events and such.

I've seen Prolog, Coq, and the like.

@IsiahMeadows Union-find is not highly theoretical. If it is, it's like saying let's stick to HTML+CSS and don't use javascript.

Fair.

And race conditions are highly non-trivial to avoid.

That is true, but it's a separate issue to what I'm looking to address. (In fact, work has been done to partially solve that in the form of substructural logics.)

I'm looking at the single-threaded side of things and bugs common to that.

And also, computers don't model addition in a way that requires nearly as much expressivity as, say, continuous integration. It's all discrete and finite.

Yes discrete theorems are typically provable using ACA, as I stated above. But that doesn't mean we should stop at ACA. Some things are just more naturally done in higher-order arithmetic.

$a + b \mod 2^32$ is equivalent to $a - (2^32 - b) \mod 2^32$, so it's not like you can't also model it using purely subtraction. Stuff like that is why I find Dan Willard's research an interesting lead nevertheless - it relies on subtraction and division as primitives, and with modular arithmetic, you can still model modular addition and multiplication in terms of subtraction. If the "modular" part of it can still fit within that framework, the lead still can work.

And I do agree that for some things, it might very well be more natural. But I want to see first how much can truly be done or at least emulated in ACA and similar.

@IsiahMeadows That doesn't make sense; a lot of facts about algorithms rely crucially on the unboundedness of naturals, since induction already does. Willard's theory doesn't do much precisely because everything is 'stuck' below bounds.

@IsiahMeadows And you should look up reverse mathematics, and learn how to encode theorems and proofs into ACA, to know more about what can or cannot be done in ACA.

That is true, but my goal isn't entirely about proving them from the algorithms themselves. A lot of languages (like TypeScript) get by with a fully deductive type system, and induction is certainly far from universal.

If you doubt induction, you basically doubt all of logic. Once you assume strings are closed under concatenation, you essentially have assumed induction!

Got to go...

👋

I found it useful to understand the difference of - for example - $\exists x Gx \implies Hx$ and $\exists x (Gx \implies Hx)$.

@BillyRubina I don't think so; it looks stand-alone and complete enough to me.

@BillyRubina It's... wrong because it can't be used for infinite domains.

@user21820 What's the trouble with it? I mean, I guess $\dots$ doesn't mean something is finite.

And even for a finite domain of size n, you have to work outside the theory because you need x[1..n] to refer to the objects in the domain.

"..." is a 100% accurate indicator of imprecision. You will not be able to reason precisely if you have "..." anywhere.

Got it.

But I guess it's not too bad to see things "intuitively".

Is it?

@BillyRubina It's not too bad; you can think of ∀ as global ∧ over the domain if you have a fixed intended domain, and likewise ∃ as global ∨ over the domain. But it must be clear to you that that is tied to the domain, and can't be expressed syntactically.

Consider "∀a,b∈R ( ∀c∈R ( a<c ⇒ b<c ) ⇒ b≤a )", where R is intended to be the reals, and see whether you can make sense of it with that interpretation of ∀. It's not impossible, but I'm not sure it's worth it most of the time.

The domain is what Magnus call "Universe of Discourse" in his "forallx"?

Yup.

@user21820 I see now. With what you wrote, I say that if something attains that conditions, then that other thing is true. If I were to use what I wrote, I'd have to specifically pinpoint each of the elements, I guess.

Or write something messy with implications.

BTW: Do you know Hirst/Hirst book? appstate.edu/~hirstjl/primer/hirst.pdf

Didn't know about it, but a quick glance tells me that it doesn't even cover the basics, since it doesn't even reach completeness for first-order logic. Also, I can't recommend it for beginners because it presents a practically useless Hilbert-style deductive system for first-order logic.

In contrast, Hannes' actually gives a sequent-style system, which is more usable and you can understand the underlying logical structure better.

Though of course, Hannes' is meant for math majors, not lay people.

I've once read about the "length of a proof". I'm not sure if this is the correct name, do you know something about it?

There is a thing called the length of a proof, and it's more or less what it sounds like. What specifically do you want to know about it?

@MaliceVidrine Can we take - for example - Riemann hypothesis and supposing it exists - speculate the length of it's proof?

Sure. You can speculate on the minimum length of its proofs, even.

I'm not sure it leads to anything helpful, of course.

Are there "impossible" lengths?

Well, trivially for the Riemann hypothesis we can rule out extremely short proofs, like length 1 where the Riemann hypoithesis would have to be an axiom :P

But the thing is once you know the minimum length, you can always just add in some trivial extra step that does nothing (at least in a Hilbert proof)

So depending on your proof system, anything above the minimum length is the length of a possible proof.

There may be ways to rule out certain lengths as being the minimum length.

But that would be some proof theory that I'm not familiar with.