Application Unification

Propositional Logic: A Programming Inspired Approach

Highschool is usually the first place people encounter any form of mathematics, and along with this setting comes some inappropriate expectations about what lies ahead in mathematics. I might go as far as to say that highschool mathematics and even first year undergraduate mathematics approaches the topic primarily from the perspective of an engineer or experimental physicist; that is mainly to say that you wouldn't call highschool mathematics even particularly 'mathematical' in the ways that a mathematician is actually concerned with the topics studied.

I myself only discovered the seriousness of this discrepency in my first real analysis class. I had lamented at the time that it felt like I was being 'expected to do math as a lawyer who writes computer compileable legalese'. However, as time has gone on, not only have I grown to embrace that description, I've also come to understand that the other classes I was taking at the time (with which I did not have this grievance) were more about applying a physicist's reasoning to geometry and calculus than true mathematics.

This 'true mathematics' is the programmatic legalese. In mathematics, we care very deeply about strict conditions and labels that tell us with certainty under what circumstances our tools will always work. A peer once even said to me that the mathematics was not in symbols, but in all of the words around them.

To that end, we will not spend this section discussing mathematics either; recalling the notion that mathematics sits in between logic and physics on an axis of rigor, we will swing all the way to the left and discuss a description of formal logic. In particular we are going to discuss formal logic in the context of type theory, which will allow us draw on programming metaphors which our society's culture has become much more familiar with in recent years.

However I must confess that the programming metaphor has a special value to me, and I hope also soon to you. As I was first coming to understand that mathematics was inseparable from its legalese, the pattern of theorems and proofs in particular (and also due in part to my double major in physics), I had a notion that one does not truly understand a proof unless one sees clearly how the steps of the proof intuitively mean that the theorem must be obvious. I now see this as wrong, or at least far too physicist-brained. There was a period in my education when I was very ill, and although feeling like I had lost half my brain, I realised that as long as you are doing pure mathematics, you only need half a brain.

The job in solving the puzzle is to connect all of the hypotheses, like pipes or belts in a factory, to the relevant machines (other theorems) that transform them into whatever they need to be to satisfy the proof obligations. Proving a theorem is then no different than playing Factorio or programming. For most jobs, the high level understanding of the whole system is completely subserviant to the low level understanding where you merely know how to correctly plug pipes into ports. If you can do that, then with sufficient effort and an open mind to understand your objects/items/constructions and use your tools/machines/theorems, you can do mathematics. It is this, among other experiences, that makes me so confident that anyone can follow this text, provided I have explained myself well enough.

1. Types, Functions, and Arguments

First I must belabor about some of the basic constructions of programming. You may of course see fit to skip this part, and that would be reasonable if you are familiar with the languages Rust or Haskell, or a similar language with a robust type system. Otherwise, or even in spite of this, it will be valuable to examine what a type is or what we might want it to be, along with what we might expect of functions or arguments.

First, what is a function? There are so many things we could say about this, but first, let us say that a function is a black box that takes an input (or an argument) and gives us back an output, in such a way that we will always get the same output if we use the same input. This could be a function like $x \mapsto x + 1$ which takes a number $x$ and adds to it one before returning it; this notation with the $\mapsto$ symbol (read as 'maps to', and distinct from $\to$) defines a function in terms of what an output looks like assuming a given input.

But a function need not be defined by the procedure we take to calculate its output; if you draw a circle of radius one, draw a straight line through its center, and then for some angle off of that straight line draw a ray, the distance perpendicular to our line to where the ray intersects the circle would be the sine of the angle. While methods to calculate this exist, what the function is here is the relationship between an input to an output, not necessarily a sequence of arithmetic operations. A function could be a pair of lists, $[1,2,3]$ and $[5,2,3]$ such that for an input, we find its position in the first list and take the number at the matching position in the second list, $1 \mapsto 5$, $2 \mapsto 2$ and $3 \mapsto 3$; we just as soon make the lists uncountably infinite, the outputs seemingly random, and we still have a function, and for this reason we also call a function a map. The function is defined by its repeatability and no more. This ambiguity about how we take a function is not a failure of the abstraction but a feature: much later on it will allow us to study functions for which we only have partial information, and perhaps even discover from that information how to calculate them.

But in each of these cases, even the most arbitrary, we have declared either implicitly or explicitly, a prerequisite condition for an input. For instance, with possible exception to the final example, we could not give any of these functions as an input, say, a letter of the alphabet. The procedure $x \mapsto x + 1$ does not admit addition of a letter, the relationship between an angle and its sine does not admit non-angles, and yet we can just as well define a function that takes a letter and sends it to its opposite letter in the alphabet $a \mapsto z$ or a word to itself interspersed with some symbol $``hello" \mapsto ``h.e.l.l.o"$, so the fault is not in the concept of a letter or a word. In fact, one might even conceive of a function which we define to take both numbers and letters, which maps a number $x \mapsto x + 1$ or a letter to its next letter $a \mapsto b$, $b \mapsto c$, selecting whether to be a function of letters or numbers be based on its input. In this case one might even say that we have extended the function to letters by treating them as numbers, using $+1$ to move from one number to the next. But what of $+27$? What is the sine of a letter? Our naive extensions break down.

It is a simple pragmatism that we decide (perhaps only as an arbitrary choice we make now then cling to dearly) that operations such as addition, or relationships that define things like the sine or cosine, fall into classes or types of what they take as inputs. We can have the type of counting numbers $\mathbb{N}$, the type of letters, etc. or the type of functions such as $f\colon n \mapsto n + 1$ which we might write as $f\colon \mathbb{N} \to \mathbb{N}$ to symbolize that it is a function-type with input type $\mathbb{N}$ and output type $\mathbb{N}$, and that this type $\mathbb{N} \to \mathbb{N}$ has as a member $f$. We would equally write $5 \colon \mathbb{N}$ in this scheme, to say that $5$, as a counting number, has type $\mathbb{N}$, of the counting number.

But we have a problem that must be examined closely if we want to make this concept robust. What is it exactly that populates our types? Where does a counting number come from, and if we have two counting numbers, how should we know that they are distinct or the same? Are complex numbers really numbers? If them then why not every clifford algebra? This may seem pedantic but in fact it is the result of carelessness; we cannot say that a type is of numbers without being stuck in the problem of 'what is a number' with its own risk of sophistry. There is a simple solution at the cost of a much more arbitrary choice than to declare that functions' inputs have types. We make a firm rule about where types come from which is the following: a type is defined as having constructors, which are function-like objects which take an object of the correct type and return as their output a new object that does not exist except as the output of this constructor when given that input. This means, among other things, that an object has only one type. We now present the typical example.

