@F.Zer For the purpose of ordinary mathematics, you should add some axioms for integers, rationals and reals. You're of course right that you can't deal with negative numbers in PA, so you do need these extra axioms. From a foundational point of view, these extra axioms are not necessary because we can construct everything. Namely, we can construct types ℤ,ℚ,ℝ and the usual arithmetic+ordering operations on them and actually prove the axioms I am going to give you. But for now just use them.

For integers, take all the axioms of PA− (from my post) except the last one, and change "ℕ" to "ℤ", and you will get axioms for ℤ. Add the binary operation − : ℤ^2→ℤ, and the axiom ∀x,y∈ℤ ( (x−y)+y = x ). Add the axioms ∀x∈ℕ ( x∈ℤ ) and ∀x∈ℤ ( x∈ℕ ∨ −x∈ℕ ). And you're good to go!

For rationals, do the same as above except that the last two are ∀x∈ℤ ( x∈ℚ ) and ∀x∈ℚ ∃p,q∈ℤ ( q ≠ 0 ∧ p = q·x ). Of course the existing operations +,· also extend to ℚ.

For reals, let's get to that another time, as it involves set theory.

@Prithubiswas You're right, but constant-symbols can be considered as 0-input function-symbols.

@Prithubiswas For the purpose of the exercises, you can ignore that part about "not appearing in S". I did make a remark on it under "Notes" but it is irrelevant for the exercises.

@F.Zer I realize I forgot to answer your question, and also you probably want to add the unary operation − : ℤ→ℤ with the axiom ∀x∈ℤ ( x+(−x) = 0 ). With that, your first proof is fine and probably ideal. Your second proof shows you that you can do it purely in PA, but surely your books won't want that! =)

@user21820 Thank you for all the explanations and insight ! I will review them carefully.

@user21820, when doing Velleman I found the exercise (Chapter 3): Suppose that a and b are nonzero real numbers. Prove that if a < 1/a < b < 1/b then a < -1.

Should I postpone for another time exercises involving reals ?

Perhaps better to focus on exercises involving integers and rationals, as a first step ?

@user21820, this is my first attempt at organising your explanations. What do you think ? Could be improved ?

@F.Zer No no that's not what I meant. I said "do the same as above", not to throw away the last two axioms of PA−. The last two are what axioms to add.

So for rationals also add subtraction and negation, and all the extra axioms I gave for integers except the last two that I gave.

@user21820 Oh, sorry. This are the last two, right ? ∀x∈ℕ ( x∈ℤ ) and ∀x∈ℤ ( x∈ℕ ∨ −x∈ℕ ). So, you gave, instead ∀x∈ℤ ( x∈ℚ ) and ∀x∈ℚ ∃p,q∈ℤ ( q ≠ 0 ∧ p = q·x ) ).

Yes. Actually it won't hurt you to drop the "0 < 1" because it's already there in PA− and the 0,1 are shared in all ℕ,ℤ,ℚ,ℝ.

@user21820 Good. But not sure I am following. If I take all the axioms of PA- but don't add "0 < 1", I won't have that axiom. I am sure I am missing point.

I don't know whether it would help, but the axioms are not just a random list; PA− can be described as "discrete ordered semiring axioms". The ordered ring axioms are all of them except the last. The last axiom is what makes it "discrete" and "semiring" (one-sided).

@user21820 I don't understand what you mean.

"Ring" is just a name. There's no meaning except for what I just said.

Never mind forget what I just said.

@user21820 Ok. So, the axiom "∀ x ∈ ℕ ( 0 = x ⋁ 1 = x v 1 < x )" makes it "discrete" and "semiring".

Yes.

Semi because that last axiom implies there is only one side; everything is either 0 on on more than 0.

Discrete because there is nothing between 0 and 1.

Good.

If you think it could be added, could you please check if this proof is correct ?

