Preamble

In my last post I gave the philosophical prerequisites needed to understand my approach to logic and mathematics. Before getting into the subject at hand, here's a clarifying remark inspired by some comments on my last post. When I say that mathematics is a social activity, I mean it's an activity that is social. Politics is also a social activity. This means that saying, for example, that mathematics is incomplete or inconsistent makes as much sense as saying that politics is incomplete or inconsistent (in the same way a formal logic might be). It's very common for someone to make mention of mathematics having some property (e.g. Gödelian incompleteness) when, in fact, it's a specific logic (such as ZFC or the totality of formal logic) which has this property. This odd synecdoche causes people to frequently confuse a part of mathematics with the whole. No one logic or collection of logics constitutes all of mathematics. The intuitions used to justify an axiom are part of mathematics, but not part of any axiom system.

With that out of the way, the point of this post is to give explicit meanings to the most basic logical connectives.

Logical Theories

A logical theory is a sort of collection of precommitments with two main kinds of judgments, $P\text{Prop}$ (read "$P$ is a proposition") and $P\text{True}$ (read "$P$ is true"). Within a logical theory, all but one of our precommitments will pertain to True. Note that any given precommitment will be about one particular thing, as previously explained. The propositional connectives we will initially deal with will be $\perp$ (falsum), $\top$ (verum), $\wedge$ (and), $\vee$ (or), and $\to$ (implies). Each will have a precommitment telling us precisely what's required for making a declaration of truth pertaining to that connective, and nowhere else will there be rules for making such declarations. Our one remaining precommitment will be the acting definition of Prop. Briefly, the precommitment for Prop says that $P$ is a proposition when we've said what's required for declaring $P\text{True}$.

These precommitments will be variously referred to as "meaning explanations", descending from the usage of Martin-Löf, which explain the rules for reasoning about a judgment. For a judgment $J$, a meaning explanation should be a series of statements of the form:

We may declare $J$ when ...

The meaning of the judgment $P\text{Prop}$ is, then, as follows:

We may declare $P\text{Prop}$ when we understand the requirements for declaring $P\text{True}$.

So, assuming that we follow our precommitments, we will only ever declare $P\text{Prop}$ when we already have prescribed the rules by which we reason about $P$. This is part of the definition of $P$. Now, the judgment $P\text{True}$ can only be declared in the case that we know the requirements for making such a declaration, meaning we should always be able to declare $P\text{Prop}$ in such a circumstance.

The judgments True and Prop are called "categorical", signifying that they lack assumptions or generality. For the sake of addressing assumptions, we introduce a new form of judgment, which we call a "hypothetical judgment". A hypothetical judgment is made under a hypothesis. Our primary hypothetical judgment will be $\frac{J^{\prime }}{J}$, pronounced "$J$ under the assumption $J^{\prime }$". Its meaning explanation is as follows:

We may declare $\frac{J^{\prime }}{J}$ when we are allowed to declare $J$ after declaring $J^{\prime }$.

Hypothetical judgment may be iterated, and $\frac{J_1{J}_2}{J}$ will be used as notation for $\frac{J_1}{\frac{J_2}{J}}$

We introduce the notion of a "general judgment", which is judgment with respect to a variable, ${|}_{x}J$, pronounced "for an arbitrary $x$, $J$". The meaning explanation for general judgments is as follows:

We may declare ${|}_{x}J$ when we are allowed to declare $J[x:=E]$ (i.e. the substitution of $E$ for $x$ in the expression $J$) for any expression $E$.

We assume that the bar symbol binds as loosely as possible. Additionally, when making multiple general judgments, we'll use the notation ${|}_{x,y}J$ for ${|}_x{|}_{y}J$.

Note that this judgment relies essentially on the notion of substitution and variable binding. This, along with a full exposition on tokens and expressions will be addressed in my next post.

One thing worth clarifying is the difference between $\frac{P\text{True}}{P\text{True}}$ and ${|}_P\frac{P\text{True}}{P\text{True}}$. That first is more like a scheme for a judgment. It's not meant to be declared on its own. Rather, $P$ has to be replaced with a concrete expression by the person asserting the judgment. The second is a complete judgment which can be made as-is.

