logic

See also boolean algebra.

Propositional Logic vs Predicate Logic

Propositional Logic (Aussagenlogik):

• Deals with simple true/false statements
• Uses logical operators (∧, ∨, ¬, →, ↔)
• Examples: “It’s raining”, “The sun is shining”

Predicate Logic (Prädikatenlogik):

• Extends propositional logic
• Adds predicates (properties/relations)
• Includes variables and quantifiers (∀, ∃)

A proposition is a statement with a truth value.
A predicate is a function that returns a truth value for given inputs.

Important equivalences

DeMorgan:

$$\begin{array}{r}\neg (A\wedge B)⟺\neg A\vee \neg B\\ \neg (A\vee B)⟺\neg A\wedge \neg B\end{array}$$

Equivalence:

$$a\iff b⟺(a\Rightarrow b)\wedge (b\Rightarrow a)$$

Indirect proof:

$$A\Rightarrow B⟺\neg B\Rightarrow \neg A$$

Implication:

$$A\Rightarrow B⟺\neg A\vee B$$

Predicate logic

In predicate logic, we use predicates to express statements about objects.
E.g.: “$11\text{ is a prime number}$”, $11$ is the subject, $\text{is a prime number}$ is the predicate. We abstract the predicat to $P$, and the subject to $x$: $P(x)=x\text{ is a prime number}$.

Quantors

$\forall xP(x)$: “for all”, “for each”, “for every” $x$ the predicate $P(x)$ is true.
$\exists xP(x)$: “there exists”, “there is” an $x$ for which the predicate $P(x)$ is true.
In maths (as opposed to logic), the notation is usually to put a colon behind the quantor: $\forall x:P(x)$.
If it’s not clear where $x$ comes from, we can specify a domain: $\forall x\in \mathbb{Z}:P(x)$.

$\nexists$: “there does not exist” an $x$ for which the predicate $P(x)$ is true.
$\exists !$: “there exists exactly one” $x$ for which the predicate $P(x)$ is true.

EXAMPLE

$P_1=$ “is a human”, $P_2=$ “is mortal”
“All humans are mortal”: $\forall x:P_1(x)\Rightarrow P_2(x)$

$Q_1=$ “is prime”, $Q_2=$ “is odd”
“Every prime number is either odd or equal to $2$”
$\forall x:Q_1(x)\Rightarrow (Q_2(x)\vee (x=2))$
… which is short for:
$\forall x\in \mathbb{N}:Q_1(x)\Rightarrow (Q_2(x)\vee (x=2))$
… which is short for:
$\forall x:(x\in \mathbb{N})\Rightarrow (Q_1(x)\Rightarrow (Q_2(x)\vee (x=2)))$

Equivalences

$$\begin{array}{rlrlrl}& \forall x\forall yP(x,y)& ⟺& \forall y\forall xP(x,y),& \exists x\exists yP(x,y)& ⟺\exists y\exists xP(x,y),\\ & a\wedge \forall xP(x)& ⟺& \forall x(a\wedge P(x)),& a\vee \exists xP(x)& ⟺\exists x(a\vee P(x)),\\ & a\wedge \exists xP(x)& ⟺& \exists x(a\wedge P(x)),& a\vee \forall xP(x)& ⟺\forall x(a\vee P(x)),\\ & \neg (\forall xP(x))& ⟺& \exists x\neg P(x),& \neg (\exists xP(x))& ⟺\forall x\neg P(x).\end{array}$$

$\forall$ and $\exists$ are not distributive over each other. E.g. $\forall x\exists yP(x,y)\ne \exists y\forall xP(x,y)$

Relating predicates to set theory

Predicates $P(\cdot )$ for a class $\Omega$ can be seen as the sets underlying the set $\Omega$,
Let $A:=\{x\in \Omega :P(x)\}$.
Then

$$\begin{array}{rlrl}& \forall x\in \Omega :P(x)& ⟺& A=\Omega ,\\ & \exists x\in \Omega :P(x)& ⟺& A\ne \varnothing ,\end{array}$$

