Syntax

We ask Coq to infer that equality of sentences is decidable

We'll give names to a few of the variables for convenience...

... and set up some pleasant notations. Notice some of these notations define new connectives, like disjunction, in terms of simpler ones. These notations use Unicode. Proof General and CoqIDE both support quick Unicode entry by typing TeX-like strings, see

• Coqide information (See "Using Unicode symbols")

• Company Coq

Next we define the semantics of our language. We want to translate sentences into Coq-level propositions, i.e. elements of type Prop. You might expect to use bool here instead. Both choices "work," but using Prop is more general and more natural for the metatheory we build here today, and ultimately it better captures the idea that a semantics maps object-level propositions into host-level propositions. Further information about this topic is provided below. A valuation might also be called an interpretation or a model, especially in the context of higher-order logics.

Model theory

We define a recursive function, denotation, which translates sentences to "actual" propositions, meaning types whose sort is Prop. Another good name for this function could be "is_true" or "translation." Notice that any valuation v defines a subset denotation v of sentences, namely the "true" ones.

Hereafter we let denotation take the valuation as an implicit argument. This follows common mathematical practice in which one generally assumes some valuation is clear from the context. Some functions, such as entails, will take valuations explicitly when this is more natural.

In this file, we're not very interested in individual valuations. Instead, we would like define a notion of "truth" which abstracts over the valuation, capturing the idea that a sentence is true under every possible interpretation.

The universal quantifier---the dependent product---can be thought of as a kind of infinite conjunction asserting the truth of ϕ under every interpretation. But we aren't just interested in tautologies. Often we want to restrict our attention to only those valuations which make certain pre-chosen sentences true. We develop this idea now. We require that the range of denotations for v : valuation satisfy the law of excluded middle. (You can read 'r' as 'range' or 'restricted', since this stipulation is only required for those propositions which are the denotation of a given valuation, i.e. in the range of some valuation.

A set of sentences is satisfied or modelled by a valuation if all of its elements are true under that valuation. Elements of Γ may also be called "axioms."

A valuation that models Γ is called a model, unsurprisingly.

A set of axioms entails a sentence when that sentence is true under all valuations that also satisfy the axioms, i.e. all models. This relation also known as semantic consequence or logical consequence. We might also read this definition as a restricted variant of tautology that intersects only over that subset of valuations which satisfy Γ. This property is sometimes known as being /valid/ for Γ (but this word is sometimes used differently). When we formalize our proof system, the most ideal outcome is that the provable formulas are precisely the valid ones.

Sample usage of the lem tactic.

Use the following tactic to quickly get rid unfold many definitions.

Exercise 1 (easy): Prove that a sentence is a tautology if and only if it is entailed by the empty set of axioms. Note: This is almost true by definition, but formalizing logics in Coq often means proving such "obvious" facts.

Exercise 2 (easy): Prove the following tautology.

Exercise 3 (medium): Have we formalized implication correctly? Check our work by proving if x ⇒ y is true and x is true, then y is true. Hint: Use the lem tactic to do case analysis on Q. You may want to Unset Printing Notations.

Logically equivalent formulas are those which have the same denotation under every interpretation. Since we are interpreting into Prop, rather than bool, we define this notion using biconditionality (at the Coq level) rather than equality of boolean values, but the idea is the same.

Exercise 4 (easy): Prove that P and P ∧ ⊤ are semantically equivalent.

Exercise 5 (medium): Prove that P and P ∨ ¬ ⊤ are semantically equivalent. Use lem P.

Exercise 6 (hard): Why did the last exercise require law of excluded middle, when Coq trivially proves the following intuitionistic tautology? Can you prove that the last exercise cannot be completed without LEM?

Proof theory

This section explores basic proof theory. The goal is to define a particular syntactical notion called "proof," where each proof is associated with a formula called its "conclusion." Formulas with proofs are "theorems." The main theorem is that a formula ϕ entailed by Γ precisely if there is a proof with conclusion ϕ using only axioms from Γ, i.e. theorems are exactly validities. The following proof system is a natural deduction, which is essentially the type system of the simply typed lambda calculus. However, we are not formalizing lambda terms here, only the type inhabitation property itself.

The next two lemmas are fundamental properties of most logics. Substitution shows that provable hypotheses are redundant. Weakening says unused hypotheses are okay and plays an important role in proving substitution.

To picture substitution, imagine a natural deduction derivation D that uses of ψ using hypotheses from Γ1, Γ2, and ϕ. Given a natural deduction derivation E of ϕ, picture "moving up" the tree of D and finding all leaves that introduce the axiom ϕ, and replace them with E. Through Curry-Howard, this is essentially function evaluation.

