@famesyasd An easier way is to use induction. Let Q(k) = ( nat k ↦ forall n in nat , forall S,T in type ( #(S) = k and #(T) = n implies #(S*T) = k·n ) ). Then it should not be too difficult to prove Q(0) and forall k in nat ( Q(k) implies Q(k+1) ).

@MaliceVidrine I wrote an informal sketch about building blocks, linking to Henry Towsner's very brief introduction to reverse mathematics, but you may want to also take a look at Stephen Simpson's SoSOA (Subsystems of Second-Order Arithmetic), which is widely touted as the standard reference text, though it is behind a paywall.

@Holo: Hello!

Hi @user21820

I'm quite happy with the proof that there is an uncountable well-ordering, but to get from that to the von Neumann ordinal ω[1] takes a bit more that seems to be tied to the peculiar choice of foundation, such as ZFC.

@user21820 you don't need C

ZF is enough, Ord is well defined in ZF, we need C to show that Card is well ordered so we can define card(A)=min(a in Ord|exists bijective from a to A)

And I am a believer in ZF(and even in C)

@LeakyNun I didn't mean to imply you need AC to construct ω[1] in ZFC.

@user21820 So you don't have a choice of foundation?

@Holo ZFC where replacement is restricted to definable functions on countable sets is strong enough to prove almost everything of interest in mathematics, but still not strong enough to construct ω[1]. It seems to me (and to Boolos and a couple of other logicians) that there is actually no non-circular justification for full replacement.

@user21820 there is the simple intuition, f restrict to f^-1[f[A]] can not have image greater than A

@Holo I don't understand what this means. Are you saying that every collection that is small enough should be a set? (It doesn't seem to correspond to what you wrote though.)

@user21820 it is what I meant

@Holo Okay that is one common response I get from set theorists, but it does not really work.

There are two main approaches in the common kinds of justifications I have seen: (1) Envision an open-ended universe constructed in stages as per the cumulative hierarchy. (2) Envision a closed platonic universe.

(1) can arguably provide ontology for ZFC with only countable replacement, but not further.

This is the point made by my linked post and by Boolos.

(2) cannot explain the specification schema.

why can't (2) explain the specifications schema?

@LeakyNun If the universe is fixed, then there is no reason that we cannot have unrestricted specification.

well it's not really unrestricted

it's restricted by the things in the universe

just like a Grothendieck universe

@LeakyNun I don't think you get my point. ZFC has a specification schema, which is not unrestricted because unrestricted specification leads quickly to contradiction.

oh

then you just answered your own question :P

@LeakyNun I still don't get you. It means there is something wrong with the justification, if the same kind of reasoning leads to an inconsistent system.

because the universe is not an object of the universe

@user21820 sorry, I am not so advanced(I only had one course in set theory) so there are few things I don't understand, but why replacement restricted to countable sequences and not with finite if you restricting it?

@LeakyNun So what? If one arbitrarily stipulates that some collections are not in the universe, then I don't see why we can equally arbitrarily stipulate that every collection that 'injects' into a set is also a set.

@Holo Well, the idea is that in the iterative conception you presume that the powerset operation is meaningful, and you collect the sets you can construct using it iteratively. The problem is that we can only iterate for as long as a sequence we have already generated. And hence we get stuck at countable replacement because we can never generate an uncountable sequence.

Of course, if you don't stick to the iterative conception, it is possible that you can evade that particular objection against full replacement. But I've not heard any justification that works for all the axioms of ZFC together.

(What "works" is of course subjective.)

So, because without ordinals we can only generate countable sequences and to define ordinals we need universe and we define universe using sequence we get to a circular logic?

Yes; every logician has to admit that the iterative conception relies on a pre-existing collection of ZFC-like ordinals, along which you can iterate. So it is circular.

What one can say is that the iterative conceptions shows that foundation is inessential because you can indeed without foundation construct all the well-founded sets via the cumulative hierarchy.

But if we define the universe like this, won't there be sets that are "larger" than the universe?

@Holo Define like what? That's why it is circular...

You can't justify ZFC without using ZFC-like assumptions.

Got to go for a while. Back later.

@user21820 See you later, I will keep thinking about this for now

Are Hilbert systems, ND systems, etc, just two different systems for proving the same stuff?

Are they both "equivalent" in terms of their usage and what they can do?

i.e. do they "do" the same thing just in different ways? (the axiom/inference rule tradeoff)

@user525966 do you know what truth table is?

Yes

the two systems (for propositional logic) prove exactly what the truth table interprets as true

I thought the semantics were more or less "assigned" after the fact (after the syntax has been established)

well you can of course build the syntax from the semantics instead

so hilbert and ND systems are (basically) "equivalent"?

sure

if they're both basically the same it makes me wonder why hilbert didn't use that style of system

why favor hard-to-use axioms rather than natural rules of inference

if you were building a logic system from scratch it seems like ND would be the first sort of system you'd intuitively come up with

not something like hilbert's

usability isn't everyone's first priority

it's always a tradeoff between how hard it is to implement and how hard it is to use

hilbert seems like it is more difficult on all fronts

what is it prioritizing or doing better than a ND system?

just having as few rules as possible?

perhaps

@user525966 It is because Hilbert was mostly interested in analyzing logic as a mathematical object. You see, Hilbert knew perfectly well that Hilbert-style systems are impractical for actual mathematical work, and he himself also didn't use that style for any of his mathematical work. However, Hilbert-style is one of the simplest to describe, and hence it is much easier to construct the Hilbert-style deductive system for first-order logic as a mathematical object.

In contrast, a Fitch-style system is nearly at the other end of the spectrum; it is one of the most troublesome to describe in a 100% precise manner, but it is one of the easiest styles to use in practical mathematical work.

This trade-off is inevitable.

There is a historical factor that probably was also quite significant in this issue: at the time of Hilbert there was still no clear notion of "algorithm", much less "computer program". So a Fitch-style system would be even harder for him to describe and analyze than it would seem to us from the modern perspective.

Does this make sense?

@user525966 Short answer is "yes" Long answer: I might have forgotten to define what is a theorem in the Fitch-style system we have gone through. A theorem is a assertion/statement that is not under any context whatsoever. For example, in the first example proof here, there are two lines that are outside all the contexts, and those two are theorems.

Since we have only covered propositional logic, every theorem in the current system will be a propositional tautology, which you can check via truth-tables.

(Later on, for first-order logic most theorems will have quantifiers in them, which you can no longer check via truth-tables.)

In a Hilbert-style system, if you wish to compare, a proof comprises some sequence of formulae, but only formulae that occurs in some proof and has no free variables is called a theorem.

@user525966 By the way, Hilbert probably came up with a natural deduction system first, and then translated it into Hilbert-style! At some point, I will explain how it is done.

@Holo: By the way, ZC already proves the well-ordering theorem and Zorn's lemma, and that is why replacement is not needed in ordinary mathematics.

He wanted to analyze logic as an object, does ND not allow this?

@user21820 so you are pro ZC+countable replacement? Now I will continue studying before I choose if I agree or not, deciding something without fully understanding it is no good

@user525966 We can analyze any deductive system, including Fitch-style. It is in fact not that hard to do so. However, if we want to perform a completely formal analysis of it, it will not be as easy as for Hilbert-style. That said, my goal is not to give machine-checkable explanations, since they would not be human-readable. Thus when I explain to other people like you, it will be relatively easy for me to convince you of certain facts about Fitch-style systems.

For example, the last time I had convinced you that the Fitch-style rules correspond to rules for writing PPs that allow you to write only valid PPs.

That reasoning I did not formalize, and there is no need for me to do so at this level.

@user525966: By the way, to ensure I see your messages, ping me by writing "@user21820 " anywhere in one of your messages.

@Holo Yup. By the way, it's not that I deny full replacement, but that I currently don't see a good way to justify it, whereas I am quite comfortable with countable replacement. Of course, some set theorists see the 'small'/'large' distinction as sufficient intuition for what should be a set, but I'm afraid I don't buy that argument, since Morse-Kelley set theory has sets and classes but again no class of classes, despite the notion of a collection of all classes clearly making sense to us.

And so if you ever see a justification of ZFC that evades the pitfalls in the iterative conception, I would be very interested to hear about it!

@user21820 if I ever see one I will PING you

Thanks! =)

@user21820 so Hilbert systems are easier to analyze with a computer but not for humans, and with ND, nice versa?

@user525966 More or less yep.

@user21820 so when we wish to combine systems do people just start a new set of proofs with various sets joined together as the assumptions?