0
$\begingroup$

For predicates, it is possible to pass multiple variables. They are called polyadic predicates in that case, for example, $P(x, y)$. But how about quantifiers. I have not seen an example of this but want to be sure.

Is there usage for something like:

a)

$$∀(x∈A, y∈B)(x | y)$$

in the first-order logic?

I could provide arguments in the following manner:

If multiple domain sets are provided, then values could be passed to the quantifier in tuples taking one item from each domain to match each argument. Say $A = [1 2 3]$ and $B = [1 2 3 4]$. Then we send arguments in groups of: $(x=1, y=1)$, $(x=2, y=2)$, and $(x=3, y=3)$ and leave the last iteration out because there is no pair for y: $(x=undefined, y=4)$. Is this too far from convention?

Or should it just be:

b)

$$∀x∈A(∀y∈B(x | y))$$

Or maybe even:

c)

$$∀x∈A∀y∈B(x | y)$$

Apparently b) and c) would give same truth value, but a) differs dramatically from the last two...

$|$ is just an arbitrary operation between $x$ and $y$.

$\endgroup$
4
  • $\begingroup$ What does '$x|y$' mean in this context? $\endgroup$
    – Dan Christensen
    Jul 30, 2017 at 3:15
  • $\begingroup$ It is any comparison operation that makes x and y relative. $\endgroup$
    – MarkokraM
    Jul 30, 2017 at 6:13
  • $\begingroup$ So, can you write $x|y$ as binary predicate instead, e.g. as $P(x,y)$? $\endgroup$
    – Dan Christensen
    Jul 30, 2017 at 15:23
  • $\begingroup$ If so, such constructs are often used mathematics. In mathematics, different quantifiers in the same statement may be restricted to different, possibly empty sets. For convenience, in most presentations of FOL, every quantifier in the same statement is assumed to be restricted to the same unspecified, non-empty "domain of discussion." $\endgroup$
    – Dan Christensen
    Jul 30, 2017 at 15:27

3 Answers 3

Reset to default
2
$\begingroup$

Technically, it all depends on how the formal syntax is exactly defined (though I have never seen a formal syntax that would support the first version, I suppose one could define syntax in a way that supports that).

But in practice everyone will understand all these three forms. So, unless you are doing a formal logic proof, go ahead and use any of those forms.

In fact, in math proofs you do often see $\forall x,y ...$

EDIT

OK, so I think I understand now what you are trying to do: you want the one quantifier to signify one object ... but it would have to be an object that exists in $A$ as well as $B$. Hmmm, 'too far from convention' is not a bad phrase to use here :). But I think it is also 'too far from useful' as well. If the quantifier signifies one object, then I would say use one variable as well. ... and if it needs to be in $A$ as well as $B$, then maybe just do:

$$\forall x \in A \cap B \ x|x$$

$\endgroup$
4
  • $\begingroup$ I added a bit more information for the first case. Can you please take a second look? $\endgroup$
    – MarkokraM
    Jul 29, 2017 at 18:45
  • $\begingroup$ @MarkokraM Oh! So your one quantifier would really denote just one object with which multiple variables would be instantiated. OK, well, that is certainly highly unusual .. hmmm... I can't say I have ever seen anything like it, but as I said, one can of course define the syntax in any way one wants, as long as one provides a semantics ... Then again, it really seems not very helpful, for if you really want just one object, then why not just use 1 variable as well? Though you would say that you are dealing with different domains ... but it needs to be in the intersection. $\endgroup$
    – Bram28
    Jul 29, 2017 at 19:09
  • $\begingroup$ Getting closer. I still made a small clarification to the argument split part. But now it seems as you stated. One could join domains and send tuples each containing two items. That would simplify quantifier to one argument. I guess, it doesnt matter if argument is a single value or tuple (set) of values. My question still is, when if ever quantifier should use multiple arguments? $\endgroup$
    – MarkokraM
    Jul 30, 2017 at 6:29
  • $\begingroup$ @MarkokraM Well, then I stand by my original observation ... whenever we do write something like $\forall x,y ...$ that is just shorthand for $\forall x \ \forall y ...$, and that will capture all possible pairs $(x,y)$ . ANd if you want $\forall x,y ...$ to mean one object, then you should really just use one variable. $\endgroup$
    – Bram28
    Jul 30, 2017 at 11:51
1
$\begingroup$

I never seen the first, and can be better write as $$ \forall(x,y)\in A\times B $$

that I prefer also to the other two notations.

$\endgroup$
2
  • $\begingroup$ Would this be equivalent to cases b) and c)? $\endgroup$
    – MarkokraM
    Jul 29, 2017 at 18:46
  • $\begingroup$ How would you denote, if domain sets A and B should provide values in pairs? I guess A×B now joins sets to correlate with cases b) and c)? $\endgroup$
    – MarkokraM
    Jul 29, 2017 at 18:48
1
$\begingroup$

The logics used in proof assistants like those in the HOL family and many others support this kind of syntax for quantifiers. It is often called "pattern-matching abstraction", because in place of the bound variable after the quantifier, we have a "pattern" $(x \in A, y \in B)$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.