Instantiation of quantifier with its domain should not be allowed in predicate logic

[kory33]

Current implementation of existential and universal quantifiers express their domain of discourse by a type variable which acts as an upper bound for the type-lambda. 'objects' that are quantified are all types(or classes), and they are all subtypes of the bound type.

Since any class is a subclass of itself, the quantifier can accept a type which is equal to the domain of discourse. This is not suitable for construction of axiom systems such as ZFC, since in ZFC, the domain of discourse(represented as Σ here) should not be treated as a set, as that leads to Russel's paradox.

To solve this, existential quantifier should require that type S(which acts as a existence proof) does not equals D, the domain of discourse.

For now, the universal quantifier is exactly equivalent to a generic function with type bounds. The above-stated change should make universal quantifier a type constructor which is as powerful as a type-bounded generic function with an implicit parameter proving type inequality.

[kory33]

As far as ZFC is concerned, this issue should not have any impact on the deduced axiom system. Although the type Σ acts as a 'class' of all sets in ZFC, it is impossible to deduce the relation _ ∈ Σ for any subclass of Σ(even Σ itself!). Given this, the type Σ should have almost the same meaning as the set given by the set existence axiom, where only the empty set can be obtained through separation.

However, this 'weakness' of the existence of reference to the universe may not be the same for other axiom systems in general, especially when the universe of discourse is talked within the axiom system(if such a system really exists). For the current aims, it is well-defined regarding this issue.