One principle worth noting is the following: in order to have declared $P\text{True}$, we must have already declared the conditions under which such a declaration could be made. This means we must be able to declare $P\text{Prop}$. This allows us to validate $\frac{P\text{True}}{P\text{Prop}}$.

I would like to digress at this point to critique the knowledge-theoretic interpretation of judgments. In Type Theory and its Meaning Explanations, for example, we read the following;

To know $P\text{Prop}$ is to know that $P$ is a proposition, which is to know what would count as a direct verification of $P$.

Though it may not be obvious before it's pointed out, this description is simply untrue. We may know what counts as a direct verification of $P$ without knowing that $P$ is a proposition. There is an extra step missing, being the act of realization. In order to know $P\text{Prop}$, we must first realize it. Let me demonstrate the importance of this distinction with an example. Here is a knowledge-theoretic meaning-explanation of sorts for prime factors;

To know that $m$ and $n$ are prime factors of $k$ is to know that $m$ is prime, that $n$ is prime, and that $m\times n=k$.

Based on that, let me ask you this. What are the prime factors of $91$? If, by chance you know a few arithmetic tricks, then replace this with a number obtained from multiplying larger primes, but without looking it up, very few people would be able to answer this quickly. Now what's $7\times 13$? Most people should be able to answer $91$ fairly quickly, as well as recognize that $7$ and $13$ are prime numbers. Now, I'll ask again, what are the prime factors of $91$?

Notice what knowledge was present. Knowledge that $7$ and $13$ were prime and that $7\times 13=91$ was present, but knowledge that $7$ and $13$ are prime factors of $91$ wasn't. In this case, the realization required computational effort. For more sophisticated mathematical notions, that computational effort may even be insurmountable.

It is not generally the case that knowing $A$ and that $A$ implies $B$ allows us to know $B$. That would take extra effort in realization, and so the knowledge-theoretic account of meaning is flawed. I've replaced references to knowledge with an appeal to precommitments and allowances, and that seems to eliminate this problem while making the account more clear and closer to practice. Additionally, we side-step issues of computer knowledge. It will become clear that the system described in this work is implementable on a computer, but we would need to address the baggage of the knowledge-theoretic account. We are begged to answer for the assertion that a computer apparently knows something, bringing into question the meaning of knowledge itself. Thankfully, this problem evaporates along with the original references to knowledge.

Basic Propositions

Now that the most commonly used judgments are out of the way, we can start populating our logical theories with specific examples of propositions.

Perhaps the thematically first proposition is trivial truth $\top$. It has a simple precommitment with only a single rule;

We may declare $\top \text{True}$.

In other words, we can assert $\top \text{True}$ regardless of circumstance. We might say that the judgment of $\top \text{True}$ is trivial. Since we have a precommitment telling us the requirements for declaring $\top \text{True}$, we are free to declare $\top \text{Prop}$.

The simplest proposition that we may consider is falsum $\perp$. To define this as a proposition, we must specify the requirements for declaring $\perp \text{True}$: there are none. In other words, we use the empty precommitment as part of our definition of $\perp$. Since we have a precommitment which, trivially, tells us the requirements for making these declarations, we are free to assert $\perp \text{Prop}$.

Next, let's define conjunction. This will be the first time we rely on a hypothetical judgment in making a precommitment. Our goal is to declare the conditions under which we can declare $P\wedge Q\text{True}$. Our full precommitment looks like;

We may declare $P\wedge Q\text{True}$ when we've declared $P\text{True}$ and $Q\text{True}$.

Consider what's necessary in order to follow this precommitment, we will need to assume that we've previously stated the conditions for declaring $P\text{True}$ and $Q\text{True}$, that is, we must already be allowed to declare $P\text{Prop}$ and $Q\text{Prop}$. Upon realizing this, we verify the following judgment;

We can also declare the following, which summarizes the truth-theoretic content of our precommitment;

We can even characterize our precommitment as the smallest one validating this judgment.

I would also like to emphasize that the above precommitment is the entire definition of the proposition. We have introduced syntax and have specified the canonical methods for introduction. There is nothing more to be done.

