Propositions as Proofsets: Unwinding the confusion

13 Replies

My type theory post about the different interpretations of a proposition caused a furor in the comments. Understand what’s going on that caused all of the confusion is going to be important as we continue to move forward into type theory.

The root problem is really interesting, once you see what’s going on. We’re taking a statement that, on the face of it, isn’t about sets. Then we’re appyling a set-based interpretation of it, and looking at the subset relation. That’s all good. The problem is that when we start looking at a set-based interpretation, we’re doing what we would do in classical set theory – but that’s a different thing from what we’re doing here. In effect, we’re changing the statement.

For almost all of us, math is something that we learned from the perspective of axiomatic set theory and first order predicate logic. So that’s the default interpretation that we put on anything mathematical. When you talk about a a proposition as a set, we’re programmed to think of it in that classical way: for any set $S$ , there’s a logical predicate $P_s$ such that by definition, $\forall x: x \in S \Leftrightarrow P_s(x)$ . When you see $P \Rightarrow Q$ in a set-theory context, what you think is something like $\forall x: x \in P \Rightarrow x \in Q$ . Under that intepretation, the idea that $P \supset Q$ is equivalent to $P \rightarrow Q$ is absolutely ridiculous. If you follow the logic, implication must be the reverse of the subset relation!

The catch, though, is that we’re not talking about set theory, and the statement $P \Rightarrow Q$ that we’re looking at is emphatically not $\forall x : P(x) \Rightarrow Q(x)$ . And that, right there, is the root of the problem.

$P \rightarrow Q$ always means $P \rightarrow Q$ – it doesn’t matter whether we’re doing set theory or type theory or whatever else. But in set theory, when we talk about the intepretation of $P$ as a set, right now, in the world of type theory, we’re talking about a different set.

Super set doesn’t suddenly mean subset. Implication doesn’t start working backwards! and yet, I’m still trying to tell you that i really meant it when i said that superset meant implication! how can that possibly make sense?

In type theory, we´re trying to take a very different look at math. In particular, we’re building everything up on a constructive/computational framework. So we’re necessarily going to look at some different interpretations of things – we’re going to look at things in ways that just don’t make sense in the world of classical set theory/FOPL. We’re not going to contradict set theory – but we’re going to look at things very differently.

For example, the kind of statement we’re talking here about is a complete, closed, logical proposition, not a predicate, nor a set. The proposition $P$ is a statement like “‘hello’ has five letters”.

When we look at a logical proposition $P$ , one of the type theoretic interpretations of it is as a set of facts: $P$ can be viewed as the set of all facts that can be proven true using $P$ . In type theory land, this makes perfect sense: if I’ve got a proof of $P$ , then I’ve got a proof of everything that $P$ can prove. $P$ isn’t a statement about the items in $P$ s proof-set. $P$ is a logical statement about something, and the elements of the proof-set of $P$ are the things that the statement $P$ can prove.

With that in mind, what does $P \Rightarrow Q$ mean in type theory? It means that everything provable using $Q$ is provable using nothing but $P$ .

(It’s really important to note here that there are no quantifiers in that statement. Again, we are not saying $\forall p: P(x) \Rightarrow Q(x)$ . $P$ and $Q$ are atomic propositions – not open quantified statements.)

If you are following the interpretation that says that $P$ is the set of facts that are provable using the proposition $P$ , then if $P \Rightarrow Q$ , that means that everything that’s in $Q$ must also be in $P$ . In fact, it means pretty much exactly the same thing as classical superset. $Q$ is a set of facts provable by the statement $Q$ . The statement $Q$ is provable using the statement $P$ – which means that everything in the provable set of $Q$ must, by definition! be in the provable set of $P$ .

The converse doesn’t hold. There can be things provable by $P$ (and thus in the proof-set of $P$ ) which are not provable using $Q$ . So taken as sets of facts provable by logical propositions, $P \supset Q$ !

Again, that seems like it’s the opposite of what we’d expect. But the trick is to recognize the meaning of the statements we’re working with, and that despite a surface resemblance, they’re not the same thing that we’re used to. Type theory isn’t saying that the set theoretic statements are wrong; nor is set theory saying that type theory is wrong.