It is reasonable to see this and wonder how this definition of the natural numbers, defined ostensibly from only two rules, populates the entire set of counting numbers we know. The simple answer to this is that you would read $\mathbf{S}$ as a function $n \mapsto n + 1$, however instead of being a function, it is in this instance the definition of what it means to count forward one number. What we have done, really, is to define the counting numbers distinctly as 'the first number' and 'the number we count after that'. What that means is that a number like $3$ would be written in its full form as $\mathbf{S}(\mathbf{S}(\mathbf{S}(\mathbf{Z})))$, and we would 'read' the number based on counting the successor functions, i.e. counting how many times we counted up one.

enum NaturalNumber {
	Z,
	S(Box<NaturalNumber>)
}

data NatNum = Z | S NatNum

enum SimpleLinkedList<T> {
	Z,
	S(Box<T>, Box<SimpleLinkedList>)
}

impl PartialEq for NaturalNumber {
	fn eq(&self, other: &Self) -> bool {
		match (self, other) {
			(Z,Z) => true,
			(S(m), S(n)) => (m == n)
			_ => false
		}
	}
}
impl Eq for NaturalNumber {}

You could reasonably ask now 'but what is $\mathbf{Z}$?' or 'but what does $\mathbf{S}$ do?' in a deeper sense of what they are rather than merely what we intend these symbols to mean. The answer to that, as in a similar fashion we will keep encountering, is whatever works. You could define a notion of natural numbers such as these in python using the notion of a list, or an array in other languages, defining $\mathbf{Z} = \mathtt{[]}$ the empty list, and $\mathbf{S}(n) = \mathtt{[n]}$ as the numeral contained in a list, such that $3 = \mathtt{[[[[]]]]}$, an empty list contained in a list, repeated three times. You could do a similar thing with nested pairs so that $2 = \mathtt{([],([],[]))}$. The instantiation of these constructors does not matter, and they can correspond 'really' (insofar as one rationalizes that there is something real about the constructs of programming languages or stories about what a CPU does with those constructs) to anything you like as long as you are able and willing to read that function as symbolizing what we intend it to mean.

In fact, this is almost literally the idea of Alonzo Church, the famous Church Numerals as they have come to be known. In his construction, constructors were literally functions, but merely functions which we commit to never defining a way to compute. In such a way, you would read ${f \circ f \circ f = x \mapsto f(f(f(x)))}$ (we read $\circ$ as 'of' or 'compose' meaning to take the output of the second function as the input of the first, $f$ of $f$) as merely $f \circ f \circ f$ and no more, since there is nothing to be done with the expression, and thus choose to read $f \circ f \circ f$ as $3$. However the idea to define natural numbers as a starting number followed by an operation to count forward is attributed to Giuseppe Peano, and typically considered a presentation of the Peano Axioms, although in his day the language of type theory was in its cradle with Bertrand Russel, the commonly referred to originator of type theory of Russel's Paradox fame. In truth, its origins stretch further back than even Russel's predecessor on the topic, Gottlob Frege, and has been a gradual progression in the development of logic. The school of thought we draw on in this section is downstream of that of the Intuitionists, in particular Martin-Löf and his various colleagues and successors.

This framework has certain powers which we will appreciate soon. One often calls the kind of natural numbers we have defined an inductive type, and it enables a suite of logical tools for which the famous 'proof by induction' is only one. However there is a general mental rule here that sums up its powers up here quite well: once a type has been defined as nothing but a collection of constructors, anything we want to do with that type need only be defined in terms of those few constructors. This introduces powers such as proof by induction, and indeed a more general form of it which apply to all other inductive types, as well as some unfamiliar responsibilities.

That is, okay, we have our natural numbers and we have confined ourselves to a relatively rigid system, that of types, to do so. Can we do anything with these natural numbers, or do we have to drop this rather laborious system just after we have defined it and return to intuitive, poorly defined notions of arithmetic? The answer is of course we can do things with these natural numbers, however to do so, almost every operation we do will appear as a recursive function. Let me give you an example.

fn add(m: NaturalNumber, n: NaturalNumber) {
	match n {
		Z => m,
		S(p) => add(S(m),p)
	}
}

What we have done then is to define addition in terms of the notion of counting upwards, just as we defined natural numbers in terms of counting upwards. Where a natural number can be thought of a tally of each successor function applied to a zero, we define addition to move each of these tally marks from the right hand side to the left hand side, until we are left with zero on the right and the sum on the left. Only then does our recursion terminate, with all 'plus one's moved to one number. Cumbersome as it may seem to define addition in such a way, the upshot is that now everything we could hope to do with a counting number is now almost exactly that hard, including some much more complicated operations.

I have slipped something by you however: we have not yet discussed formally what it means for a function to take more than one input, and instead I have merely presented one to you with the nebulous function type $\mathbb{N} \to \mathbb{N} \to \mathbb{N}$ with no explanation. This is not a notation that we will see in the rest of mathematics (in fact, in spite of all the sense it could make, mathematicians generally invent new notations just to not need to use this one), and is usually reserved for the purer functional programming languages such as Haskell, however it exposes certain questions and concepts that are valuable to us here. In a programming language, it is common to write $f(x,y,z)$ to use a function, and in many languages (and indeed to us now) it is reasonable to speak of $f$ as a function alone, but then what is $(x,y,z)$ exactly?

Most programming languages have a notion of a tuple related to this, a generalization of an ordered pair to as many terms as necessary, allowing one to combine objects into one without forcing them to interact or relate to one another; $x$ and $y$ could be different types entirely and this is fine. We also have a variety of similar notions in mathematics, chiefly the Cartesian Product which we invoke when we say $(2,3)$ is a coordinate on a 2D plane combined of two mere numbers. It will also be necessary for us to define the notion of a Product type, the type theory equivalent to the tuple which solves this problem by defining functions such as $\mathtt{add}$ as of type $(\mathbb{N},\mathbb{N}) \to \mathbb{N}$, however I pose to you that this is not, at this stage, necessary.

But how then will we pass a second input into a function, if not to force it to ride in a pair with the first input? The answer lies in how one should read $\mathbb{N} \to \mathbb{N} \to \mathbb{N}$. That is, what does the $\to$ operation do exactly? Let us for a moment compare it to our addition function, which also is written in the form $m + n$; then one might say that $\to$ is itself a function with two inputs, except that these inputs are not elements of a type, they are types, and it produces a function type. But if the function type it produces is to be thought of as new, then by the rules we have established, $\to$ is not merely a function but a constructor!

