Hi Matteo,
Thank you for your corrections. This is a terminological issue where I have counted on google-trans:-) Yes, for the term "периодическая группа" in Russian we have the equivalent "torsion group" in English:-) And now let's continue my example (a) with the English book.
The point of Barwise about this formula
∀x∃n≥1 [nx=0] (8)
is written directly in the book (p.9) just after the formula itself:
"This is a sentence of weak second-order logic but it is not first-order
because it has the quantifier ∃n over natural numbers."
And this is what is important for me and is an initial topic: we take formulas - and we classify them as FOL, SOL, HOL...
So (8) is SOL. And look, we have a definition to be SOL "it has the quantifier ∃n over natural numbers".
And here for me is a point where we have a theory namely Group theory (p.7). And we begin its formalization. For me, it is important to point out that we have a structure (algebraic) that may satisfy or not to features (1)-(3) p.8, and Barwise directly pointed out on p.8 that
And we create our theory keeping as primary these terms, symbols: 0 - constant, "+" - binary operation, function.
If you take as a primary ∈, you need to define or introduce somehow Nat, 0, + and maybe in this case we should say that (8') is anyway an SOL.
But definitions first.
So when we have a theory (for example petrology) we are trying to find out its primary terms and express inevitable features of the domain area in axioms using these terms.
These axioms may be FOL, SOL, HOL. Why not?
For formalization of FOL see p.17, but let me say that now we have formalism of Context-free grammars (CFG) where the same syntactic structures may be defined even in a more compact and formal way.
The CFG of FOL languages is a very simple one:-)
Formalization of theoretical knowledge of sciences and technologies should follow the math way shown by Barwise on Group theory as an example:-)
Formalizing a particular theory (Group for example) we may study this theory and its structures, models without any connection with formal Set theory;-)
We formalize to get some advantages as we discussed [1] one year ago.
Alex
[1] https://www.researchgate.net/publication/349164216_Advantages_of_Formal_Definitions
Hi Matteo,