When is a definition via properties considered valid?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 ∀ x ∈ 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 : ⟺ ( ∀ z : ( x ∈ z ⟺ y ∈ z ) ∧ ∀ w : ( w ∈ x ⟺ w ∈ 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 + 1as they are just directly replaceable short-hand notations.

Question

When is a definition via properties considered valid?How one would define the validity of a definition of an object by its properties?Little background: I&#039;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 &quot;valid&quot;.Example: If we consider G to be a group and + its group operation, we can define   ∀  x  ∈  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  :    ⟺    (  ∀  z  :  (  x  ∈  z    ⟺    y  ∈  z  )  ∧  ∀  w  :  (  w  ∈  x    ⟺    w  ∈  y  ), so basically in any formula of set theory we can freely replace x with y and vice versa. But what if we don&#039;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 &quot;equality&quot; and then proving that in these formulas they are indeed interchangeable. This issue does not arise when considering objects defined through expressions   3  :=  2  +  1as they are just directly replaceable short-hand notations.

Patrick Arnold · Accepted Answer

A partial answer that works in first-order logic is to have a definitional principle that says that if you can prove   ∀      x    1    ,  …      x    n        ∃          1        y  ϕ  (  y  ,      x    1    ,  …  ,      x    n    ), then you can introduce a new n-place function symbol f, whose defining property is   ∀      x    1    ,  …  ,      x    n    ϕ  (  f  (      x    1    ,  …  ,      x    n    )  ,      x    1    ,  …  ,      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&#039;t increase the logical strength of the theory), see Mendelson&#039;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).

Answered question

Answer & Explanation

New Questions in High school statistics