# Is it the case that a proposition is equal to the product of all propositions implied by it?

Is it the case that a proposition is equal to the product of all propositions implied by it?

More formally, it the case that

$$\forall A. \left( A \leftrightarrow \underset{A \rightarrow B}{\bigwedge} B \right)$$

Also I think the logical dual should be something like

$$\forall A. \left( A \leftrightarrow \underset{B \rightarrow A}{\bigvee} B \right)$$

but I can't quite make sense of that.

This seems right to me under some logics but not right for others. In particular for some incomplete logics it seems to me that there are some statements that are true if some statement is true but are not necessarily provably so. Basically, some statements $A \rightarrow B$ are not necessarily true or false but are unprovable either way and so it is not possible to get a sensible definition of the set of all such statements.

• For what it's worth, in natural language I would interpret second first version as "anything true is true for a reason" (thinking of $B\rightarrow A$ as meaning that $B$ is one reason for $A$ to be true - this is just another way of saying that $B$ is sufficient for $A$). Of course, by the contrapositive this lets us interpret the first as "anything false is false for a reason." Commented Jun 19, 2017 at 5:31
• In classical logic all statements are provably either true or false: $\vdash A \lor \lnot A$. Incompleteness means that there are statements $A$ such that neither $\vdash A$ nor $\vdash \lnot A$ is provable. If you don't allow the principle of excluded middle: $\vdash A \lor \lnot A$, then you are in the realm of intuitionistic logic (which does not accept the first of your equivalences, but does accept the second). Commented Jun 19, 2017 at 21:48

Bear in mind that the infinite conjunction: $$\bigwedge_{A \to B}B$$ is not valid object language syntax in ordinary (finitary) first-order logic. If you treat it as a metanotation, you can explain it semantically as in the other answers. The natural way to view it syntactically is in second-order (propositional) logic, where it would be written thus: $$\forall B. ((A \to B) \to B)$$ and then it is indeed the case (in classical and intutionistic logic) that the following sentence is provable: $$\forall A. (A \leftrightarrow (\forall B. ((A \to B) \to B)))$$ (The left-to-right direction is trivial and the right-to-left direction follows by instantiating $B$ to $A$.)

What you refer to as the "dual" statement, restated in second-order logic: $$\forall A. (A \leftrightarrow (\exists B. ((B \to A) \land B)))$$ is also provable (in classical or intuitionistic logic). (Right-to-left is now trivial and you can take $A$ as the witness going left-to-right.)

• The first is also provable in intuitionistic logic under that encoding as one can simply apply the rule (A -> A). It is the closely related $(A -> \forall B. B) \rightarrow \forall B. B$ which is not provable under intuitionistic logic. Commented Jun 19, 2017 at 22:31
• As a minor note, to talk about (the quantificational) formulas like these one only needs second order propositional logic, a much simpler system than full second order logic, though not much studied traditionally as it isn't particularly interesting classically. The corresponding (usually intuitionistic) type theory is widely studied. It is described in Chapter 12 of Lectures on the Curry-Howard Isomorphism. Commented Jun 19, 2017 at 22:48
• @StevenStewart-Gallus: I have difficulty relating your comment to my answer, but the right-to-left direction in $\forall A. (A \leftrightarrow (\forall B. ((A \to B) \to B)))$ is not intuitionistically valid: if you instantiate $B$ to $\mathsf{false}$, it gives $\lnot\lnot A \to A$. Commented Jun 20, 2017 at 14:52
• @RobArthan I think you're thinking of $\exists B. ((A \rightarrow B) \rightarrow B)$. Suppose you have the program $f : \forall A. (Nat \rightarrow A) \rightarrow A := \lambda g. g(4)$. Then you can recover 4 from passing the identity function. Commented Jun 21, 2017 at 17:36
• @RobArthan You can simply apply the identity function for any type A. More precisely, $f : \forall A. (\forall B. (A \rightarrow B) \rightarrow B) \rightarrow A := \lambda g. g (\lambda x. x)$ Commented Jul 18, 2017 at 17:49

If you're interested in questions of this type, you might enjoy looking at algebraic logic.

