Anki Deck Changes

However, it's never possible to create a proof system that captures all such statements, especially self-referential statements.

The syntax defines:
1. An alphabet \(\Lambda\) of allowed symbols
2. Which strings in \(\Lambda^*\) are valid formulas (syntactically correct)

If \(i \in free(F)\), then the symbol is said to occur free in \(F\).

The semantics defines:
1. A function \(free\) that assigns to each formula which symbols occur free
2. A function \(\sigma\) that assigns truth values to formulas under interpretations
3. The meaning and behavior of logical operators

Often the domain is defined in terms of the universe \(U\) where a symbol can be a function, predicate or element of \(U\).

They are the same! In logic, one often writes \(\mathcal{A}(F)\) instead of \(\sigma(F, \mathcal{A})\) and calls \(\mathcal{A}(F)\) the truth value of \(F\) under interpretation \(\mathcal{A}\).

If \(\mathcal{A}\) is not a model for \(M\) one writes \(\mathcal{A} \not\models M\).

It's unsatisfiable otherwise: denoted \(\perp\).

Symbol: \(\top\)
Also written as \(\models F\)

\(F\) model for \(G\) means:  \(\mathcal{A} \models F \implies \mathcal{A} \models G\).

Each one is a logical consequence of the other: \(F \models G\) and \(G \models F\).

Thus \(\{F_1, \dots, F_n\}\) is equivalent to \(F_1 \land \dots \land F_n\).

\(F \models \emptyset\) means that \(F\) is unsatisfiable, as the empty set cannot be made true under any interpretation (it has no literals to set to true).

This is a notational convention.

This is important for resolution calculus!

The fact that \(F \models G\) is equivalent to \(\{F, \lnot G\}\) being unsatisfiable makes the resolution calculus powerful enough to also show implications, not just unsatisfiability.

There are also calculi in which more complex objects are manipulated.

Formally, a derivation rule \(R\) is a relation from the power set of the set of formulas to the set of formulas.

More precisely: \(M_0 := M\), \(M_i := M_{i-1} \cup \{G_i\}\) for \(1 \leq i \leq n\), where \(N \vdash_R G_i\) for some \(N \subseteq M_{i-1}\) and for some \(R_j \in K\), and where \(G_n = G\).

more complex formulas, ex: \(\{(A \lor B) \land (C \lor B)\} \vdash_R A \lor B\)

Hence, it's sound and complete if \(M \vdash_K F \Leftrightarrow M \models F\).

(modus ponens)

(case distinction)

A truth assignment \(\mathcal{A}\) is suitable for a formula \(F\) if it contains all atomic formulas appearing in \(F\).

For every row evaluating to 0:
1. Take the disjunction of \(n\) literals
2. If \(A_i = 0\) in the row, take \(A_i\)
3. If \(A_i = 1\) in the row, take \(\lnot A_i\)
4. Then take the conjunction of all these rows

This works because \(F\) is \(0\) exactly if every single disjunction is true, which is the case by construction.

Rows evaluating to 0.

- If \(A_i = 0\) in the row, take \(A_i\)
- If \(A_i = 1\) in the row, take \(\lnot A_i\)

- Within a row: disjunction (\(\lor\))
- Across rows: conjunction (\(\land\))

For every row evaluating to 1:
1. Take the conjunction of \(n\) literals
2. If \(A_i = 0\) in the row, take \(\lnot A_i\)
3. If \(A_i = 1\) in the row, take \(A_i\)
4. Then take the disjunction of all these rows

This works because \(F\) is \(1\) exactly if one of the rows is \(1\), which is the case by construction.

Rows evaluating to 1.

- If \(A_i = 0\) in the row, take \(\lnot A_i\)
- If \(A_i = 1\) in the row, take \(A_i\)

- Within a row: conjunction (\(\land\))
- Across rows: disjunction (\(\lor\))

We can construct many equivalent ones.

Example: \(\{A, \lnot B, \lnot D\}\) is a clause. The empty set \(\emptyset\) is also a clause.

 \[K = (K_1 \setminus \{L\}) \cup (K_2 \setminus \{\lnot L\})\]

NO! The resolution calculus doesn't allow removing two complementary literals at once.

The derivation \(\{A, \lnot B\}, \{\lnot A, B\} \vdash_{\text{res}} \emptyset\) is wrong and illegal!

For \(A = 1\), \(B = 1\) both clauses are true, so this would derive unsatisfiability from satisfiable clauses.

If \(\mathcal{A}\) models the set \(K_1, K_2\) then it makes at least one literal in both true. Case distinction:
- If \(\mathcal{A}(L) = 1\), then \(K_2\) (which has \(\lnot L\)) must have at least one other literal that evaluates to true, so the union (resolvent) is also true
- Similarly for \(\mathcal{A}(L) = 0\)

Show that \(M \cup \{\lnot F\} \vdash_{\text{res}} \emptyset\).

This works by Lemma 6.3: \(M \models F\) is equivalent to \(M \cup \{\lnot F\}\) being unsatisfiable.

embedded into predicate logic as a special case.
We extend it by the concept of predicates.

Function symbols for \(k = 0\) are called constants.

For \(k = 0\) one writes no parenthesis (constants).

YES! The same variable can occur both bound in one place and free in another.

We can then replace all occurrences of the bound variable with another letter without changing the meaning.

YES! Quantifier order matters for nested variables.

\(\exists x \forall y P(x, y)\) is NOT equivalent to \(\forall y \exists x P(x, y)\)!

Example: \(\exists x \forall y (x < y)\) means "there exists a smallest element", while \(\forall y \exists x (x < y)\) means "for every element, there exists a smaller one".

For example, \(\exists x \forall y P(x, y)\) is not equivalent to \(\forall y \exists x P(x, y)\).

If the \(\exists\) is the first quantifier in the formula, then it doesn't depend on anything, and we can just replace it by a constant function \(a\) that always returns the \(x\) for which our formula is true: \(\exists x f(x) \equiv f(a)\).

\[\forall s \forall x \forall y F(s, f(s), x, y, g(s, x, y))\]

The \(t\) depends only on \(s\), so it becomes \(f(s)\). The \(z\) depends on \(s\), \(x\), and \(y\), so it becomes \(g(s, x, y)\).

We can eliminate the quantifier by replacing \(x\) by one specific \(t\). As \(F\) is true for all \(x\), this holds for the free variable \(t\).

\(\lor\)

\(\land\)

The premises or preconditions.

A formula of the form \[Q_1 x_1 \ Q_2 x_2 \ \dots \ Q_n x_n G\]where the \(Q_i\) are arbitrary quantifiers and \(G\) is a formula free of quantifiers.