@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).

@user400188 Your error is in the phrase "name for every object in the language".

Languages don't have objects.

The language has constant-symbols, yes, but those are not objects.

What domain?

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.

No, your error is in "the model which satisfies the theory".

A theory has many models; you can't imply or assume that it has only one.

The point is, a theory is defined solely by its language (the symbols) and the sentences in it.

There is no link to any "domain".

How do you know what/(how many) names to use without some kind of link to the domain?

You have to define them as part of the theory. If you cannot do so, then you cannot have those symbols!

For example, PA has the language (0,1,+,·,<). There are only 2 constant-symbols there.

I think the proof will still work in the particular case that the model contains the natural numbers as objects.

wait no it wont, as the model formed using compactness may be a different model.

Exactly my point...

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 It's just a set of formulae. Like the set of well-formed formulae over some language. All these can be constructed in meta-system MS.

But clearly some sets of formulae can't be constructed. Is there any reason we can believe that the set used in that particular proof is legal?

@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.

@user21820 What was the meta function? When I wrote out the set, I simply meant for each of it's members to be part of the theory.

@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.

Sorry, I'm not familiar with the notation you are using. By P[1], do you mean a predicate that cannot have a new name substituted?

You wrote "P_1,P_2,...". I use square brackets for subscripts in chat because it is clearer.

Let me give an example of what you can do and what you cannot.

Thank you.

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".

Another example.

@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.

Ok.

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.

I think so, the names cannot be the objects themselves.

Thank you for all the time you spent helping me. I really appreciate it, and it clarifies a lot.

You're welcome!

Reminder: Read the room description before posting.