@F.Zer That's right! Did you notice what the tautology means? It means that if f∘g = id[T] and g surjects from T to S then f is an injection on S. =)

This shows that FOL is powerful enough that if you only need to deal with fixed functions/predicates/sets you don't actually need any set theory. Do you get what I mean?

@user21820 No, I do not get it :-) Explain, please.

First you have to get the first comment...

Do you?

@user21820 Yes ! Thank you for your first comment ! I do understand it.

In plain terms, surjection means every element of the codomain is image of some element of the domain.

Injection means no two distinct elements in the domain have the same image.

@F.Zer So the point is that the tautology manages to say something about 'functions' f,g, even though f,g are not objects in the domain.

If you want to do general reasoning about arbitrary functions, then such tautologies are not enough, since in FOL we cannot quantify over arbitrary function-symbols.

However, this issue can be resolved easily by using higher-order sorts, still without going to a 'real' set theory.

I do understand a little more. Thank you. However, I will ask you about higher-order sorts in due time.

(Q6):
	∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ) ⇒ ∀ x ∈ S ( f(x) = x ), where f : S -> S.
	If ∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ):
		∀ x ∈ S ( f(f(f(x))) = f(f(x)) )
		∀ x ∈ S ∃ y ∈ S ( x = f(y) )
		Given a ∈ S:
			∃ y ∈ S ( a = f(y) )
			Let b ∈ S such that a = f(b)
			a = f(b)
			f(f(f(a))) = f(f(a))
			f(f(f(b))) = f(f(b))
			f(f(a)) = f(f(b))
			f(f(a)) = f(a)
			...

@user21820, I reached a dead end in Q6. Could you give me a little hint ?

@F.Zer Hint: Once only?

@user21820 I don't know what does it mean. Perhaps, doing Universal Elimination once ?

@F.Zer Well, I can't tell you too much without giving the key idea away. Just keep trying.

Good. I will keep trying. One question: Can I use Universal Elimination with function symbols, @user21820 ? Or, should I only use letters ? For example, taking f(a) as an element of S.

@F.Zer Check the ∀elim rule; it allows you to use it on any object expression E.

Thank you. I see.

@F.Zer I was going to say more but was away just now. To obtain HOL in many-sorted FOL (which is what my deductive system supports), we can have base sorts obj,ℕ,bool and the sort (S→T) for any sorts S,T, and then we can get the following tautology:

The first line expresses that you can construct predicate T from a function f from objects to predicates.

So everyone agrees that the first line is innocuous.

The second line is essentially Cantor's theorem, but expressed in HOL rather than a set theory.

There's a small issue here with the syntax. I wrote "f(x)(y)" and you should know what I mean, but this syntax is technically not supported by my system. That's not a big problem, you could simply have a function-symbol "app" specifically for this, and write "app(app(f,x),y)" instead. This just clutters things, and there is no harm in extending my system a bit to support HOL in exactly the way we want here.

The same holds for other sorts in place of obj, such as ℕ:

Something interesting about this is that it shows that we cannot write down a single 2-input predicate on ℕ that can be used to express every possible 1-input predicate on ℕ! To see why, again note that the first line is not contentious, and the second line says that there is no function f from ℕ to predicates on ℕ such that every predicate S on ℕ is equivalent to f(x) for some x∈ℕ.

@user21820 I am not ready to understand your explanation but I appreciate the response.

Ok no problem. You can come back to it later. =)

@user21820 I really do not have any idea about Q6. Could you tell me if my proof skeleton is correct ? Is that idea going to work or should I take a totally different route ?

@F.Zer Try using your intuition; think of f as some directed graph.

@user21820 So, f = (N, E) where N is the set of nodes and E the set of pairs of nodes ? A directed graph is a pair, not a set of pairs (like a function). Could you clarify what you mean ?

S is the nodes. f is the edges.

@user21820 Good. Thank you.

@user21820 That's very interesting. Does f represent a binary symmetric and reflexive relation ?

@F.Zer What does the conclusion you want say about f?

@user21820 f is a reflexive relation ?

I'm not sure why you bring up those properties on "relations". I thought I told you to just think of it as a directed graph. Yes, it's reflexive, but that's not what the conclusion says.

@user21820 Well, every node is connected with itself. Is that what the conclusion says ?

@F.Zer Yes. So you just want to prove that. Just look at what the given conditions say, and try to use them.

Good.

(Q6): ∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ) ⇒ ∀ x ∈ S ( f(x) = x ), where f : S -> S.
If ∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ):
	∀ x ∈ S ( f(f(f(x))) = f(f(x)) )
	∀ x ∈ S ∃ y ∈ S ( x = f(y) )
	Given a ∈ S:
		∃ y ∈ S ( a = f(y) )
		Let b ∈ S such that a = f(b)
		a = f(b)
		Let f(b) ∈ S such that a = f(f(b))
		a = f(f(b))
		f(f(f(b))) = f(f(b))
		f(a) = a
	∀ a ∈ S ( f(a) = a )
	∀ x ∈ S ( f(x) = x )
∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ) ⇒ ∀ x ∈ S ( f(x) = x )

@user21820, I think it is correct, now. Could you tell me what do you think ?

@F.Zer No it's wrong; you used ∃elim wrongly.

Ok

@user21820 Could you tell me why I used that rule incorrectly ?

Um, actually you should tell me what you did wrong, because the rule is clear enough. =)

@user21820 Seems fair. f(b) is not fresh ?

It's not even a variable!

Good !

So, you should be able to fix it now.

(Q6): ∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ) ⇒ ∀ x ∈ S ( f(x) = x ), where f : S -> S.
If ∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ):
	∀ x ∈ S ( f(f(f(x))) = f(f(x)) )
	∀ x ∈ S ∃ y ∈ S ( x = f(y) )
	Given a ∈ S:
		∃ y ∈ S ( a = f(y) )
		Let b ∈ S such that a = f(b)
		Let c ∈ S such that b = f(c)
		a = f(b)
		b = f(c)
		a = f(f(c))
		f(f(f(c))) = f(f(c))
		f(f(f(c))) = a
		f(f(b)) = a
		f(a) = a
	∀ a ∈ S ( f(a) = a )
	∀ x ∈ S ( f(x) = x )
∀ x ∈ S ( f(f(f(x))) = f(f(x)) ) ∧ ∀ x ∈ S ∃ y ∈ S ( x = f(y) ) ⇒ ∀ x ∈ S ( f(x) = x )

@user21820, done !

@F.Zer Right, but you didn't need so many lines. You already had "a = f(f(c))" so from "f(f(f(c))) = f(f(c))" you only need two steps to get to "f(a) = a".

And I purposely included this exercise to make sure you realize that you sometimes need to apply ∀elim on an object expression that contains a variable that arose via ∃elim.

(Well technically more than two if you respect the =elim rule properly, but I don't care about the order of the expressions around the equality anymore.)

Yea.

@user21820 That's excellent. Thank you for including that.

Alright I got to go. See you next time!

@user21820 Thank you very much for all the explanations ! See you !

You're welcome!

@user21820 can you tell me any book or videos which are best for correct precise mathematics ?

@Rover Well, you should definitely study Spivak's "Calculus" (I think there are some freely available older editions online), as it is well-written and rigorous and definitely what you need to learn in undergraduate real analysis. But before that you might want to read Daniel Velleman's "How to Prove It". But if you want to learn absolutely 100% precise mathematics, you must learn basic FOL, like F.Zer has been doing.

@user21820 Ok I will try to make use of them..