3 added 252 characters in body
source | link

No, they do not. First, even if opicturepicture proofs did make itwere empirical it does not mean that it can not be derived by other, non-picture, means. Just because we can surmise 1+1=2 from our experience with common objects does not mean that it is empirical either. "An a priori science is one whose knowable truths are all knowable in an a priori way, allowing that some may be knowable also in an a posteriori way", as Giaquinto puts it. 

More importantly, writing/typing a sentence/formula is also a strictly empirical act, and no "purely theoretical axioms" can be expressed without that. So if a picture proof makes the theorem empirical then all of mathematics is empirical. A "picture" (diagram) is simply an alternative means for expressing geometric relations, it can be converted into symbolic form, if one so wishes, as Hilbert famously did.

The non-empiricity (in the usual sense) of diagrammatic reasoning itself was already pointed out by Kant, who coined a specific new category for this type of reasoning, synthetic a priori. Kant also suggested that we have a special faculty for this sort of thing, pure a priori intuition. That was and remains controversial, but it turned out that he did not need to. The detailed analysis of Euclidean reasoning by Manders showed that diagrammatic reasoning involves nothing epistemologically different from the familiar symbol manipulationin axiomatic systems, whatever "apriority" status one wants to assign to it. See his classical work Euclidean Diagram (published in Mancosu edited volume, freely available).

Subsequently, formalizations of Euclidean geometry were developed that use diagrams directly. The most attractive one, due to Mumma, is called Eu. Some of the axioms are directly stated in a diagrammatic form, and its proofs closely mimick Euclid's diagrammatic demonstrations, much more closely than Hilbert's symbolic axiomatics. One can see multiple descriptions and expositions of it on his homepage. For philosophical discussions see his Synthese papers Proofs, Pictures, and Euclid, Constructive Geometric Reasoning and Diagrams, and Azzouni's That Some Diagrammatic Proofs Are Perfectly Rigorous. Here is from Mumma's The role of geometric content in Euclid’s diagrammatic reasoning:

"Manders’ general philosophical concern in the paper iswith mathematical justification — i.e. what is required for it, and the nature of the techniques developed to meet these requirements. His specific topic is the role of diagrams in Euclid’sElements... The result is a compelling analysis which reveals that diagrams have a principled, theoretical role in the Elements. Only a restricted range of a diagram’s properties are permitted to justify inferences for Euclid, and these self-imposed restrictions can be explained as serving the purpose of mathematical control.

[...] My case... consists in an account of the informal proofs of Euclid’s elementary geometry, an account based on recent formalizations of Euclid’s diagrammatic proofs. The account confirms the Rav/Leitgeb view in that it identifies an irreducible role for geometric content in the reasoning. Yet the role played by geometric content is highly constrained, and the constraints are explicated in formal terms. Inferences grounded on an understanding of geometric content occur within a sharply defined formal structure [of Eu]. Accordingly, geometric proof is relativized to a formal framework, a feature that Leitgib identifies with formal proofs. What is and isn’t provable is relative to the formal syntax of the framework and the rules for how it can be used."

One can generalize this to reasoning about non-Euclidean geometries as well, by altering how the diagrammatic information is read. This was done already by Lobachevsky, see Did Lobachevsky Have A Model Of His "imaginary Geometry"? by Rodin, and even before him by Saccheri and Lambert.

No, they do not. First, even if opicture proofs did make it empirical it does not mean that it can not be derived by other, non-picture, means. Just because we can surmise 1+1=2 from our experience with common objects does not mean that it is empirical either. More importantly, writing/typing a sentence/formula is also a strictly empirical act, and no "purely theoretical axioms" can be expressed without that. So if a picture proof makes the theorem empirical then all of mathematics is empirical. A "picture" (diagram) is simply an alternative means for expressing geometric relations, it can be converted into symbolic form, if one so wishes, as Hilbert famously did.

The non-empiricity (in the usual sense) of diagrammatic reasoning itself was already pointed out by Kant, who coined a specific new category for this type of reasoning, synthetic a priori. Kant also suggested that we have a special faculty for this sort of thing, pure a priori intuition. That was and remains controversial, but it turned out that he did not need to. The detailed analysis of Euclidean reasoning by Manders showed that diagrammatic reasoning involves nothing epistemologically different from the familiar symbol manipulationin axiomatic systems, whatever "apriority" status one wants to assign to it. See his classical work Euclidean Diagram (published in Mancosu edited volume, freely available).

