I have an infinite set of variables X and I want to state that the property that there is a unique variable in X with value 2.
For a finite set, I would write the first-order logic formula: $$ (x_0 = 2 \wedge x_1 \neq 2 \wedge ... \wedge x_n\neq2) \vee (x_0 \neq 2 \wedge x_1 = 2 \wedge ... \wedge x_n\neq2) \vee ... $$
For the infinite set X, I could do the same but using infinite conjunction/disjunction.
Alternatively, using second-order logic, I could (if I understand correctly) quantify over X stating. $$ \exists x\in X. (x=2 \wedge (\forall y\in X. (x=y \vee y\neq 2))) $$
- Is there a name for first-order logic with infinite conjunction/disjunction?
- Does the example demonstrate that this logic is then more expressive than first-order logic with finite/binary conjunction/disjunction?
I am clearly not a logician so please don't overwhelm me too much :D
The name you are looking for is infinitary logic.
And yes, this is a simple example to show that first order logic cannot do everything.
To makes things a bit more formal: in logic "$X$" is a set of "constant symbols", or "0-ary function symbol", each element of $X$ is an element of your language, and not some set/number.
If you have a set $Y$ of elements of the model(for example, $Y$ is a set of integers), then FOL is enough: $∃y∈Y(y=2)$. But because $X$ is a set of elements of the language, and not the model you are working in you cannot talk about $X$ directly in FOL.