Theorem. Suppose 𝓕 and 𝓖 are families of sets, and 𝓕 ⋂ 𝓖 ≠ ∅. Then ⋂𝓕 ⊆ ⋃𝓖.
  Given 𝓕,𝓖 ∈ set:
    If 𝓕 ⋂ 𝓖 ≠ ∅:
      If a ∈ ⋂(𝓕):
        ∀ S ∈ set ( ⋂(S) = { x : ∀T ∈ set ( T ∈ S ⇒ x ∈ T ) } [intersection ?]
        ⋂(𝓕) = { x : ∀T ∈ set ( T ∈ 𝓕 ⇒ x ∈ T ) }
        a ∈ { x : ∀T ∈ set ( T ∈ 𝓕 ⇒ x ∈ T ) }
        E ∈ {x : P(x)} ⇔ P(E) [type-notation]
        ∀T ∈ set ( T ∈ 𝓕 ⇒ x ∈ T )
        ∃ X ∈ 𝓕 ⋂ 𝓖
        Let A ∈ ℕ such that A ∈ 𝓕 ⋂ 𝓖
        A ∈ 𝓕 ∧ A ∈ 𝓖
        A ∈ 𝓕 ⇒ a ∈ A

Now ℤ is supposed to extend ℕ; it includes every member of ℕ plus 'negative' ones. Of course if we want to have stuff less than 0 the last axiom cannot hold if "ℕ" is changed to "ℤ". It turns out that we can keep all the axioms of PA− for ℤ simply changing "ℕ" to ℤ" except the last axiom.

Ignoring subtraction and negation, which are not technically necessary, the extra two axioms ∀x∈ℕ ( x∈ℤ ) and ∀x∈ℤ ( x∈ℕ ∨ −x∈ℕ ) simply say that ℕ⊆ℤ and every integer is either a natural or a negated natural.

@F.Zer Why do you think they need to be added? You should be able to easily prove the second one from the empty-set axiom.

@user21820 I'll try to prove the second one.

@user21820 Thank you. Understood.

The first one is actually false because there cannot be an intersection of ∅ in ZFC.

What is true is: ∀S∈set ( S≠∅ ⇒ ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) ) ).

And this you can also prove.

Hello!

@user21820 Good. So, is the definition given in Velleman's book: ∀ S ∈ set ( ⋂(S) = { x : ∀T ∈ set ( T ∈ S ⇒ x ∈ T ) } incorrect ? Or, perhaps it is incorrect in the context of ZFC ?

@F.Zer Lol? Velleman gave that wrong definition? Can you quote precisely, just in case his version is not actually wrong?

So, is it possible to define ⋂(S) with S ∈ set in your system ?

@user21820 I will quote precisely in a moment.

@user21820, here it is.

@F.Zer Did he actually claim that the intersection is always a set?

@soupless Before your message scrolls off the screen.. Hello! =)

@user21820 Let me check.

@user21820 Please ping me again after you and F.Zer are done talking to each other. (To avoid any interference in your conversation :>)

@soupless Ok!

@F.Zer That's unfortunately not answering the question of whether he says the intersection is still a set.

@user21820 Sorry. Checking again.

You can see that Intersect(∅) by his definition includes every object as a member, since ∀A∈∅ ( ... ) is trivially true.

@F.Zer Ok so he did say that he will only use intersection of non-empty families. That aligns with my version:

@user21820 Good. But isn't "∀T ∈ set ( T ∈ ∅ ⇒ x ∈ T )" also trivially true ? Why do you say my version fails ?

@F.Zer Your version fails if you treat what you wrote using the {} notation as a set.

Because there cannot be a universal set.

That is, ∀S∈set ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) ) is false.

@F.Zer Anyway, since in your desired theorem F⋂G ≠ ∅, from that you can easily prove that F ≠ ∅ so you can apply the correct version of intersection. You made a mistake in "If a∈Intersect(F):"; "a" is not defined, and you don't want an "if" anyway. You also had a weird "Let A∈ℕ" when clearly you want "Let A∈set". The rest of your proof is fine.

Please don't use those mathcal symbols though, as they are taller than usual symbols and make it hard to select text. And in the absence of the big symbols I'd just use "Intersect" and "Union", since "⋂" and "⋃" are already used for binary intersection and union.

I’m studying your explanations.

@soupless: What's your question?

@user21820 Thank you for the explanation. I've finished studying it. So, {x : ∀ T ∈ set ( T ∈ ∅ ⇒ x ∈ T ) } gives the set of all objects ?