The catch is simple: we’re trying to inject a kind of quantification into the statement $P \Rightarrow Q$ which isn’t there; and then we’re using our interpretation of that quantified statement to say something different.

But there’s an interpretation of statements in type theory which is entirely valid, but which trips over our intuition: our training has taught us to take it, and expand it into an entirely different statement. We create blanks that aren’t there, fill them in, and by doing so, convert it into something that it isn’t, and confuse ourselves.

13 thoughts on “Propositions as Proofsets: Unwinding the confusion”

Brian Slesinsky February 27, 2015 at 1:07 am

Very clear. Thanks!

Loading...

Reply ↓
John Armstrong February 27, 2015 at 11:34 am

I think it cuts closer the the nub of the problem to just say that $\supset$ means something different in logic than in set theory, just like $\pi$ means different things in different contexts. There may be some way of interpreting a logical “type” like $P\supset Q$ in a set-theoretic context, but it’s at odds with the more widely-known correspondence between set theory and classical logic, as taught in freshman or sophomore college CS classes, and the notation happens to be exactly backwards between the two. Bringing up the set-theoretic interpretation before cementing the logical meaning of $\supset$ we actually care about here just ends up confusing people.

Loading...

Reply ↓
1. markcc Post authorFebruary 27, 2015 at 11:44 am
  
  I disagree.
  
  Superset means *exactly* the same thing that you expect it from set theory. The proof-set of a proposition $P$ is a classical set of objects (provable facts). The proof set of a proposition $Q$ is also a classical set-theoretic set of objects. And the set of proof objects in $P$ is a superset, by exactly the classical set-theoretic definition, of the set of proof objects in $Q$ . Every object that is a member of the set $Q$ is also a member of the set $P$ .
  
  The only type theoretic thing we’re doing here is allowing a logical proposition to be represented as a set of the facts that it can be used to prove.
  
  Standard FOPL says that, without further qualification, a predicate $P$ and a set $P$ are the same thing – that given any predicate $P$ , the set for $P$ is the collection of objects that satisfy the predicate.
  
  In the current stuff in type theory, we’re not talking about predicates. We’re talking about propositions. In set theory/FOPL, we don’t associate sets with propositions. A proposition is simply true or false; the idea of identifying a set with it is foreign.
  
  In this bit of type theory, we are identifying sets with closed propositions. That’s the only really new thing. And yes, the logical relationships between the sets identified with propositions are different than the logical relationships between sets identified with predicates – which makes perfectly reasonable sense, since they’re different things!
  
  But at the level of sets? These are still sets, and they behave exactly as you’d expect sets to behave. But (to repeat myself) the relationship between the logical operations on propositions and the set-theoretic operations on sets are new.
  
  Loading...
  
  Reply ↓
Brian Slesinsky February 27, 2015 at 1:14 pm

On further thought, I’m still confused. It seems strange to say that P->Q doesn’t add any new information that wasn’t already in P. This isn’t like traditional logic where you’d say:

(1) P
(2) P->Q
———–
(3) Q

Here, facts (1) and (2) are independently asserted as premises and you can’t get to (3) without both of them. That is, (3) depends on both (1) and (2).

But apparently in this new theory, the entire proof of Q is included in P alone? Is “P” is associated with a set including facts (1), (2), and (3)?

Loading...

Reply ↓
1. markcc Post authorFebruary 27, 2015 at 1:20 pm
  
  We’ll get to more details later – for now, remember that we’re still in the land of an informal definition, so when we get to formalisms, there are (naturally) lacks.
  
  The gist is that because we’re dealing with simple propositions, then yes, all of it is in P.
  
  In classical logic, you can’t do much with propositions. The set of all things provable by a simple proposition within a given system of axioms is closed. The set of all things provable by $P$ isn’t really a property of $P$ – it’s a property of $P$ within a specific inference system and a specific set of axioms. $P$ and $P \Rightarrow Q$ exist within the same closed system, and because $P \Rightarrow Q$ is part of that system, $Q$ is part of the provable-set of $P$ .
  
  Loading...
  
  Reply ↓
