\part{Advanced}



\chapter{Propositional logic}



The previous part of this book gave a high level overview of logic for students starting out in higher mathematics. This section turns towards serious discourse in the field of logic and alludes to problems in the fields of proof theory, model theory.


However before our journey begins, we must have a necessary (and possibly disturbing) conversation regarding a limitation in developing logic.

When styding mathematics, we develop further mathematics based on our current knowledge of mathematics. The unfortunate case is that mathematical logic is the most fundemental area of mathematics; there isn't really anything to develop logic from!

This means that we have to rely on a \emph{metalanguage} in our construction of logic; a language used to describe another language. In our case, our metalanguage will be English and naive set theory.

Note that English is not completely unambigous, and naive set theory is defined by English (in our case). Indeed, naive set theory has paradoxes that we must be careful to avoid. 


We could actually use English to define all of logic, but the notation and concepts of naive set theory makes things much quicker; it's essentially abbreviates some of our English. Furthermore, the use of naive set theory also allows us to make explicit reference to formal language theory, which is extremely helpful becausle logic is syntactically defined by a formal language!


Perhaps it is a bit disheartening that we have to rely on informal language to define our formal system, however there is hope; if we do a good job at using English and naive set theory to create a formal logic, then our formal logic can be used to create an axiomatic set theory which is free of paradoxes. We could then use our formal logic and axiomatic set theory to define formal logic again as a formal language within an axiomatic set theory; therefore we'd be using a formal metalanguage!






\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)