$A⟹B$ : $A\subseteq B$, i.e. $A\cap B=A$. If $A$ is true, then $B$ must also be true. If $A$ is false, then $B$ can be either true or false.
$A\wedge B$: $A\cap B$, i.e. both $A$ and $B$ are true.
$A\vee B$: $A\cup B$, i.e. at least one of $A$ or $B$ is true.
$A^C$: $\neg A$, i.e. $A$ is false.

Propositional logic

The strictly formal syntax definition from the lecture:

Note: Only the symbols used here allowed; every expression must be enclosed in parentheses.

Alternative notation / terminology:

![[logic-1760348746395.webp]]
![[logic-1760348758819.webp]]
![[logic-1760350968485.webp]]
![[logic-1760351026760.webp]]
![[logic-1760351130505.webp]]

Terminology

Model = Satisfying assignment
Clause = Disjunction of literals (e.g. $a\vee \neg b\vee c$) … set of clauses = CNF
Term = Conjunction of literals (e.g. $a\wedge \neg b\wedge c$) … ) … set of terms = DNF
Empty clause $\perp$
Empty term $\top$

Consequence $\models$

$\models$ means “entails” or “proves”. It is a meta-level claim about all possible truth asignments, denoting that a statement is a logical consequence of another statement / series of statements (it’s a relation between formulas not within formulas).
If $A\models B$, then $B$ is a logical consequence of $A$, by definition whenever $A$ is true, $B$ must also be true.

$\models F$ … the formula $F$ is a tautology (“valid”/“gültig”). The left side (empty set of premises) is $\top$.
$\models \neg F$ … $F$ is a contradiction (“unerfüllbar” / unsatisfiable).
$/\models F$ … $F$ is not true in all interpretations → $F$ is “widerlegbar” (falsifiable / refutable).
$/\models \neg F$ … $F$ is not a contradiction → $F$ is “erfüllbar” (satisfiable).

$a\models a\vee b$ … $a\vee b$ is true whenever $a$ is true. $a,b\models a\wedge b$ … $a\wedge b$ is true whenever both $a$ and $b$ are true. $a/\models a\wedge b$ … $a\wedge b$ is not necessarily true whenever $a$ is true (it also depends on $b$). $\models a\vee \neg a$ … $a\vee \neg a$ is always true (tautology). $/\models a\wedge \neg a$ … $a\wedge \neg a$ is never true (contradiction). $a,a⟹b\models b$ … if $a$ is true and $a$ implies $b$, then $b$ must also be true (modus ponens). $\perp \models a\wedge \neg a$ … from falsehood, anything follows (ex falso quodlibet).

Strength of formulas

A formula $\varphi$ is stronger than formula $\psi$ iff $\varphi \models \psi$, i.e. $\text{Models}(\varphi )\subseteq \text{Models}(\psi )$.
A formula $\varphi$ is weaker than formula $\psi$ iff $\psi \models \varphi$, i.e. $\text{Models}(\psi )\subseteq \text{Models}(\varphi )$.
Formulas $\varphi$ and $\psi$ equally strong iff $\varphi \models \psi$ and $\psi \models \varphi$, i.e. $\text{Models}(\varphi )=\text{Models}(\psi )$ (logical equivalence).

Stronger = more specific = fewer models
Weaker = more general = more models
Equally strong = the same models

EXAMPLE

$a\oplus b$ is stronger than $a\vee b$, since $a\oplus b$ is only true if exactly one of $a$ or $b$ is true, while $a\vee b$ is true if at least one of them is true.
$a\wedge b$ is stronger than $a\vee b$, since $a\wedge b$ is only true if both $a$ and $b$ are true, while $a\vee b$ is true if at least one of them is true.
$\perp$ is the strongest formula. There’s no world in which it is true $\text{Models}(\perp )=\varnothing$, and since $\varnothing \subseteq \text{Models}(F)$ for every formula $F$, $\perp \models F$ for every formula $F$.
$\top$ is the weakest formula. It’s true in every world $\text{Models}(\top )=\text{All}$, and since $\text{Models}(F)\subseteq \text{All}$ for every formula $F$, $F\models \top$ for every formula $F$.

Transclude of SAT

