I know that it may be rather self-evident that every statement must possess an inverse, however, is there a way to prove this in propositional calculus or is it considered an axiom?
(Note: By the inverse of a statement I mean its negation)
I know that it may be rather self-evident that every statement must possess an inverse, however, is there a way to prove this in propositional calculus or is it considered an axiom?
(Note: By the inverse of a statement I mean its negation)
On
Yes: given a quantified wff F, there is an algorithm to negate F: you start with the outermost quantifier, negate it, and do so until you are done with the quantifiers. Negation at each point preserves well-formedness. Negations are done like this:
1)~$(\forall x P_{xyz..})$ is $\exists x $ ~P
2)~$(\exists x P_{xyz..})$ is $\forall x$ ~$P_{xyz..}$
And this allows you to construct a negation.
EDIT: You can see propositional logic as having 0-predicates and being unquantified. It ultimately comes down to DeMorgan's rules:
$1)$ ~($A$ or $B$)=~A or ~B . $2)$ ~(A and B)= ~ A or ~B . This gives you all you need. Expanding: We have that $ A \implies B$ is equivalent to ~$A$ or $B$.
We then have a finite collection of connctives like And, Or, and $\implies$ from which we can construct all formulas ( we also have the Prenex form , which I can expand on if you would like me to ), together with a finite collection of atomic formulas $A,B,C$. We then apply DeMorgan's rules to the formulas.
We then do something similar to the above case.
On
More formal proofs exist, but basically:
Every atomic predicate always has a negation. If $p$ is such a predicate, $\neg p$ is the negation.
Every logical connective will have a dual; thus every compound predicate has a negation through deMorgan style rules of dual negation. If $\circ, \bullet$ are such duals, and $p, q$ are predicates, then $\;\neg(p \circ q) = \neg p \bullet \neg q\;$.
[Note: $\neg (p\to q) \;=\; \neg\neg p \wedge \neg q$]
Every quantifier will have a dual; thus every quantified statement has a negation. If $\mathcal {Q, \bar Q}$ are dual quantifiers, and $p$ a predicate, then $\;\neg (\mathcal Q p) = \mathcal {\bar Q} (\neg p)\;$.
Thus every well formed statement will have a negation, which is a well formed statement.
On
In general science, there's a distinction between definitions and axioms that I think is important to recognize.
Axioms are propositions that need not be proved; definitions are not propositions and thus cannot be proved or disproved.
I could point to a red house and say "I declare this color is called Moob." It's nonsensical and backwards to ask, "Can you PROVE that it's Moob?" The only "proof" to be given is the tautology that it meets the requirements of the definition I just gave.
Logical negation of a statement, in its rawest form, is arbitrarily defined as the statement that has opposite truth values to the original statement. The existence of a negation is implied by the presence of the elements of its definition, namely, the existence of a statement that HAS truth values upon which the definition can be applied.
As others have already suggested, if the logical inverse is defined in your branch of logic then there is no proof to be made.
On
There's a related question, which I suspect might be part of what the OP intends to ask:
Is "logic without negation" a thing?
The answer is yes, in a variety of ways:
In intuitionistic logics, we do have the symbol "$\neg$"; however, it does not behave the way we might expect negation to behave. For example, "$\varphi \vee \neg\varphi$" is usually not provable. Now, an intuitionistic logician may well argue that really, it's classical logic which has a weird notion of negation; however, I'm assuming the OP is coming from the perspective of classical logic, in which case I think intuitionistic logic is at least partially a "logic without negation" (but, don't push that too far!). A related class of examples is paraconsistent logics.
Another example, without anything that even looks like negation, is dependence logic or its variants. Dependence logic is the logic of, well, dependence: it's the natural logical system you would use to express statements like "for each $x$ and $y$, there is a $z$ depending only on $x$ and a $w$ depending only on $y$ such that . . .". Such statements are in general not expressible in first-order logic; they correspond the $\Sigma^1_1$ assertions, which are not closed under negation. Perhaps surprisingly, if there are sentences $\varphi,\psi$ of dependence logic such that every structure satisfies exactly one of $\varphi$ and $\psi$, then $\varphi$ (and $\psi$) is actually a first-order sentence! So first-order logic captures the "negation-friendly" part of dependence logic.
There are other examples you may or may not find relevant - some many-valued logics might count, depending on what exactly you're asking for - but these are a good starting point.
The fact that you can form a negation of every formula is simply a property of the logical language. It will be formally stated as part of the definition of "well-formed formula": Whenever $\varphi$ is a formula, $¬(\varphi)$ is a formula too. You could consider that an "axiom" (the distinction between axioms and definitions being somewhat fluid) if you want.