So suppose that there is an undirected graph with edge connections known. Now in first-order logic there is quantifier $\forall x$. Then does this automatically refer to vertexes, or can we use relation like $v(x)$ to say that $x$ is a vertex?
-
$\begingroup$ Strictly speaking, no, though the universe (vertices, in your case) is often clear from context and might be omitted. $\endgroup$– Rick DeckerCommented Aug 6, 2014 at 16:56
-
1$\begingroup$ How is universe defined? Is it dependent on the graph input given? So like if a graph is 5-vertex graph, then there is only 5 elements in universe? $\endgroup$– DESCommented Aug 6, 2014 at 17:01
-
1$\begingroup$ Or are we allowed to form any structure out of a graph then form a language/universe? $\endgroup$– DESCommented Aug 6, 2014 at 17:02
-
$\begingroup$ What are you doing or trying to express? $\endgroup$– JuhoCommented Aug 6, 2014 at 18:00
-
$\begingroup$ Yes, when describing graph properties, the universe consists of all vertices, and there's an edge predicate. $\endgroup$– Yuval FilmusCommented Aug 8, 2014 at 3:19
3 Answers
(First-order logic) formulae are independent of structures; you just have variables, predicates and possibly functions (in addition to the syntactical symbols). To decide whether a formula $\varphi$ is true in a given structure $S$ (consisting of a universe of individuals $U$ and an interpretation of predicates $I$), i.e. whether $S$ is a model of $\varphi$, you apply the semantic rules of first order logic.
Concerning your specific question: if you have $\varphi = \forall x: F$ where $F$ is some formula, then $x$ denotes exactly all vertices iff you defined your structure $S = (U,I)$ such that $U$ contains exactly all vertices. Note that if you do that and want access to the edges, then you'll need to define some predicate $e(x,y)$ such that $e(x,y) \Leftrightarrow \text{there is an edge between } x \text{ and } y$.
More generally: the quantifiers do not differentiate between elements of your universe, the predicates will have to do that. If you want to check $F$ only for all vertices but your universe contains elements that are not vertices, then you do what you suggested: introduce a predicate $v(x)$ and use $\varphi' = \forall x: (v(x) \rightarrow F)$
Let me quote from Immerman's survey on descriptive complexity: In Descriptive Complexity we view the input as a finite logical structure. A graph is a logical structure whose universe is the set of vertices and $E_G$ is the binary edge relation.
So when describing graph properties, qualifiers quantify over all vertices, and edges are encoded by a binary relation. This is the convention in descriptive complexity. If you follow some other convention then you might get different behavior.
Typically, when referring to vertices in a graph, one does by the following. Let $G=(V,E)$ be a graph such that $V$ is the set of vertices and $E$ is the set of edges. Then you would proceed $\forall x \in V$ etcetera.