This does not resolve our problem of how to read types of form $A \to B \to C$ however; instead that is done by our insistence that the operation is defined right-associative. Consider, if $\to$ takes only two types and produces another type, then absent all other reasoning, you could immediately place brackets to attempt to make this form sensible, considering either $(A \to B) \to C$ or $A \to (B \to C)$. However, consider the form of the former: we know that $A \to B$ must be a function type, taking inputs of type $A$ and producing outputs of type $B$, which means a type $(A \to B) \to C$ takes functions of type $A \to B$ and somehow turns these functions into elements of $C$. A function is however, itself, a single value, and so we have not constructed a function of multiple inputs as desired. The latter, $A \to (B \to C)$ considers a function that takes an element of type $A$ and outputs a function $B \to C$; consider, this output which is a function could now have an input passed to it! This is the meaning of a right-associative operation, one where there are implicit brackets making the right-most operation be performed first. $$\begin{gather*} A \to B \to C \to D \to E \\[0em] = \\[0em] A \to (B \to (C \to (D \to E))) \end{gather*}$$

Right-associativity is perhaps poorly named, as it is distinctly non-associative. Usually in mathematics we only care about whether an operation is equivalent no matter where you put the brackets (associative, or equivalently right-associative and left-associative) or not (non-associative), and certainly in common mathematics almost every binary operation you have encountered is associative (addition, multiplication) at its core (since subtraction and division are inversions of addition and multiplication, they are fundamentally associative, but as written they are not, hence the common memes about disagreeing calcuators) with exception to the cross product. Here however, right-associativity of function types enables us to do something special.

It is of course possible merely to replace functions of form $A \to B \to C$ with those of form $(A,B) \to C$, but consider the latter, it requires that the inputs come as a pair prepared and packaged in one single input. Do inputs need to come prepared as a collection? If we write $5+$, is this object meaningless, or have we invented a function? The right-associative notation $\to$ would imply the latter, since $\mathbb{N} \to (\mathbb{N} \to \mathbb{N})$ is still a function with one input and one output, and with one input (five), that output will be of type $\mathbb{N} \to \mathbb{N}$, an operation that adds $5$ to its input. That is, a side effect of this notation is that it allows us to postpone this process of providing inputs; in the same way that a function exists without any inputs, and exists with all of its inputs as its final output, now it exists with only some of its inputs. This is called Currying for Haskell B. Curry, and is common in languages such as Haskell (sharing a namesake) although it existed in this form as early as Church's lambda calculus. Such a concept is exceedingly common in algebra under a different presentation (and different historical lineage), although mathematicians have relatively clumsy notation to do this at best and use it only very conservatively, an error on both counts in my opinion.

Since currying is so natural to the functional mode of operation, they dispense with the $f(x,y,z)$ notation of function application entirely and often write $f \hspace{1pt} x \hspace{1pt} y \hspace{1pt} z$, since then it is equally natural to write $f \hspace{1pt} x \hspace{1pt} y$ meaning the curried form defined $z \mapsto f \hspace{1pt} x \hspace{1pt} y \hspace{1pt} z$. In this frame, one provides an input $x$ to $f$, at which point we say that '$x$ has become an argument of $f$', and then when we later provide $y$, we have $(f \hspace{1pt} x) \colon y \mapsto (f \hspace{1pt} x \hspace{1pt} y)$ where $x$ has become a parameter. The distinction between these terms is thus: an argument is what is provided in the moment of a function's application, and a parameter is some value that exists fixed in an expression that defines a function's output. In our example, $x$ appears as a parameter at the time that $y$ is an argument, due to our currying; if instead we had $(x,y,z) \mapsto f(x,y,z)$ then we might call each of $x,y,z$ arguments at the same time. Equally, you would say that a function $x \mapsto x + 1$ has as a parameter $1$, since one could imagine this is also the function $(+1)$ curried. This distinction might seem moot now, but later we will see that while the notion of an argument is a formalism, the notion of a parameter is deeply tied up with scientific notions of independent and dependent variables, chiefly as those held fixed in an experiment.

2. Proposition Types and Basic Propositional Logic

We are now ready to use type theory for its principle purpose in this section, bringing home multiple threads we have left open in the previous subsection. First, let us discuss basic logic so we can in some sense define our conceptual targets, what our theory of types must model in order to describe logic.

We have notions of true and false, which we denote $\top$ and $\bot$ respectively, and we have, famously three atomic logical operations we can do with them: $\mathtt{AND}$, $\mathtt{OR}$, and $\mathtt{NOT}$. In many programming languages, these are written $\mathtt{\&\&}$, $\mathtt{||}$ and $\mathtt{!}$, however in formal logic they are written $\wedge$, $\vee$ and $\neg$. Then if we have two propositions $P,Q$ (you can think of these as representing something like "the ground is wet" or "I played basketball") then famously, their rules are:

• $P \wedge Q = \top$ only if both $P= \top$ and $Q = \top$, otherwise $P \wedge Q = \bot$.

• $P \vee Q = \top$ if either $P = \top$ or $Q = \top$ otherwise $P \vee Q = \bot$ (or equivalently $P \vee Q = \bot$ if $P = \bot$ and $Q = \bot$ otherwise $P \vee Q = \top$)

• $\neg P = \bot$ if $P = \top $ and $\neg P = \top$ if $P = \bot$

In order to define propositions as types, we will need to consider, just like the counting numbers type $\mathbb{N}$ is populated with the counting numbers themselves, what is it that populates a proposition? We call these elements of the proposition type 'witnesses' or 'evidence'; you might think of the members of the proposition type "is the ground wet" as testimony that "I went outside and touched the grass and it made my hand wet", however a proposition's witness is never considered in doubt unlike real witnesses.

If we think of propositions as types which are populated (or not populated if they are false and thus have no witnesses) then we know some things about what our logical operations have to be. $\mathtt{AND}$ must create a new type which has witnesses only when both of its argument types have witnesses, $\mathtt{OR}$ must have the witnesses of both types so that it is true if either is true, and $\mathtt{NOT}$ must be a type that somehow has witnesses when its argument type has no witnesses. In fact, we have actually already discussed one of these!

This notation introduces an ambiguity, since we do not literally mean every comma we use in a formal context to be an element of the product type, but it has a value. That is, as a right-associative constructor, we have not only defined pair types but also triples, etc. since any $(a,b,c,d)$ is to be read as nested pairs $(a,(b,(c,d)))$. To avoid confusion however, we use brackets where possible.

The product type also allows us to now formalize what we mean when we say curried and uncurried functions are equivalent. That is, we can always turn a function $f \colon A \times B \to C$ into a function $g\colon A \to B \to C$ and vice versa, because we can set $f \hspace{0.2em} (a,b) = g \hspace{0.2em} a \hspace{0.2em} b$ or $g \hspace{0.2em} a \hspace{0.2em} b = f \hspace{0.2em} (x,y)$ respectively.

