# Defining our Logic

I’ve recently become interested in model theory, and as I’ve started reading about it, one question in particular has been eating on me: why do we need to do model theory at all? This series of posts will answer that question, hopefully saving others the trouble of figuring it out for themselves. This post defines the logic that we want to model.

- Part 1: What is a Model?
- This post describes the motivation for model theory and the language these posts will model. Why do we need models, and how do they help us understand logic?
- Part 3: A Logic in Coq
- With the logic defined in words, we want to formalize it in Coq, both to make sure we don’t make any mistakes, and to take advantage of the “assistant” part of “proof assistant”. I explain how to encode our syntax and our transformation rules in Coq, using dependent types. (I also complain about Coq’s dependent matcher.)
- Part 4: Defining a Model
- Now that we have a logic, we need a model—a “real” mathematical object that behaviors just as the logic dictates. In our case, that is a Heyting algebra: a mathematical structure which mirrors the mechanics of constructive logic. I’ll define Heyting algebras (in words and in Coq), and then demonstrate one obvious Heyting algebra, and one non-obvious Heyting algebra.
- Part 5: A Model in Coq
- The model is defined in words, but we want that same model in Coq. I use the type-class mechanism to define both the obvious and the non-obvious Heyting algebra, and prove that they satisfy all associated laws.
- Part 6: Non-standard Models
- Now that we have a logic and a structure that models it, we can discuss facts about the logic by using the model. One nice fact about the logic is that
*any*Heyting algebra can model our logic; our logic should not be able to distinguish between different models. So we can show that certain facts are*unprovable*in our logic, by showing that they are false in some models. This is cool, because they may be facts true of the models we’re used to thinking about.

## Defining a logic: propositions

As discussed in the last post, a logic is just a set of strings of symbols, and a set of rules for transforming strings of symbols into one another. Usually, both of these are defined inductively: the strings of symbols are defined in terms of abstract syntax trees, and the transformation rules are defined in terms of an inductive relation between these syntax trees.

The logic I’m going to be talking about intuitionistic predicate logic. I’ll be talking about only a fragment, because my logic won’t include a `∃`

quantifier (I’ll discuss why in part 4).

Let’s start by writing down the syntax—the strings of symbols that this logic describes—and then we can talk about the semantics. Our fragment of intuitionistic logic describes strings made up of the *connectives* `→`

, `∨`

, `∧`

, `⊤`

, `⊥`

, and `∀`

(they’re called connectives because they connect other things) and variables. To define this formally, we need to give an inductive definition for this syntax. For now, we’ll make do with:

**Definition**: a *proposition* in our logic is one of:

`⊤`

,`⊥`

, or a variable;`e₁ → e₂`

,`e₁ ∨ e₂`

, or`e₁ ∧ e₂`

, where`e₁`

and`e₂`

are propositions;

To state this in Coq, we’ll need to refine how variables work, but this definition is more than enough when we’re working in text. Note that we have not defined the *meaning* of `∨`

or `∧`

; in fact, so far they are indistinguishable.

## Defining a logic: transformation rules

To define the meaning of the various expressions, we will define transformation rules on symbols. These rules will, of course, distinguish between `∨`

and `∧`

. The intuition for these rules is that they should transform “true” propositions only into “true” propositions. (Of course, we aren’t really talking about truth—just syntax—but that’s the intuition).

As it happens, almost all of these rules will be phrased as things that transform into `⊤`

. This isn’t necessary, though it is very neat. It’s due to the fact that I got these rules by munging a natural deduction presentation of intuitionistic logic. In all these rules, all variables are arbitrary propositions. A rule is written `e₁ = e₂`

, meaning that either of `e₁`

and `e₂`

can be transformed into the other. (In principle, one could have one-way rules; this logic doesn’t have any.)

The first two rules describe “implies”; namely, they demonstrate *weakening* and *substitution*:

`e₁ → (e₂ → e₁) = ⊤`

`(e₁ → e₂ → e₃) → ((e₁ → e₂) → (e₁ → e₃)) = ⊤`

, with implication associating to the right

The next three rules describe “and”; they are two *elimination* rules and one *introduction* rule:

`e₁ ∧ e₂ → e₂ = ⊤`

and`e₁ ∧ e₂ → e₁ = ⊤`

`e₁ → e₂ → e₁ ∧ e₂ = ⊤`

The next three describe “or”; they are one elimination rule and two introduction rules:

