Table of Contents

Logic and Computation

Introduction

Superficial knowledge of computational complexity theory is assumed. You should be familiar with concepts such as PTIME, EXPSPACE etc.

Other than that, notes should be mostly self-sufficent for someone with the knowledge of at least basic set theory and simple combinatorics.

Due to nature of these notes we will mostly work in second-order ordinary set-theoric logic.

TODO. Add appendix for these prerequisites to superficially define them, or redirect to my or to online other resources.

Resources

Notation

10. Propositional Logic

Syntax and Semantics

Theorems and definitions we prove and define here are actually meta-theorems and meta-definitions in our meta-language. Note that we haven’t yet shown propositional logic (which is also called zeroth-order logic) is a subset of our meta-language. It is just, kind of, nonsense syntax at this moment.

Notation. Truth

Syntactically, we will use the symbols

Semantically, we will use the symbols

Def. Alphabets and Words

By an alphabet \Sigma we mean a non-empty set of symbols (or letters).

A finite sequence of symbols over an alphabet \Sigma is called a word (or a string). Moreover, \Sigma^* denotes the set of all words and the length of a word w is the number of letters (that is size of the finite sequence) denoted with |w|. The empty word denoted with \epsilon is the word of length 0.

Def. Language and Syntax

Let \Sigma be an alphabet. Any subset L of \Sigma^* is called a (formal) language over \Sigma. Moreover, let

L = \Set{w \in \Sigma^* | \varphi(w)}

be a language and \varphi be the definition of that language, then \varphi is called the syntax of the language L.

Thm. Cardinality of \Sigma^*

Let the alphabet \Sigma be at most countable, then the set \Sigma^* of words over \Sigma is countable.

Def. Propositional Formulas

Let \mathcal{P} be a, possibly empty, countable set called the atomic formulas (or prime formulas).

The set \mathcal{L}_0(\mathcal{P}) called the propositional formulas for the atomics \mathcal{P} defined inductively as the smallest set such that:

  1. \mathcal{P} \subseteq \mathcal{L}_0(\mathcal{P}),
  2. If F \in \mathcal{L}_0(\mathcal{P}), then \neg F \in \mathcal{L}_0(\mathcal{P}),
  3. If F, G \in \mathcal{L}_0(\mathcal{P}), then \land \> F \> G \in \mathcal{L}_0(\mathcal{P}),

This definition of formulas until here suffice as we can define other operators from \neg and \land. Indeed, we will sometimes use only these when proving theorems (or even defining concepts).

With just the NAND operator, \bar{\land}, alone, it is possible to build other logical operators, so that (2) and (3) can be reduced to \bar{\land} \> F \> G and negation and logical and can be semantically defined via NAND.

Notice that \mathcal{L}_0(\mathcal{P}) is a language over \Sigma = \mathcal{P} \cup \{\neg, \land \} with the syntax given above where intersection of \mathcal{P} and the logical connectives is empty.

When we refer an object F as a propositional formula, we simply mean it is an element of \mathcal{L}_0(\mathcal{P}) for some set of atomic variables \mathcal{P}.

With the use of Polish Notation here we have removed the need for parenthesis so that, for example, \land \neg \> A \> B means (\neg A \land B). Since we know the arity of each operator, compositions of operators is also well-defined (exercise). But note that this notation, although this is the way we defined, is hard to follow for us mere humans, so we will mostly stick to our classical infix notation for the rest of the notes. Moreover, when using infix notation, we will omit the use of brackets for readibility when it is appropriate.

Finally, we will denote the propositional logic with \bot as its only atomic formula with \mathcal{L}_0 that is \mathcal{L}_0 := \mathcal{L}_0(\{\bot\}).

One could, of course, relax or even contradict these definitions, which is not uncommon in logic. What matters is the core intuition.

Def. Syntactic Identity

With =, we will denote the syntactic identity. That is, if F and G are strings and are formulas, then F=G will simply denote they are strings of symbols of same lenght with same symbols in each place. Notice that this is a semantic defintion for our syntactic model.

Notation. Operators

Given the logical operators \neg and \land and the atomic variable \bot, we define for formulas F and G

Notice that we have just defined some syntactic abbreviations, didn’t prove anything. Exercise and write these polish notational definitions in ordinary infix notation.

Def. Subformula

