Proposal for a new logic

 A new logic based on the following two rules:

1. There are no formulas besides sentences. Expressions with 'free variables' have no place either syntactically, deductively or semantically.

2. Unbounded quantifiers are meaningless. All quantifiers must specify a domain in which the variable is quantified. For instance in the form $\forall x. M(x) \rightarrow \phi$ which we write $\forall_{x \in M}. \phi$. In CIL $log^Q$ would be a binary operator $log^Q T^{(1)} S$.

Hence ordinary equality $x = x$ must already express a restrictive condition. There must be some $A$ such that $\exists_{x \in A}.x \neq x$.  

For a concept we can distinguish its comprehension from its extension.  There is a duality between the two. The greater the one, the smaller the other and vice-versa.  But this is what we find in algebraic geometry in the duality between (radical) ideals of a finitely generated $k$-algebra and affine varieties. Maximal ideals have the smallest extension but the greatest comprehension.