0

I am really struggling to build intuition with regards to how to do this sort of question.

The abstract: A graph is a set (whose elements are called nodes) together with a symmetric relation on that set (related nodes are said to have an edge between them). A binary tree is a graph which has a distinguished node, called the root, which is connected to two other (distinct) nodes, and every other node is connected to three distinct nodes or one (distinct) node.

The question: How would I define a suitable set of predicate symbols and function symbols together with their arities that give rise to a first order language suitable for specifying binary trees?

  • 1
    A domain for the variables dentong the vertex and a binary relation $E$ such that $E(x,y)$ holds if the two vertex $x,y$ are connected by and edge. – Mauro ALLEGRANZA Jan 19 '15 at 17:36
  • How would I define the predicate and function symbols? –  Jan 19 '15 at 18:02
  • the predicate symbol for "$x$ and $y$ connected by an edge" is as per @MauroALLEGRANZA described. I do not think you need any function symbols to specify a binary tree. – jh4 Jan 19 '15 at 18:37
  • oh ok, its just the question was 4 marks –  Jan 19 '15 at 18:40
  • I really do not understand this topic, what is the intuition to get that answer? What is the domain for the variables denoting the vertex? –  Jan 19 '15 at 18:53
  • The question asks for function symbols though as well –  Jan 19 '15 at 18:59

1 Answers1

0

A graph is a pair $\mathcal G = (V,E)$ where $V$ is a set of elements called vertices (or nodes) and $E$ is an anti-reflexive and symmetric binary relation on $V$ called the edge relation.

This means that the relation $E$ must satisfy the following axioms :

$\forall x \lnot E(x,x)$

meaning that there is no edge "looping" on a single vertice (this is anti-reflexivity), and :

$\forall x \forall y (E(x,y) \rightarrow E(y,x))$

meaning that if there is and edge connecting the vertices $x$ and $y$, the same edge connects $y$ and $x$ (this is symmetry).


For a binary tree we can try adding to the above language an individual constant $r$ for the root and a unary function symbol : $f$ for the "father" of a node.

They have to satisfy the following axioms :

$\forall x (x \ne r \rightarrow \exists y (x = f(r)))$

$\forall x \forall y \forall z(E(x,y) \land E(x,z) \rightarrow (x=f(y) \land x=f(z)))$.

  • Hey I am not allowed to post anymore questions today because I have reached my 24 hour limit therefore I will ask you here. In sequent calculus, how do you know whether to use left inference rules or right inference rules? –  Jan 19 '15 at 20:48
  • @user204450 - in sequent calculus working bottom-up (i.e. in a root-first proof search) the R rules give as a conclusion a sequent with the principal formula, i.e., the formula with the connective of the rule, at right of the derivability relation symbol ($\vdash$); the L rules with the principal formula at left. – Mauro ALLEGRANZA Jan 19 '15 at 21:06
  • Thanks, what about cut rule? Where does the extra A come from in the cut rule theorem? –  Jan 19 '15 at 21:24
  • so how does the formula change in relation to using the right or left inference rules? –  Jan 19 '15 at 21:29