The subformula function \text{sub} is defined on the language \mathcal{L}_0(\mathcal{P}) inductively as

\def\arraystretch{1.25} \begin{array}{rcl} \text{sub}(p) &:=& \{p\} \\ \text{sub}(\neg p) &:=& \{p\} \\ \text{sub}(\land \> p \> q) &:=& \{p, q\} \\ \end{array}

where p and q are atomic formulas in \mathcal{L}_0(\mathcal{P}). Moreover, the proper subformula function \text{sub}^+ is defined as

\text{sub}^+ := \text{sub}(p) \setminus \{p\} .

Thm. Principle of Induction on Propositional Formulas

Since we are going to use induction heavily, we will prove that if \phi is any property which

  1. Holds for all atomic formulas,
  2. If holds for F, it also holds for \neg F, and
  3. If holds for F and G, it also holds for \land \> F \> G,

Then \phi holds for all formulas (of propositional logic).

Proof


TODO:

Def. Formation Sequence for Propositional Formulas

Let’s stick to ordinary infix notation from now on until we define the syntax of first-order logic.

A finite sequence (F_0, ..., F_n) is called a formation sequence for the formula F if F = F_n and for all i \leq n, either

  1. F_i is atomic formula, or
  2. there exists j,k \lt i such that, either
    1. F_i = \neg F_j,
    2. F_i = (F_j \land F_k).

Example

For example, for atomics p_0, p_1, p_2 \in \mathcal{P} the sequence

(p_0, p_1, (p_1 \land p_0), \neg (p_1 \land p_0))

is a formation sequence for \neg (p_1 \land p_0), as is

(p_0, p_1, p_0,(p_1 \land p_0), (p_0 \land p_1), \neg (p_1 \land p_0))

Thm. Existence of Formation Sequence

Every propositional formula has a formation sequence.

Def. Valuation

Given a set \mathcal{P} of atomic variables, a valuation (or assignment) v is a function

v: \mathcal{P} \to \mathcal{V} = \{\mathbb{T}, \mathbb{F}\}

which simply assigns semantic true or false to atomic variables.

So from now on, depending on context, we may assume \bot \in \mathcal{P} and always define v(\bot) = \mathbb{F}, thus v(\top) = \mathbb{T}.

Ponder what would happen if it were the case that \mathcal{V} = [0,1] where \mathbb{F} = 0 \in \R and \mathbb{T}=1. Obviously, most of our definitions and theorems wouldn’t make sense in this setting.

Def. Evaluation

Let F be a formula and v some valuation. We will abuse notation and also use v(F) for the evaluation of a formula F, defined naturally.

If v(F) = \mathbb{T}, then we say v models F denoted by v \models F. Equivalently, we say F holds under v.

Notice that this is the first time we have defined the sign \models.

Def. Satisfiability

A formula F is said to be satisfiable if there exists an valuation v such that v \models F. Otherwise, it is called unsatisfiable.

Def. Tautology and Contradiction

Def. Entails

We say a formula F entails the formula G denoted by F \models G if every valuation which models F also models G. In this case, we also say G is a consequence of F.

Notice how we are overloading (and will keep on overloading) the infix notation \models with valuations, formulas etc. So the elements left or right handside of “models” sign is context-dependent.

Def. Semantic Equivalence

Let F and G be formulas. If they entail each other, then we say they are equivalent. This is denoted by F \equiv G.

Exercise 1. Symmetry of \land

(F \land G) \equiv (G \land F)

Exercise 2. Distributivity Rules

Exercise 3. De Morgan’s Rules

Def. A Set of Formulas

From now on, when we say \Gamma is a set of formulas, we will mean \Gamma \subseteq \mathcal{L}_0(\mathcal{P}). So it is not the set of formulas, but rather a set of formulas.

We will make use of the letters such as \Gamma, \Delta to usually denote a set of formulas and uppercase latin letters A, B, F, G, ... et cetera to denote formulas.

Moreover, we’ll overload the \models notation further in respect to this notion. Let \Gamma be a set for formulas such that \Gamma = \Set{F_0, F_1, ...}, then we say

Now, let’s look at some basic semantic properties of propositional logic.

Thm. Semantic Modus Ponens

Let \Gamma be a set of formulas and A, B formulas. If \Gamma \models A and \Gamma \models (A \to B), then \Gamma \models B.

