Title: Theory / Unimportant / Math / Logic / Proof complexity
Tags: fromMath mathToDef hasSeenConjDef mathToSee multipartite
On every note of this deck, unless a note says otherwise:
Chapter: II

Name: Propositional variable
Page: 9
Section: 1
Notation: \(P,Q,R,...\)
Name2: Atoms
Assuming: Each variable represents something distinct

Name: Formulas
Definition: \(\bot\), \(\top\), propositional variable, \(\neg A\), \(A\land B\), \(A\lor B\).
Page: 9
Section: 1
Denoted by: \(A,B,C,...\)

Definition: \((\neg A\lor B)\).
Page: 9
Section: 1
Variables: \(A,B\) formulas
Notation: \(A\supset B\)

Definition: \(((A\supseteq B)\land (B\supseteq A)\).
Page: 9
Section: 1
Variables: \(A,B\) formulas
Notation: \(A\iff B\)

Name: A truth assigment
Definition: Assignment of truth values to atoms.
Page: 9
Section: 1

Name: A proof assigment which satisfies \(A\)
Definition: A proof asignment \(\tau\) such that \(A^\tau=T\).
Page: 10
Section: 1
Variables: \(A\) a formula
Kind: Def

Name: A proof assigment which satisfies \(\Phi\)
Definition: A proof asignment which satisfies each element of \(\Phi\).
Page: 10
Section: 1
Variables: \(\Phi\) a set of formulas
Kind: Def
Extra: proof assignment?

Name: A satisfiable set of formulas
Definition: A set of formulas such that some \(\tau\) satisfies it.
Page: 10
Section: 1
Kind: Def

Name: An unsatisfiable set of formulas
Definition: A set of formulas which is not satisfiable.
Page: 10
Section: 1
Kind: Def

Name: \(A\) is a logical consequence of \(\Phi\)
Definition: Each truth assignments satisfying \(\Phi\) satisfies \(A\).
Page: 10
Section: 1
Variables: \(\Phi\) a set of formulas
\(A\) a formula
Notation: \(\Phi\models A\)
Kind: Def

Name: \(A\) is valid
Definition: \(\models A\)
Page: 10
Section: 1
Variables: \(A\) a formula
Kind: Def
Definition2: For each truth assigment \(\tau\), \(A^\tau=T\).

Name: Two equivalent formulas
Definition: Two formulas \(A\) and \(B\) such that \(A\models B\) and \(B\models A\).
Page: 10
Section: 1
Kind: Def

Name: A sequent
Page: 10
Section: 1.1
Notation: \(A_1,\dots,A_k\longrightarrow B_1,\dots, B_l\)

Name: The antecedents
Definition: \(A_1,\dots, A_k\)
Page: 10
Section: 1.1
Variables: \(A_1,\dots,A_k\longrightarrow B_1,\dots, B_l\) a sequent

Name: The succedents
Definition: \(B_1,\dots, B_l\)
Page: 10
Section: 1.1
Variables: \(A_1,\dots,A_k\longrightarrow B_1,\dots, B_l\) a sequent
Name2: The consequent

Name: The cedents
Definition: The antecedents and succedents
Page: 10
Section: 1.1
Variables: \(A_1,\dots,A_k\longrightarrow B_1,\dots, B_l\) a sequent

Name: A truth assigment which satisfies this sequent
Definition: falsify some \(A_i\) or which satisfies some \(B_i\)'s.
Page: 10
Section: 1.1
Variables: \(A_1,\dots,A_k\longrightarrow B_1,\dots, B_l\) a sequent
Definition2: satisfies \(\bigvee \neg A_i\lor\bigvee B_i\)
Conjdef: Equivalently a truth assigment which

Name: Weakening rule
Definition: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta$ }
\UnaryInfC{ $\Gamma,A\longrightarrow\Delta$ }
\end{prooftree}
[/latex], [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta$ }
\UnaryInfC{ $\Gamma\longrightarrow\Delta,A$ }
\end{prooftree}
[/latex].
Page: 10
Section: 1.1

Name: Exchange rule
Definition: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma_1,A,B,\Gamma_2\longrightarrow \Delta$ }
\UnaryInfC{ $\Gamma_1,B,A,\Gamma_1\longrightarrow\Delta$ }
\end{prooftree}
[/latex], [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta_1,A,B,\Delta_2$ }
\UnaryInfC{ $\Gamma\longrightarrow\Delta_1,B,A,\Delta_2$ }
\end{prooftree}
[/latex].
Page: 11
Section: 1.1
Context: Formal proof

