Here is another logical question that I've been trying to solve for the last 3 days, and feeling terribly dumb about this.
In the following, the actual meaning of “metric space,” of “converge,” and of “subsequence” is not important. Consider the following definition: A metric space X is compact if every sequence on X has a subsequence that converges to some point of X. 1. Let X be a given metric space and S(X) denote the set of sequences on X. Introduce appropriate predicates to formalize symbolically the statement that X is compact.
Okay, so this is how I tried to tackle it: it is clear that the general form of the statement is going to be a conditional, of the form: "If every sequence on X has a subsequence..., then there exists a metric space X with property compactness".
My first difficulty is deciding on what the universe of discourse should be. One would think that 'the set of all metric spaces' should do the job (and it goes very well for the consequent: [∃X C(X)], where C(X) would be the predicate 'X has the property of compactness'), but when I look at the antecedent, the universe of discourse I seem to be needing there is something like "the set of all sequences". Then I imagine the antecedent would work like this: let CS(x): x is a (sub)sequence that converges on some point in X). Then:
[∀x∈ S(X) ∃x ∈ Cs(x))]
And connecting the two, [∀x∈ S(X) ∃x ∈ Cs(x))] → [∃X C(X)]
I don't feel too satisfied with this (and don't think you can use two universes of discourse even if you are using two variables). Can you have a hint on what I am doing wrong?
Thanks in advance for your time and words.