Although it may not be obvious, the product type is exactly our $\mathtt{AND}$ operation, since to form an element of $P \times Q$ we require some $p \colon P$ and $q \colon Q$ to form $(p,q) \colon P \times Q$. For example, let $P$ be the proposition that the ground is wet with witnesses which are days that the ground was wet, and $Q$ be "I played basketball" with witnesses which are days I played basketball. Then $P \times Q$ is the type of pairs of a day the ground was wet together with a day I played basketball. If there was a day the ground was wet but not a day where I played basketball, such a pair cannot be formed. This is what gives it its logical 'and' structure; if either fails to have a witness, we will be left stuck in producing such a pair. We do not have an element of the product type $A \times B$ with merely $(a,)$, even now that we can curry. Although, knowing what we do about currying, it will also sometimes be appropriate to read a function $P \to Q \to R$ as not just 'if $P$ then if $Q$ then $R$' but 'if $P$ and $Q$ then $R$'.

Using this as inspiration, we can immediately figure out that the analogous $\mathtt{OR}$ operation will also have a more general use, that is, injecting elements of two types into the one.

These constructors, like all constructors, have no additional structure other than that stated. $l$ will take any $a \colon A$ and merely dump it in $A + B$, just as $r$ will, just as $\mathbf{S}$ would take any natural number and count it up. This is the general case of the example we discussed earlier in which a function has an input type defined of 'either numbers or letters'. In this way, if we have even one of $p \colon P$ or $q \colon Q$, we will populate $P + Q$; we could just as well have $Q$ be a type that is empty of witnesses and we will still have $l \hspace{1pt} p \colon P + Q$ as witness. One could imagine this type as a hat; we would write down the days the ground was wet on pieces of paper, likewise with the days we played basketball, and throw them into the hat, forgetting which was which. Only on noticing that the hat is indeed not empty (i.e. it was wet or we played basketball on at least one day) that we may pull out the piece of paper and distinguish which type it originated from (via. was it $l$ or $r$?). This is our logical $\mathtt{OR}$.

Before we proceed to $\mathtt{NOT}$, we must notice two things. First, that there is another kind of logical operation, one that does not appear in programming in quite so obvious a fashion, that is of great relevance to us. That is, we have been ignoring logical implication the entire time. This is perhaps because it has been obvious to us the whole time as well. Our logical implication operator, 'if $P$ then $Q$', is the function type $\to$. When we say $P \to Q$ we mean to say that witness of one is witness of the other. For instance, if we use our ongoing example about wet ground and playing basketball, we could say that a witness $f \colon P \to Q$ is a witness that says "we play basketball whenever the ground is wet". Thus, on providing a day that the ground was wet, we could clearly say "ah, I remember now, we played basketball on that day when it was wet".

Second, we must think more about what it means for a proposition to be false. The primary thing we are trying to manouver around, given that a proposition type's members are witnesses, is the case where a type has no witnesses and is thus false. This prompts us to codify something we had not said earlier, which is the following:

Our archetypal false type is explicitly the type that is empty, identified with all other types when they are empty, and thus we can say things like $P \times Q = \bot$ when $Q = \bot$. It is not necessarily so simple when a proposition is true however, since there are often multiple witnesses to a true proposition, and the unit proposition only has one constructor. Regardless, with this codified, we may now ask a question: what does $\to$ do to an empty type, i.e. what does it mean to imply false or derive from it? Let us examine this as removed from analogies for a moment.

Consider our responsibilities when defining a function: a function is a map which assigns to every valid input a valid output. So for a type $A$, the function type $\bot \to A$ is populated with what exactly? There are no valid inputs, and so we say that there exists immediately a trivial function $f \colon \bot \to A$. It is common to be confused when seeing this, but consider that from what we know about functions, we have no grounds with which to argue $f$ is not a function; it does its job as a function, since in this case it has no job to do. There simply are no inputs to which we must find outputs. This has another consequence, which is that for all types $P$, the trivial function $\bot \to P$ will exist even if $P$ is a false proposition with no witnesses; again, the space of outputs does not matter since there are no inputs. In fact, what we have described in a trivial function is the type theory version of the 'principle of explosion', often stated as 'if false then anything', with the trivial function as its witness.

The reverse is equally interesting: for a type $A$, just as $\bot \to A$ is always populated with the trivial function, $A \to \bot$ is never populated so long as $A$ is populated. In this case, we have inputs for which we must find valid outputs, but no such outputs exist. The only way we can short circuit this is if indeed we are discussing $\bot \to \bot$, in which case there is still the trivial function. In fact, this function-type is our $\mathtt{NOT}$ operator.

Unlike our other logical operations, strictly speaking we have not defined a new type here; that was done back when we formally discussed $\to$. This is merely a function on types, in fact it is a shorthand for the curried $(\to \bot)$, rather than a constructor. It works as logical negation, as discussed earlier, since $\neg P$ is populated with the trivial function only when $P = \bot$ since if we have a witness $p \colon P$, we will have no outputs to assign for a function $f \colon P \to \bot$, thus falsifiying the function and leaving $P \to \bot$ empty. Returning to our example about days the ground was wet and days we played basketball, let $Q$ be days we played basketball, but say that the proposition type is empty, i.e. we never played basketball, and thus $Q = \bot$. We can still construct $f \colon P \to Q$, or $f \colon P \to \bot$ rather, still saying "we played basketball on every day the ground was wet" just so long as there were no days the ground was wet.

This now makes it possible to discuss certain basic deductions of logic, the most basic theorems, and see that these will take the form of functions. It is my intention that above all else, what you take away from this section is the ability to read a mathematical theorem as a kind of function, and so we have a preliminary example.

This will be our first ever proof and so I would like to note and emphasize some things. First, for the love of god, please do not let the proofs frighten you. In a proof, we merely step through a series of reasoned logical statements to deduce a conclusion. If you are following with the background of a programmer, then you should think of all proofs in this section as programs; indeed all of them can be written verbatim as code in at least some language, and many of them can be written in rust.

The following proof is such a case, and so if matching rust code will make this make sense to you, please see the code below the proof. In either case, this proof most of all is to be regarded as merely a program which we take cares to explain the writing of.

enum SumType<S,T> {
	inl(S),
	inr(T)
}

fn trivial_function(x: !) -> Q { match x {} }

fn theorem<P,Q>(
	s: SumType<P,Q>,
	g: impl Fn(p: P) -> !
) -> Q
{
	match s {
		inl(p) => trivial_function(g(p)),
		inr(q) => q
	}
}

