Convert one proof into another

Question

For a long time I have been investigating this question on my own, but it seems impenetrable. The question is this: To find a method whereby it becomes possible to convert proof A into proof B, where the proofs A,B can be of anything, e.g. a lemma, theorem, etc.

For example, it is possibly in geometry to solve something by means of coordinates or by means of euclidean geometry. However, these proofs are usually found one after the other, independently, and not derived one from the other. I am asking if it is possible to derive the euclidean geometry proof directly from the coordinate proof, or vice versa.

I would really appreciate any insights regarding this from experts, or papers/articles that touch on this topic. Thanks.

Answer 1

To long for a comment but not a complete answer sorry, Iam interested in a publication that explains it more exhaustive as well , but hope this helps a bit)

You mean something like

I have proven $ P \to Q $ in system 1

and you want to transform it into a proof of $ A \to B$ in system 2

what you need is some dictionary that relates P and Q from system 1 to A and B in system 2

• $ A \equiv P $
• $ B \equiv Q $

(or in fact you only need $ A \to P $ and $ B \to Q $ )

But still the directory is the big problem, how do you relate A to P and B to Q?

you can see small examples of this in hyperbolic geometry (Poincare disk model http://en.wikipedia.org/wiki/Poincar%C3%A9_disk_model ) vs euclidean geometry:

• point on plane in Euclidean geometry <-> point inside disk in hyperbolic geometry

• a line on plane in Euclidean geometry <-> circle arc orthogonal to disk inside the disk (this is not complete see below)

• segment between two points <-> part of the arc between the points

• angle between two lines <-> angle between the tangent lines of the arcs at the intersection.

Then you need to check this directory:

• all axioms of system 1 should be theorems in system 2 and vv

some examples:

• two lines cut in only one point <-> circle arc orthogonal to disk cut eachother at most once inside the disk (points outside the disk are not poi ts in the poincare disk geometry) ..... Check yes

• congruent angles .... check yes

• between every two points you can draw a line <-> there is a circle arc orthogonal to disk trough any two points (inside the disk) .... check FAILS. (this failing is recoverable , you can change the definition of lines in the Poincare disk to cover the exeption.)

and so for every axiom.

A you can see this is a rather complicated procedure, and here it is between two axiomatic geometries.

(there is a simpler method for projective geometry of points <-> projective geometry of lines but that was not instructive enough for me.)

To do it between an axiomatic and an analytical geometry, it is possible, but it gets very complicated. but It is possible.

hopes this helps.