The term 'some' is known as a quantifier, i.e. a term that indicates what proportion of a collection is supposed to have some property, and 'some' means that not every element of the collection lacks the property.

In standard logic, the term 'some' is used as an equivalent of 'there is' and 'there are', in that each is taken in the sense that a predicate does hold of at least one element in the domain, and this is taken as the sufficient and necessary reason to say that some things have the predicate, and that there is a thing or there are things that have the predicate.

In natural language there may be subtle differences in the usage or meaning of 'some' and 'there is', notably the following: Most speakers of English have no trouble with 'Some Greek gods dallied sexually with human virgins', since this is part of the tales told about Zeus and other Greek gods, but many speakers of English do not believe this implies that 'There is a Greek god who dallied sexually with human virgins', since they do not believe there really are or ever were any Greek gods.

These differences can be accounted for by other means, such as introducing a predicate for existence, which allows the formulation of statements to the effect that some things exist and some things do not exist.

In standard logic, 'some' and 'every' are interdefinable, in that 'some' amounts to 'not every not' and 'every' to 'not some not', as in 'some women are blond iff not every woman is not blond' and 'every man is rational iff not some man is not rational' and 'every prime has one factor iff it is not true there is a prime with more or less than one factor'.

This interdefinability of 'some' and 'every' is not the case in intuitionist logic, where 'some' has the reading 'there is' and 'there is' requires some sort of proof that one can construct a thing that is said to be amongs those things that there is. This makes sense in many cases, but leads to problems with statements like 'There is a number no one ever thought of' or 'There are specific numbers so large that no one will ever mention them'. Also, it excludes constructions and proofs in standard mathematics that conclude that there is a such-and-such merely because one can prove that if this is not so one can derive a contradiction.

Also, one difference between 'some' as used in formal logic and as used in natural language is that in formal logic 'some' is used in combination with variables, that do not occur in natural language. Thus, 'some man is rational' gets translated into formal logic on the pattern of 'for some x, x is a man and x is rational'.

In formal logic, 'some' is often written as '(jx)(Fx)' and rules that are adopted for 'some' are often like these:

From (jx)(Fx) it follows that (Fa), provided a does not occur elsewhere in the proof.
From (Fa) it follows that (jx)(Fx), provided x does not occur elsewhere in (F).

Thus, what holds for some variable also holds for some constant, and what holds for some constant also holds for some variable. The reason for the proviso in the first rule is that if the constant a does occur in elsewhere in the proof additional restrictions may be imposed on it, but if it does not one can use it. (See below). And the reason for the proviso in the second rule is that if the variable x occurs elsewhere in (F) writing (jx)(Fx) may be false, but if it does not one can use the variable. 

Both provisos are meant to exclude possibilities that may make the conclusion invalid. In the inference of (Fa) from (jx)(Fx) the constant a is often called a quasi-constant, because it tends to function not as a real constant but as a place-taker for a constant, as in 'Suppose there is a largest number in the set of things that are F. Let's call that number a.'