Part of the power of using type theory is that, as discussed before but more obvious now, a function (and thus a theorem) is defined so long as one can account only for every constructor the function may receive. This case is simple, asking what constructors $P + Q$ could have and then taking any member of $\neg P$ absent a question about which constructor it is exactly, however as we will see going forward, theorems of arbitrary complexity will yield to this kind of case analysis since we are merely fulfilling our obligation to provide an output for every input. Thus the question 'which witnesses did we receive?' is merely to divide our sets of inputs/witnesses/circumstances into classes which may individually have easier proofs.

Before moving on, note that we have introduced a split in the notation of constructive mathematics and classical mathematics: in type theory, propositions and their operations exist at the same level as objects, and use the same tools. As our intention here is to proceed, after this section, to classical mathematics, it would be better practice to give our operations appropriate aliases so that we are not confused in future.

3. Dependent Types and Example Proposition Types

We have of course not yet given an example of a real proposition type with its own constructors yet, and the reason for that is this: while we have the tools to discuss a proposition type now, we don't have the tools to discuss whole classes of propositions, and thus to deduce anything that could actually have generality or be useful. The unit type and empty type are technically examples of propositions, and yet they do not say anything. What we need, more than the ability to discuss witnesses or implications about the ground being wet or having played basketball, is a reliable way to discuss witnesses which specify which day the ground was wet or which day we played basketball. It is not on its own useful to deduce that that because the ground was once wet ever that we did play basketball, we need tools that allow us to discuss propositions like "we play basketball the day after it rains".

Since we are preparing to speak about mathematics, most often of all, the things we will have to say with a proposition is to speak of equality, this equals that. And yet equality is not useful if we must manually define a new type for every pair of items we want to claim are equal. We can of course make functions between types, as seen by $\to$, but, consider for equality of natural numbers, we need something of the form $\mathbb{N} \to \mathbb{N} \to \mathtt{Type}$. And yet even in that case, we will certainly need constructors that are somehow dependent on the arguments, lest we populate a proposition type that says any random pair of numbers is equal.

Let us think then about what properties equality has that could found its type. In mathematics, we say that a 'relation' in general describes an equivalence when it has three properties: every thing is equal to itself (reflexivity), an equality is the same backwards as it is forwards (symmetry), and equalities can be chained together to make new equalities (transitivity). A broader discussion of equivalence relations will appear in the following section, however for now, one of these does indeed look like a constructor.

There are a number of peculiar things about this type, least of all how to interpret what it means. First, to avoid confusion, we have used the symbol $\equiv$ rather than $=$ in order to separate the rules of $\equiv$ from out existing notions of equivalence; instead we will deduce them. Second, its constructor doesn't look like a function in the way we are familiar, since now the type of output depends on the individual input rather than merely its type, i.e. $(\mathtt{refl} \hspace{3pt} a) \colon (a \equiv a)$ and $(\mathtt{refl} \hspace{3pt} b) \colon (b \equiv b)$ are members of separate, mutually incomparable types. The constructor we've given this represents the expectation that equality relations are reflexive, so what we've really said is 'in the case where $b$ is both equal to $a$ and literally the symbol $a$, $a \equiv b$ has constructor $\mathtt{refl} \hspace{2pt} a$'.

But we cannot use this yet; the same issue that constructors for this type have, a bizarre dependency of their output type on their input element, is also necessary for any theorem that speaks about equality. Otherwise, more than just having to make each equality type one at a time, we'd have to define a new version of each theorem for each equality type used. We must generalize this concept of dependent function types.

This construction allows us to do something we really have not been able to before. Before, for instance, we could speak of a function which takes letters of the alphabet to words that start with that letter, like $a \mapsto \text{Apple}$ or $b \mapsto \text{Banana}$, and in that way, functions have always depended on their inputs. But now, we can speak of a function that maps $a$ to a particular apple in the type $\mathtt{Apple}$ or $b$ to a particular banana in the type $\mathtt{Banana}$. It is called a dependent function precisely because the type of the output now changes depending on the particular input given. To map that onto the formalization above, we might say that $A$ is the type of alphabetic letters, and $B$ is a family of types of foods which each start with a different letter of the alphabet.

This may seem abstract, but in fact the reason we are discussing it in the first place is because it concretizes a much more natural concept; when $P \colon \mathbb{N} \to \mathtt{Type}$ is a family of propositions depending on a natural number, we can speak of $n \colon \mathbb{N}$ where $P(n)$ is true; this is the type theoretic form of a condition on $n$. This allows us to do two things very interesting things with respect to functions. We can speak of a function of type $(n \colon \mathbb{N}) \to P(n) \to Q(n)$ which, since it takes a witness of $P(n)$ as an argument, is a statement of the form 'when $P$ is true for $n$ then $Q$ is true for $n$'. If instead we have a function of form $(n \colon \mathbb{N}) \to P(n)$ then we have promised that we can reliably produce a witness that condition $P$ is true for any $n$ we give; we have said 'for all $n \colon \mathbb{N}$, $P(n)$ is true'.

In effect, we have gained the ability to speak about propositions in generalities. To say that 'in an entire class of circumstances, it remains true that...'. This concept is so ubiquitous in mathematics that there will be very few sections of this text which do not refer to it literally or implicitly.

Here, the deeper value of the type theory metaphor for propositional logic begins to show itself. In mathematics, we tend to use $\Pi$ in a similar way as above to denote large repetative multiplications, which we sometimes call 'product notation'. This is in fact entirely apt as a choice of notation against the backdrop of our other names. Consider what it means to have a function with a dependent output type: we require of a function that for every input there is an output, and so, what it means to have found a witness for a dependent function proposition type is that we have a member of every type in the type family $P\colon A \to \mathtt{Type}$.