Relating proofs to truths

The following exercise is mostly straightforward but requires a good grasp on the definitions in play. By unfolding the definitions, we see that soundness is a computation with two inputs:

• a "proofs" of a "proposition"
• a model of the axioms Γ

and the output is exactly a (Coq-level) proof of the (Coq-level) proposition which interprets the "proposition" in that model! Exercise 7 (medium/hard): Prove that all sentences provable from Γ are logically entailed by Γ. The negation introduction and double negation elimination cases may require some pen-and-paper thinking.

This next theorem is difficult to show, even for such a simple logic. In fact, that we won't even try to prove it in Coq. You are encouraged to attempt it to find where the difficulty lies. Why should this be hard to prove? Consider the premise: In all valuations satisfying every sentence of Γ, ϕ is true. This quite abstract condition is essentially a statement about truth tables: "If all rows of a truth table that also satisfy each formula in Γ also satisfy ϕ, find a natural deduction derivation of ϕ." Notice the premise gives us almost no information about ϕ, not even its basic structure. The sentences of Γ may also be very complex, perhaps more complex than ϕ, so they don't necessary tell us anything about ϕ's subformulas. In fact, while ϕ may be true under every (Γ-satisfying) valuation, each row of the truth table might make ϕ true "for different reasons," so to speak. Where do we get started? Nonetheless, this theorem is true, and can even be proved constructively.

Exercise 8 (easy? hard?): Attempt to prove the following: "There is a sentence of propositional logic that is neither provable nor disprovable from the empty set of axioms." Use the formula P (a simple propositional variable) as ϕ. Attempt to prove this by induction on the derivation of P. A template has been provided. What happens?

We want to scrutinize the supposed derivation of P. If we just do induction J, Coq will automatically generalize over the context and conclusion P, as if were trying to show there are no proofs of anything. To avoid this silly behavior, we tell Coq to remember both the conclusion P and the emptiness of the context. We also discharge trivial cases instantly.

Exercise 9 (easy): What do the hard cases above have in common? (Hint: Look at the names of the rules that caused us difficulty.). The theorem above seems obvious, but it is hard to show by examining proof trees. The trouble is that in each elimination rule, we cannot be confident that the rule used to prove the hypothesis is a corresponding induction rule. Indeed, it might not be: Perhaps we prove P by proving P /\ Q, and perhaps to prove /that/ we use double negation elimination (for example). Can you rule this out? Although implication is not defined primitively, it is an illustrative example: Perhaps we prove P by showing Q ⇒ P and Q. How can we rule this out? Fundamentally we need a cut-elimination theorem, specifically the corollary of a canonical form lemma (or inversion lemma). We won't prove this hard theorem here. Instead, we can show the above theorem by using soundness: We cannot prove P because it is not true in all models!

Exercise 10 (medium): Prove the following statement using the two constant valuations defined above.

Commentary

Understanding Incompleteness