Subsequently, formalizations of Euclidean geometry were developed that use diagrams directly. The most attractive one, due to Mumma, is called Eu. Some of the axioms are directly stated in a diagrammatic form, and its proofs closely mimick Euclid's diagrammatic demonstrations, much more closely than Hilbert's symbolic axiomatics. One can see multiple descriptions and expositions of it on his homepage. For philosophical discussions see his Synthese papers Proofs, Pictures, and Euclid, Constructive Geometric Reasoning and Diagrams, and Azzouni's That Some Diagrammatic Proofs Are Perfectly Rigorous. Here is from Mumma's The role of geometric content in Euclid’s diagrammatic reasoning:

"Manders’ general philosophical concern in the paper iswith mathematical justification — i.e. what is required for it, and the nature of the techniques developed to meet these requirements. His specific topic is the role of diagrams in Euclid’sElements... The result is a compelling analysis which reveals that diagrams have a principled, theoretical role in the Elements. Only a restricted range of a diagram’s properties are permitted to justify inferences for Euclid, and these self-imposed restrictions can be explained as serving the purpose of mathematical control.

[...] My case... consists in an account of the informal proofs of Euclid’s elementary geometry, an account based on recent formalizations of Euclid’s diagrammatic proofs. The account confirms the Rav/Leitgeb view in that it identifies an irreducible role for geometric content in the reasoning. Yet the role played by geometric content is highly constrained, and the constraints are explicated in formal terms. Inferences grounded on an understanding of geometric content occur within a sharply defined formal structure [of Eu]. Accordingly, geometric proof is relativized to a formal framework, a feature that Leitgib identifies with formal proofs. What is and isn’t provable is relative to the formal syntax of the framework and the rules for how it can be used."

One can generalize this to reasoning about non-Euclidean geometries as well, by altering how the diagrammatic information is read. This was done already by Lobachevsky, see Did Lobachevsky Have A Model Of His "imaginary Geometry"? by Rodin, and even before him by Saccheri and Lambert.

No, they do not. First, even if picture proofs were empirical it does not mean that it can not be derived by other, non-picture, means. Just because we can surmise 1+1=2 from our experience with common objects does not mean that it is empirical either. "An a priori science is one whose knowable truths are all knowable in an a priori way, allowing that some may be knowable also in an a posteriori way", as Giaquinto puts it. 

More importantly, writing/typing a sentence/formula is also a strictly empirical act, and no "purely theoretical axioms" can be expressed without that. So if a picture proof makes the theorem empirical then all of mathematics is empirical. A "picture" (diagram) is simply an alternative means for expressing geometric relations, it can be converted into symbolic form, if one so wishes, as Hilbert famously did.

The non-empiricity (in the usual sense) of diagrammatic reasoning itself was already pointed out by Kant, who coined a specific new category for this type of reasoning, synthetic a priori. Kant also suggested that we have a special faculty for this sort of thing, pure a priori intuition. That was and remains controversial, but it turned out that he did not need to. The detailed analysis of Euclidean reasoning by Manders showed that diagrammatic reasoning involves nothing epistemologically different from the familiar symbol manipulationin axiomatic systems, whatever "apriority" status one wants to assign to it. See his classical work Euclidean Diagram (published in Mancosu edited volume, freely available).

Subsequently, formalizations of Euclidean geometry were developed that use diagrams directly. The most attractive one, due to Mumma, is called Eu. Some of the axioms are directly stated in a diagrammatic form, and its proofs closely mimick Euclid's diagrammatic demonstrations, much more closely than Hilbert's symbolic axiomatics. One can see multiple descriptions and expositions of it on his homepage. For philosophical discussions see his Synthese papers Proofs, Pictures, and Euclid, Constructive Geometric Reasoning and Diagrams, and Azzouni's That Some Diagrammatic Proofs Are Perfectly Rigorous. Here is from Mumma's The role of geometric content in Euclid’s diagrammatic reasoning:

