Fdtxjr

I just noticed there is a similarity between logic operations on propositions and the operations of set theory. It seems:

$$beginarrayllll
textrmdisjunction & (-)vee (-)& textrmcorresponds to union& (-)cup (-)\
textrmconjunction & (-) wedge (-)& textrmcorrespons to intersection & (-)cap (-)\
textrmnegation & sim (-) & textrmcorrespons to taking complements & c(-),
endarray
$$
and I conjecture:

$$beginarraylll
textrmconditional & (-)rightarrow (-) & textrmcorresponds to inclusion & subset\
textrmbiconditional & (-)leftrightarrow (-) & textrmcorresponds to equality & =
endarray$$

How far does it go? I believe there is some kind of functor between some category whose objects are propositions and the category of sets, is that right?

Thanks

"How far does it go ?" : as far as it can get !

Here's a general idea about how set theory is a semantics for classical propositional logic (note that if we change the formal system we're looking at without changing our assumptions on sets, for instance if we're studying intuitionistic logic from a classical point of view, then we have to take another semantics, in this specific case, topological spaces can be appropriate) :

Suppose you have a set of propositional variables $V$, a "global" set $E$, and a function $[-] :Vto mathcalP(E)$. Then you can build a function that goes from the set $mathrmForm$ of formulas to $mathcalP(E)$ by expanding $[-]$ according to the rules you displayed : if $varphi, psi$ are formulas and you already defined $[varphi]$ and $[psi]$, then define $[varphi land psi] = [varphi]cap [psi]$, similarly for $lor, neg$, and define $[varphiimplies psi]$ as $xin Emid xin [varphi]implies xin[psi]$.

These rules allow you to define $[varphi]$ for any formula $varphi$ by induction, going from the variables and gaining complexity.

Then you can prove the following things : if $varphi$ is a theorem of classical logic, then $[varphi] = E$, which tells you that the set-operations behave according to the logical ones, but also you can prove : if for any $E$ and any $[-] :Vto mathcalP(E)$, $[varphi] = E$, then $varphi$ is a theorem of classical logic ! This tells you that actually the logical operations behave just like set-theoretic operations as well.

There's actually a lot more you can say about this sort of thing (for instance : what happens if you add quantifiers ? Or in another direction what happens if we replace $mathcalP(E)$ by some other type of object ? If we completely change the type of object, what kind of logic do we get ? etc. etc.)

If you absolutely want to use the words "functor" and "category" you can, but at this level they're not the most relevant thing.

Yes, there is an abstract isomorphism here and the likeness of the symbols $lor$ and $cup$, as well as that of $land$ and $cap$ is of course no accident!

Also, if you use the formal definition of the set operators, we see the connection there as well:

Union:

$forall A forall B forall x (x in A colorredcup B leftrightarrow (x in A colorredlor x in B))$

Intersection:

$forall A forall B forall x (x in A colorredcap B leftrightarrow (x in A colorredland x in B))$

Complement:

$forall A forall B forall x (x in Acolorred' leftrightarrow colorredneg x in A)$

And your conjecture is right in that we also have:

Inclusion:

$forall A forall B (Acolorred subseteq B leftrightarrow forall x (x in A colorred rightarrow x in B))$

Equality:

$forall A forall B (Acolorred = B leftrightarrow forall x (x in A colorred leftrightarrow x in B))$

The connection is math is a logical science. It's built on a foundation of axioms and definitions, from which ideally, all statements can be proven, or disproven ( though some are undecideable sadly). You can have logical properties with set operations, Sets equipped with operations, having certain properties applied on the set, are the basis for: magmas, monoids, loops, semigroups, quasigroups, groups, abelian groups, rings, commutative rings, and fields, just to name a few buzzwords. Mathematical logic, can be defined in terms of other more basic logics.