@user21820 I can't see why your symbolisation is equivalent to "∀ S ∈ set ( ⋂(S) = { x : ∀T ∈ set ( T ∈ S ⇒ x ∈ T ) } ". In particular, why do you use an existential ?

@user21820 That's good. I'll drop the use of mathcal symbols altogether.

@user21820 Thank you. My "a" is undefined. I should've said "Given a..."

The version I wrote with the existential captures your potential claim that such an intersection set exists, and it turns out to be false.

@user21820 "you have not defined Intersect(S)". I just copied your union axiom and replaced it accordingly. That's the definition of Intersect(S). I wonder what I am missing.

@F.Zer I stated that if S∈set and ∀x∈S ( x∈set ) then Union(S)∈set. That is what you are missing.

@user21820 Ohh !

I forgot about that.

You could anyhow add your axiom anyway, without claiming that Intersect(S)∈set, but then you would have a very strange world in which you have an object U := Intersect(∅) that is not a set but is a member of some sets, such as {U,U}. I don't think there is any contradiction, but ZFC is strange enough and this would be worse.

In contrast, in the way I set it up, you should not be able to construct an object that is provably not a set. (It doesn't prove that there are no such things, but at least it doesn't claim that there is a type that is an object but not a set!)

Good.

Before moving on to the Theorem Proof, I still do not understand why Intersect(∅) fails. I'll give it more thought.

@user21820 I will use Intersect and Union instead of the other symbols.

It is false because you can apply it to ∅ to get Intersect(∅). And why is Intersect(∅) not a set? Because it is a universal set. I'm sure your book mentioned why there cannot be a universal set? You can use the same proof to show that Intersect(∅) is not a set.

@user21820 If the Universal set includes every object, I've heard it also includes itself.

@F.Zer: Sorry I forgot that we're not working in pure set theory... I shouldn't assume that all members of a set are sets, so the false statement ought to be:

> (false) ∀S∈set ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈S ⇒ x∈T ) )

Equivalently, you can deduce contradiction from "{ x : ∀T∈set ( T∈S ⇒ x∈T ) }∈set".

Interesting. I'll try to understand.

@F.Zer Yes, though self-membership isn't problematic. If your book didn't mention it, from "{ x : ∀T∈set ( T∈∅ ⇒ x∈T ) }∈set" let U be that purported set and let R = { x : x∈U ∧ x∉x } and show that R∈U and then get a contradiction.

The same proof easily gives a disproof of the false statement.

@user21820 Wow. Seems really hard. I'll think about it.

∀x∈S(P(x))
Given y∈S
  y∈S
  ∀x∈S(P(x))
  P(y)
∀y∈S(P(y))

@user21820 Attempt for proving ∀rename.

Is it correct?

@F.Zer It's just Russell's paradox. Comprehension gives R∈set, so R∈obj, so R∈U, and either R∈R or R∉R but both give contradiction.

@Prithubiswas Yes it's correct, and that's why ∀rename is redundant and you can use it freely.

@user21820 I got lost in that chain of derivations. How did you go from R∈set to R ∈ obj. On the other hand, I can see why R ∈ U; because from a Given T ∈ set and assuming T ∈ ∅, I can derive anything.

@Prithubiswas Very technically, your attempt is wrong because you need to deal with two cases. If x,y are the same variable, then that instance of ∀rename is just restatement. If x,y are distinct variables, and y does not appear in P, then your subproof shows that that instance of ∀rename is valid. However, I said it's correct because you did get the main idea.

@user21820, Also, comprehension requires an S ∈ set. Which one is it ?

@F.Zer Well I guess you're right; it so happens that my system doesn't technically allow you to get from "x∈set" to "x∈obj"... Let's just disprove the false statement to see what's going on.

@user21820 Good. I'll try.

@user21820 But , if x, y are the same variable , then it wouldn't be variable renaming anymore(?)

@Prithubiswas Exactly, that's why it's just restatement.

@user21820 So, I should prove: "∃S∈set ∀I∈set ∃ x∈obj ( x∈I ⇔ ¬∀T∈set ( T∈S ⇒ x∈T ) )" ?