"Manders’ general philosophical concern in the paper iswith mathematical justification — i.e. what is required for it, and the nature of the techniques developed to meet these requirements. His specific topic is the role of diagrams in Euclid’sElements... The result is a compelling analysis which reveals that diagrams have a principled, theoretical role in the Elements. Only a restricted range of a diagram’s properties are permitted to justify inferences for Euclid, and these self-imposed restrictions can be explained as serving the purpose of mathematical control.

[...] My case... consists in an account of the informal proofs of Euclid’s elementary geometry, an account based on recent formalizations of Euclid’s diagrammatic proofs. The account confirms the Rav/Leitgeb view in that it identifies an irreducible role for geometric content in the reasoning. Yet the role played by geometric content is highly constrained, and the constraints are explicated in formal terms. Inferences grounded on an understanding of geometric content occur within a sharply defined formal structure [of Eu]. Accordingly, geometric proof is relativized to a formal framework, a feature that Leitgib identifies with formal proofs. What is and isn’t provable is relative to the formal syntax of the framework and the rules for how it can be used."

One can generalize this to reasoning about non-Euclidean geometries as well, by altering how the diagrammatic information is read. This was done already by Lobachevsky, see Did Lobachevsky Have A Model Of His "imaginary Geometry"? by Rodin, and even before him by Saccheri and Lambert.

2 added 521 characters in body
source | link

WritingNo, they do not. First, even if opicture proofs did make it empirical it does not mean that it can not be derived by other, non-picture, means. Just because we can surmise 1+1=2 from our experience with common objects does not mean that it is empirical either. More importantly, writing/typing a sentence/formula is also a strictly empirical act, and no "purely theoretical axioms" can not be expressed without that. So if drawing a picture proof makes itthe theorem empirical then allall of mathematics is already empirical. A "picture" (diagram) is simply an alternative means for expressing geometric relations, it can be converted into symbolic form, if one so wishes, as Hilbert famously did.

The non-empiricity (in the usual sense) of diagrammatic reasoning itself was originallyalready pointed out by Kant, who coined a specific new category for this type of reasoning, synthetic a priori. Kant also suggested that we have a special faculty for this sort of thing, pure a priori intuition. That was and remains controversial, but theit turned out that he did not need to. The detailed analysis of Euclidean reasoning by Manders showed that itdiagrammatic reasoning involves nothing epistemologically different from the familiar symbol manipulationin axiomatic systems, whatever "apriority" status one wants to assign to it. See his classical work Euclidean Diagram (published in Mancosu edited volume, freely available).

Subsequently, formalizations of Euclidean geometry were developed that use diagrams directly. The most attractive one, due to Mumma, is called Eu. Some of the axioms are directly stated in a diagrammatic form, and its proofs closely mimick Euclid's diagrammatic demonstrations, much more closely than Hilbert's symbolic axiomatics. One can see multiple descriptions and expositions of it on his homepage. For philosophical discussions see his Synthese papers Proofs, Pictures, and Euclid, Constructive Geometric Reasoning and Diagrams, and Azzouni's That Some Diagrammatic Proofs Are Perfectly Rigorous. Here is from Mumma's The role of geometric content in Euclid’sdiagrammaticEuclid’s diagrammatic reasoning:

"Manders’ general philosophical concern in the paper iswith mathematical justification — i.e. what is required for it, and the nature of the techniques developed to meet these requirements. His specific topic is the role of diagrams in Euclid’sElements... The result is a compelling analysis which reveals that diagrams have a principled, theoretical role in the Elements. Only a restricted range of a diagram’s properties are permitted to justify inferences for Euclid, and these self-imposed restrictions can be explained as serving the purpose of mathematical control.

[...] My case... consists in an account of the informal proofs of Euclid’s elementary geometry, an account based on recent formalizations of Euclid’s diagrammatic proofs. The account confirms the Rav/LeitgibLeitgeb view in that it identifies an irreducible role for geometric content in the reasoning. Yet the role played by geometric content is highly constrained, and the constraints are explicated in formal terms. Inferences grounded on an understanding of geometric content occur within a sharply defined formal structure [of Eu]. Accordingly, geometric proof is relativized to a formal framework, a feature that Leitgib identifies with formal proofs. What is and isn’t provable is relative to the formal syntax of the framework and the rules for how it can be used."

