Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: theory: mathematics

Topic: Relating Top and Bottom to True and False


view this post on Zulip Julius Hamilton (Nov 14 2024 at 19:30):

If I were to try to model something like propositional logic from scratch, a natural mathematical structure to express the idea that “statements can be true or false” would seem to be a function, eval:PropBool\text{eval} : \text{Prop} \to \text{Bool}, and two terms true:Bool,false:Bool\text{true} : \text{Bool}, \text{false} : \text{Bool}.

The next two things that would strike me as ‘missing’ would be adding structure both to Prop\text{Prop} and to Bool\text{Bool}.

The most essential aspect of truth-values seems to me to be their complementary relationship: true is the “opposite” of false; and we can define this with not:BoolBool\text{not} : \text{Bool} \to \text{Bool}, and equations not(true)=false,not(false)=true\text{not}(\text{true}) = \text{false}, \text{not}(\text{false}) = \text{true}. There are various ways to axiomatize this; I am pretty sure double negation elimination follows from what I just wrote, but you could also have one ground term, one function, and double negation elimination: true:Bool,not:BoolBool,x:Bool[not(not(x))=x]\text{true} : \text{Bool}, \text{not} : \text{Bool} \to \text{Bool}, \forall x : \text{Bool} [\text{not}(\text{not}(x)) = x].

I believe we are showing that true/false under negation is the cyclic group of order 2, a.k.a. the integers mod 2.

What is interesting to me is how it feels more conceptually accurate to separate truthhood and falsehood as elements, from propositions. We could either say that truthhood and falsehood are actually properties of propositions - expressed like true(P),false(Q)\text{true}(P), \text{false}(Q), or that they are elements which a truth-function “corresponds propositions to”.

It feels like we often see propositional logic presented in a way that lumps together propositions and their truth-values. To me, this can lead to some confusion.

It actually seems like some of the operations we commonly see in the axioms of a Boolean algebra much more naturally apply to propositions. For example, “and” and “or” are compositional operations which build new propositions out of other ones: and:Prop,PropProp\text{and} : \text{Prop}, \text{Prop} \to \text{Prop}. I’m saying that if starting from first principles, I find it more intuitive to locate “and” as being an operation on propositions, and “not” as an operation on truth values: we then have to define how “and” on propositions corresponds to some operation on those propositions’ truth values, but that is not “where you start out” from.

I think propositions naturally have an associated concept of their meaning. So we can think of “and” and “or” as being, on the one hand, syntactic operations on the linguistic units we associate with “propositions”, but which correspond to a certain kind of “composition of meanings”, on the meaning side.

Now it seems like our basic ability to say meaningful things, compose those meanings, and evaluate those meanings, can be modeled with three types: Sentence (“abskekc”, “kejebeiekn”), Meaning (some way of expressing “something about something”; like a property of a thing, a structural characteristic), and Judgment (“yes or no”).

A compact presentation of a Boolean algebra makes it seem like a lot of the above can be bundled together. The element “\top” in some situations can be interpreted as “truth”, but it isn’t. It is a sentence which evaluates to true. Even under that conception, it isn’t that well-defined, in my opinion. We asserted there was an evaluation function eval\text{eval}, but we haven’t yet explained under what conditions a sentence could “always evaluate to true”. So far, we made it seem like every sentence, hypothetically, is contingent - all assertions have the potential to be either true or false. (I also find this to be a more defensible “first principle”, to define propositional logic from.)

So if a priori, a sentence has a meaning, and it can, conceivably, be true or false, the idea that certain compositions of propositions would in a more a posteriori way turn out to always evaluate to true, seems to be more like a property we added in, on top of our “base” system.

I need a moment to think about how I would prefer to define / introduce that concept, though.

All in all, I felt like sharing this idea that had been in the back of my mind, that it feels like the standard way one discusses propositional logic in terms of a Boolean algebra, is actually very much an a posteriori finding that the structure of propositional logic kind of mathematically/algebraically can be “reduced” to that set of axioms, but it feels like it deeply masks the justification for where that structure originally comes from.

view this post on Zulip Josselin Poiret (Nov 15 2024 at 18:38):

Julius Hamilton said:

For example, “and” and “or” are compositional operations which build new propositions out of other ones: and:Prop,Prop→Prop. I’m saying that if starting from first principles, I find it more intuitive to locate “and” as being an operation on propositions, and “not” as an operation on truth values

what makes "not" different from "and" and "or"? why would the former apply more naturally to truth values?

view this post on Zulip Mike Shulman (Nov 15 2024 at 21:21):

Yeah, I would say that both propositions and truth values each have their own notions of "and", "or", and "not".