It is more common in works of logic to "define" a piece of the theory in terms of some collection of inference rules which themselves are taken as a foundation which is not itself justified. By a meaning explanation account, such rules must be validated, are taken as derived, as something that must be realized, not given.

Throughout this work, I will make reference to a judgment being validated. A validation is not necessarily part of our logic proper. Rather, it is an account of how we may come to realize that a judgment can be made. We may employ rather sophisticated reasoning in making a realization, in validating a judgment.

Moving on to disjunction, we can state the precommitment for $\vee$ as;

We may declare $P\vee Q\text{True}$ when we've declared $P\text{True}$.

We may declare $P\vee Q\text{True}$ when we've declared $Q\text{True}$.

As with $\wedge$, in order for this precommitment to be followed, we must have already declared what's required for declaring $P\text{True}$ and $Q\text{True}$. That is, we must already be allowed to declare $P\text{Prop}$ and $Q\text{Prop}$. Upon realizing this, we verify the following declaration;

The precommitment pertaining to $\vee$ can be characterized as the smallest precommitment validating the following two judgments;

To end this section, we should address implication and define the circumstances under which $P\to Q$ is true.

We may declare $P\to Q\text{True}$ when we've declared $\frac{P\text{True}}{Q\text{True}}$.

It's worthwhile to ponder what exactly is required to follow this precommitment, as it's more complicated than the previous ones. Consider the requirements for declaring $\frac{P\text{True}}{Q\text{True}}$. In order to state this, we must have stated two previous things. Firstly, we must have said what's required for declaring $P\text{True}$, that is, we must be able to declare $P\text{Prop}$. Secondly, under the assumption of $P\text{True}$, we must have stated the requirements for declaring $Q\text{True}$, that is, we must be able to declare $Q\text{Prop}$ when we've already declared $P\text{True}$: we must be able to declare $\frac{P\text{True}}{Q\text{Prop}}$. From this reasoning, we can validate the following judgment;

Upon declaring the precommitment for $\to$, we can make the following judgment, characterizing the truth-theoretic content of our precommitment;

Witnesses

So far we have taken the Martin-Löf approach of prescribing the meaning of a proposition by specifying the conditions under which it can be introduced. This has been called the verificationist approach. In particular, it should be clear that, assuming we've accomplished the requirements for declaring $P\text{Prop}$, in declaring $P\text{Prop}$ we are saying that we have specified precisely what $P$ means.

One question that lingers is the notion of proof. I'll say variously that we can prove something, but I've not said what a proof actually is. That is, we've given meanings to the propositions themselves but not to their proofs. Fundamentally, the difference between logic and mathematics in general is that logic cares if something is true while mathematics cares why something is true. This may seem confusing at first, but we will see by the end of the fourth post of this series that the ability to do mathematics emerges from specifying and differentiating between proofs.

Before jumping in, we should discuss the notion of an elimination rule. To start, let's look at conjunction. There are two methods for eliminating $A\wedge B$. Firstly,

How might one verify this? Consider the meaning of $A\wedge B\text{True}$. In order to make that conclusion, it must have already been the case that we can conclude $A\text{True}$. This is similarly the case with $B\text{True}$, allowing us to verify the second elimination rule;

There is a duel perspective to verificationism called pragmatism. In pragmatism, instead of prescribing the meaning of something in terms of how it's introduced, we prescribe meaning by how it's eliminated. So we'd have a precommitment for $\wedge$ which looks something like;

We may declare $A\text{True}$ when we may declare $A\wedge B\text{True}$.

We may declare $B\text{True}$ when we may declare $A\wedge B\text{True}$.

And it is precisely the elimination rules of $\wedge$ that contain the truth-theoretic content of the pragmatist precommitment.

Remember, a precommitment is only a list of rules for making judgments. We do intend to make cheap the ontological commitment to the ideas who's meaning is encoded in these precommitments, and to that end the verificationist approach seems, prima facie, more palatable. However, as we will see in a much later post on codata, the pragmatist approach is necessary to make sense of, for example, languages with infinite sentences. For now, we will focus on how these dual perspectives interact.

One thing that we can see by using both the introduction and elimination rules is that information is always traceable through the rules. Consider the derivation;

