@user21820 Regarding our previous discussion, I have another question. I was able to show that there is no infinite disjunction by using the concept of an infinite set of formulae. However, I now have a problem with said infinite set of formula.
Consider that there exists an infinite set of formula comprising of the negation of a property for every name in the language, and that we have a name for every object in the language: $\{\lnot P_1,\lnot P_2,\dots\}$ (1 of 6).
Then consider those same formula in a theory $T$, which also contains the sentence $\exists x P_x$. (2 of 6).
A model consists of a domain and an interpretation. So I am considering that we have a name for every object in the domain which is part of the model which satisfies the theory.
Ok then. Well, the final thing I was going to ask at the end of the question was, why was the assumption of an infinite set of formulae permitted in the proof of inexpressibility?
@user400188 And by the way, your second error is that you attempted to force a meta function ( k ↦ P[k] ) into the theory as a predicate-symbol. That is clearly not what an FOL theory is permitted to be, though it turns out to not be the key issue here.
@user400188 All sets of formulae that you encounter in basic FOL are sets of strings that satisfy some first-order property about strings, so nobody doubts that they are legitimate conceptual collections.
@user400188 The meta function is exactly what I wrote; the mapping from an index k to a predicate-symbol P[k]. If you have a theory that has 0-input symbols P[1], P[2], ..., it does not mean that you have a theory with a 1-input symbol P.
Let N be the structure of the naturals over language L = (0,1,+,·,<). Let L' = (0,1,+,·,<,c) where c is a new constant-symbol (i.e. different from 0,1). Let T be the theory PA + { c≠1 , c≠1+1 , c≠1+1+1 , ... }. You can make this precise in MS as an exercise (i.e. don't use "..."). Then T is finitely satisfiable because N can be extended to a structure in which c is interpreted large enough to satisfy all the extra axioms in any finite subset of axioms of T. Thus T is satisfiable.
But N is not a model of T! Every model of T has objects that are not of the form "1+1+...+1".
@user21820 To give you an idea of the level I am at: I have covered the first example in a lecture on non-standard models, but this lecture lasted 20 minutes and took me a whole day to digest. If I saw your comment for the first time here, then I probably would not get it.
Maybe let's leave the other example for another time then.
The point is that you must very clearly distinguish the type of every object you reason about. If a symbol is a symbol in some FOL theory, you cannot use it as an object inside a model of a theory.
The fact that you number the predicate-symbols P[1], P[2], ... means that they are separate symbols, since the numbers 1,2,... are objects in MS, not necessarily objects in a model of the theory you want to build.
So writing "∃x ( P(x) )" is syntactically malformed from the start.
Do you get the point?
I'm going off soon, so I'll address any more inquiries later.