On the definition of `ModelTheory.Basic.Language`

Stream: mathlib4

[Kijeong Lim]

Why are there sets of function symbols for each arity?
https://github.com/leanprover-community/mathlib4/blob/ba454ce1f3d3aabc948e53f57d8f06854c4f6eb1/Mathlib/ModelTheory/Basic.lean#L57
I think that there should be a set of function symbols and each function symbol should be assigned its arity.

[Yaël Dillies]

Why does the difference matter to you?

[Kijeong Lim]

The interpretation of a symbol may be overloaded by the arity. Indeed, I'm not satisfied by the fact that the same symbols may have two different arites.

[Yaël Dillies]

cc @Aaron Anderson

[Edward van de Meent]

If you look at docs#FirstOrder.Language.Symbols, they actually don't overlap, since it uses a disjoint union, I think...

[Edward van de Meent]

Can you give a concrete #mwe where it makes a difference?

[Kijeong Lim]

Thank you for the response. But, we may still take L.Functions l := Unit.
However, I admit that the definition in Mathlib4 is not bad.
Actually, developing meta-theory in the setting I suggested is more difficult than that of Mathlib4.

[Kijeong Lim]

Also, I don't think that it will make a significant difference.

[Edward van de Meent]

Kijeong Lim said:

we may still take L.Functions l := Unit.

Yes, but does that allow you to construct an ambiguous sentence?

[Kijeong Lim]

No. Since l is in the constructor func, it is impossible.

[Kijeong Lim]

This is what I want to know:
"If I rewrite my proof of the soundness and completeness theorems in Lean4,
will it be merged with Mathlib4?"( I've already written the proof in Coq.8.20.0. )
I think that there will be no hope because the definitions of Language differ.
(However, the completeness theorem works for only countable languages in my code.)

[Aaron Anderson]

I doubt this difference in presentation would present much of a problem. There is still a type of all function symbols - Σ l, L.Functions l, and the function assigning an arity to its symbol is Sigma.fst.

[Kijeong Lim]

Yes, there is no problem. There may be many ways to describe one thing.