I am working 1 with a certain structure, and I wonder if someone has seen it before. I am no mathematician, so all I can say is that I will do my best to describe this structure. It is actually very simple. I am sure I have seen it (and its interpretation) somewhere, years ago, perhaps in some old first year university textbook on the philosophy of language, but haven't been able to find it.
The structure is a first order theory, with predicates similar to those of a formal set theory (of the ZFC type). The main difference with set theory is that it doesn't incorporate the axioms Fraenkel called "constructive" (e.g. in the introduction to Paul Bernays' "Axiomatic set theory" ), and limits itself to the basic axioms of equality and extensionality and definition of subset.
Appart from this, the theory only defines a tuple operator and a few primitive atoms (see 1, the "words" section). This, and a few relations among these atoms (given by the quasy-set-theoretic predicates outlined above), result in a very simple and limited structure, consistent and complete - as its full expansion is just a handful of sentences.
This structure is used by extending it with new ad hoc atoms, relations among the atoms, and rules (implications), to model natural language "texts". The interesting thing here is to model assertive, factual natural sentences as tuples, instead of as actual formal sentences. As an example, we might have
(john loves sue) belongs_to fact.
Here, 'john', 'loves', 'sue', and 'fact' would be atomic terms, individuals; '(john loves sue)' would be an operation, valued as an individual; '()' would be the tuple operator; and 'belongs_to' would be a predicate symbol.
This allows us to reason about (sufficient enough) sentences of the natural language without any restriction, and use first order variables indistinctly for "facts", "verbs", "nouns", or "names".
I oppose this to the idea of representing natural sentences as formal sentences, using predicate symbols to represent all verbs, and running to limitations with classes, quantification of predicates, and Russell's paradox.
"Copular" sentences (formed with copular verbs, such as "to be") are excluded from the above, and are represented as formal sentences; i.e., the formal predicates are interpreted as the copular verbs. So "a person is a thing", or "john is a person", might be expressed as:
person subset_of thing.
john belongs_to person.
And that's it, more or less.
Does this make any sense? My memory may have failed me and I may have implemented some deranged half baked scheme; On the other hand, I do think that my work with it is allowing me to express some "ontologies" that, in my (limited) experience, cannot be easily expressed with other systems.
Edit in response to the comment:
You are making Triple Knowledge Base. You may find this interesting: ILP & Triple Knowledge Bases Anton
@Anton: What I see as a technological advantage is the separation between copular verbs and other verbs. Consider this:
john isa man. (john loves sue) isa fact.
It allows you to take advantage of the obvious and hard earned correspondence between "to be" and set theory, and at the same time allows you to use other verbs without problems - without running into fundamental antinomies.
In your references, I see the the possibility of saying:
john isa man. john loves sue.
Inmediately after this, you need unrestricted comprehension; you need variables ranging over verbs and predicates. Google for "OWL Full semweb" if you want proof of that need.
That is what Gottlob Frege was doing that Bertrand Russell showed was wrong.
With the first expression, you don't need unrestricted comprehension to keep talking. It's amazing, see  for an example.