Thm. Compactness (1)

Let \Gamma be a set of formulas. If \Gamma is satisfiable, then so is every finite subset of it.

This is the easy (to prove) direction of what is called the compactness (of propositional logic), we will see the other direction is also true in the later sections.

Thm. Semantic Monotonicity

Let \Gamma and \Delta be a set of formulas such that \Gamma \subseteq \Delta and F a formula. If \Gamma \models F then \Delta \models F.

Thm. Semantic Transitivity

Let \Gamma and \Delta be a set of formulas and A,B formulas. If \Gamma \models A and \Delta \cup \{A\} \models B, then \Gamma \cup \Delta \models B.

Thm. Semantic Deduction Theorem

Let \Gamma be a set of formulas and F a formula. Then, \Gamma \models F if and only if \Gamma \cup \{\neg F\} is unsatisfiable.

20. Propositional Derivations

We want to formally define a syntactic model such that given a set of assumptions (or axioms; whatever they are) we want to derive (reach) further truths (of the model) based on these assumptions. Of course, those truths of our model should also somehow correspond to truths in our meta-model (or meta-language). It wouldn’t really make sense otherwise. So, all it takes is to blindly follow the syntactic rules of our syntactic model to reach our semantic truths. In essence, that is what a derivation system is. We derive further truths from assumptions (which we usually assume to be the truth) with syntactic wizardry.

In this section we will define \vdash notation called the derives which is pretty similar to \models except models was being used semantically whereas \vdash will be used syntatically.

In propositional logic, with \models we were able to keep track of entailment. That is, given a set of formulas \Delta, we said \Delta entails F written as \Delta \models F. It simply meant that for each valuation which holds for the set \Delta also holds for F. Philosophically, we gave the meaning of being true in the form of boolean truths. We will further explore this concept later on.

In propositional logic, with \vdash we want to do something similar, but syntatically. From a set of formulas \Delta we want to be able to arrive true formulas F such that they are also (correspondingly) true in our meta-theory.

Def. Derives

Let \Gamma be a set of formulas and F, G, and H formulas. Then we define (for our propositional logic model) the derives operator \vdash by the (basic) rules of derivations which are

\def\arraystretch{1.25} \begin{array}{llll} \text{\small Premise} && \text{\small Conclusion} & \text{\small Name} \\ \hline G \in \Gamma && \Gamma \vdash G & \text{\small Assumption} \\ \Gamma \vdash G \text{ and } \Gamma \subseteq \Delta && \Delta \vdash G & \text{\small Monotonicity} \\ \Gamma \vdash G && \Gamma \vdash \neg \neg G & \text{\small Double }\neg \\ \Gamma \vdash F \text{ and } \Gamma \vdash G && \Gamma \vdash (F \land G) & \land\text{\small -Introduction} \\ \Gamma \vdash (F \land G) && \Gamma \vdash F & \land\text{\small -Elimination} \\ \Gamma \vdash (F \land G) && \Gamma \vdash (G \land F) & \land\text{\small -Symmetry} \\ \end{array}

Note that, for brevity, we didn’t include the rules for brackets such that (F) and F are derived from each other etc.

We can extend these rules of derivations in any way we want (as long as it makes sense which we will define later), for example to include \lor and \to.

We can also reduce these rules, indeed we only need 3 which is a topic of no concern in these notes.

Def. Syntactic Proof

A syntactic proof (sometimes called formal proof, or simply a proof if not to be confused with a proof in our meta-language) in propositional logic is a finite sequence of statements of the form \Gamma \vdash F where \Gamma is a set of formulas and F is a formula.

Notice how a syntactic proof is our “witness” to the claim that F is derivable (in our model) from \Delta by following some syntactic rules.

We say F can be derived from \Gamma if there exists a formal proof with the final step \Gamma \vdash F.

Example

Let \Gamma = \Set{(\neg F \lor G)} and derive F \to G from \Gamma.

Solution


\begin{array}{ll:l} \Gamma \cup \{F\} & \vdash F & \text{Assumption} \\ \Gamma \cup \{F\} & \vdash (\neg F \lor G) & \text{Assumption} \\ \Gamma \cup \{F\} & \vdash (F \to G) & (F \to G) \triangleq (\neg F \lor Q) \\ \Gamma \cup \{F\} & \vdash G & \text{Modus Ponens} \\ \Gamma & \vdash (F \to G) & \text{Modus Ponens} \\ \end{array}

