@NNem The term "direct proof" is often used by non-logicians in a rather inconsistent manner. The term "formal proof" is vague but usually has the following kind of meanings:
There is actually a whole spectrum of "formality" in mathematics. In informal terms, "formal" it refers to what is considered as rigorous, but that is of course subjective.
Absolutely formal: Written in a language that can be verified by a program that implements some formal system. Check out M...
You may also wish to read the following post about proofs by contradiction, specifically explaining why it is legitimate for statements that you believe have a truth-value:
Proof by contradiction, as you stated, is the rule$\def\imp{\Rightarrow}$ "$\neg A \imp \bot \vdash A$" for any statement $A$, which in English is "If you can derive the statement that $\neg A$ implies a contradiction, then you can derive $A$". As pointed out by others, this is not a valid rule i...
@Typhon Thanks for clarifying, but your original statement is still false. It is not true that a definition's purpose is to "show something exists in whatever universe you are constructing". In fact your intended meaning is still wrong, because a definition does not show that anything exists at all. Either you can make a definition or you cannot, and that is governed by the rules of your foundational system. It is those rules stipulate what definitions exist in the sense of permissibility.
You still cannot say that the definitions themselves show their own existence in any meaningful sense, just as you cannot say that a theorem shows its own existence.
You can say that a sentence written down is a witness of its own existence as a symbol string, but again, it cannot show its own existence. If you do not get the logical distinction, then for example in plain English you can say that this message is a witness of the fact that I can chat in this room, but this message did not actually show that I can chat in this room; you still need to invoke your own reasoning to conclude from observing the witness to inferring the claim.
@LeakyNun Well by power-set axiom of course X ⊆ N.
@Typhon I totally agree with that. Furthermore, you could also read the comments starting from here for why we do need definitions besides just as a means to highlight what we are interested in.
