When is a definition via properties considered valid?

Question

How one would define the validity of a definition of an object by its properties?

Little background: I'm trying to implement a kind of framework of mathematics in which the user is not restricted to any formal system, but can define anything at will just like in english but imposing logical constraints on the steps possible during a proof preventing mistakes. This obviously requires to prove that the definition is "valid".

Example: If we consider $G$ to be a group and $+$ its group operation, we can define $0\in G$ s.t. $\forall x\in G : x+0=0+x=x$, we can prove that two sets with such property are equal ($0_1 = 0_1 + 0_2=0_2$) so the definition is solid. Here equality is by definition $x=y :\iff (\forall z:(x\in z \iff y\in z)\land \forall w:(w\in x \iff w\in y)$, so basically in any formula of set theory we can freely replace $x$ with $y$ and vice versa. But what if we don't want to be restricted to set theory? Then what seems reasonable is to require for every definition a list of formulas(not necessarily of set theory) which constitutes the notion of "equality" and then proving that in these formulas they are indeed interchangeable. This issue does not arise when considering objects defined through expressions($3:=2+1$) as they are just directly replaceable short-hand notations.

Answer 1

A partial answer that works in first-order logic is to have a definitional principle that says that if you can prove $\forall x_1, \ldots x_n\exists_{1}y\phi(y, x_1, \ldots, x_n)$, then you can introduce a new $n$-place function symbol $f$, whose defining property is $\forall x_1, \ldots, x_n\phi(f(x_1, \ldots, x_n), x_1, \ldots, x_n)$. The special case when $n = 0$ lets you introduce new constant symbols. For a proof that this definitional principle is conservative (i.e., that it doesn't increase the logical strength of the theory), see Mendelson's Introduction to Mathematical Logic section 2.9.

Definitional principles along these lines are implemented in interactive proof systems such as the various members of the HOL family. The definitional principles are formulated as inference rules (they have one or more antecedent theorems) that make theory extensions (the signature of the language is extended in the theorem that is the succedent of the rule).

Answer 2

As Henning has already said, you need to decide on an underlying logical system, because there are incompatible logical systems and you cannot prove anything without using any logic. Suppose you pick (classical) first-order logic. Then once you implement the deductive system, you basically can use it for any finitely axiomatized first-order theory; to verify $T \vdash P$ where $T$ has axioms $X$, you simply prove $\bigwedge_{A \in X} A \to P$.

However, if you want to be able to handle any recursively axiomatizable first-order theory, you clearly need something more. One way would be to have meta rules for assuming schemas. Also, presumably you want to be able to define new constants, functions and predicates, so you would probably want to add full abbreviation power. You might want to have namespaces so that you can restrict added stuff to only where they are needed.

It would be a good idea to study how programming languages are designed, since a lot of issues for formal systems have already been studied and solved by programming language designers long ago.

Answer 3

If we go into the mathematical realm a "thing which does not exist" is just a set of properties which cannot be satisfied.