`(e₁ → e₃) → (e₂ → e₃) → (e₁ ∨ e₂ → e₃) = ⊤`

`e₁ → e₁ ∨ e₂ = ⊤`

and`e₂ → e₁ ∨ e₂ = ⊤`

Finally, we have one rule each for “true” and “false”:

`e₁ → ⊤ = ⊤`

`⊥ → e₁ = ⊤`

We’re missing only “for all”; describing that will require using substitution, which I’ll write `e₁[x ↦ e₂]`

(meaning, substitute `e₂`

for each occurrence of `x`

in `e₁`

). This rule is one-directional; this logic has a for-all connective only in a very limited way.

`(∀ x, e₁ → e₁[x ↦ e₂]) = ⊤`

`(∀ x, e₁) = e₁`

, if`e₁`

does not mention`x`

.

When we do proofs in this logic, we usually it by substituting inter-convertible expressions for each other. There’s a sort of meta-rule, that if `e₁ = e₂`

, and `P[e₁] = Q`

, where `P`

is some large expression with a hole filled by `e₁`

, then `P[e₂] = Q`

. To make this meta-rule more powerful, we’re going to say that propositions that imply one another are equal:

- If
`e₁ → e₂ = ⊤`

and`e₂ → e₁ = ⊤`

, then`e₁ = e₂`

. - If
`⊤ → y = ⊤`

, then`y = ⊤`

.

Now that we’ve defined a logic, we should be able to prove some facts by pure symbol-manipulation.

## Internal characterizations

We’ve defined some rules by which expressions can be transformed; but how does that lead to *proving* properties? We only want to prove “true” properties, but we haven’t yet defined truth. So instead, we’ll take an *internal* notion of truth.

This is incredibly important, so I want to take a moment to dwell on it. The notion of “truth” is complex and slippery (we’ll get to it in the next post). Because it’s hard to describe which things are “true”, we’ll take a conservative approach. Instead of defining which things are true and which are not, we’ll only define a *conservative* notion of truth: we’ll define a way to describe only true properties, but not necessarily all true properties. We do this by describing a set of building blocks, which can only combine into true properties.

This is called an *internal* characterization of truth, because we don’t have to actually define truth; we just define a small set of building blocks and proclaim them to only produce true things. But it’s weaker than external notions of truth, because there may be true properties that are not captured by our building blocks. One of the incredible things about first-order logic is that this internal notion ends up being complete—it ends up being equivalent to an external notion of truth (this is a rough and informal view of Gӧdel’s Completeness Theorem).

## Proving things

So what’s our internal characterization? What’s our conservative estimate of truth? It will be this: `⊤`

is true, and truth is maintained by the transformations we’ve defined.

A proof is only a check-able record of the internal notion of truth that we’ve just defined; so, it must be a sequence of transformations that transform a given statement into just `⊤`

.

For example, let’s try to prove that `∀ x, (x ∧ (x → ⊥)) → ⊥`

. If we define `¬ x`

to be `x → ⊥`

, this is `∀ x, ¬ (x ∧ ¬ x)`

. To make things easier to read, I’ll write `e₁`

for the string `x ∧ (x → ⊥)`

. This is not a variable in the logic itself—it is a meta-variable, to be interpreted by us humans. The proof is:

`⊤`

is true, so`∀ x, ⊤`

is true, so`∀ x, (e₁ → x → ⊥) → (e₁ → x) → (e₁ → ⊥)`

is true by the substitution rule, so`∀ x, ⊤ → (e₁ → x) → (e₁ → ⊥)`

is true by and-elimination, so`∀ x, ⊤ → ⊤ → (e₁ → ⊥)`

is true by and-elimination, so`∀ x, ⊤ → (e₁ → ⊥)`

is true by the second equality rule, so`∀ x, e₁ → ⊥`

is true by the second equality rule, which is`∀ x, (x ∧ (x → ⊥)) → ⊥`

by expanding`e₁`

.

This proof was ugly and at least a bit tedious, but it should give you reason to think that the logic we’ve defined is at least a little bit useful. This trick of “substituting `⊤`

for things” is the main activity of these proofs. Sometimes (though not here), the proofs branch by proving a lemma of the form `x = y`

by showing `x → y = ⊤`

and `y → x = ⊤`

.

## Conclusion

We’ve now defined a logic, as a collection of strings of symbols and a collections of valid transformations on those symbols. We’ve also defined an internal notion of truth, as things provable by transforming things into `⊤`

(or vice versa). The next post will formalize these definitions in Coq.