Assume we have declared $A\text{True}$ and $B\text{True}$. We can conclude $A\wedge B\text{True}$. After that, we know that, in order to declare $A\wedge B\text{True}$, we must have been able to declare $A\text{True}$, and so we do, we declare $A\text{True}$.

For any given declaration, there must be some justification for making it. Typically, such justifications boil down to appeals to some precommitment. It's obvious that the justifications used to justify both instances of $A\text{True}$ are, on some level, the same. We can see the traceability of this justification through the derivation, that the only information present at the conclusion of the derivation was already present at the outset. This property is called soundness, and essentially acts as our justification for calling the idea of $\wedge$ coherent: we cannot come to know something which we did not already know purely by reasoning about $\wedge$, and so is the case with all logical and mathematical operators.

We can express this traceability of information with a reduction, of sorts, that the above derivation should reduce, in some sense, to

Assume we have declared $A\text{True}$.

This, fundamentally, is the motivation for type theory. We can represent the rules of a commitment themselves with symbols in the same way we have done for the propositions. This also allows us to be precise with our claims of a validated derivation. We may say that "$M$ is a derivation validated by the precommitment for $P$", and be sure that this is true based on the form of $M$. We will denote this relation between $M$ and $P$ as $M:P$, pronounced "$M$ witnesses $P$". When such a judgment can be made, we call $P$ a type, and refer to our broader theory as a type theory rather than a logical theory.

We could try specifying a meaning like this;

We may declare $M:P$ when $M$ is the name of a rule in the precommitment for $P$.

But, as stated in the introduction, this is insufficient. We may have, instead of a rule directly, a plan for deriving a rule or series of rules for witnessing $P$, an algorithm which, when run, will give a canonical witness in the same way $1+1$ is a natural number, but not a canonical one. Reduction to a canonical form will be represented by a judgment $M\downarrow M^{\prime }$ , pronounced "$M$ evaluates to $M^{\prime }$".

We may declare $M\downarrow M^{\prime }$ when, in any declared judgment, $M$ may be replaced with another expression $M^{\prime }$, creating a new judgment which can still be declared.

The meaning explanation for $P\text{Prop}$ must be accordingly modified to take into account the computational behavior of expressions. We may now have non-canonical propositions, that is, expressions that evaluate to a proposition but don't themselves have associated precommitments. We will call this judgment "$P\text{prop}$". Furthermore, we need a notion of canonical truth. Within our precommitments defining canonical propositions, we will use the judgment $P\text{True}$, and outside we will have $P\text{true}$ for non-canonical propositions. So we now have the three meaning explanations;

For Prop:

We may declare $P\text{Prop}$ when we understand what's required to declare $P\text{True}$.

For true:

We may declare $P\text{true}$ when there is a $P^{\prime }$ such that we may declare $P\downarrow P^{\prime }$ and $P^{\prime }\text{True}$.

For prop:

We may declare $P\text{prop}$ when there is a $P^{\prime }$ such that we may declare $P\downarrow P^{\prime }$ and $P^{\prime }\text{Prop}$.

As an example we will update the justification for the following derivation:

The verification of this rule must change to correspond to our new understanding of prop. $P\to Q$ is already in a canonical form. That is, we can declare $P\to Q\text{prop}$ so long as we can declare $P\to Q\text{Prop}$. From there, we need to establish what we need in order to declare $\frac{P\text{true}}{Q\text{true}}$. In order to state this, we must have stated two previous things. Firstly, we must have said what's required for declaring $P^{\prime }\text{True}$, where we may declare that $P\downarrow P^{\prime }$. That is, we must be able to declare $P\text{prop}$. Secondly, under the assumption of $P\text{true}$, we must have stated the requirements for declaring $Q^{\prime }\text{True}$, where we may declare that $Q\downarrow Q^{\prime }$. That is, we must be able to declare $Q\text{prop}$ when we've already declared $P\text{true}$: we must be able to declare $\frac{P\text{true}}{Q\text{prop}}$.

We will also modify previous meanings to make them more flexable. For example;

We may declare $P\wedge Q\text{True}$ when we've declared $P\text{true}$ and $Q\text{true}$.

This allows our connectives to operate on non-canonical propositions.