One can generalize this to reasoning about non-Euclidean geometries as well, by altering how the diagrammatic information is read. This was done already by Lobachevsky, see Did Lobachevsky Have A Model Of His "imaginary Geometry"? by Rodin, and even before him by Saccheri and Lambert.

Writing a sentence/formula is also a strictly empirical act, and "purely theoretical axioms" can not be expressed without that. So if drawing a picture makes it empirical then all of mathematics is already empirical. A "picture" (diagram) is simply an alternative means for expressing geometric relations, it can be converted into symbolic form, if one so wishes.

The non-empiricity (in the usual sense) of diagrammatic reasoning was originally pointed out by Kant, who coined a specific new category for this type of reasoning, synthetic a priori. Kant also suggested that we have a special faculty for this sort of thing, pure a priori intuition. That was and remains controversial, but the detailed analysis of Euclidean reasoning by Manders showed that it involves nothing epistemologically different from the familiar symbol manipulationin axiomatic systems, whatever "apriority" status one wants to assign to it. See his classical work Euclidean Diagram (published in Mancosu edited volume, freely available).

Subsequently, formalizations of Euclidean geometry were developed that use diagrams directly. The most attractive one, due to Mumma, is called Eu. Some of the axioms are directly stated in a diagrammatic form, and its proofs closely mimick Euclid's diagrammatic demonstrations, much more closely than Hilbert's symbolic axiomatics. One can see multiple descriptions and expositions of it on his homepage. For philosophical discussions see his Synthese papers Proofs, Pictures, and Euclid, Constructive Geometric Reasoning and Diagrams. Here is from The role of geometric content in Euclid’sdiagrammatic reasoning:

"Manders’ general philosophical concern in the paper iswith mathematical justification — i.e. what is required for it, and the nature of the techniques developed to meet these requirements. His specific topic is the role of diagrams in Euclid’sElements... The result is a compelling analysis which reveals that diagrams have a principled, theoretical role in the Elements. Only a restricted range of a diagram’s properties are permitted to justify inferences for Euclid, and these self-imposed restrictions can be explained as serving the purpose of mathematical control.

[...] My case... consists in an account of the informal proofs of Euclid’s elementary geometry, an account based on recent formalizations of Euclid’s diagrammatic proofs. The account confirms the Rav/Leitgib view in that it identifies an irreducible role for geometric content in the reasoning. Yet the role played by geometric content is highly constrained, and the constraints are explicated in formal terms. Inferences grounded on an understanding of geometric content occur within a sharply defined formal structure [of Eu]. Accordingly, geometric proof is relativized to a formal framework, a feature that Leitgib identifies with formal proofs. What is and isn’t provable is relative to the formal syntax of the framework and the rules for how it can be used."

No, they do not. First, even if opicture proofs did make it empirical it does not mean that it can not be derived by other, non-picture, means. Just because we can surmise 1+1=2 from our experience with common objects does not mean that it is empirical either. More importantly, writing/typing a sentence/formula is also a strictly empirical act, and no "purely theoretical axioms" can be expressed without that. So if a picture proof makes the theorem empirical then all of mathematics is empirical. A "picture" (diagram) is simply an alternative means for expressing geometric relations, it can be converted into symbolic form, if one so wishes, as Hilbert famously did.

The non-empiricity (in the usual sense) of diagrammatic reasoning itself was already pointed out by Kant, who coined a specific new category for this type of reasoning, synthetic a priori. Kant also suggested that we have a special faculty for this sort of thing, pure a priori intuition. That was and remains controversial, but it turned out that he did not need to. The detailed analysis of Euclidean reasoning by Manders showed that diagrammatic reasoning involves nothing epistemologically different from the familiar symbol manipulationin axiomatic systems, whatever "apriority" status one wants to assign to it. See his classical work Euclidean Diagram (published in Mancosu edited volume, freely available).

