Beth definability theorem

This section needs expansion. You can help by adding to it. (April 2014)

The Beth definability theorem states that for first-order logic a property (or function or constant) is implicitly definable if and only if it is explicitly definable. Further explanation is provided under Beth definability.

Semantic tableaux

Beth's most famous contribution to formal logic is semantic tableaux, which are decision procedures for propositional logic and first-order logic. It is a semantic method—like Wittgenstein's truth tables or J. Alan Robinson's resolution—as opposed to the proof of theorems in a formal system, such as the axiomatic systems employed by Frege, Russell and Whitehead, and Hilbert, or even Gentzen's natural deduction. Semantic tableaux are an effective decision procedure for propositional logic, whereas they are only semi-effective for first-order logic, since first-order logic is undecidable, as showed by Church's theorem. This method is considered by many to be intuitively simple, particularly for students who are not acquainted with the study of logic, and it is faster than the truth-table method (which requires a table with 2ⁿ rows for a sentence with n propositional letters). For these reasons, Wilfrid Hodges for example presents semantic tableaux in his introductory textbook, Logic, and Melvin Fitting does the same in his presentation of first-order logic for computer scientists, First-order logic and automated theorem proving.

One starts out with the intention of proving that a certain set ${\displaystyle \Gamma \,}$ of formulae entail another formula ${\displaystyle \varphi \,}$, given a set of rules determined by the semantics of the formulae's connectives (and quantifiers, in first-order logic). The method is to assume the concurrent truth of every member of ${\displaystyle \Gamma \,}$ and of ${\displaystyle \neg \varphi }$ (the negation of ${\displaystyle \varphi \,}$), and then to apply the rules to branch this list into a tree-like structure of (simpler) formulae until every possible branch contains a contradiction. At this point it will have been established that ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ is inconsistent, and thus that the formulae of ${\displaystyle \Gamma \,}$ together entail ${\displaystyle \varphi \,}$.

Beth models

This section needs expansion. You can help by adding to it. (April 2014)

These are a class of relational models for non-classical logic (cf. Kripke semantics).