So how can we understand Gödel's incompleteness theorem? Let's imagine starting over at the beginning. Suppose instead of formalizing propositional logic, we allowed propositions to vary over tuples of /terms/, as well as introducing quantifiers. This would be first-order logic (FOL). Formalizing the syntax is not particularly hard (albeit tedious). The semantics are also straightforward: The valuation primarily consists of a type D called the /domain/, with constants mapped to terms of D, and functions denoting Coq-level functions over D. Finally, relations will denote subsets of D (e.g., binary relations are of type D -> D -> Prop. The proof rules are also not too complicated: To prove a universally quantified sentence, give a natural deduction proof of the body after substitution by a fresh variable known as a /parameter/. Existentials are proved by proving the body for an arbitrary closed term. It turns out, this logic is also complete: if ϕ is true in all models satisfying Γ, there is a natural deduction proof of ϕ using the set Γ as axioms. This is Gödel's completeness theorem. First order logic is essentially the strongest logic that can have this property, as provability (as a semi-decidable property) is too weak to properly capture the semantics of higher logics. Finally, instead of considering an arbitrary Γ, consider a particular set of sentences called the /Peano axioms/. (This set is actually infinite due to the induction schema, so we would need to tweak our definitions to handle this.) This combination of first-order logic with a fixed set Γ of Peano axioms is first-order Peano arithmetic. Coq's natural numbers type nat is a model of this theory, but one can show there are other models. Gödel proved the following fact (actually, Gödel's theorem is significantly more general. But the following is a corollary.): There is a sentence ϕ of the language which is:

• True, in the sense that it is true when interpreted into the model given by nat.
  • Unprovable: There is no natural deduction derivation of
  this sentence.
  Since Gödel also proved first-order logic is complete, as an instant corollary we see ϕ is:
  • invalid: There are models in Coq of first-order Peano arithmetic in which the sentence is not true.

This last fact is somewhat of a coincidence. Gödel's incompleteness theorem applies equally to say, second-order arithmetic. That theory also has a (different!) sentence which is true when interpreted into Coq's nat type, but unprovable in this theory. However, this sentence is valid because second order arithmetic has only one model, nat, in which the sentence is true.

Why is incompleteness important? Or is it?

Clearly, syntactical incompleteness is not generally surprising. For instance

• Coq is incomplete because it neither proves nor disproves LEM
• Group theory is incomplete because it neither proves nor disproves the commutativity property
• Propositional logic is incomplete because it neither proves nor disproves any atomic propositional symbol P

It is somewhat surprising that Peano arithmetic is incomplete, because it is not at all obvious which properties of nat are being left out. What else can we add? But it's still not terribly hard to understand, either. But Gödel's theorem says a lot more than this, because the real theorem proves that **any** theory of natural numbers is incomplete, provided:

• we can recognize valid proofs when we see them
• the theory can prove basic facts (things which can be proved without even using induction)

Surely it is reasonable to say Gödel's theorem proves the incompleteness of any reasonable number theory. It is the fundamental inability to every form a complete number theory which is so surprising. Furthermore, some additional logic from Gödel proves that such a theory cannot prove its own consistency. But why do we care? After all, if we don't trust a logic, then we would never trust such a proof of consistency in the first place. The answer is simple: Because if arithmetic can't prove the consistency of itself, obviously it could never prove the consistency of all of mathematics! This effectively invalidates Hilbert's program to "finitize" mathematics.

Does this mean natural numbers can't be defined?

Not in any mathematical sense. Coq can prove the uniqueness of nat with some ease. ZFC (set theory) can also prove that there is a set, omega, with the properties of natural numbers which is unique up to ordinal isomorphism. If we upgrade first-order Peano arithmetic to its second-order version, both Coq and ZFC (etc.) prove that there is exactly one type/set that can model this theory. And so provided you are willing to work within a powerful theory like Coq, there is absolutely a unique "thing" called the natural numbers. It just happens that there will be some sentence of our logic that we cannot prove, even though it is true if you interpret your metalogic as a formal theory (inside some other theory).

Interpreting into Prop and bool

You might expect that we would translate propositional logic into bool instead. This would work for most purposes, and might better align with your normal intuition for propositional logic, but there are several reasons to prefer translation into Prop over bool: 1.) Due to Coq's constructive nature, we can only write functions of type sentence -> bool that we can compute. This means we can only describe computable models in Coq, which rules out much of mathematics if you extend this to higher-order logics. In the best case scenario, this is just an artificial limitation on which individual models we can define in Coq. In some scenarios, it might limit what we can prove about the metatheory, since we can't describe uncomputable counterexamples, for example. 2.) Ultimately a semantics **must** map object-level propositions into meta-level propositions, since X ⊧ ϕ is a proposition in the host logic--that's the whole point. If we used a boolean valued semantics in Coq, the notion X ⊧ ϕ must be understood as the Coq-level proposition ⟦ ϕ ⟧ = 1 (for valuations satisfying X), which means our boolean-semantics must be composed with the function fun b : bool => b = true : bool -> Prop. Again, this "works," but it is somewhat awkward for some purposes in Coq. A bool-valued semantics might be preferred if we want to compute with propositional logic (such as to model circuits), but our perspective is that Prop-valued interpretations are the more general approach, and more illuminating when understanding the relationship between the host and guest logics. This approach is called algebraic semantics, and with propositional logic it means our valuatons can be any Boolean-algebra homomorphism. Using bool is then a kind of degenerate case. How is our approach more general? Consider that ⟦ p → p ⟧ is a propositional tautology, and accordingly ⟦ p ⟧ → ⟦ p ⟧ is provable in Coq no matter what Prop we assign to p, even if that proposition is not itself provable in Coq. This illustrates that the soundness of propositional logic does not depend on the fact that we often study computable models of this logic. However, there are some caveats to the algebraic approach in Coq: 1. We must assume LEM, or at least assume (or prove) this property for every valuation we consider in order to have soundness. This is a result of interpreting propositional logic into a constructive logic. 2. If we want to "count" valuations (common when thinking about circuits), the right notion of equivalence between two valuations is that two interpretations yield equi-provable sentences in Coq. Different valuations are rarely literally equal.