@user21820 why do we have to deal with two cases? When we do variable renaming , x and y can't be the same variable (isn't that the whole point of variable "re" naming?).So we only have to deal with one case. Although I will say that in your post for the renaming rule , even though it is called renaming , it is not told that x and y cant be the same . So in that case , I guess there is 2 cases instead of one.

@Prithubiswas Ya you got it. It's just a silly thing. After my first reply to you, I went to look to see whether I required x,y to be different, and lol it didn't require...

@F.Zer Yes, though we already know the witness so you just have to prove ¬∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ) ).

Let me just give you the proof, then you can slowly think through it.

@F.Zer Also, I realize that we can get from "x∈set" to "x∈obj", as I had thought last time.

Given x∈set:
  x∈obj.  [universe]
∀x∈set ( x∈obj ).

@user21820 Understood.

Case 1:
∃x∈S(P(x))
∃x∈S(P(x))

Case 2:
∃x∈S(P(x))
Let y∈S such that P(y)
y∈S
P(y)
∃y∈S(P(y))

@user21820 Attempt for proving ∃rename.

@Prithubiswas Why do the first and last line in your case 2 look identical?

Lol.

Typo

Is it now correct?

Ok, but it's still wrong after your fix, because after "Let y∈S ..." y is a used variable and cannot be used in the last line.

You need a third variable, and technically you need to say you pick a fresh variable that is never used anywhere in the proof at all (so that it doesn't interfere with something else).

It's interesting to see you try to prove these rename rules, and at first I wanted to say you don't have to but after your attempt at ∃rename I think it's a good choice that you tried, since it helps you work through some subtleties.

@F.Zer: Here is one main approach:

Given U∈set:
	If ∀x∈set ( x∈U ):
		Let R = { x : x∈U ∧ x∉x }.
		R∈set.  [comprehension]
		R∈U.
		If R∈R:
			R∈U ∧ ¬R∈R.
			⊥.
		¬R∈R.
		R∈U ∧ ¬R∈R.
		R∈R.
		⊥.
	¬∀x∈set ( x∈U ).
If ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ) ):
	Let U∈set such that ∀x∈obj ( x∈U ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ) ).
	Given x∈set:
		x∈obj.
		x∈U ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ).
		Given T∈set such that T∈∅:
			T∉∅.  [empty-set]
			⊥.
			x∈T.
		x∈U.
	∀x∈set ( x∈U ).
	¬∀x∈set ( x∈U ).  [above]
	⊥.

First half proves that there is no universal set, in the form "every set does not include some set".

Second half proves essentially that there cannot be a set that represents Intersect(∅) otherwise it would be a universal set.

@user21820 Thank you. This was my first attempt:

