In our logic class, we just we just completed the proofs of soundness and completeness. To me, these proofs hinge on models being filtered through first order logic.
For instance, I could set up a trivial formal system, with only one wff. Let's say that it is "yes".
For soundness, I define a mapping from any model to "yes".
For completeness, if given "yes", I return a model that exhibits "yes", so return your favorite model (Natural numbers with less then?).
Are there any nontrivial formal systems that have soundness and completeness?
(As always, apologies if this is a silly question)