3

A semantic tableaux proof tries to prove that A entails B by using a tree search to try to find a model for $\{A, \lnot B\}$. If a model is found, then A does not semantically entail B, and so cannot syntactically entail B either. If no model is found, then assuming that the search is complete, then there is no model in which both A and $\lnot B$ hold. Hence, in every model where A holds, B holds too. In other words, A semantically entails B.

Are semantic and syntactic entailment the same thing for semantic tableaux proofs, or is there some notion of syntactic entailment distinct from semantic entailment?

Peter Smith
  • 54,743
DavidA
  • 563

2 Answers2

2

I think it is helpful to think along the following lines (which are developed more fully -- with lots of nice tree diagrams which I can't reproduce here! -- in my Intro. to Formal Logic, which you might find helpful).

Think of trees (tableaux) as coming in three flavours. First, we set out to -- as it were -- do a truth table backwards. Instead of evaluating an argument $\varphi_1, \varphi_2, \ldots \varphi_n \therefore \psi$ by hacking through a truth table to see if there is a valuation which makes the premisses true and conclusion false, we go the other way about. We start by assuming that $\varphi_i$ is true, $\varphi_2$ is true, $\ldots$, $\varphi_n$ is true and $\psi$ is false, and then try to see whether we can work backwards to find a valuation which yields these assignments to the $\varphi_i$ and $\psi$. We may have to consider branching possibilities (e.g., from $P \lor Q$ is true, we can only infer that either $P$ is true or $Q$ is true). This sort of doing-a-truth-table-backwards, sometimes having to split our reasoning to consider alternative paths, is naturally set out using signed trees where the nodes on the tree are decorated by expressions of the kind "$\varphi \Rightarrow T$" or "$\psi \Rightarrow F$" (where "$\Rightarrow T/F$" means "is assigned the value $T/F$"). These signed trees are evidently introduced as a way of setting our metalogical semantic reasoning, to establish whether the semantic entailment $\varphi_1, \varphi_2, \ldots \varphi_n \vDash \psi$ holds.

Second, instead of having some wffs assigned $T$ and others assigned $F$, why not just rewrite trees so that every wff appearing on them is assigned $T$? Whenever you are tempted to write "$\varphi \Rightarrow F$" write instead "$\neg\varphi \Rightarrow T$". You'll end up with uniformly signed trees, with every wff decorated the same way.

Third, since in the second version all the wffs are decorated the same way, you can just drop the assignments of values to get unsigned trees. Now, the original motivation for these signed trees remains semantic, so the natural way of reading them, as they are first introduced, is still as shorthand for semantic reasoning to establish semantic entailment.

However, we can now think of these unsigned trees a different way -- as formal proof objects involving no mention of truth (we've dropped the assignments of truth-value remember). And we can define a corresponing notion of syntactic entailment where $\varphi_1, \varphi_2, \ldots \varphi_n \vdash_T \psi$ [that's subscript $T$-for-trees] just when there is a closed tree whose trunk starts $\varphi_1, \varphi_2, \ldots \varphi_n, \neg\psi$. A closed tree can then be regarded as exhibiting a syntactic entailment in this sense. (We then need a proof that trees in any flavour work as advertised, and in particular we will want it to be the case that $\varphi_1, \varphi_2, \ldots \varphi_n \vdash_T \psi$ iff $\varphi_1, \varphi_2, \ldots \varphi_n \vDash \psi$.)

Peter Smith
  • 54,743
  • Are there any circumstances then under which semantic and syntactic entailment could fail to coincide? – DavidA Sep 27 '13 at 18:18
  • Syntactic entailment in which proof-system? – Peter Smith Sep 27 '13 at 18:50
  • Well how about a semantic tableau proof system for classical first-order arithmetic? (Is there a choice of such systems, as there is for Gentzen systems?) – DavidA Sep 27 '13 at 19:06
  • (But my original motivation for asking the question was doubts about semantic tableau for non-classical logics - so if they coincide in the classical but not in the non-classical case, I'm interested to know.) – DavidA Sep 27 '13 at 19:17
  • There are semantic tableau systems for various non-classical logics: see Graham Priest's fantastic An Introduction to Non-classical Logic. – Peter Smith Sep 27 '13 at 19:30
0

When we are talking about finite tableaux (e.g. when the root is labeled with a finite list of formulas), the tableaux are syntactic objects, and they establish syntactic entailment. The fundamental goal of the tableau method is to give finite, syntactic derivations or refutations of mathematical statements.

Indeed, computers are able to manipulate finite tableaux, and I have seen automated theorem provers that use them.

However, because syntactic and semantic entailment are extensionally the same for propositional and first-order logic, tableau derivations also establish semantic entailment.

Carl Mummert
  • 81,604