1. ## A question about inference rules of parthood relation symbol

There are some ways of regimenting plural quantificational statements like "There are some apples on the table" as:

(∃xx)(∀u)(xx ≤ u → Au & Tu)

which translates into "There exist some xx such that for every u, if xx is part of u, then u is an apple, and u is on the table" in semi-formal language mixed with logic and English.

The symbol '≤' means '...is part of...', that is, the parthood relation. I think that the symbol of parthood must have inference rules like other logical symbols have.

My question is "What are the inference rules of parthood relation symbol???"

2. ## Re: A question about inference rules of parthood relation symbol

Originally Posted by mosesquine
There are some ways of regimenting plural quantificational statements like "There are some apples on the table" as:
(∃xx)(∀u)(xx ≤ u → Au & Tu)
which translates into "There exist some xx such that for every u, if xx is part of u, then u is an apple, and u is on the table" in semi-formal language mixed with logic and English.
The symbol '≤' means '...is part of...', that is, the parthood relation. I think that the symbol of parthood must have inference rules like other logical symbols have.

My question is "What are the inference rules of parthood relation symbol???"
I think that is topic is in category theory?
If that is correct then this webpage will help.
If not, I have no clue.

3. ## Re: A question about inference rules of parthood relation symbol

That webpage introducing inclusion based point-free geometry and connection theory is really helpful. However, what I want to get is an explanation of so-called introduction-rules and elimination-rules that can be used for natural deduction proofs. It's more like identity-introduction rule, identity-elimination rule in predicate logic, for parthood relation symbol.