Name: Contraction rule
Definition: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma,A,A\longrightarrow \Delta$ }
\UnaryInfC{ $\Gamma,A\longrightarrow\Delta$ }
\end{prooftree}
[/latex], [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta,A,A$ }
\UnaryInfC{ $\Gamma\longrightarrow\Delta,A$ }
\end{prooftree}
[/latex].
Page: 11
Section: 1.1
Context: Proof tree

Name: \(\neg\) introduction rules
Definition: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta,A$ }
\UnaryInfC{ $\Gamma,\neg A\longrightarrow\Delta$ }
\end{prooftree}
[/latex], [latex]
\begin{prooftree}
\AxiomC{ $\Gamma, A\longrightarrow \Delta$ }
\UnaryInfC{ $\Gamma\longrightarrow\Delta,\neg A$ }
\end{prooftree}
[/latex].
Page: 11
Section: 1.1

Name: A PK proof of \(S\)
Definition: A finite tree whose nodes are labeled with sequents, whose root is \(S\) and is written at the bootom, whose leaves are logical axioms such that each non leaf sequent follows from the sequent(s) immediately above by some PK rules.
Page: 10
Section: 1.1
Variables: \(S\) a sequent

Name: The cut
Definition: \(A\)
Page: 11
Section: 1.1
Variables: [latex]\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow A ,\Delta$ }
\AxiomC{ $A,\Gamma\longrightarrow \Delta$ }
\BinaryInfC{ $\Gamma\longrightarrow\Delta$ }
\end{prooftree}
[/latex]

Name: A proof of \(A\)
Definition: A proof of \(\longrightarrow A\)
Page: 11
Section: 1.1
Variables: \(A\) a formula
Index: 3
Kind: Def

Name: Soundness
Definition: Provability implies validity.
Page: 11
Section: 1.1
Index: 7
Kind: Theo

Name: Completeness
Definition: Validity implies provability.
Page: 11
Section: 1.1
Index: 7
Kind: Theo

Smaller0: \(S\) is valid
Greater0: \(S\) is provable in PK
Page: 11
Chapter: II
Section: 1.1
Variables: \(S\) a sequent
Index: 9
Kind: Lem
Smaller to greater: iff
Hide middle: yes
Name: Inversion Principle
Greater1: \(S\) is provable in PK without cut nor contraction

\(R\) is not weakening and the bottom sequent is valid implies the top sequent is valid.
Page: 11
Chapter: II
Section: 1.1
Variables: \(R\) a rule of PK system
Index: 7, 8
Kind: Theo
Name: Inversion principle

Name: A sequent which is a logical consequence of \(\Phi\)
Definition: A sequent \(S\) such that each truth assignment satisfying \(\Phi\) satisfies \(S\).
Page: 13
Section: 1.3
Variables: \(\Phi\) a set of formulas

Name: A \(\mathbf {PK}-\Phi\) proof
Definition: A proof whose leaves may be logical axiom or elements of \(\Phi\).
Page: 13
Section: 1.3
Variables: \(\Phi\) a set of formulas

Name: A non-logical axiom
Definition: An element of \(\Phi\).
Page: 13
Section: 1.3
Variables: \(\Phi\) a set of formulas,
\(P\) a \(\mathbf {PK}-\Phi\) proof

Smaller0: \(S\) is a logical consequence of a set \(\Phi\)
Greater0: \(S\) is provable in \(\mathbf{PK}-\Phi\)
Page: 14, 15
Chapter: II
Section: 1.3
Variables: \(\Phi\) a set of formulas,
Index: 10, 13
Kind: Theo
Smaller to greater: iff
Name: Derivational Soundness and Completeness
Greater1: \(S\) is provable in \(\mathbf{PK}-\Phi\) using an anchored proof

Q: [...].
A: An instance of the cut rule whose cut appears in a non-logical axiom
Page: 14
Chapter: II
Section: 1.3
Variables: \(\Phi\) a set of formulas,
\(P\) a \(\mathbf{PK}-\Phi\) proof,
Index: 12
Kind: Def
Name: An anchored instance of a cut rule

Smaller0: \(P\) is anchored
Greater0: a subformula of a formula either in \(S\) or in some nonlogical axiom of \(P\)
Page: 15
Chapter: I
Section: 1.3
Variables: \(\Phi\) a set of formulas,
\(S\) a sequent,
\(P\) a \(\mathbf{PK}-\Phi\) proof of \(S\)
Prefix Greater: every formula in every sequent of \(P\) is

