tcswiki

wiki-style
git clone https://a3nm.net/git/tcswiki/
Log | Files | Refs

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$.