Thm. Soundness

Let \Gamma be a set of formulas and F a formula in propositional logic such that \Gamma \vdash F, then \Gamma \models F.

Proof


TODO:

Therefore

Def. Literal

A literal is either an atomic formula, or the negation of an atomic formula. The former is called a positive literal and the latter is called a negative literal.

Def. Conjuctive Normal Form

A propositional formula F is in conjuctive normal form (CNF) if it is a conjuction of disjunctions of literals, that is

F = \bigwedge_{i = 1}^{n} \left(\bigvee_{j = 1}^{m} \right) L_{ij}

where m,n \in \N^+ and each L_{ij} is a literal.

Def. Disjunctive Normal Form

A propositional formula F is in disjunctive normal form (DNG) if it is a conjuction of disjunctions of literals, that is

F = \bigvee_{i = 1}^{n} \left(\bigwedge_{j = 1}^{m} \right) L_{ij}

where m,n \in \N^+ and each L_{ij} is a literal.

Thm. CNF and DNF Duality

Negation of a formula in DNF is equivalent to a formula in CNF. Similarly, negation of a formula in CNF is equivalent to a formula in DNF.

Thm. Generality of CNF and DNF

Any propositional formula F is equivalent to some formula F_\text{CNF} in CNF and some formula F_\text{DNF} in DNF.

The cannonical algorithms to build equivalent formulas in CNF and DNF are straightforward and simple. Curious reader may exercise or check out such algorithms.

Def. Horn Formula

A propositional formula F is a Horn formula if its in CNF and every disjunction contains at most one positive literal.

A Horn formula is called basic if it does not use any conjunction. Therefore, every Horn formula is a conjuction of basic Horn formulas.

Notice that, for example, the basic Horn formula \neg A_1 \lor \neg A_2 \lor \neg A_3 \lor A_4 is equivalent to (A_1 \land A_2 \land A_3) \to A_4. Therefore, every Horn formula can be written as conjuction of implications. In the case that there are no positive literals, say no A_4 above, we have (A_1 \land A_2 \land A_3) \to \bot.

Thm. HORNSAT

TODO

To-Do’s

30. First-Order Logic

In this section we will define what we refer to as first-order logic which is a much more powerful (in expressive sense) language compared to our previous propositional (zeroth-order) logic. It’s lexicon, who also contains zeroth-order logic defined as

Def. Alphabet

Note that if your meta-theory is strong enough in the sense that it allows you to work with classes, say NBG/GB unlike ZFC, you may allow \mathbf{S} to be a proper class.

The alphabet of a first-order logic denoted by \mathbf{A}_\mathbf{S} is the union of disjoint sets \mathbf{A} and \mathbf{S} where \mathbf{A} is called the set of (first-order) logical symbols which is the union of disjoint

  1. (a set of) variables \{v_0, v_1, v_2 ...\},
  2. (the set of) connectives \{\neg, \land\},
  3. (the set of) quantifiers \{\exists\},
  4. the syntactic equality \{=\}

and (possibly empty) set of non-logical symbols \mathbf{S} called the symbol set (or vocabulary) which is the union of disjoint

  1. (a set of) constants \{c_0, c_1, c_2, ...\},
  2. (a set of) n-ary relations \{P, Q, R, ...\} for each n \geq 1,
  3. (a set of) n-ary functions \{f, g, h, ...\} for each n \geq 1.

Notice that, especially if we consider variables fixed, the set \mathbf{A} is independent of \mathbf{S} and static in the sense that is the same for all first-order logic alphabets.

Def. Term

Let \mathbf{A}_\mathbf{S} be an alphabet of a first-order logic, then the set of terms over \mathbf{A}_\mathbf{S} denoted with \text{Term}(\mathbf{A}_\mathbf{S}) is the smallest subset of {\mathbf{A}_\mathbf{S}}^* such that

  1. Every variable symbol and constant symbol in \mathbf{S} is a term, and
  2. For all n \geq 1, if t_1, ..., t_n are terms, then f_n \> t_1 \cdots t_n is also a term where f_n \in S is an n-ary function symbol.

Notice that we are working in Polish Notation here. Otherwise, in ordinary infix notation, we also need to add comma and parentheses to our set of non-logical symbols.