Subsequently, formalizations of Euclidean geometry were developed that use diagrams directly. The most attractive one, due to Mumma, is called Eu. Some of the axioms are directly stated in a diagrammatic form, and its proofs closely mimick Euclid's diagrammatic demonstrations, much more closely than Hilbert's symbolic axiomatics. One can see multiple descriptions and expositions of it on his homepage. For philosophical discussions see his Synthese papers Proofs, Pictures, and Euclid, Constructive Geometric Reasoning and Diagrams, and Azzouni's That Some Diagrammatic Proofs Are Perfectly Rigorous. Here is from Mumma's The role of geometric content in Euclid’s diagrammatic reasoning:

"Manders’ general philosophical concern in the paper iswith mathematical justification — i.e. what is required for it, and the nature of the techniques developed to meet these requirements. His specific topic is the role of diagrams in Euclid’sElements... The result is a compelling analysis which reveals that diagrams have a principled, theoretical role in the Elements. Only a restricted range of a diagram’s properties are permitted to justify inferences for Euclid, and these self-imposed restrictions can be explained as serving the purpose of mathematical control.

[...] My case... consists in an account of the informal proofs of Euclid’s elementary geometry, an account based on recent formalizations of Euclid’s diagrammatic proofs. The account confirms the Rav/Leitgeb view in that it identifies an irreducible role for geometric content in the reasoning. Yet the role played by geometric content is highly constrained, and the constraints are explicated in formal terms. Inferences grounded on an understanding of geometric content occur within a sharply defined formal structure [of Eu]. Accordingly, geometric proof is relativized to a formal framework, a feature that Leitgib identifies with formal proofs. What is and isn’t provable is relative to the formal syntax of the framework and the rules for how it can be used."

One can generalize this to reasoning about non-Euclidean geometries as well, by altering how the diagrammatic information is read. This was done already by Lobachevsky, see Did Lobachevsky Have A Model Of His "imaginary Geometry"? by Rodin, and even before him by Saccheri and Lambert.

1
source | link

Writing a sentence/formula is also a strictly empirical act, and "purely theoretical axioms" can not be expressed without that. So if drawing a picture makes it empirical then all of mathematics is already empirical. A "picture" (diagram) is simply an alternative means for expressing geometric relations, it can be converted into symbolic form, if one so wishes.

The non-empiricity (in the usual sense) of diagrammatic reasoning was originally pointed out by Kant, who coined a specific new category for this type of reasoning, synthetic a priori. Kant also suggested that we have a special faculty for this sort of thing, pure a priori intuition. That was and remains controversial, but the detailed analysis of Euclidean reasoning by Manders showed that it involves nothing epistemologically different from the familiar symbol manipulationin axiomatic systems, whatever "apriority" status one wants to assign to it. See his classical work Euclidean Diagram (published in Mancosu edited volume, freely available).

Subsequently, formalizations of Euclidean geometry were developed that use diagrams directly. The most attractive one, due to Mumma, is called Eu. Some of the axioms are directly stated in a diagrammatic form, and its proofs closely mimick Euclid's diagrammatic demonstrations, much more closely than Hilbert's symbolic axiomatics. One can see multiple descriptions and expositions of it on his homepage. For philosophical discussions see his Synthese papers Proofs, Pictures, and Euclid, Constructive Geometric Reasoning and Diagrams. Here is from The role of geometric content in Euclid’sdiagrammatic reasoning:

"Manders’ general philosophical concern in the paper iswith mathematical justification — i.e. what is required for it, and the nature of the techniques developed to meet these requirements. His specific topic is the role of diagrams in Euclid’sElements... The result is a compelling analysis which reveals that diagrams have a principled, theoretical role in the Elements. Only a restricted range of a diagram’s properties are permitted to justify inferences for Euclid, and these self-imposed restrictions can be explained as serving the purpose of mathematical control.

[...] My case... consists in an account of the informal proofs of Euclid’s elementary geometry, an account based on recent formalizations of Euclid’s diagrammatic proofs. The account confirms the Rav/Leitgib view in that it identifies an irreducible role for geometric content in the reasoning. Yet the role played by geometric content is highly constrained, and the constraints are explicated in formal terms. Inferences grounded on an understanding of geometric content occur within a sharply defined formal structure [of Eu]. Accordingly, geometric proof is relativized to a formal framework, a feature that Leitgib identifies with formal proofs. What is and isn’t provable is relative to the formal syntax of the framework and the rules for how it can be used."