There's a natural way to make this precise (let's work in classical propositional logic for simplicity). Fix a (possibly incomplete) theory $T$; this yields a Boolean algebra $B(T)$, the Lindenbaum algebra of $T$, consisting of equivalence classes of propositional formulas modulo $T$-provable equivalence. For instance, if $T=\{a, a\wedge b\rightarrow c\}$, then $[b]_T=[c]_T$. The partial ordering is given by $x\le y\iff T\cup\{y\}\vdash x$ (I'm putting truth $\top$ at the bottom, here, which I think is the standard convention).

Now this Boolean algebra, like all Boolean algebras, has a completion $B(T)^+$ (I don't know how this is usually denoted); $B(T)$ contains $B(T)^+$, and in $B(T)^+$ we can talk about meets and joins of arbitrary sets. (We need to pass to the completion to ask your question appropriately, since you're generally taking the meet/join over an infinite set of sentences.) The questions you're asking then can be phrased as:

• In $B(T)^+$, is $[a]_T=\bigwedge_{b\le a}[b]_T$ for all $a$?

• In $B(T)^+$, is $[a]_T=\bigvee_{a\le b}[b]_T$ for all $a$?

Unfortunately, the answers to both questions are trivially "yes" - this is because $a\le a$. Regardless of what $T$ is, it always proves "$a\rightarrow a$," and so "$\bigwedge_{b\le a}\varphi(b)$" can always just be replaced with "$\varphi(a)$," regardless of what expression $\varphi(\cdot)$ is (and identically with "$\bigvee_{a\le b}\varphi(b)$").

This problem can't be fixed by replacing "$\le$" with "$<$," either, unless $T$ is very special: usually, for any $a$ not provable from $T$ we can find some $c$ such that both $a\vee c$ and $a\vee\neg c$ are strictly $<a$ in $B(T)$; but $(a\vee c)\wedge (a\vee\neg c)\equiv a$, so this again trivializes (and a similar statement holds for the dual of course). So there are very few times when replacing "$\le$" with "$<$" improves the situation substantially - in particular, for this to happen we either need $a$ to be decided by $T$ (that is, $[a]_T=[\top]_T$ or $[a]_T=[\perp]_T$) or for $T$ to be "close to complete."

For an example of how $T$ being "close to complete" can make the answer negative: consider the language with a single proposition letter "$a$," and $T$ the empty theory. $B(T)$ now has four elements: $[\top]_T, [a]_T, [\neg a]_T, [\perp]_T$. It's an easy exercise to check that $B(T)$ is complete, hence $B(T)=B(T)^+$. Now the only things $a$ strictly implies are tautologies, and the only things strictly implying $a$ are contradictions, and same with $\neg a$; so $a$ and $\neg a$ are not captured by the strict implication version of your operations. It's a good exercise to go from this to a characterization of when an element of the Lindenbaum algebra provides a counterexample to the strict version of each of your questions.

I don't see a way to really fix things if we change to a non-classical underlying logic, either, but I could be wrong - I'm not very well-versed in such things. (In particular, the first objection would apply to any logic validating "$x\rightarrow x$," which holds of every one I've heard of; and the second relies on less trivial, but still fairly basic, principles.)

• Well I'm a programmer so when I think nonclassical logic I think Type Theory or Set Theory. So, $A = \underset{B \subset A}{\bigcup} B$. So, I think I got it flipped around and it is more like $A = \underset{A \rightarrow B}{\bigvee} B$ and $A = \underset{B \rightarrow A}{\bigwedge} B$. Commented Jun 19, 2017 at 5:35
• @StevenStewart-Gallus Well those are obviously false: $A\rightarrow \top$ and $\perp \rightarrow A$ are tautologies for all $A$, so "$\bigvee_{A\rightarrow B}B$" is always true and "$\bigwedge_{B\rightarrow A}B$" is always false, regardless of what $A$ is. You've got your interpretation of sets in this context backwards: we interpret $A$ as the proposition "the point we're thinking about is in $A$", so $B\subseteq A$ means $B\rightarrow A$, not $A\rightarrow B$. (Of course this clashes unfortunately with the usual notation "$A\supset B$" for "$A$ implies $B$.") Commented Jun 19, 2017 at 5:59
• @StevenStewart-Gallus Another way to interpret this approach is to identify $A$ with the set of possible worlds in which $A$ is true; if $B\subset A$ - that is, in every possible world in which $B$ is true, $A$ is also true - then clearly we have $B\rightarrow A$. The use of "possible worlds" is philosophically loaded, but I think it's useful in this context. (Forcing is another context where the inequality goes in a possibly nonintuitive direction: $p\le q$ means $p$ is a stronger condition than $q$, since it is less likely to be true.) Commented Jun 20, 2017 at 16:33
• (cont'd) Now what about the old connective notation, $A\supset B$ for $A\rightarrow B$? This corresponds to a different interpretation: we identify $A$ with the information $A$ provides, that is, the set of things we know if we know $A$. Then $A\rightarrow B$ means $A$ tells us more information than $B$, that is, $A\supset B$. This shows the subtlety of identifying propositions with sets: you need to be explicit in how you do this, since there are reasonable but opposite choices. Commented Jun 20, 2017 at 16:35

A different perspective on this is that it is a special case of the Yoneda lemma from category theory. In fact, it's exactly the decategorification of a common corollary of the Yoneda lemma.

The (covariant form of the) Yoneda lemma is usually written like: $$\mathsf{Nat}(\mathcal{C}(A,-),F)\cong FA$$ where $$F$$ is a functor $$\mathcal{C}\to\mathbf{Set}$$ and $$\mathsf{Nat}$$ stands for the set of natural transformations from $$\mathsf{Hom}(A,-)$$ to $$F$$.

Decategorifying, $$\mathcal{C}$$ goes from a category to a preordered set, $$F$$ becomes a monotonic function, $$\mathbf{Set}$$ becomes the poset $$\mathbf{2}$$. (Note, $$X\leq Y$$ for $$X,Y\in\mathbf{2}$$ means $$X \Rightarrow Y$$.) In our case, the ordering is the entailment relation, i.e. $$A \leq B \iff A \vdash B$$. $$\mathsf{Nat}(F,G)$$ instead of being the set of natural transformations is just the proposition that $$F\leq G$$ in the pointwise sense. Expanding it out we get: $$\bigwedge_{B\in\mathcal{C}}(A\vdash B)\leq FB \iff FA$$ Let's set $$FA$$ to the predicate that states that $$A$$ is provable. Conveniently, we already have what we need, $$FA\equiv \top\vdash A$$. We get: $$\bigwedge_{B\in\mathcal{C}}(A\vdash B)\leq (\top\vdash B) \iff \top\vdash A$$ Recategorifying for a moment, this is $$\mathsf{Nat}(\mathcal{C}(A,-),\mathcal{C}(T,-))\cong \mathcal{C}(T,A)$$, an absolutely ubiquitous corollary of the Yoneda lemma. At any rate, the above says, "$$A$$ is provable if and only if for all propositions $$B$$, if $$A$$ entails $$B$$, then $$B$$ is provable". Choosing $$FA\equiv A\vdash\bot$$ meaning "$$A$$ is refutable" (which is an anti-monotonic function from $$\mathcal{C}$$), the contravariant Yoneda lemma leads to: $$\bigwedge_{B\in\mathcal{C}}(B\vdash A)\leq (B\vdash\bot) \iff A\vdash\bot$$ If it's the case that $$A\vdash \bot \iff \neg(\top\vdash A)$$ for any $$A$$, i.e. every proposition is either provable or refutable, then we have:\begin{align} \left[\bigwedge_{B\in\mathcal{C}}(B\vdash A)\leq (B\vdash\bot) \iff A\vdash\bot\right] & \iff \left[\bigwedge_{B\in\mathcal{C}}(B\vdash A)\leq \neg(\top\vdash B) \iff \neg(\top\vdash A)\right] \\ & \iff \left[\bigwedge_{B\in\mathcal{C}}\neg(B\vdash A)\lor\neg(\top\vdash B) \iff \neg(\top\vdash A)\right] \\ & \iff \left[\bigwedge_{B\in\mathcal{C}}\neg((B\vdash A)\land(\top\vdash B)) \iff \neg(\top\vdash A)\right] \\ & \iff \left[\neg\bigvee_{B\in\mathcal{C}}(B\vdash A)\land(\top\vdash B) \iff \neg(\top\vdash A)\right] \\ & \iff \left[\bigvee_{B\in\mathcal{C}}(B\vdash A)\land(\top\vdash B) \iff \top\vdash A\right] \end{align}

The outer, overall equivalence requires the assumption that $$A\vdash\bot\iff\neg(\top\vdash A)$$, but the last inner equivalence ($$\bigvee_{B\in\mathcal{C}}(B\vdash A)\land(\top\vdash B) \iff \top\vdash A$$) holds regardless and is the decategorified version of a special case of the co-Yoneda lemma.