We will make a new judgment, $P\text{type}$, which modifies our prop judgment. The only real distinction is that types have names for each precommitment rule. We have two precommitments for the canonical and noncanonical forms.

For Type:

We may declare $P\text{Type}$ when we understand the requirements for declaring $M;P$ for all applicable expressions $M$.

For type:

We may declare $P\text{type}$ when there is a $P^{\prime }$ such that we may declare $P\downarrow P^{\prime }$ and $P^{\prime }\text{Type}$.

When a name appears within a precommitment, we call it a canonical witness of the type. Here, $;$ is used to denote that something is a canonical witness. The $:$ token, however, is intended to relate non-canonical expressions as well, so we have the further meaning explanation in the case that $M$ is non-canonical;

We may declare $M:A$ when we have an $M^{\prime }$ and $A^{\prime }$ such that we may declare $M\downarrow M^{\prime }$, $A\downarrow A^{\prime }$, and $M^{\prime };A^{\prime }$.

We may now modify our meaning of $\wedge$ with a named witness;

We may declare $(a,b);A\wedge B$ when we may declare $a:A$ and $b:B$.

Note that $a$ and $b$ do not have to be canonical. Even if $a$ and $b$ are non-canonical, $(a,b)$ is canonical, as it's subject to the rules of the precommitment.

It's useful to start declaring non-canonical witnesses at this point. We do this simply by declaring a sequence of tokens, along with reduction rules. For example we have;

Note the new kind of meaning, signified by $\downarrow$. Note that these aren't the meanings themselves. Instead, we have a meaning like;

In any declared judgment, ${\pi }_1\left(\right(a,b\left)\right)$ may be replaced with $a$, creating a new judgment which can still be declared.

This models the meaning of $\downarrow$, and allows us to validate ${\pi }_1\left(\right(a,b\left)\right)\downarrow a$. However, that's quite long-winded, so I'll just state the reduction rules themselves.

Each reduction rule constitutes a new precommitment. We ought to be concerned by the ontological cost of such a commitment. We can, at least, see that so long as our source expression is not in any kind of canonical form, we're neither introducing a new idea nor modifying an old one. If all of our reduction rules are of this form, the precommitment is free of cost, it doesn't make our ideas incoherent. We may think of the reduction rules as the precommitment defining the meaning of the operators they reduce. If we were to assert a reduction rule for an operator which already has a meaning explanation, such as $\wedge$, for instance, then we'd be breaking the precommitment which is its meaning explanation.

As long as they do not conflict with any previous precommitment, we may freely assert any reductions we want, including looping and exploding expressions. These declarations, however, may not interface well with our previous ones, they do have to answer to the meaning explanations of our theory in order to be useful. For example, we may want to validate a derivation such as this;

To validate this rule, we observe that, in order for $p:A\wedge B$ to have been concluded, it must reduce to a canonical $p^{\prime };A\wedge B$ (by the meaning of $:$ on non-canonical terms). The only canonical witnesses of $A\wedge B$ are of the form $(a,b)$, where $a:A$ and $b:B$. This brings our target judgment to;

Since we've declared that ${\pi }_1\left(\right(a,b\left)\right)\downarrow a$, we may alter our goal to

which is easily declarable.

We use the expression ${\pi }_1\left(\right(a,b\left)\right)$ to stand for the proof tree expressed by the reasoning in the earlier derivation. The previous validation acts as a precise restatement of that derivation where our justifications were named by the witnesses. The reduction rule gives a precise description for how to extract the assumption we initially made.

A First Pass at Lambda Expressions

In the case of implication, we can easily transform the previous meaning explanation for the sake of making $\to$ a type;

We may declare $\lambda x.y;A\to B$ when we may declare $\frac{x:A}{y:B}$.

For example, we may validate the following judgment;

To do so, we must be able to state

