\part{Advanced}



\chapter{Propositional logic}



Logic is merely the foundation for creating mathematics. Mathematical logic is the study of logic \emph{within a mathematical framework}, where we have access to tools such as set theory, formal language theory, and abstract algebra. This allows us to say things about logic rather than just using it as a language for mathematics.

In this way, mathematical logic and logic have a positive feedback loop with eachother; logic defines mathematics and mathematical logic actually studyies properties of logic. Some say that mathematical logic uses mathematics as a metalanguage to discuss logic.


We first consider propositional logic which studies propositions; statements that are either true or false.

Understanding propositional logic will give us an idea of the basic building blocks and concepts of logic that are found in higher order logics and often in other logical systems.



This raises a (possibly disturbing) question; if logic is the base of all mathematics and we use mathematics to define logic, does this mean mathematics is the result of circular reasoning?

One way to think about this is by considering 2 types of logic; formal and informal logic. Mathematics can be used to define and study systems of formal logic, and informal logic can be used to define the language to express mathematical statements, hence mathematics and logic create a 'positive feedback loop' that support eachother.

This is the viewpoint of \emph{logicism}, there exist other viewpoints for interpreting mathematics that are considered in the philosophy of mathematics.



\section{Formal language of propositional logic}

The first step is to syntactically define the language of our logic.


\begin{definition}[Propositional formula]
A \emph{propositional formula} or just \emph{formula} is a string of propositional variables and logical connectives. Defined in the following manner.
\begin{itemize}
\item $\top$ is a formula
\item $\bot$ is a formula
\item If $p$ is a propositional variable then $p$ is a formula
\item If $\varphi,\psi$ are formulae, then $(\varphi \land \psi)$ is a formula
\item If $\varphi,\psi$ are formulae, then $(\varphi \lor \psi)$ is a formula
\item If $\varphi,\psi$ are formulae, then $(\varphi \implies \psi)$ is a formula
\item If $\varphi,\psi$ are formulae, then $(\varphi \iff \psi)$ is a formula
\item If $\varphi$ is a formula, then $\neg (\varphi)$ is a formula
\item Nothing else is a formula
\end{itemize}
Let $\mathcal{L}_{0}$ be the set of all such formulae
\end{definition}


Our formal language for propositional logic is $\mathcal{L}_{0}$, so we are syntactically done. It remains to define what these formulae mean regarding the truth they express.

\section{Semantics of propositional logic}

We can give a meaning to our formulae by the use of valuations. 


\subsection{Valuations}

The only type of propositional formula that we know to create are propositional variables. This is quite limited; we want to show relationships between multiple propositional variables 


This is either expressed by the use of \emph{Boolean functions} or \emph{truth tables}.

\begin{metadefinition}[Boolean function]
A \emph{Boolean function} is a function mapping a tuple of truth values to a truth value..
\[f : \{ \top , \bot \}^n \to \{ \top , \bot \}  \]
\end{metadefinition}


\begin{definition}[Valuation]
A \emph{valuation} is a boolean function mapping settings of atomic fomrulae (propositional variables) to truth values. Its mapping is done by a certain setting of the propositional variables.
\end{definition}

Combinatorics implies this function has $2^n$ mappings if there are $n$ propositional variables involved.

Valuation allows us to give semantic value to our syntactic formulae; we can show the truth of any formula under any propositional variable setting!
\begin{metadefinition}[Valuation of logical connectives]
\end{metadefinition}


For a visual description, truth tables are a convenient way to describe the mappings of a a Boolean function and hence the behaviour of a logical connective. Here are the truth tables of our 5 fundamental logical connectives

1
2
3
4
5


Using this truth table as a reference, one can understand the way in which these logical connectives connect formulae.


We've now completely defined our propositional logic! Now we direct our attention to propounding metatheorems of our propositional logic. Such metatheorems are technically unsound since we've used informal language to define our propositional logic, but you can trust me that these can be proven in any useful axiomatic set theory.





\begin{metadefinition}[Tautology]
A \emph{tautology} is a formula that yields the top for any valuation.
\[ \varphi \text{ is a tautology } \iff \models \varphi \]
\end{metadefinition}

\begin{metadefinition}[Contingent formula]
A \emph{contingent formula} is a satisfiable formula $\varphi$ that is not a tautology.
\end{metadefinition}

\begin{metadefinition}[Satisfiable formula]
A \emph{satisfiable formula} is a formula $\varphi$ such that there exists at least 1 valuation that yields the top. Such a valuation is called the \emph{satisfying assignment of $\varphi$}, and we say that this satisfies $\varphi$.
\end{metadefinition}


