git clone
Log | Files | Refs

commit cccd5fd093787466a34fbc945fb85df08ad376e5
parent aaabefd23fdc873434433891c9d1a32348f58b48
Author: a3nm <>
Date:   Sun, 17 Jun 2018 01:39:01 +0200


Diffstat: | 62++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 62 insertions(+), 0 deletions(-)

diff --git a/ b/ @@ -0,0 +1,62 @@ +# Basic terminology + +A **signature** (with relation names and arities) is defined [like in databases](Basic database terminology#signatures). A **structure** for a signature $\sigma$ consists of a **domain** of elements and an **interpretation** for each relation $R$ of $\sigma$, i.e., a set of $n$-tuples of elements of the domain, where $n$ is the arity of $R$. This definition is similar to that of a [database instance](Basic database terminology#instances) except that the domain is explicitly given, and it may be the case that some domain elements do not occur in the interpretation of any relation. + +# First-order logic + +A **first-order logic** formula is defined over a [signature](Basic database terminology#signatures) $\sigma$, and consists of an expression built from [atoms](Basic database terminology#facts-and-atoms) and using + +- the logical connectives $\land$ (AND), $\lor$ (OR), and $\neg$ (NOT), as well as connectives that can be defined using those, e.g., the implication $\rightarrow$ (where $x \rightarrow y$ is equivalent to $\not x \lor y$) +- optionally, **equality atoms** of the form $x = y$ (see [Equality](#equality) below) +- existential quantification $\exists x ~ \phi$ +- universal quantification $\forall x ~ \phi$ + +## Bound and free variables + +TODO inductive def + +A formula is called **Boolean** if it has no free variables. + +## Constants + +A formula features **constants** if TODO. + +## Equality + +We may talk of first-order logic **with equality**, or **without equality**, to indicate whether formulas are allowed to contain + +## Satisfaction of a formula + +The notion of a structure $S$ **satisfying** a Boolean FO formula $\phi$ is defined inductively on the subformulas of $\phi$ in the expected way: + +TODO + +If $\phi$ holds in $S$, we can equivalently say that $S$ **satisfies** $\phi$. + +Satisfaction can also be defined using [Logical games](). + +## Examples + +One example of a first-order logic formula is the Boolean formula $\phi: \forall x ~ R(x) \rightarrow \exists y ~ S(x, y)$, stating that for every $x$ in the unary relation $R$ there exists an $y$ to which it is connected by the binary relation $S$. This formula $\phi$ is also a [tuple-generating dependency](Constraints#tuple-generating-dependencies). + +Another example is the formula $\psi: \forall x \, y \, y' ~ R(x, y) \land R(x, y') \rightarrow y = y'$. This formula $\psi$ is also a [functional dependency](Constraints#functional-dependencies) + +## Inexpressivity results and useful properties + +- Consider the signature $\sigma$ of [directed graphs](Basic graph terminology#directed-graph) consisting of one binary relation. It is known that first-order logic cannot express the formula $\phi$ asserting that the graph is connected: this is a consequence of [locality](). + +- The [zero-one law]() intuitively states that the probability of any first-order logic formula is either 0 or 1 as the domain size of structures goes to infinity. + +# Fixpoints + +TODO + +# Second-order logic + +TODO + +# Problems + +The [model-checking problem]() asks, given a Boolean logical formula $\phi$ and a structure $S$, whether $\phi$ holds in $S$. It is the analogue of the [query evaluation problem]() in databases. + +The [satisfiability problem]() asks, given a Boolean logical formula $\phi$, whether there is a structure $S$ that satisfies $\phi$.