Said another way, imagine a type family dependent on the unit type, $Q \colon \top \to \mathtt{Type}$. Since $\top$ only has one element, the $*$ element, there is only one type $Q(*)$ in the type family, and so $\prod_{* : \top} \hspace{0.05em} Q(*)$ is still a type of functions, but with no real dependency left. Nonetheless, an element $f \colon (* : \top) \to Q(*)$ still selects an element of $Q(*)$ to be its output, $q = f(*)$. Then the data, the information that could be said to be contained in $f$, the choices required to define it, lie only in the choice of $f(*) \colon Q(*)$. What we have done in finding a member $f \colon \prod_{* : \top} \hspace{0.05em} Q(*)$ is merely to find a member $q \colon Q(*)$. Now consider, for a type, let's call it $\mathtt{Bool}$ with only two members $\mathtt{on}\colon \mathtt{Bool}$ and $\mathtt{off} \colon \mathtt{Bool}$; then the dependent type $\prod_{b : \mathtt{Bool}} P(b)$ contains functions that still assign an output to every input, and so it finds a witness for both $P(\mathtt{on})$ and $P(\mathtt{off})$. The data required to define a function $f \colon \prod_{b : \mathtt{Bool}} P(b)$ is then contained in each element of $P(\mathtt{on}) \times P(\mathtt{off})$, since each $(p_{\mathtt{on}},p_{\mathtt{off}}) \colon P(\mathtt{on}) \times P(\mathtt{off})$ corresponds to a possible $f$ which is defined $f(\mathtt{on}) = p_{\mathtt{on}}$ and $f(\mathtt{off}) = p_{\mathtt{off}}$. If extended, the conclusion one reaches is that $\forall (n \colon \mathbb{N}), P(n)$ is to be read as $P(0) \times P(1) \times P(2) \times ...$, i.e. "for all $n$, we have $P(n)$" is an identical statement to "$P(0)$ and $P(1)$ and $P(2)$ and ...". In fact, this interpretation is ostensibly correct, and the intuitions garnered from it generalize.

Holding that thought for a moment, we must first complete our suite of tools. If we are to think of the $\Pi$-type as generalizing the notion of a product type to entire families of types, then can we generalize the sum type to an entire family of types? Let us think for a moment: if a dependent function generalizes the product type since there must exist an output in each type of the type family to correspond to an input, then to generalize the sum type means to say there exists at least one type with a witness amongst an entire family of types. The tool we are looking for is a dependent pair type.

It is of course possible to set $B \colon A \to \mathtt{Type}$ to be some constant family, say, a type $C \colon \mathtt{Type}$, in which case the $\Sigma$-type trivializes back down to the standard pair, $A \times C$. This is important however; as we discussed earlier about currying, a pair argument $(a,b)$ for a function $A \times B \to C$ is the same as a curried function $A \to B \to C$. But then we defined dependent functions that could be $(a \colon A) \to P(a) \to Q(a)$; can we uncurry those? With the dependent pair, we can try writing $\sum_{a : A} P(a) \to Q(a)$ but this would be very bad practice. The natural currying of dependent functions allows us to speak of $(a \colon A) \to P(a) \to Q(a)$ as a dependent function where indeed the family of types $A \to \mathtt{Type}$ is $P(a) \to Q(a)$, or $\prod_{a : A} \big(P(a) \to Q(a)\big)$ with the entire function type as dependent on $a$; if we hide this $a$ in a dependent pair, it is not reasonable to say that it suddenly starts behaving as a dependent function argument later.

The principle is however, sound in a sense. It is reasonable to desire that in the way $P \to Q \to R$ can be read as 'if $P$ and $Q$ then $R$' via currying, that we might use dependent pairs to speak of $\sum_{n : \mathbb{N}} P(n)$ as 'we have a number $n$ and we know that $P(n)$'. In fact, if we have $(a \colon A) \to P(a) \to Q$ where $Q$ is merely a proposition rather than a family of propositions, we can in fact uncurry this to 'if we have a number $n$ and $P(n)$ is true then $Q$'. This should be peculiar in a sense; if $Q$ does not depend on a choice of $n$, then we are saying that $Q$ is implied true merely because there exists a $n \colon \mathbb{N}$ which satisfies the condition $P$, without care of which number $n$ is. This an extremely useful concept.

In propositional logic, the $\Sigma$-type $\sum_{x : A} B(x)$ describes the quantifier 'exists', the same one as in statements like "for all $n$, there exists a prime number $p$ which is greater than $n$". In fact, pending a definition of $>$ (greater than) and letting $P(n)$ be the proposition that $n$ is prime, we could now describe that proposition literally by the type $\prod_{n : \mathbb{N}} \sum_{p : \mathbb{N}} P(p) \wedge (p > n)$. Such a pattern of pairing 'for all' with 'there exists' is a common one, however, it is usually written with the following notation.

It should also be mentioned at least briefly that although in type theory, all objects must belong only to one type, dependent pairs give us the closest thing we have to a subtype. Consider for example, the type $$\begin{gather*} \sum_{n : \mathbb{N}} \exists (m \colon \mathbb{N}) \hspace{0.2em} (n \equiv m + m) \end{gather*}$$ The use of $\Sigma$ here together with $\exists$ is a purely notational choice (indeed, the symbols are intended to be equivalent as just defined) but we write it this way because we are in fact interested in the particular $n \colon \mathbb{N}$. Then in fact all $n \colon \mathbb{N}$ for which there exists a pair of type $\exists (m \colon \mathbb{N}) (n \equiv m + m)$ must be the even numbers, since we will be unable to form such pairs if $n$ is odd, and thus no $m$ with $2m = n$ exists. That is, our closest notion of a subtype of all $a \colon A$ that satisfy a proposition family $P\colon A \to \mathtt{Type}$ is exactly the dependent pairs of $a \colon A$ together with the evidence that they satisfy $P$.

Together, the operations we have described above show how this dependent type theory, one that exists in computer programming languages with operations and objects $\to, \times, +, \top, \bot, \Pi, \Sigma$, has a one-to-one mapping with the logical operations used in mathematics, $\Rightarrow, \wedge, \vee$, true, false, $\forall, \exists$. This is a consequence of the Curry-Howard correspondance, often stated simply as "proofs are programs".

4. Formal Theorems

The whole reason we are discussing type theory is to recontextualise what it means to prove a theorem; what we do in pure mathematics often has less in common with the deductions of a detective eliminating possible stories and more in common with a programming problem. That is, although we are certainly making deductions, the manner in which one does this in every day life can sometimes lead one to think logical statements can be weakened or strengthened with synonyms or by persuading oneself with some argumentative sleight of hand. Although for much of this text we will write proofs in the form of worded deductions, those deductions are written each as the application of some function that transforms a logical context.

To that end, it helps to see propositions as not merely statements to be read as true or false, and theorems as statements which are conditionally true, but that propositions have witnesses, and those theorems act on those witnesses and are incomplete if every single hypothesis is not proven. Moreover, we do not accept a statement merely because it seems like it should be true, but because we have a transformation of existing witnesses to propositions that produces a new witness that the statement is true. With addition to some core axioms, we hold ourselves to this high a standard in mathematics.

This also means that everything you think you know to be true about the typical mathematical objects, rules like $a + (b + c) = (a + b) + c$ are, if not assumed, propositions that have explicit witnesses. It is no longer enough to expect that things should be true, or ought to be true of mathematical objects or objects which we intend to describe things in the real world. If they are true, then they have witnesses. This will expose certain things about how the mathematical mode of thought differs from the logical one, or rather, that many things one believes to be true about mathematics are not necessarily true but are in fact distinct choices we make about the system of logic we work in.