$\varphi$ is valid → $\neg \varphi$ is unsatisfiable
$\varphi$ is refutable → $\neg \varphi$ is satisfiable
$\varphi ⟺\psi$ → $\neg (\psi ⟺\varphi )$ is unsatisfiable
${\varphi }_1,\dots ,{\varphi }_n\models \psi$ → ${\varphi }_1\wedge \cdots \wedge {\varphi }_n\wedge \neg \psi$ is unsatisfiable

Resolution

Resolution proves UNSAT by refutation:
To show a set of clauses is unsatisfiable, you try to derive $\perp$ (a contradiction).
To show a statement $\phi$ is valid (a tautology), you show $\neg \phi$ is unsatisfiable (derive $\perp$).
To show $\Gamma \models \phi$, you add $\neg \phi$ to $\Gamma$, convert to CNF, and try to refute. If you get $\perp$, then indeed every model of $\Gamma$ is a model of $\phi$.

$$\frac{x\vee C\neg x\vee D}{C\vee D}$$

The top two are the parents.
$x$ is the pivot (it appears positive in one parent and negated in the other).
The bottom is the resolvent: you drop $x$ and $\neg x$, and keep the disjunction of what’s left.
$C$ or $D$ could be empty.
If both are empty, resolving $x$ and $\neg x$ gives the empty clause $\perp$ .
If one is empty, you get a clause with just the literals from the other parent.

Resolution is used on formulas in CNF. You repeatedly apply the rule to the set of clauses to derive new clauses.

Two key meta-properties:
Sound: every resolvent you derive is a logical consequence of the parents (and thus of your original clauses). So you never “invent” something false ($A\wedge B\models R$, where $R$ is the resolvent of parents $A$ and $B$).
Complete (for refutation): if your clause set is unsatisfiable, then by applying resolution cleverly enough, you can eventually derive the empty clause . (So if it’s impossible to satisfy all clauses, resolution can prove that.)

Derivation of a tautology: From $x\vee a$ and $\neg x\vee \neg a$, pivot on $x$; the resolvent is $a\vee \neg a$, which is $\top$ (always true). This is sound (because $\top$ follows from anything), just useless—a tautology doesn’t constrain anything and doesn’t help you reach a contradiction, so it can be safely discarded.

Sequent

$${\phi }_1,\dots {\phi }_n⊢\psi$$

… from assumptions (or atecedent / context) ${\phi }_1,\dots ,{\phi }_n$, we can derive the goal (or succedent) $\psi$.

Assuming all ${\phi }_i$, you can prove $\psi$ (e.g. $a,a⟹b⊢b$; modus ponens).
When there are no assumptions, we just write $⊢\psi$, i.e. $\psi$ is valid / a tautology (e.g. $⊢a\vee \neg a$).
$K\dots {\phi }_i⊢\psi$ is notation for highlighting that ${\phi }_i$ is in the context $K$.
Order of assumptions doesn’t matter.

Relation to $\models$:
$\Gamma ⊢\psi$ … there is a proof of $\psi$ from assumptions $\Gamma$.
$\Gamma \models \psi$ … every model that satisfies all formulas in $\Gamma$ also satisfies $\psi$.
${\phi }_1,\dots ,{\phi }_n⊢\psi$ iff ${\phi }_1,\dots ,{\phi }_n\models \psi$

$\frac{\text{premise sequents}}{\text{conclusion sequent}}$

?????????????????????????????????????????????????????????????

you can imagine it as a graph. when you have the left side, A1, A2, ..., then you can assume that the right side is true / you can walk to the next node. it's essentially a more fancier form of the modus ponens: A1 and A2 and ... => B1, B2, ... So in classical logic, you can essentially "weaken" (replace) your A's with B's. (and in this tree-ish notation, you put the right side below to left side, A1, ... |- B1, ...)

https://notes.lukasl.dev/Knowledge/Resolution-(Logic)

so you put things on the right side (ors) to the left and negate them
then you eliminate the double negation
then you turn ands into commas since you can view them independently ofc
then you take that other or term to the left, negate it
and then…idfk

this is the best lecture I’ve ever had. just stating definitions and axioms and algorithmis to apply like a calculator with 0 motivation or intuition or build up. reminds me of my high school math classes.

https://chatgpt.com/c/68efe8e3-a964-8326-b599-1b85f72199a8