Equivalently:
-\(\Phi\) is unstatisfiable set of formulas implies a finite subset of \(A\) is unsatisfable.
-For each \(A\) a formula and \(\Phi\) a set of formulas, \(A\) is a consequence of \(\Phi\) implies \(A\) is a consequence of a finite subset of \(\Phi\).
Page: 16
Chapter: I
Section: 1.4
Variables: \(\Phi\) a set of formulas
\(A\) a formulas
Index: 4
Kind: Theo
Name: Propositional compactness

Smaller0: \(T\) is infinite
Greater0: there exists an infinite path
Page: 16
Chapter: I
Section: 1.4
Variables: \(T\) a rooted tree
Index: 18
Kind: Lem
Smaller1: each node has finite degree
Name: Kônig's lemma

Name: \(\land\) introduction rules
Definition: [latex]
\begin{prooftree}
\AxiomC{ $A,B,\Gamma\longrightarrow \Delta$ }
\UnaryInfC{ $(A\land B),\Gamma\longrightarrow\Delta$ }
\end{prooftree}
[/latex].
Page: 11
Section: 1.1
Definition2: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta,A$ }
\AxiomC{ $\Gamma\longrightarrow \Delta,B$ }
\BinaryInfC{ $\Gamma\longrightarrow\Delta,(A\land B)$ }
\end{prooftree}
[/latex]
Conjdef: Both

Name: Cut rule
Definition: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow A, \Delta$ }
\AxiomC{ $A,\Gamma\longrightarrow \Delta$ }
\BinaryInfC{ $\Gamma\longrightarrow\Delta$ }
\end{prooftree}
[/latex].
Page: 11
Section: 1.1

Name: initial seqent
Definition: The bottom sequent
Page: 10
Section: 1.1
Variables: \(P\) a proof tree

Definition: \(A=\top\),
Page: 9
Section: 1
Variables: \(\tau\) a truth assigment
\(A\) a formula
Notation: \(A^\tau\)
Definition2: \(A=B\land C\) and \(B^\tau=C^\tau=T\),
Conjdef: \(T\) if either
Definition3: \(A=B\lor C\) and \(B^\tau\) or \(C^\tau\) is T
Definition4: \(A=\neg B\) and \(B^\tau\) is F.
Definition5: Otherwise \(F\)

Name: An anchored \(\mathbf{PK}-\Phi\) proof
Definition: A proof such that every instance of the cut rule is anchored
Page: 14
Section: 1.3
Variables: \(\Phi\) a set of formulas
Index: 12
Kind: Def

Name: \(\lor\) introduction rules
Definition: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta,A,B$ }
\UnaryInfC{ $\Gamma\longrightarrow\Delta, (A\lor B)$ }
\end{prooftree}
[/latex].
Page: 11
Section: 1.1
Context: all of
Definition2: [latex]\begin{prooftree}
\AxiomC{ $A,\Gamma\longrightarrow \Delta$ }
\AxiomC{ $B,\Gamma\longrightarrow \Delta$ }
\BinaryInfC{ $(A\lor B),\Gamma\longrightarrow\Delta$ }
\end{prooftree}
[/latex]

Name: root seqent
Definition: A sequent at the top of the proof tree
Page: 10
Section: 1.1
Variables: \(P\) a proof tree
Name2: endsequent

Name: The rules of PK
Definition: Weakening rule
Page: 10
Section: 1.1
Variables: \(S\) a sequent
Definition2: exchange rule,
Conjdef: All of
Definition3: contraction rule,
Definition4: \(\neg,\land,\lor\) introduction rule,
Definition5: cut rule

Name: \(\land\) introduction rules
Definition: [latex]
\begin{prooftree}
\AxiomC{ $A,B,\Gamma\longrightarrow \Delta$ }
\UnaryInfC{ $(A\land B),\Gamma\longrightarrow\Delta$ }
\end{prooftree}
[/latex].
Page: 11
Section: 1.1
Definition2: [latex]
\begin{prooftree}
\AxiomC{ $\Gamma\longrightarrow \Delta,A$ }
\AxiomC{ $\Gamma\longrightarrow \Delta,B$ }
\BinaryInfC{ $\Gamma\longrightarrow\Delta,(A\land B)$ }
\end{prooftree}
[/latex]

Name: The logical axioms
Definition: \(A\longrightarrow A\)
Page: 10
Section: 1.1
Definition2: \(\bot\longrightarrow\) and \(\longrightarrow\top\)
Conjdef: All of