Let us begin with some proofs of familiar concepts.

Let us digress briefly to discuss how the statements of theorems correspond to their propositional counter parts. In mathematics we will often see statements of this form, in particular 'Let $a,b,c$ be of type $A$. If $a \equiv b$ and $b \equiv c$ then $a \equiv c$'. Obviously the proposition 'if $a \equiv b$ and $b \equiv c$ then $a \equiv c$' doesn't make a lot of sense on its own since we must specify what $a,b,c$ we are talking about, and this is done by 'let $a,b,c$' and interpretted as $\forall (a,b,c) \colon A \times A \times A$.

But since most theorems do not have their propositional forms written symbolically, we must be able to read which parts of the theorems are contextualised and which are not. For instance, when we say $a,b,c \colon A$, we do this only after we have said 'let $A \colon \mathtt{Type}$'. Perhaps then it would be more appropriate to first write $\forall (A \colon \mathtt{Type})$ but this would be superfluous since we can't even state the theorem without a choice of type in the first place. Similarly, we may then only write the theorem as $(a \equiv b) \Rightarrow (b \equiv c) \Rightarrow (a \equiv c)$ since we have already contextualised that $a,b,c$ must be of the same type.

It is common in mathematics to drop conditions from statements of the form 'if ... then ...' and instead propose them first as statements 'let ...'; since our theorem can only be applied in a relevant context anyway, our let statements turn arguments into contextual requirements for purely notational clarity. While there exists a broader study of logical context, its rules and manipulations (and if you are interested in this, look into the turnstile), this study exists to split more hairs than even dependent type theory. Contextual manipulations are, as far as we are concerned, equivalent to additional 'for all' arguments.

The mode of reasoning in this proof also applies immediately to certain things about numbers. For instance, the idea that $m \equiv n$ implies $m + 1 \equiv n + 1$ is immediate in this manner: a function $$\begin{gather*} \forall (m, n) \colon \mathbb{N} \times \mathbb{N}, (m \equiv n) \Rightarrow (\mathbf{S}(m) \equiv \mathbf{S}(n)) \end{gather*}$$ has its witness easily since in the moment that we pattern match on $m \equiv n$, we see that the only constructor could have been $\mathtt{refl} \hspace{0.3em} n$, and thus the case we are proving is exactly $$\begin{gather*} (n \equiv n) \Rightarrow \big(\mathbf{S}(n) \equiv \mathbf{S}(n) \big) \end{gather*}$$ with witness given trivially by $\mathtt{refl} \hspace{0.3em} (\mathbf{S}(n))$. This is the extended utility of the inductive type. The mere fact of saying that a function is defined if we know what output to assign to every case of constructor inputs is equivalent also to eliminating the cases where our prerequisite propositions were untrue. In this instance, the only way we could say the relatively trivial solution $\mathtt{refl} \hspace{0.3em} (\mathbf{S}(n))$ fails to be a solution is if our final type were not $\mathbf{S}(m) \equiv \mathbf{S}(n)$. And yet it must be that type since evidence of $n \equiv m$ was supplied, and the only form that evidence could have been was $\mathtt{refl} \hspace{0.2em} n$, meaning $n \equiv m$ must have been $n \equiv n$.

But our system can do much more than just make things we knew intuitively to be true much more burdensome to prove, it can make things which are often difficult for students to comprehend become equally as concrete as those we knew to be obvious already. The famous 'proof by induction' is brought into crystal clarity by our technique, and in fact deduced.

In practice, we will rarely reason about mathematical objects themselves at the type constructor level. While it is a useful tool for being absolutely certain no logical error has been made, we typically try to adjust our intuitions so that we can reason such steps automatically. That is not to say, in this moment at least, that the rigidity we expect of pure mathematics is any weaker, but that statements such as $a = b \Rightarrow a + c = b + c$ is one we train our intuitions on so that we know automatically how to make algebraic deductions.

When we lack such intuitions, or when we know our intuitions are at risk of failing us, this system or modes of reasoning like it are there to catch us. This is often the case when we speak about the various refactorings we can do to statements to make them easier to prove related to negation. It is a common mistake for students to set out to prove by contradiction, only to structure the negated form of the proposition incorrectly and make the proof trivial but wrong. With the benefit of this system, we will not be making such mistakes.

Many of the proofs for this theorem will depend on applying right-associativity, since if the final type we want to show is of form $\to \neg P$, then this is the same as $\to P \to \bot$. Just like in our previous proofs involving negation, we can indulge a counterfactual case, however proofs ending in negation are special in a certain respect. That is, when we engage the counterfactual, we do not need to apply the principle of explosion (the trivial function) in order to obtain any proposition we want, because our final proposition type is $\bot$. Said another way, we can reinterpret $\to \neg P$ as $\to P \to \bot$ and supply a witness $p \colon P$, and this is equivalent to saying "$P$ is false and we will show it's false by showing absurdity is derived from it being true". This is a very specific form of proof by contradiction.

This proof will be the longest we've ever seen before, a record to be almost immediately broken again. For that reason, it is on the website displayed as a minimized box by default. I do recommend looking over this proof, so please click it.

Notice however that these four statements we prove are clearly not all the logical statements we tend to consider about negation. For instance, we cannot prove 'if not both then one is false' ($\neg (P \wedge Q) \Rightarrow \neg P \vee \neg Q$) because our system has hamstrung us. Or more interestingly, it has in fact revealed to us that there are things we believe to be true about logic that are not true a priori.

Consider for example, the concept of proof by contradiction. Since $\neg \neg P$ is read as 'not not P' you would be forgiven for thinking that it is true only when $P$ is true, but that is not the case. In fact, to believe $\neg \neg P \Rightarrow P$ is a strong statement, implying in particular that you believe all propositions are either true or false ($\forall (P \colon \mathtt{Type}), P \vee \neg P$), a property called 'being decidable'. In our every day life, this seems to reflect our experiences, and yet there are rare cases when a question must be undecidable, as is famously the case in Alan Turing's solution to the Halting Problem.

In fact, to consider dependent type theory as the basis of logic would force one to accept a bizarre truth: that there is more than just true or false, but a secret third thing, the not false. We can prove (and this is a fun exercise you are now well equipped to do) that $\neg \neg \neg P \to \neg P$, that is, 'not not not $P$ implies not $P$', but we cannot do anything about $\neg \neg P$. So if we (circularly) think of $\bot = \neg \top$, then we must accept that there is in fact a third outcome, that of $\neg \bot = \neg \neg \top$ in a distinct and meaningful way where there is no fourth (since $\neg \neg \bot = \neg \neg \neg \top$ would be $\neg \top$ as above). We must ask ourselves, is this the system of logic we want to work within? Does this reflect our goals in mathematics?

