First-order, non-modal definition of 'bag/multiset'

honestrosewater

A bag, or multiset, is a set whose members are not necessarily distinct, i.e., it can contain duplicates. I can't think of a way to say this in a classical first-order language with equality, i.e., using only variables, function symbols, predicate symbols, implication (or conjunction or disjunction), negation, and universal (or existential) quantifier. Do I need to add modal operators? How do I say 'x shows up y many times in z'? What if I take bags as undefined and define sets in terms of bags? This shouldn't be stumping me, so I only want a hint please.

Oh, I suppose the 'power set' of a multiset could have some equal sets. So I can maybe define a set as a multiset whose power set contains no equal sets?

Multisets are also just unordered n-tuples.

If I keep the normal set definitions, noting that the members of my domain are sets and

[tex]\forall x \exists z \forall y (y \in z \leftrightarrow y \subseteq x)[/tex],

where z is called the power set of x, denoted P(x), then a multiset w is a set such that the cardinality of P(w) can be less than the cardinality of w.

__
Okay, nevermind. I looked it up.

honestrosewater

Okay, the following should say 'there exists a multiset'. You'll have to grant me N. Is this correct?

(Something is apparently wrong LaTeX. It didn't like my array, so here's my best fix. To make it a little easier to read: Multiset, Argument, Underlying set, function.)

∃N
∃M
∃A_M1 ∃A_M2
∃U ∃f
∃A_f1 ∃A_f2
∀u ∃u^f
∀x

(
A_M1 ∈ M ∧ A_M2 ∈ M
∧ U ∈ A_M1 ∧ U ∈ A_M2 ∧ f ∈ A_M2
∧ u ∈ U →
(
u ∈ A_f1 ∧ u ∈ A_f2 ∧ u^f ∈ A_f2
∧
(
(
u ∈ A_f1 ∧ u ∈ A_f2 ∧ u^f ∈ A_f2
)
∧
(
u ∈ A_f1 ∧ u ∈ A_f2 ∧ x ∈ A_f2
)
→ x = u^f
)
)
∧ u^f ∈ N
)

[ tex]\begin{array}{l}
\exists \mathbb{N} \\
\exists M \\
\exists A_{M1} \exists A_{M2} \\
\exists U \exists f \\
\exists A_{f1} \exists A_{f2} \\
\forall u \exists u^f \\
\forall x \\

( \\
A_{M1} \in M \ \wedge \ A_{M2} \in M \\
\wedge \ U \in A_{M1} \ \wedge \ U \in A_{M2} \ \wedge \ f \in A_{M2} \\
\wedge \ u \in U \ \rightarrow \\
( \\
u \in A_{f1} \ \wedge \ u \in A_{f2} \ \wedge \ u^f \in A_{f2} \\
\wedge \\
( \\
( \\
u \in A_{f1} \ \wedge \ u \in A_{f2} \ \wedge \ u^f \in A_{f2} \\
) \\
\wedge \\
( \\
u \in A_{f1} \ \wedge \ u \in A_{f2} \ \wedge \ x \in A_{f2} \\
) \\
\rightarrow \ x = u^f \\
) \\
) \\
\wedge \ u^f \in \mathbb{N} \\
) \\
\end{array}[/tex]

gnome

I don't think first order logic, even with equality, can allow a multiset. Aren't the individual variables we use in FOL, when bound, bound to unique objects? Quantification in FOL only gives us "for all ..." or "not for all ...", not "how many". When equality is included in the logic, we use it to indicate that two variables are bound to the same object. There is no concept of multiple copies of the same object, and no way to count them.

honestrosewater

When I said that the members of my domain are sets, I meant the domain of my interpretation. I'm using a FOL to talk about set theory. The interpretation I = (U, ∅, {∈, =}), i.e., a set of sets, no operations, and the relations of membership and equality. You can say 'how many' in set theory using bijections. I didn't feel like spelling it all out, which is why I asked for N.
Depends on what you mean by 'object'. Would you say that x in ∀x (x = x) refers to a single object?

In my experience, variables aren't usually said to be 'bound to' objects; rather, they are 'bound by' quantifiers. Quantifiers can let a variable refer to any subset of your domain. So if you mean 'objects' to be the members of your domain, then no, a bound variable can refer to more than one object. It's a valuation, not a quantifer, that assigns variables to members of your domain.

As for the uniqueness bit, yes, valuations are usually defined to be functions, but they don't have to be. They also don't have to be injections or surjections. A valuation not being injective means roughly that you can have more than one name for something.

gnome

Yes, in the sense that while it refers to all x collectively, it tells something about each x individually, i.e. each x is identical to itself.

I'd like to try to understand what you wrote in post #2. Please explain what you mean by these terms:
[tex]A_{M1}[/tex]

[tex]A_{f1}[/tex]

[tex]u^f[/tex]

and how do you define [itex]\in[/itex] in your interpretation?

AKG

[tex]\begin{array}{l}
\exists \mathbb{N} \\
\exists M \\
\exists A_{M1} \exists A_{M2} \\
\exists U \exists f \\
\exists A_{f1} \exists A_{f2} \\
\forall u \exists u^f \\
\forall x \\

( \\
A_{M1} \in M \ \wedge \ A_{M2} \in M \\
\wedge \ U \in A_{M1} \ \wedge \ U \in A_{M2} \ \wedge \ f \in A_{M2} \\
\wedge \ u \in U \ \rightarrow \\
( \\
u \in A_{f1} \ \wedge \ u \in A_{f2} \ \wedge \ u^f \in A_{f2} \\
\wedge \\
\end{array}[/tex]
[tex]\begin{array}{l}
( \\
( \\
u \in A_{f1} \ \wedge \ u \in A_{f2} \ \wedge \ u^f \in A_{f2} \\
) \\
\wedge \\
( \\
u \in A_{f1} \ \wedge \ u \in A_{f2} \ \wedge \ x \in A_{f2} \\
) \\
\rightarrow \ x = u^f \\
) \\
) \\
\wedge \ u^f \in \mathbb{N} \\
) \\
\end{array}[/tex]

I don't know about you, but this is pretty nasty to read. Maybe if things were indented like a program code it would be easier to look at. By the way, honestrosewater, the only problem with your LaTeX was that it was too long. I just split it up into two parts, and everything was okay.

gnome

If every subset of a multiset is a set, not a multiset, do you then have a separate "sub-multiset" relation for comparison of two multisets?

honestrosewater

I think I can give a nice, thorough explanation of everything (which I'd like to do in order to get it all straight in my head anyway), but it might be a day or two before I get around to it.
Yeah, thanks. I figured that out earlier... after checking EVERY other possible thing that could be wrong. I'll find a better way to represent embedding too.