[FOM] The denial of '~p'

[Andrej Bauer]

> One anomaly in thinking of 'p' as the denial of '~p' is that while it is
> immediately clear that it must be the case that one of the two is true. It
> is not immediately clear that this disallows them from being jointly true.

[I hope I am reading you correctly.] Quite the contrary. It is always
the case that p and ~p are not both true. Whatever ~p might be
according to you, it should certanly be disjoint from p, i.e., "p and
~p" should be false. For example, in a Heyting algebra ~p is the
pseudocomplement (the largest q such that "p and q" is false). In a
Boolean algebra it is the (proper) complement, which is a q such that
"p and q" is false and "p or q" is true. Essentially, the property "p
or ~p is false" is built into the definition of negation.

Examples when "p or ~p" holds but neither p nor ~p does arise easily.
For example, if B is the Boolean algebra 2 x 2, the product of two
Boolean algebras 2 = {0,1}, then taking p = (0,1) gives us

p = (0,1)
~p = (1,0)
p or ~p = (1,1)

As we see, p or ~p is true (no surprise since B is a Boolean
algebra...), but neither p nor ~p is true.

With kind regards,

Andrej