5. The Problem with Constructive Mathematics

To believe that all propositions are either true or false is in fact a distinct axiom, called the Law of Excluded Middle (LEM) in this case, a statement which we consider to be true and do not question precisely because it is part of the foundation of our system of reasoning. To claim an axiom in one's reasoning is a profoundly dangerous step that must be exercised with caution; presume the wrong thing, and you will end up in a counterfactual, but axiomitise the wrong thing, and your entire logical system is vulnerable to the principle of explosion.

And yet if it is dangerous to believe this axiom since it has clear contradictions, why is it that proof by contradiction is commonly accepted in mathematics?

Here we meet the difference between mathematics and logic; there is a sense in which mathematicians are more interested in the metaphysical behaviour of the objects they study than the logical soundness of them. This is not to say that mathematicians are willing to accept contradictions (in fact they are repulsed by them!) but it is just not their primary concern. To a mathematician, the fact that almost every object they encounter is decidable is enough to consider these rare cases the exception to the rule, i.e. statements are decidable until proven or cautioned otherwise.

Moreover, this more metaphysical interest means that there are circumstances when even mathematicians, looking at a statement that agrees with their metaphysical understanding of an object, will be tempted to say 'this seems true enough'. Such is famously the case with the axiom of choice.

This axiom is famously difficult to comprehend, and many on encountering it are unclear on why exactly it is an axiom which must be asserted rather than a straight forward logical operation. To us, with the benefit of type theory, we see the axiom of choice as a clear assertion of type $$\begin{gather*} \Big(\forall (a : A), \exists (b : B), P(a,b) \Big) \hspace{0.5em} \to \hspace{0.5em} \exists (f : A \to B), \forall (a : A), P(a,f(a)) \end{gather*}$$ given a family of types $P \colon A \to B \to \mathtt{Type}$. We read this statement as "if for all $a$ there exists a $b$ so that $P(a,b)$ is true, then there exists a choice function $f$ which for all $a$ will choose the $b = f(a)$ satisfying $P(a,b)$". Yet even here you may begin to see why such a statement makes one question why it is an axiom: if we know the $b$ exists, then surely it is right there, and we can just choose it, right? But in fact, it can be shown that the axiom of choice implies the law of excluded middle. It is the nature of the mathematician (more particularly the naive one) to look at such a statement and be unconcerned with it; their attention is instead focused on the nature of the type or set that they are choosing from. One might remark even in the other direction, that the great success of mathematics is not in spite of a blindness to logic but because of their singleminded metaphysical curiosity. For much of the remainder of this text, we will embrace that curiosity, and the mindset of the mathematician.

We may even point out a distinct failure of the system we have been working within. That is, while we can prove quite sophisticated mathematical theorems in dependent type theory, we do so with a stipulation that is not the case in mathematics. A witness to the type $\exists (a : A), P(a)$ is not just evidence that it is true that there exists $a$ satisfying $P(a)$, it is an example of it being true $(a,p)$. The functional nature of our deductions means that we cannot merely prove an example exists, we must construct it, hence the name constructive mathematics.

This burden of proof is distinctly higher than necessary. There are valuable things we can say when we are able to prove examples or counter-examples exist where the example itself does not particularly matter. We can even reverse the accusatory finger; since constructive proofs are computational (indeed there are many languages that will run them), to expect all of mathematics to be fully constructive corresponds in some sense to an axiom itself, that the world we live in is a computable one. Does every question that has an answer have a procedure to find that answer? This is an assumption mathematicians do not make.

6. De Morgan's Laws and Proof Techniques

As I said many times before, the rules of dependent type theory remain valuable to us despite our disinterest in its strict adherence. Instead, we know now what it means exactly to presume something is true: treating our theorems as types and our proofs as functions, we can use our intuition to guide our steps and know what type-form a presumption might have, noting immediately if it is reasonable or in fact a much more dangerous statement.

Accordingly, we can now give a more full set of rules for how to manipulate negations, paying off one of the uses of type theory that we will continue to return to throughout this text.

This is the promised even-longer proof, so we have minimized it on the web. I do recommend taking a look however, particularly in the last thing we prove.

It is worth noting that this also pays off our earlier mention of universal quantifiers generalizing and statements and existential quantifiers generalizing or statements. The generalized De Morgan's laws show that the way a for all statement negates with respect to a there exists statement is indeed the same relationship we see between and and or. For instance, we have both 'not both, if and only if either is false' and 'not for all if and only if there exists a counter example'.

7. Into Mathematics

This system of deductions will remain close with us. It is not strictly that the system of dependent type theory is a bad one for logic, but merely that it does not automatically provide a great model for our interests in mathematics. This is largely solved by augmenting our system with the axioms we insist to be true.

In the context of dependent type theory, an axiom can be thought of as insisting a witness of some proposition or theorem exists with no way to define it or find it. Once we add even one axiom, we are in the non-constructive regime, since if theorems are functions, our axioms are functions with no procedure to execute them. Computers can still check such theorems however, and they do this at the level that a computer program merely checks to see that there are no type errors; the lack of a procedure does not change the fact that if such a procedure existed, the theorem would then run without error.

But as we move forward, we will be doing more than merely making our theorems non-constructive with our axioms. We, as mathematicians, are not logicians. There will be times when we strike off one of our axioms and insist that it does not apply in the case we are in. We will even do this without strict rules, but by reasoning about our system, or simply by a known counter-example. That is, as mathematicians, we can know an inconsistency exists somewhere in our system, and simply choose to avoid it as a false branch of conclusions. We do not, for instance, neurotically emphasize solutions to Russel's paradox to avoid even the slightest risk of paradox, we simply avoid the mechanism that causes Russel's paradox to occur as implicitly solving the paradox.

That is neither to say that we merely allow the risk of paradoxes due to our axioms. Due to over a century of knit-picking out of concern for this exact problems, we know what our axioms are in mathematics, and just as in our proof of De Morgan's laws we wrote axioms not as functions that were merely available in context, but as specific conditions, we can simply fail to provide those conditions in the situations where they are not true.

Dependent type theory, with the appropriate asterisks, will form a scaffold by which we continue to reason about logic, and by which we intuit what behaviours we might desire from other structures. For instance, moving forward, we largely put the idea of constructive numbers behind us, but we know that we can construct inductive natural numbers, and thus we can do proof by induction on them. Moreover, seemingly qualitative statements can now be made quantitative by interpretting our conditions for when they are true as constructors, by our so called universal and existential quantifiers.