How to think of formal derivation $\Gamma \vdash \phi$ in terms of trees/graphs?

99 Views Asked by At

According to my text, a finite set of formulas $\Gamma$ in a given language $L$ is derivable, denoted $\vdash \Gamma$, if $\Gamma$ belongs to the least collection of finite sets of formulas, denoted $X$, such that:

1) If $\Delta \cup\{\phi\} \in X$ and $\Delta \cup\{\psi\} \in X$ then $\Delta \cup \{(\phi \wedge \psi)\} \in X$.

2), 3), 4) Similar rules for $\lor$, $\exists$ and $\forall$. I don't want to get bogged down in definitions, I think this won't be important.


I try to think of $X$ as a tree. Where the branches are created by these four rules of inference, so that if a node represents a subset of formulas that include, for example, $\phi$ and $\psi$, then it can branch into that same subset of formulas with $\phi \wedge \psi$ included. This way, $X$ is the set of all well-formed formulas one can create from the language $L$ with the usual rules of inference. Is this a correct/standard approach to visualizing derivability? If so, what would the root node of this tree be? Should I think of $X$ as an inverted tree where all the atoms of $X$ form an initial node from which rules of inference can be used to grow further branches to infinity? This seems like it would no longer be a tree but some other sort of graph.


Now, the book defines: $\Gamma \vdash \phi$ if there exists a finite subset $\Gamma_0 \subseteq \Gamma$ such that $\vdash (\sim \Gamma_0) \cup \phi$.

This makes sense, if everything in $\Gamma_0$ holds then $\sim \Gamma_0$ does not hold so that $\phi$ must hold. The intuition is clear. However, how do I fit this into the picture of $X$ as a tree described above? Is $\phi$ derivable from $\Gamma$ if I can find a branch of this tree that contains all the formulas in the set $(\sim \Gamma_0) \cup \phi$? This seems a little unnatural, I think of a proof as exploring the tree starting from $\Gamma$ and branching out until I find $\phi$, not negating all of $\Gamma$.

1

There are 1 best solutions below

0
On

$X$ isn't a tree nor are the elements of $X$1. What is a tree is the evidence that some formula is an element of $X$. To state this a bit more formally, $\varphi\in X$ if and only if there exists a tree with root $\varphi$ satisfying some rules. These trees are usually called derivations. There can be multiple derivations of a single formula. Derivations are often illustrated in the following way: $$\dfrac{\dfrac{\vdash \varphi \qquad \vdash \psi}{\vdash \varphi\land \psi}\qquad\vdash \chi}{\vdash (\varphi\land\psi)\land\chi}$$ which clearly illustrates a tree-like structure.

You can and it would be a good exercise to give a formal construction of the set of derivations. You could then prove something like: $\vdash \varphi \iff \exists d\in\mathcal D.\mathsf{root}(d)=\varphi$ where $\mathcal D$ is the set of derivations and $\mathsf{root}$ is a function which gives you the formula that $d$ is a derivation for. (You could represent this in some other way, e.g. as a relation producing: $\vdash \varphi\iff \exists d.(x,d)\in\mathcal D$.

1 Well, they might be depending on how you represent formulas.