Def. \text{var}(t)

The variable function \text{var} is defined on the domain \text{Term}(\mathbf{A}_\mathbf{S}) inductively as

\def\arraystretch{1.25} \begin{array}{rcl} \text{var}(x) &:=& {x} \\ \text{var}(c) &:=& \varnothing \\ \text{var}(f_n \> t_1 \cdots t_n) &:=& \text{var}(t_1) \cup \cdots \cup \text{var}(t_n) \\ \end{array}

where x is a variable symbol, c is a constant symbol, and t_1, ..., t_n are terms provided to the n-ary function symbol f_n in \mathbf{S}.

Def. Formula

Let \mathbf{A}_\mathbf{S} be an alphabet of a first-order logic, then the set of formulas over \mathbf{A}_\mathbf{S} denoted with \text{Form}(\mathbf{A}_\mathbf{S}) is the smallest subset of {\mathbf{A}_\mathbf{S}}^* such that, for t_1, t_2, ..., t_n \in \text{Term}(\mathbf{A}_\mathbf{S})

  1. t_1 = t_2 is a formula,
  2. R_k \> t_1 \> t_2 \cdots t_k is a formula where R_k is an k-ary relation symbol in \mathbf{S},
  3. If \varphi \in \text{Form}(\mathbf{A}_\mathbf{S}), then \neg \varphi \in \text{Form}(\mathbf{A}_\mathbf{S}),
  4. If \varphi, \psi \in \text{Form}(\mathbf{A}_\mathbf{S}), then \land \> \varphi \> \psi \in \text{Form}(\mathbf{A}_\mathbf{S}),
  5. If \varphi \in \text{Form}(\mathbf{A}_\mathbf{S}), then \exists x \varphi \in \text{Form}(\mathbf{A}_\mathbf{S}) where x is a variable symbol in \mathbf{S}.

The formulas which are constructed by (1) or (2) is called atomic.

From now on we will denote the first-order language we have just defined above with \mathcal{L}(\mathbf{A}_\mathbf{S}) or simply \mathcal{L}(\mathbf{S}). This language, which is a subset of {\mathbf{A}_\mathbf{S}}^*, consists of words which we call formulas that are defined inductively.

Def. \text{Sub}(\varphi)

The subformula function \text{Sub} is defined on the domain \text{Form}(\mathbf{A}_\mathbf{S}) inductively as

\def\arraystretch{1.25} \begin{array}{rcl} \text{Sub}(t_1 = t_2) &:=& \text{var}(t_1) \cup \text{var}(t_2) \\ \text{free}(R_n \> t_1 \cdots t_n) &:=& \text{var}(t_1) \cup \cdots \cup \text{var}(t_n) \\ \text{free}(\neg \varphi) &:=& \text{free}(\varphi) \\ \text{free}(\land \> \varphi \> \psi) &:=& \text{free}(\varphi) \cup \text{free}(\psi) \\ \text{free}(\exists x \varphi) &:=& \text{free}(\varphi) \setminus \{x\} \end{array}

Notation. First-Order Logic

Let \varphi \in \mathcal{L}(\mathbf{S}), then we define — in addition to its \lor, \to, \leftrightarrow counterparts in propositional logic

Def. \text{free}(\varphi)

The free variable function \text{free} is defined on the language \mathcal{L}(\mathbf{S}) inductively as

\def\arraystretch{1.25} \begin{array}{rcl} \text{free}(t_1 = t_2) &:=& \text{var}(t_1) \cup \text{var}(t_2) \\ \text{free}(R_n \> t_1 \cdots t_n) &:=& \text{var}(t_1) \cup \cdots \cup \text{var}(t_n) \\ \text{free}(\neg \varphi) &:=& \text{free}(\varphi) \\ \text{free}(\land \> \varphi \> \psi) &:=& \text{free}(\varphi) \cup \text{free}(\psi) \\ \text{free}(\exists x \varphi) &:=& \text{free}(\varphi) \setminus \{x\} \end{array}

where x is a variable symbol, t_1, ..., t_n are terms, R_n is an n-ary relation symbol, and \varphi and \psi are formulas in \mathcal{L}(\mathbf{S}).

A variable which is not free is called bound.

Def. Sentence

A sentence in a first-order logic is a formula without free variables.

To-Do’s

40. Structures

Def. Structure