# Are there non-trival logics that exibit soundness and completeness that are not first order?

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)

• It is not clear to me what are you meaning with non-trivial... Classical FOL is sound and complete with respect to "standard" semantics. Intuitionistic logic and many modal systems are s&c with respect to the corrisponding Kripke semantics. Second-order logic is s&c with respect to "general" semantics ... – Mauro ALLEGRANZA Dec 2 '14 at 20:50
• That's pretty much the answer I'm looking for – user833970 Dec 2 '14 at 22:06
• @MauroALLEGRANZA Second order logic is complete w.r.t. general semantics? What do you understand by general semantics? – M. Winter May 15 '17 at 19:00

## 1 Answer

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.