@user21820 In the message you linked to , the definitorial expansion seems to be something like this:

But it seems to me like there is no such rule in your FOL post.

Or maybe it is something we can prove?

@Prithubiswas Yes that's why I said "I didn't mention definitorial expansion in that SE post". In the next revision of that post I do plan to mention it.

@Prithubiswas It's not something you can derive because the system given in that post doesn't enable you to create new function/predicate-symbols. However, this kind of extensions is called a conservative extension, which means that everything you can prove in the new system that uses only the old symbols can already be proven in the old system.

@Prithubiswas And the rule you stated is indeed exactly what I meant there. But I'm not sure why I didn't just give the simpler equivalent:

> Definitorial expansion: ∀x[1]∈S[1] ... ∀x[k]∈S[k] ∃!y∈T ( Q(x[1],...,x[k],y) ) ⊢ ∀x[1]∈S[1] ... ∀x[k]∈S[k] ( f(x[1],...,x[k])∈T ∧ Q(x[1],...,x[k],f(x[1],...,x[k])) ). [where f is a fresh function-symbol]

Well okay maybe it's not exactly simpler, but it's easier to use.

@user21820 So , in your next revision of your post , would you put the "definitorial expansion" rule immediately after the "Variable Renaming" rule? [Between "variable renaming" and "short forms"]

@Prithubiswas I guess so. For a general deductive system one would have 3 types, for constant-symbols and function-symbols and predicate-symbols. My system happens to be of the type where the ∃elim rule introduces a fresh variable in the current context, so that rule already functions exactly as definitorial expansion for constant-symbols. What is left is the rule above for function-symbols and the simpler rule for predicate-symbols that we talked about before. For reference here are both together:

Definitorial expansion:

But things like 'equals' and 'for all' and 'there exists' seem a bit more out of reach. The semantics of FOL = relies on metatheoretic equality. Similarly, ∀ relies on metatheoretic 'for all'.

@user21820 Hi, there ! Could you explain how would you use function-notation to define abs ?

@F.Zer That is what I was saying above, starting from the comment at which I pinged you. If you don't define abs0, then you can't use the function-notation because you can't form the object expression that you need.

@Threnody What's the difference between those and "and"? How did you define "both"?

Ultimately, the definition of semantics for FOL does rely on every single bit of the FOL used by MS (meta-system). That's why I always say it's impossible to truly understand logic until you can actually work formally in some deductive system. Although what I wrote in the linked message is not formal, it is closer to formal than majority of introductory logic textbooks, so the reliance I talked about should be 100% clear.

room mode changed to Gallery: anyone may enter, but only approved users can talk

@F.Zer: Do you get my explanation?

@user21820 Mmm...OK, so you defined abs0, but how would you use function-notation rule ? What's ∀ x ∈ S (E(x) ∈ T) and f = (S x ↦ E(x) ) ?

Sorry, I didn't find the correct symbol.

@F.Zer "↦".

Thank you.

@F.Zer ∀x∈ℝ ( abs0(x)∈ℝ ).

Let abs = ( ℝ x ↦ abs0(x) ).

abs∈FN(S,T) ∧ ∀x∈S( abs(x) = abs0(x) ).

@user21820 Oh, wonderful. S = ℝ, T = ℝ, f = abs and E = abs0. What a useful skill you have. I haven't developed that skill yet. I mean, the ability to replace general patterns with specific instances. Very important.

@F.Zer Haha no this is just because it's the first time you're seeing these two different definition mechanisms working together. I ought to have explained it earlier when you were doing the proofs regarding "abs", but I thought maybe we could ignore it since at that time you only needed the function-symbol.

Good :-)

In fact, it's an important thing to realize that what Set Theory is doing as a foundational system is to represent some (definable) function/predicate-symbols by objects.

That's great. Should be starred, I think.

For (definable) function-symbols, we have this rule. For predicate-symbols, take a look at the comprehension rule and see whether you can see why it allows you to capture some (definable) predicate-symbols by sets. Namely, when you restrict it to an existing set.

Naive set theory with full comprehension allows constructing the set { x : Q(x) } for any property Q, but of course that runs straight into Russell's paradox and destroys the set theory.

Zermelo found that the paradox appears to vanish when we only allow constructing the set { x : x∈S ∧ Q(x) } for a property Q and existing set S. Effectively that means that we can only capture some but not all (definable) predicates.

We of course still don't know whether ZFC is consistent or not (hence "appears to vanish").

@user21820 Since you can't prove x ∉ x, there isn't a problem. Is that correct ?

@F.Zer No, not because of that. The S must be defined before you construct { x : x∈S ∧ Q(x) }.

@user21820 Good. What's your symbolisation of Russell's paradox ?

¬∃R∈set ∀x∈obj ( x∈R ⇔ x∉x }.

@user21820 Good. So, to prove it within your system, I should find R ∈ set before using comprehension; but that's impossible.

@F.Zer Why do you think you need comprehension? Just try proving it.

I will.

	If ∃R∈set ∀x∈obj ( x∈R ⇔ x∉x ):
		Let R' ∈ set such that ∀x∈obj ( x∈R' ⇔ x∉x )
		∀x∈obj ( x∈R' ⇔ x∉x )
		...
¬∃R∈set ∀x∈obj ( x∈R ⇔ x∉x )

@user21820 The domain could be empty. So, I can't guarantee there exists x ∈ obj; is that right ?

@F.Zer If R∈set then R∈obj as well.

@user21820 Oh, right. We discussed that three months ago, I think.

	If ∃R∈set ∀x∈obj ( x∈R ⇔ x∉x ):
		Let R' ∈ set such that ∀x∈obj ( x∈R' ⇔ x∉x )
		∀x∈obj ( x∈R' ⇔ x∉x )
		R' ∈ obj
		R'∈R' ⇔ R'∉R'
		If R' ∈ R':
			R'∉R'
			⊥
		If R'∉R':
			R'∈R'
			⊥
		⊥
¬∃R∈set ∀x∈obj ( x∈R ⇔ x∉x )

@user21820 I am using LEM. Is that good ?

@F.Zer That's right! You don't need LEM, but it's about the same.

If R'∈R':
  R'∉R'.
  ⊥.
¬R'∈R'.
R'∈R'.
⊥.

Good ! I like that version.

I will go out now. See you !

I don't think I've seen a book that nails down what a MS is supposed to be. I've glossed over Tourlakis' book, but it's very dense. So far it seems to be the only book that even bothers mentioning a metatheory at all with some detail.