Logic.page (3530B)
1 # Basic terminology 2 3 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. 4 5 Unlike in some mathematical fields, none of the logics presented here feature **function symbols**, so we are defining **function-free logics** in the terminology of these fields. 6 7 # First-order logic 8 9 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 10 11 - 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$) 12 - optionally, **equality atoms** of the form $x = y$ (see [Equality](#equality) below) 13 - existential quantification $\exists x ~ \phi$ 14 - universal quantification $\forall x ~ \phi$ 15 16 ## Bound and free variables 17 18 TODO inductive def 19 20 A formula is called **Boolean** if it has no free variables. 21 22 ## Constants 23 24 A formula features **constants** if TODO. 25 26 ## Equality 27 28 We may talk of first-order logic **with equality**, or **without equality**, to indicate whether formulas are allowed to contain 29 30 ## Satisfaction of a formula 31 32 The notion of a structure $S$ **satisfying** a Boolean FO formula $\phi$ is defined inductively on the subformulas of $\phi$ in the expected way: 33 34 TODO 35 36 If $\phi$ holds in $S$, we can equivalently say that $S$ **satisfies** $\phi$. 37 38 Satisfaction can also be defined using [Logical games](). 39 40 ## Examples 41 42 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](Constraint languages#tuple-generating-dependencies). 43 44 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](Constraint languages#functional-dependencies). 45 46 ## Inexpressivity results and useful properties 47 48 - 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](). 49 50 - 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. 51 52 # Fixpoints 53 54 TODO 55 56 # Second-order logic 57 58 TODO 59 60 # Problems 61 62 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. 63 64 The [satisfiability problem]() asks, given a Boolean logical formula $\phi$, whether there is a structure $S$ that satisfies $\phi$.