which we, in fact, have already done. However, there's an extra consideration which must be made. For an expression $\lambda x.y;P\to Q$ may be the case that $y$ is a non-canonical witness of $Q$ and that $y$ actually mentions $x$. Consider that, in order for $\lambda x.y$ to truly be a proof of $A\to B$, we must be able to construct a witness of $B$ out of $x$, assuming only that $x$ is a witness of $A$. That is to say, if we know more about the specific structure of $x$, then it may not be fully general, it may be creating a witness of $B$ out of a special case of $A$ rather than $A$s in general. As a consequence, the meaning explanation above fails to capture what we intend. To demonstrate this, consider the following meaning for $\text{Maybe}\left(A\right)$;

We may declare $\text{Nothing};\text{Maybe}\left(A\right)$.

We may declare $\text{Just}\left(a\right);\text{Maybe}\left(A\right)$ when we may declare $a:A$.

We'll consider these kinds of constructs more deeply later on, but for now, consider that a $p$ such that $p:\text{Maybe}\left(A\right)$ could have been declared in two canonical ways; one which contains a witness to $A$, and one which doesn't. Now, consider the judgment;

Assuming our previous meaning explanation was correct, then it should be the case that $\lambda \text{Just}\left(a\right).a:\text{Maybe}\left(A\right)\to A$, but this obviously shouldn't hold in general. Lambda expressions should only be able to bind variables, treated as witnesses of unknown structure, but not expressions containing constants. As a consequence, the previously stated meaning explanation is insufficient for characterizing functionality, the type-theoretic generalization of implication will need something more powerful than hypothetical judgment. A simple solution presents itself. We may use a generalized judgment;

We may declare $\lambda x.y;A\to B$ when we've declared ${|}_x\frac{x:A}{y\left(x\right):B}$.

where that $y\left(x\right)$signifies that $x$ may be mentioned in $y$, but not in $A$ or $B$. This kind of abstract binding will be dealt with in the next post, and functional contexts will be defined in the post after that.

In the case of propositional implication, we may validate the following elimination rule;

Consider that, in order to have concluded $A\to B\text{true}$, we must have been able to conclude $\frac{A\text{true}}{B\text{true}}$, rendering our goal;

which is easily declarable.

Using this reasoning, we can make the following deduction;

Assume we have declared $A\text{true}$ and may declare $\frac{A\text{true}}{B\text{true}}$ by some means. We can, by the meaning of $\to$ conclude $A\to B\text{true}$. From the elimination rule, we may conclude $B\text{true}$.

It's clear that $A\to B\text{true}$ is simply an internalization of the judgment $\frac{A\text{true}}{B\text{true}}$. We may conclude that the above deduction should, in some sense, be equivalent to;

Assume we have declared $A\text{true}$ and may declare $\frac{A\text{true}}{B\text{true}}$ by some means. By the meaning of hypothetical judgments, this means precisely that we may declare $B\text{true}$ when we've declared $A\text{true}$, and so we do, we declare $B\text{true}$.

In the expression $\lambda x.y$, we have that $y$ is a recipe of sorts for building our conclusion out of our assumption $x$. We define a new reduction rule, application which we will denote $\text{ap}(x;y)$ with the following reduction rule;

We may validate the following judgment;

To do so, we note that we need to be able to state $\text{ap}(p;x):B$ in the case that we've stated $x:A$ and $p:A\to B$, by the meaning of hypothetical judgments. In order to have stated $p:A\to B$, we must have some $p^{\prime }$ such that $p^{\prime };A\to B$ and $p\downarrow p^{\prime }$. The only canonical witness of $A\to B$ is of the form $\lambda a.b$, so our goal becomes $\text{ap}(\lambda a.b;x):B$.

We may reduce our goal, and also point out that, in order to have concluded $\lambda a.b;A\to B$, we must be able to declare ${|}_a\frac{a:A}{b:B}$.

In order to declare ${|}_a\frac{a:A}{b:B}$, we must have been able to declare $\frac{a:A}{b:B}[a:=E]$ for any expression $E$. In particular, this allows us to use $x$ in place of $E$, allowing us to judge $\frac{x:A}{b[a:=x]:B}$. This makes our goal

This is easily declarable.

Consider that, if we stuck with our previous meaning that didn't make use of hypothetical judgment, we would eventually get stuck on;

We've solved that major problem with the meaning explanation, but we are begged to answer for our specification of variable usage. This can be clarified by an understanding of free variables, as described in the next post.