Russ Abbott February 27, 2015 at 5:09 pm

That was a clear explanation. What I don’t understand is why the => symbol is used. Is there a good English term/phrase for => that is consistent with both the forward pointing nature of => and its interpretation as you explained it?

Loading...

Reply ↓
1. markcc Post authorFebruary 27, 2015 at 5:37 pm
  
  The $\Rightarrow$ statement is still plain-old logical implication.
  
  If I’ve got a proposition $P$ , which is true, and I’ve got the implication $P \Rightarrow Q$ , then I can combine them to infer $Q$ . Absolutely bog-standard logic.
  
  The only thing here that’s at all new is the basic idea of constructive/computational proofs as an intrinsic part of the semantics. $P$ is true means that there is a proof for $P$ . $P \Rightarrow Q$ means that if I have a object that is a proof of $P$ , then I can computationally produce a proof of $Q$ . from that proof of $P$ .
  
  Loading...
  
  Reply ↓
Matti February 28, 2015 at 12:31 pm

That explanation makes sense. I think I know where the misunderstanding came from, at least for me: in the previous post you talked about “proofs of A”, and also referred to the “proof-set of A”. Those words sound like the proof-set of A would be the “set of proofs of A”, which it isn’t! The proof-set of A is more like the set of consequences of A, i.e. things that A can prove.

Am I on the right track?

Loading...

Reply ↓
1. markcc Post authorFebruary 28, 2015 at 1:26 pm
  
  Yes.
  
  Loading...
  
  Reply ↓
Robert March 2, 2015 at 6:17 am

Mark, I have some comments on your book at:http://robertvienneau.blogspot.com/2015/02/bad-math-in-good-math.html.

I found the chapter on typed lambda calculus to be the most advanced chapter.

Loading...

Reply ↓
Michael Norrish March 4, 2015 at 10:53 pm

If you identify propositions with the set of all possible consequences of those propositions, then you do indeed get the implication symbol to map to superset. Unfortunately, this view is not compatible with the idea of propositions being identified with sets of their proofs (as is traditional, and as you had it in your first post).

Consider the case of F(alse). In this post’s explanation, F corresponds to the universal set because every possible proposition is a consequence of F, and indeed, we have F ⊃ P, for all propositions P.

But if propositions should be identified with the sets of their proofs, then F should correspond to the empty set because F doesn’t have any proofs.

In this setting, talk of subsets and supersets is totally bogus. For one thing, a proof of A is manifestly not a proof of B unless A = B, and vice versa. Thus elements of one type aren’t even comparable with elements of the other. As you did say, if A ⊃ B, there is a function that transforms proofs of A into proofs of B (the type theory literature tells us that implications map to function spaces). We can’t judge the relative cardinality of the spaces from this fact. Perhaps B is something that has 1 proof and A has 10million. Perhaps it’s the other way round. Both are possible. In neither case is one a subset of the other.

Loading...

Reply ↓
1. Brian Slesinsky March 23, 2015 at 1:23 pm
  
  That’s an interesting paradox but I can guess at a way to resolve it. From a constructivist standpoint, perhaps False as a proposition shouldn’t even exist because there is no proof of it? If so, it’s not the empty set or the universal set. It’s not a set at all; it’s just undefined.
  
  (Pure speculation; I’d be curious if that’s actually true.)
  
  Loading...
  
  Reply ↓
  1. markcc Post authorMarch 23, 2015 at 1:39 pm
    
    You’ve got it almost exactly.
    
    If you’re looking at a proposition as the set of everything that it proves, then what you’re doing is looking at the set of everything that it proves, not the set of everything that it could prove if it were true. (Remember, this view only works in simple propositional logic, and there, the set of things proven by a given proposition is closed and finite!)
    
    So in this view, “false” taken as a proposition is always false, which means that it can’t ever be used to prove anything. So “false” is the empty set – which is exactly what you should expect!
    
    Loading...
    
    Reply ↓