One thing I find confusing in propositional logic is that we have things like axioms and inference rules but then we seem to be able to define whatever we want in syntax that doesn't necessarily adhere to the axiom formats.
For example
https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system
This example system uses the modus ponens inference rule:
$P, P \to Q \vdash Q$
And the following axioms:
I. $(p \to (q \to p))$
II. $((p \to (q \to r)) \to ((p \to q) \to (p \to r)))$
III. $((\lnot p \to \lnot q) \to (q \to p))$
We have the $\lnot$ and $\to$ operator in the language but then we define $a \land b = \lnot(a \to \lnot b)$ even though this format does not match any of the three axioms, nor have we defined equality.
Why is this permitted? What are we allowed to define? What are we even using modus ponens and the axioms for if we can just make up whatever?
Best Answer
You can define anything you want. However, the point of defining something is to make it easier to refer to, which means that the most useful definitions are for things that are:
(a) frequently referred to;
(b) not trivial; and often
(c) similar to something else
So, for example, we define $\wedge$ because it allows for a lot of shortcuts in writing the propositional logic, and it happens to align with the general understanding of the word "and". The "=" in the definition isn't really part of the logic, it's a part of the language surrounding it, and we know that there's a level at which we have to resort to shared understanding since you can only abstract things so far.
On the other hand, I probably wouldn't bother coming up with a definition for "the set of all even prime numbers in $\mathbb{N}$", because it's simple enough to just say $\{2\}$. Or if I did define it, it would only be for a very limited context (for example, one where I actually needed to prove that 2 is the only element in the set), so I could get away with a generic definition like $A$.