If we take $\lambda x.b$ and $\text{ap}$ on their own, ignoring any idea that it has anything to do with logical formulas, we get a self-contained model for computation called the lambda calculus. It is, on its own, Turing complete. It was the second such system discovered which has this property all the way back in the 1930s by Alonzo Church. At that time, the connection to logic that I showed here was not known, only to be described in 1969 by William Alvin Howard. In many ways the lambda calculus can be thought of as the computational component of deduction, describing precisely, through substitution alone, how justifications in deductive inferences flow through an argument.

Disjunction and Generalized Eliminators

We may straightforwardly alter the meaning precommitment for $\vee$ to incorporate witnesses;

We may declare $\text{inl}\left(p\right);P\vee Q$ when we've declared $p:P$.

We may declare $\text{inr}\left(q\right);P\vee Q\text{true}$ when we've declared $q:Q$.

Characterizing the elimination rule for $\vee$ is a bit more complicated. Consider the following judgment.

to validate it, we consider what requirements are necessary to conclude $A\vee B\text{true}$. There are only two; either we declared $A\text{true}$ or we declared $B\text{true}$. This splits our goal into two separate cases which we must validate individually;

Both are easily declarable. Skipping some intuition, we declare the following;

case acts as a non-canonical witness for elimination. To see why the computation rules hold, consider the following judgment;

This should remind you of the introduction rule for implication. We first note that, in-order to declare $d:A\vee B$ we must have already a $d^{\prime };A\vee B$ where $d\downarrow d^{\prime }$. To validate our goal, we do a similar case split on $d^{\prime }$, which can only be of the form $\text{inl}\left(x\right)$ where $x:A$ or $\text{inr}\left(y\right)$ where $y:B$. We'll focus on the first of these cases, since the other is more-or-less the same. We have our new goal;

By the reduction rule for case, the conclusion reduces to $p[a:=x]:C$. We can see from the assumption ${|}_a\frac{a:A}{p\left(a\right):C}$ that we may conclude $\frac{x:A}{p[a:=x]:C}$, which allows us to trivially finish validating our goal.

Note the $.$ used in the syntax for case, similar to $\lambda x.y$. This will be our standard notation for variable binding outside of contexts and generalized judgments. This will be discussed in detail in the next chapter.

We may alter our elimination implementation to rely on implication. We define a modified case;

We may make a similar judgment through the fact that we can internalize generalized judgments using $\to$.

We can employ a similar trick to unify our two rules for $\wedge$ into a single generalized elimination rule. For $\vee$, we needed two functions to account for all possibilities. The issue with the $\wedge$ eliminators is not that they don't account for all possibilities, after all, there is only one, the pair. The issue is that neither one on their own accounts for all data. If we look at ${\pi }_1$;

we notice that it throws away half of our pair. Likewise with ${\pi }_2$. We need to have functions which account for all possibilities and all data if we want to have a unified eliminator.

Generically, we need a function which potentially operates on all internal data of our type constructor. For $\wedge$ we only have the two types it has as input. So, to eliminate a $A\wedge B$ in general, we need a single function $f:A\to (B\to C)$. To figure out what the return value will be, we just issue the components of the pairs to $f$. So we have;

From which we can verify;

We can recover the original eliminators by setting $f$ to be $\lambda x.\lambda y.x$ and $\lambda x.\lambda y.y$ since ${\pi }_f(\lambda x.\lambda y.x;(a,b\left)\right)\downarrow a$ and ${\pi }_f(\lambda x.\lambda y.y;(a,b\left)\right)\downarrow b$.

Furthermore, we can obtain ${\pi }_f$ from our old eliminators by defining it as $\lambda p.\lambda f.\text{ap}\left(\text{ap}\right(f;{\pi }_1\left(p\right));{\pi }_2(p\left)\right)$. This is just a different form of an eliminator we already had, not a more powerful principle.

We could also make a generalized eliminator like so;

It's this sort of eliminator which we'll make most often as we move onto mathematics in general.

Verum and Falsum

It's far easier to deal with verum and falsum when it comes to witnesses. The meaning explanation for trivial truth is simply;

We may declare $\text{tt};\top$.

and the meaning explanation for trivial falsehood is still the empty precommitment.

