4

I am someone who likes precise definitions for mathematical terminology. So, is there some text where there is a precise definition of an effective proof? The notion is vague to me.

user107952
  • 20,508
  • A good start is the wiki. It is a big question you ask, effectively vague due to the enormity of the subject. A good/important question nonetheless. – J. W. Perry Jan 11 '14 at 04:33
  • This is intimately related to computability. – Avi Steiner Jan 11 '14 at 06:19
  • Can you say something about the context in which you are encountering the term? There is not any single formal definition, but there are uses that are clear from context. – Carl Mummert Jan 11 '14 at 14:20
  • @CarlMummert What I mean is, an existence proof that gives an algorithm for constructing the object. – user107952 Jan 11 '14 at 17:33
  • You can look at Errett Bishop, Foundations of Constructive Analysis (1967) : Chapter 1 deals with this topic, like "constructive existence". – Mauro ALLEGRANZA Jan 12 '14 at 21:35

2 Answers2

4

There is no single formal definition of an "effective proof", just as there is no single formal definition of a "constructive proof".

It is known is that, if the existence of a mathematical object is provable from particular axiom systems, then the object itself must be computable. This is clearest when the object is of a type to which "computable" easily applies: a set of natural numbers, a function from natural numbers to natural numbers, etc.

One such axiom system, using classical logic, is the system of second-order arithmetic known as $\mathsf{RCA}_0$. Because this system has a model in which every object is computable, any object that the theory proves to exist must be computable. There are systems that have similar properties but use non-classical intuitionistic logic.

In non-classical logic, another way of getting computable witnesses for existential statements is the method of realizability; this is closely related to the BHK interpretation of constructive mathematics. There are systems for which each provable statement has a computable realizer, and these realizers give computable witnesses.

Also closely related are the fields of computable analysis (which, by convention, uses classical logic) and constructive analysis (which, by convention, will use intuitionistic logic). These areas are directly concerned with proofs for which the constructed objects are computable or constructive in various senses.

Carl Mummert
  • 81,604
  • Perhaps this does not answer the question "what is an effective proof". If we don't try to find a formal definition, one informal definition is just what you have stated: an effective proof, it could be said, provides an algorithm to compute the object which is being constructed. – Carl Mummert Jan 11 '14 at 23:21
0

A strickly formal definition of an axiomatic proof:

A proof of a theorem is a list of formulas where:

1) Each formula is

1a) an axiom or

1b) can be deducted from one or more earlier formulas in the list by a given inference rule.

and

2) the theorem to proof is the last formula in the list.

Notice that hardly any proof is given this way.

Willemien
  • 6,582
  • While true, note that this isn't what the OP is asking about (the word "effective" is an important one here); see their comments. – Noah Schweber Nov 17 '20 at 18:35