Brouwer-Heyting-Kolmogorov Interpretation of Logical Connectives

1. From Truth-Conditions to Proof-Conditions

Classical logic, as developed by Frege and Tarski, is grounded in truth-conditional semantics. The meaning of a logical connective is defined by how it contributes to the truth or falsity of a sentence. For example, the meaning of '$\wedge$' is captured by its truth table, which states that $P\wedge Q$ is true if and only if $P$ is true and $Q$ is true. This approach presupposes that every statement has a definite truth-value (true or false), independent of our ability to know it—the principle of bivalence.

Intuitionism rejects this picture. If truth is the existence of a proof, then a theory of meaning cannot be based on abstract truth-conditions. Instead, it must be based on proof-conditions. The meaning of a logical connective is explained by specifying what counts as a proof of a complex sentence in terms of proofs of its constituent parts.

This shift from a metaphysical to an epistemological theory of meaning was championed by the philosopher Michael Dummett.

Dummett's perspective provides the philosophical motivation for what is formally known as proof-theoretic semantics. Instead of asking "In what state of the world is this sentence true?", we ask "What kind of proof would justify asserting this sentence?". The BHK interpretation is the archetypal example of such a semantics.

2. The Clauses of the BHK Interpretation

The BHK interpretation provides a set of clauses that define the meaning of each logical connective by specifying what constitutes a proof for a statement containing that connective. This is sometimes called a "proof interpretation" or, in Kolmogorov's version, a "problem/solution interpretation".

Let's examine these clauses one by one.

Here is a breakdown of those clauses, which define the meaning of logic in terms of proofs, constructions, and transformations.

• Atomic Propositions & Contradiction ($\perp$):

  • The interpretation takes the notion of a proof for an atomic mathematical proposition as basic.
  • A proof of $\perp$ (the absurd proposition, or contradiction) is taken to be impossible.

• Conjunction ($\wedge$): A proof of $P\wedge Q$ consists of a proof of $P$ and a proof of $Q$.

  • This is the most straightforward clause and aligns perfectly with classical intuition. To prove two things, you must prove each one.

• Disjunction ($\vee$): A proof of $P\vee Q$ consists of a proof of $P$, or a proof of $Q$.

  • As we saw last lesson, this is a key point of divergence. To prove a disjunction, you must constructively prove one of the disjuncts. You cannot assert $P\vee Q$ simply because it's impossible for both to be false.

• Implication ($\to$): A proof of $P\to Q$ is a construction (a method or function) which transforms any given proof of $P$ into a proof of $Q$.

  • This is perhaps the most philosophically significant clause. An implication is not a static statement about truth-values; it is a promise of a transformation. Given your experience with functions in mathematics, you can think of a proof of $P\to Q$ as a function f whose domain is the set of proofs of P and whose range is the set of proofs of Q.

• Negation ($\neg$): Negation is typically defined in terms of implication and contradiction: $\neg P\equiv (P\to \perp )$.

  • Therefore, a proof of $\neg P$ is a construction that transforms any hypothetical proof of $P$ into a proof of a contradiction. This formalises the intuitionistic idea of a refutation.

• Quantifiers: The BHK interpretation extends naturally to quantifiers, highlighting the constructive nature of existence.
  • Existential Quantifier ($\exists$): A proof of $\exists xP(x)$ consists of presenting a specific object $d$ from the domain, along with a proof of $P(d)$. You must provide a "witness".
  • Universal Quantifier ($\forall$): A proof of $\forall xP(x)$ is a construction (a method) that, for any given object $d$ from the domain, produces a proof of $P(d)$.

3. Evaluating the BHK Interpretation

The BHK interpretation is not merely a technical curiosity; it represents a profound philosophical shift. It grounds logic not in a static, metaphysical picture of reality, but in the dynamic, epistemic activity of proving.

Strengths:

1. Philosophical Coherence: It provides a systematic and coherent semantics that flows directly from the constructivist premise that truth is proof.
2. Epistemically Grounded: Meaning is tied to what is knowable or demonstrable, avoiding commitment to verification-transcendent truths. For thinkers like Dummett, this is a major philosophical advantage, as it ensures our theory of meaning is tied to our linguistic practices.
3. Formalisation: This approach has been rigorously formalised in systems like Martin-Löf's constructive type theory, where propositions are identified with the types of their proof objects. This creates a deep connection between logic and computer science (via the Curry-Howard correspondence).

Challenges and Points of Debate:

One of the most interesting points of evaluation concerns the justification of the principle Ex Falso Quodlibet (from a falsehood, anything follows), which corresponds to the formula $\neg P\to (P\to Q)$.

According to the BHK clause for implication, a proof of this formula requires a general method that:

1. Takes a proof of $\neg P$ (i.e., a method f that turns any proof of $P$ into a contradiction).
2. Produces a new method, g, that turns any proof of $P$ into a proof of $Q$.

How can this be justified constructively? If we have a proof of $\neg P$, we believe that no proof of $P$ can ever be constructed. So the input for method g is impossible. How can we build a genuine construction on an impossible assumption? This has been a point of contention.

These justifications reveal a potential tension in the constructivist programme.

• Kolmogorov's approach is pragmatic and stipulative. It completes the logical system but arguably steps outside the strict 'meaning-as-construction' framework.
• Heyting's approach feels more like a post-hoc rationalisation, using phrases like "in a sense" to justify a principle that doesn't seem to have a direct constructive interpretation.

This shows that even within a proof-theoretic framework, there are subtle and difficult philosophical choices to be made about what counts as a valid justification. The debate over Ex Falso led some, like the logician Johansson, to develop "minimal logic," which is intuitionistic logic without this principle.

Conclusion

Today we have moved from the negative project of critiquing classical logic to the positive project of building an alternative. The BHK interpretation provides a complete, proof-conditional semantics for the logical connectives, systematically redefining logic in epistemic terms.

Key Takeaways:

• Proof-Conditions vs. Truth-Conditions: The BHK interpretation is a form of proof-theoretic semantics. It defines the meaning of a connective by what counts as a proof, not by its abstract truth-conditions.
• The BHK Clauses:
  • $\wedge$: Proof of both conjuncts.
  • $\vee$: Proof of one of the disjuncts.
  • $\to$: A method for transforming a proof of the antecedent into a proof of the consequent.
  • $\exists$: A specific witness and a proof for that witness.
• Philosophical Shift: This represents a move from a metaphysical view of logic (describing reality) to an epistemological one (codifying valid reasoning and justification).
• Points of Evaluation: While elegant, the BHK interpretation faces challenges in providing a purely constructive justification for all classical tautologies accepted by intuitionists, with Ex Falso Quodlibet being a prime example.

Preview of the Next Lesson:

We have now laid the full groundwork for intuitionistic logic. In our next lesson, we will see how Michael Dummett builds upon these ideas to construct one of the most influential philosophical arguments of the 20th century. We will analyse Dummett's argument that a theory of meaning must be grounded in the public manifestation of understanding, and explore why he believed this argument provides a powerful case for preferring intuitionistic logic over classical logic.