\begin{metadefinition}[Set of satisfiable formulae]
A \emph{set of satisfiable formulae} is a set $\Gamma$ of formulae such that there exists at least 1 valuation that yields the top for every formula in $\Gamma$. A valuation on this set with such a property is called the \emph{satisfying assignment of $\Gamma$}.
\end{metadefinition}


\begin{metadefinition}[Semantic consequence (ENTAILS)]
Let $\Gamma$ be a set of formulae, then \emph{$\Gamma$ entails $\varphi$} iff any satisfying assignment of $\Gamma$ satisfies $\varphi$.
\[ \Gamma \models \varphi \]
\[ \emptyset \models \varphi  \iff \models \varphi \]
\[ \{ \psi \} \models \varphi  \iff \psi \models \varphi \]
\end{metadefinition}


Law of the Excluded Middle
\[ \vDash p \lor \neg p\]
Double negation
\[ \vDash \neg \neg p \iff p \]
Self implication
\[ \vDash p \implies p \]
Self equivalence
\[ \vDash p \iff p \]

\begin{metaproposition}[Contraposition]
\[ (P \implies Q) \vDash \Dashv (\neg Q \implies \neg P)\]
\end{metaproposition}


\begin{metatheorem}[De Morgan's laws]
\[\neg (p \land q) \vDash \Dashv (\neg p \lor \neg q)\]
\[\neg (p \lor q)  \vDash \Dashv (\neg p \land \neg q)\]
\end{metatheorem}


\[(p \implies q) \vdash \dashv (q \lor \neg p)\]
\[(P\iff Q) \vdash \dashv [ (P \land Q) \lor \neg (P \lor Q) ] \]
\[(P\lor Q) \vdash \dashv \neg ( \neg P \land \neg Q)\]


\section{Adequacy and normal forms}



\begin{metaproposition}[Adequacy of $\neg,\lor,\land,\implies,\iff$]
All Boolean functions are the valuation of some formula.
\[f \text{ is a Boolean function } \implies \exists \varphi \in \mathcal{L}_0 [ v(\varphi)=f ] \]
\end{metaproposition}

What's cool is that we can form an even stronger version of this proposition by using less propositions.

\begin{metaproposition}[Adequacy of $\neg,\implies$]
All Boolean functions are the valuation of some formula where the only logical connectives used are negation ($\neg$) and the conditional ($\implies$).
\end{metaproposition}


Various formulae can be generated using the formal language, however each formula has infinitely many other formulae equivalent to it.

There exists the idea of \emph{normal forms}; a special class of formulae that offers a standard representation for formulae.

\begin{definition}[Conjunctive Normal Form (CNF)]
Conjunction of a disjunction of literals.
	\[ \bigwedge \]
\end{definition}

\begin{definition}[Disjunctive Normal Form (DNF)]
Disjunction of a conjunction of literals.
	\[ \bigvee \]
\end{definition}

\begin{metatheorem}
Any formula is equivalent to some CNF.
\end{metatheorem}


\begin{metatheorem}
Any formula is equivalent to some DNF.
\end{metatheorem}




\section{A proof calculus for classic propositional logic}


Though we've defined propositional logic syntactically and given semantics to its formulae, how do we actually construct proofs within the language, rather than in the metalanguage? That is, if a set $\Gamma$ of formulae are given to be true, how can one use $\gamma$ to prove that some $\varphi$ is true, all within the system (that means comparing boolean functions or truth tables is invalid since this is a metalinguistic construct)?

This is why formal systems require a proof calculus; a definition for what constitutes a proof when working within the formal system. It works on a syntactic basis, demonstrating legal ways to mechanically manipulate formulae.

There are many proof calculi that one can endown propositional logic with, and they have different consequences mathematically. We will develop a \emph{Hilbert calculus} on $\mathcal{L}_0$. It will have 4 axioms and 1 inference rule; \emph{modus ponens}. The result of this specific proof calculus on $\mathcal{L}_0$ is \emph{classic truth-functional propositional logic}.

\begin{definition}[Hilbert calculus for classical truth-functional propositional logic]
If ........., then we say \emph{$\Gamma$ yields $\varphi$}, or $\Gamma \vdash \varphi$.

\end{definition}

\begin{definition}[Classical truth-functional propositional logicical proof]
\end{definition}



\begin{metadefinition}[Turnstile (YIELDS)]
Let $\Gamma$ be a set of formulae, then \emph{$\Gamma$ yields $\varphi$}.
\[ \Gamma \vdash \varphi \]
\end{metadefinition}


An interesting type of formula is one that happens to always be true regardless of the outcome of its underlying propositonal variables; these are called tautologies.



Modus ponens
\[p \implies q , p \vDash q\]






\subsection{Important metatheorems for propositional logic}

We'll now view the properties of propositional logic as a structure.


\begin{metatheorem}[Semantic Deduction Theorem]
\end{metatheorem}


\begin{metatheorem}[Syntactic Deduction Theorem]
\end{metatheorem}


\begin{metatheorem}[Soundness Theorem]
\end{metatheorem}


\begin{metatheorem}[Completeness Theorem]
\end{metatheorem}







\section{Propositional substitution}


















































\chapter{Formal systems}




\section{Formal systems}


\begin{metadefinition}[Formal system]
A \emph{formal system} is a 3-tuple $(\mathcal{L},P)$
\begin{itemize}
	\item $\mathcal{L}$ is the language of formulae
	\item $R$ are the rules of inference
	\item $R$ are the rules of inference
\end{metadefinition}


\section{Proof calculus}
Suppes-Lemmons notation

	\begin{metadefinition}[Formal proof (Hilbert calculus)]
A \emph{formal proof of $A$ from $\Gamma$} is a finite sequence $(A_i)^{n}_{i=1}$ with $A_n=A$ that satisfies the following properties.
	\begin{itemize}
		\item $A_i \in \mathcal{A}$
		\item $A_i \in \Gamma$
		\item $A_i$ is derived from a rule of inference on previous terms of the sequence.
	\end{itemize}
\end{metadefinition}

\section{Extra}


\begin{metadefinition}[Semantic consequence (ENTAILS)]
Let $(\mathcal{L},\Sigma, R,A)$ be a formal system and $\Gamma \subseteq \mathcal{L}$, then \emph{$\Gamma$ entails $\varphi$} iff any satisfying assignment of $\Gamma$ satisfies $\varphi$.
\[ \Gamma \vDash \varphi \]
\[ \emptyset \vDash \varphi  \iff \vDash \varphi \]
\[ \{ \psi \} \vDash \varphi  \iff \psi \vDash \varphi \]
\end{metadefinition}

\begin{metadefinition}[Syntactic consequence (YIELDS)]
Let $(\mathcal{L},\Sigma, R,A)$ be a formal system and $\Gamma \subseteq \mathcal{L}$, then \emph{$\Gamma$ yields $\varphi$} iff there is a formal proof of $\varphi$ from elements of $\Gamma$.
\[ \Gamma \vdash \varphi \]
\[ \emptyset \vdash \varphi  \iff \vdash \varphi \]
\[ \{ \psi \} \vdash \varphi  \iff \psi \vdash \varphi \]
\end{metadefinition}









\begin{metadefinition}[Sound theory]
Any theorem of the formal system is semantically true
\[ \Gamma \vdash \varphi \implies \Gamma \vDash \varphi \]
\end{metadefinition}

\begin{metadefinition}[Complete theory]
Anything semantically true is a theorem in the formal system.
\[ \Gamma \vDash \varphi \implies \Gamma \vdash \varphi \]
\end{metadefinition}

\begin{metadefinition}[Consistent theory]
Anything semantically true is a theorem in the formal system.
\[ \nexists \varphi [ \Gamma \vDash \varphi \land \Gamma \vdash \neg(\varphi) ] \]
\end{metadefinition}



\section{Philosophy of mathematics}

Formalism Vs Constructivism
Classical logic
Intuitionistic logic

If one wants to formali


















































\chapter{First Order Logic}


With the knowledge of formal systems under our belt, we can use it to develop first order logic rather hastily.

An extension of propositional logic is first order logic; a logic which replaces propositions with predicates and employs the use of quantifiers.

We will go through the process of defining a formal system for first order logic by specifying its formal language and proof system, however let's ex

\section{Predicates}


Predicate
Symbol that evaluates its truth by whether its argument of a certain type satisfies some relation
P(x)


\section{Quantifiers}

Universal quantifier (FORALL)
Existential quantifier (EXISTS)

De morgan's law (first orde)





\chapter{Boolean algebrae}

\section{Boolean ring}

\begin{definition}[Boolean ring]
A \emph{Boolean ring} is a ring where multiplication is idempotent
$r^2=r$
\end{definition}