Complete calculus of first-order logic working for empty structures too
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:
- http://math.uga.edu/~pete/modeltheory2010FULL.pdf
- http://www.math.uni-hamburg.de/home/geschke/teaching/ModelTheory.pdf
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.