Log in

No account? Create an account
social proofs and formal proofs - язык, на котором не говорят [entries|archive|friends|userinfo]

[ website | personal website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]
[ tags | journal tags ]

social proofs and formal proofs [Sep. 2nd, 2017|08:39 am]
[Tags|, ]

There are two distinct viewpoints of what a mathematical proof is. The first view is that proofs are social conventions by which mathematicians convince one another of the truth of theorems. That is to say, a proof is expressed in natural language plus possibly symbols and figures, and is sufficient to convince an expert of the correctness of a theorem. Examples of social proofs include the kinds of proofs that are presented in conversations or published in articles. Of course, it is impossible to precisely define what constitutes a valid proof in this social sense; and, the standards for valid proofs may vary with the audience and over time. The second view of proofs is more narrow in scope: in this view, a proof consists of a string of symbols which satisfy some precisely stated set of rules and which prove a theorem, which itself must also be expressed as a string of symbols. According to this view, mathematics can be regarded as a ‘game’ played with strings of symbols according to some precisely defined rules. Proofs of the latter kind are called “formal” proofs to distinguish them from “social” proofs.

In practice, social proofs and formal proofs are very closely related. Firstly, a formal proof can serve as a social proof (although it may be very tedious and unintuitive) provided it is formalized in a proof system whose validity is trusted. Secondly, the standards for social proofs are sufficiently high that, in order for a proof to be socially accepted, it should be possible (in principle!) to generate a formal proof corresponding to the social proof. Indeed, this offers an explanation for the fact that there are generally accepted standards for social proofs; namely, the implicit requirement that proofs can be expressed, in principle, in a formal proof system enforces and determines the generally accepted standards for social proofs.

“Handbook of Proof Theory.” Buss, Editor. (“Studies in Logic and the Foundations of Mathematics.” Volume 137.)

The viewpoint that proofs are “convincing arguments” is an amusing one. A gun is more convincing than any mathematical argument. Or other threats. Still, mathematicians do not use them. Why are such arguments forbidden?

Of course, the author could not resist repeating the lie that formal proofs are not intuitive.

Взгляд на доказательства как на «убедительные аргументы» занимателен. Пистолет более убедителен, чем любой математический аргумент. Или другие угрозы. Тем не менее, математики их не используют. Почему такие аргументы запрещены?

Конечно, автор не смог удержаться от повторения лжи, что формальные доказательства не интуитивны. Это как в том анекдоте. Для вас, Козлов, придумали естественный вывод.