Usually, in model theory, one presupposes that structures (models) are non-empty. I don’t like this (related: What's the deal with empty models in first-order logic?). So let us explicitly permit empty structures.
My requests are:
- Can you give a complete calculus of first-order logic that works for empty structures too? By “working for empty structures too”, I mean that if the demanded calculus proves a sentence, then this sentence should hold in all structures, also in the empty structures.
- Can you give a completeness proof for this calculus?
You may wonder: why don’t you look in the standard logic texts, where a complete calculus + proof of the completeness should be given?
But my problem is: In every logic text which allows empty models, they do not give a complete calculus and proof the completeness. Instead, they prove the compactness theorem and other standard results with purely model theoretic methods, rather than proof theoretic methods. Examples of such texts:
There is a full treatment of empty-domain models in MENDELSON: Introduction to Mathematical Logic. You will see there why they are a special case of First Order Logic.