Prove ¬∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ) )
  If ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ) ):
    Let I' ∈ set such that ∀x∈obj ( x∈I' ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ) )
    ∀x∈obj ( x∈I' ⇔ ∀T∈set ( T∈∅ ⇒ x∈T ) )
    ∀x∈set ( x∈obj ) [Lemma]
    I' ∈ obj
    I'∈I' ⇔ ∀T∈set ( T∈∅ ⇒ I'∈T )
    Given T ∈ set:
      If T ∈ ∅:
        T ∈ obj
        ∀ x ∈ obj ( ¬x ∈ ∅ )
        ¬T ∈ ∅
        ⊥
        I' ∈ T
   ∀T∈set ( T∈∅ ⇒ I'∈T )
  I' ∈ I'
  ...

Case 1:
∃x∈S(P(x))
∃x∈S(P(x))

Case 2:
∃x∈S(P(x))
Let z∈S such that P(z) [z is a fresh variable]
z∈S
P(z)
∃y∈S(P(y))

@F.Zer Well just look at my proof and check whether I made any mistake. It's always best to understand in the two parts; no universal set, and that Intersect(∅) would be a universal set if it is a set.

@Prithubiswas Yup that's right. Take note that as I mentioned you need z to be different from even the variables used later in the proof, because here you are manipulating proofs to show that the ∃rename rule is redundant, so you need to make sure your proof-manipulation doesn't cause trouble for later steps.

When you're actually doing proofs in the system, you of course don't need to care about what comes later.

That's partly why I don't really ask students to prove rules redundant.

@user21820 So you mean when we expand the rename step , we have to use variables that are different from every variable in the proof so that it doesnt interfere with the rest of the proof. right?

@Prithubiswas Right.

@user21820 Thank you ! I will review your proof carefully. See you next time !

@F.Zer See you!

Why is it that |x + 3| < 1, not |x + 3| < 2 or |x + 3| < 3? Is it because of the fact that x approaches -3 and the nearest value of |x + 3| is 1?

@soupless The author simply wanted |x+3| < 1. But yes the given proof is confusing; you see later on that the author chose δ = min(1,...) so that any x within δ from −3 would satisfy |x+3| < 1.

Ok, that makes sense. This will be my last question for now. From the proof of the second statement, why choose δ = min{δ_1, δ_2}? Is it enough to choose the smaller value of δ_i instead of choosing a value that is smaller that both δ?

@soupless Isn't min(x,y) the smaller of x,y? It's not smaller than both x,y.

I mean, for example, min(4,5) is 4, right?

Sorry, the topic seemed to shift away. What I want to ask is the reason why δ = min(δ_1, δ_2) is enough, instead of choosing something that is smaller than min(δ_1, δ_2).

(I'll leave the room for now, bye everyone!)

If ¬∀x∈S(P(x)):
   If ¬∃x∈S(¬P(x)):
      Give¬ y∈S    [y is a fresh variable]
         If ¬P(y)
            y∈S
            ∃z∈S(¬P(z)) [z is a fresh variable]
            ¬∃x∈S(¬P(x))
            ¬∃z∈S(¬P(z)) [rename]
            ⊥
         P(y)
      ∀u∈S(P(u)) [u is a fresh variable]
      ¬∀x∈S(P(x))
      ¬∀u∈S(P(u)) [rename]
      ⊥
   ∃x∈S(¬P(x))

@user21820 attempt at Q1

@soupless Oops I didn't see your message. Well if x < min(δ1,δ2) then x < δ1 and x < δ2, so why would we need something small than both?

@Prithubiswas Haha I see a "Give¬" lol. You don't need a fresh variable for ∀sub; the rule only requires an unused variable. Same with ∃intro. Also, your ∀intro step is wrong; it only allows you to use exactly the same variable as you used in the ∀sub-header.

If ¬∀x∈S(P(x)):
   If ¬∃x∈S(¬P(x)):
      Given y∈S    [y is a fresh variable]
         If ¬P(y)
            y∈S
            ∃z∈S(¬P(z)) [z is a fresh variable]
            ¬∃x∈S(¬P(x))
            ¬∃z∈S(¬P(z)) [rename]
            ⊥
         P(y)
      ∀y∈S(P(y))
      ¬∀x∈S(P(x))
      ¬∀y∈S(P(y)) [rename]
      ⊥
   ∃x∈S(¬P(x))

@Prithubiswas It's correct now, but don't mislead yourself with the "fresh variable" comment, as they are not needed in those steps.

@user21820 I think they are needed for the renaming steps.

Because of the criteria for renaming.

@Prithubiswas No. Look at my rules; they didn't make any such requirement.

If you think there is an error, then to demonstrate it you need to actually produce a contradiction (from no assumptions) using my rules.

Note that what you use in your proof that the renaming rules are redundant does not imply anything about whether additional requirements need to be imposed on the original rules. Besides, your proofs didn't actually require the final renamed variable to be fresh!

@user21820 It seems like my renaming steps are not correct Because I am trying to rename something that has a negation.

@Prithubiswas Oh yes I missed that issue. Well just rename the earlier one without the negation.

And in the first instance you don't even need renaming:

If ¬∀x∈S(P(x)):
   If ¬∃x∈S(¬P(x)):
      Given y∈S:
         If ¬P(y)
            y∈S
            ∃x∈S(¬P(x))
            ¬∃x∈S(¬P(x))
            ⊥
         P(y)
      ∀y∈S(P(y))
      ∀x∈S(P(x)) [rename]
      ¬∀x∈S(P(x))
      ⊥
   ∃x∈S(¬P(x))

@Prithubiswas Yes, it doesn't occur in P. It is allowed to occur in "P(y)".

It must not occur in the property itself, such as in quantifiers in P.

So you cannot rename "∀x∈S ∃y∈T ( Q(x,y) )" to "∀y∈S ∃y∈T ( Q(y,y) )".

For the renaming step:

∀y∈S(P(y))
∀x∈S(P(x)) [rename]

How do we make sure that x does not occur in P?

@user21820

I think I have to think about the rename rules more carefully.

@user21820 I've understood both halves of the proof. Thank you for such a clear outline. One question: we've already discussed it, but could you please remind me how do you justify the line: "Let R = { x : x∈U ∧ x∉x }." ?

@F.Zer That's right.

So, yes, sorry what I did there isn't technically allowed directly. I just have a habit because it's convenient.

Basically, if in any context you have an object expression E, you can say "Let y = E." where y is a fresh variable. It is clear that this is redundant because you could just copy-paste "E" everywhere in place of "y".

I should have added it into my post, but I don't want to edit my post too often as it bumps it to the front page.

@user21820 Perfect. Makes sense. However, where do we have the expression: "{ x : x∈U ∧ x∉x }" ? Does it have to do with type-notation rule ?

@Prithubiswas You just read the symbols of "P" itself. See, the rules apply to any property "P", and property here just means that you have some boolean statement with some blanks, such that "P(E)" means the string obtained from filling each of those blanks with "E".

"P" is not a variable, and should not be treated as such. It's just a means for us to refer to a property instead of saying the whole long sentence I just did.

For example "∀x∈S ∃y∈T ( Q(x,y) )" is "∀x∈S ( P(x) )" where P is essentially "∃y∈T ( Q(?,y) )" where the "?" denotes the blank.

So you can read the symbols of P to check whether it uses a variable or not.

@F.Zer The comprehension rule explicitly states that we can write "{ x : x∈U ∧ x∉x } ∈ set" once we have deduced "U∈set" (and if "x" is an unused variable).

Sorry I mixed up; it's not quite the type-notation rule but the comprehension rule.

@user21820 Sorry, I was referring to your comment about "if in any context you have an object expression E, you can say "Let y = E." where y is a fresh variable". So, I wondered about where we do have the expression "{ x : x∈U ∧ x∉x }" so we can write "Let R = { x : x∈U ∧ x∉x }".

@F.Zer Then yes it's indeed the comprehension rule.

Because after you have "{ x : x∈U ∧ x∉x } ∈ set" you can apply ∀x∈set ( x∈obj ) to get "{ x : x∈U ∧ x∉x } ∈ obj".

@user21820 Perfect.

My point was that I do not need that extra line; I just have to copy-paste "{ x : x∈U ∧ x∉x }" everywhere in place of "R".

But to make life easy, we can add the rule ( E∈obj ⊢ y = E. [where y is a fresh variable] ). And the "Let " in front is just sugar.

Makes complete sense now?

@user21820 Oh, it is starting to make complete sense ! Via comprehension rule, we get "{ x : x∈U ∧ x∉x } ∈ set". But, in order to write "Let y = { x : x∈U ∧ x∉x }", that expression should be an object expression. So, we can apply "∀x∈set ( x∈obj )" to it and proceed !

@F.Zer Yes.

Great.

Do note that in pure set theories, namely those that have an embedded assumption that everything is a set, there won't be a distinction between obj and set, so there would be less of these hoops to jump through. However, the advantage of impure set theories is that we are clearer about the ontological assumptions we make of the objects we are dealing with.

That is why I did not require ℕ⊆set.

And yet it turns out that there is no drop in strength.

@user21820 Could you tell me why do you say so ? In which way this is related with your comment about the advantage of impure set theories ?

Alright, I'm going to do something else now. See you next time!

@F.Zer That is, my system doesn't make any claims about whether naturals are sets or not.

@user21820 Very clear ! Thank you so much ! See you !

Anyone who does programming may be interested in this 'crazy' heuristic answer I wrote, followed by simulation data that supports the crazy answer: