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)
Henkin showed that the higher-order logic known as Church's simple type theory is sound and complete for what are now called Henkin models. Henkin's paper Completeness in the Theory of Types is not very long and is very readable (once you know that Church and Henkin write $\alpha\beta$ for the type of functions from type $\beta$ to type $\alpha$, which we would now write as $\alpha \rightarrow \beta$).
Surprisingly, because higher-order logic is so much more expressive than first-order logic, Henkin's completeness proof is in many ways a lot simpler than the proof of completeness for first-order logic.