For the elimination of $\top$, we consider the following;

Consider what's necessary to declare $\frac{\top \text{true}}{A\text{true}}$. We would need to be able to declare $A\text{true}$ whenever we can declare $\top \text{true}$. By the meaning of $\top$, we may always declare $\top \text{true}$, meaning that we must always be able to declare $A\text{true}$. We reduce our goal to;

which is trivially verifiable. Using this, we can construct the following;

Using a similar strategy to before, we may verify;

Of course, this is somewhat trivial, as the generalized judgment which we're assuming covers $\text{tt}$. All this leads us to conclude that we can't really eliminate out of $\top$ since it doesn't contain any information.

Regarding $\perp$, we have something more interesting. Consider the following;

how might this be verified? Consider all the cases from which we can conclude $\perp \text{true}$. Well, there are none, we're done. We've verified this judgment for all the cases we may consider.

Some reader's unfamiliar with logic may find this reasoning a bit difficult to wrap they're head around, but it's called the principal of explosion, and is completely consistent with our previous forms of reasoning. For $\vee$ we needed to verify our elimination on two different cases. For $\top$, it was one case. For $\perp$, it's zero, allowing us to trivially finish verification.

For the lack of witnesses to $\perp$, we may verify, through similar reasoning as before, the following;

Defined Connectives

There are a handful of connectives which I've neglected to give meaning explanations to. Most significantly are negation, $\neg$ and the biconditional $\leftrightarrow$. They are defined in terms of what we have already defined. We simply assert the following;

Starting with the biconditional, we can validate the following judgments;

which sums up most use cases for $\leftrightarrow$.

$\neg$ is more interesting. We can investigate it by considering how excluded middle interacts with the logic I've so far presented. Excluded middle states that every proposition is either true or false, that $A\vee \neg A\text{true}$. This is NOT declarable in the logic I set out. Consider how this might interact with our proof theory. If it were declarable then there should be some uniform algorithm which, given any arbitrary proposition $A$, would return either $\text{inl}\left(a\right)$ where $a:A$ or $\text{inr}\left(na\right)$ where $na:\neg A$. There are, indeed, some logics which have this property, which will be discussed in a later post. For now, we can prove $\neg \neg (A\vee \neg A)\text{true}$. How would we verify this judgment?

We can reduce $\neg \neg (A\vee \neg A)$ to $\left(\right(A\vee (A\to \perp ))\to \perp )\to \perp$. To prove this, we start with a lambda term $\lambda x.{?}_1$, where $x:(A\vee (A\to \perp \left)\right)\to \perp$, and we need to find a ${?}_1:\perp$. Well, if we constructed a proof of $A\vee (A\to \perp )$, then we could apply it to $x$ to get our ${?}_1$. The only way we can get a proof of a $\vee$ is to use either $\text{inl}$ or $\text{inr}$. Off the bat, there's no clear way to give a proof of $A$, but maybe there's a way to prove $A\to \perp$, so let's go with $\text{inr}$.

$\text{inr}$ wants a proof of $A\to \perp$, so we start with a lambda term $\lambda y.{?}_2$, where $y:A$ and we need to find a ${?}_2:\perp$. Hey, now we have a proof of $A$, so we have $\text{inl}\left(y\right):A\vee (A\to \perp )$. We can issue that into $x$ to get $\text{ap}(x;\text{inl}(y\left)\right):\perp$, which is our ${?}_2$.

Rolling that into our lambda term, we have $\lambda y.\text{ap}(x;\text{inl}(y\left)\right):A\to \perp$. We then have $\text{inr}(\lambda y.\text{ap}(x;\text{inl}\left(y\right)\left)\right):A\vee (A\to \perp )$. We can issue this to $x$, obtaining $\text{ap}(x;\text{inr}(\lambda y.\text{ap}(x;\text{inl}(y\left)\right)\left)\right):\perp$, which is our ${?}_1$ goal. Rolling this into our outermost lambda term, we finally arrive at the following judgment;

which contains all the information necessary to recover our reasoning, compressed into a single line. More importantly, that expression can itself be reasoned about. It's not just an elegant presentation of our justification, it's data as well.