# 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:

1. 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.
2. 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

#### Solutions Collecting From Web of "Complete calculus of first-order logic working for empty structures too"

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.