Talk:Formal proof

Insufficiently general

The definition given here applies only to the simpler proof calculi. I does not work for natural deduction beyond propositional logic, and also not for the sequent calculus, in which one works with judgments rather than sentences.  --Lambiam 10:57, 20 May 2008 (UTC)

Nonsense

The following, which is currently the first sentence of the article, is nonsense:

"A formal proof or derivation is a formal theory consisting of a finite sequence of formulas each of which is an axiom or is derived as a logical consequence of the preceding formulas within some formal system."

A formal theory is a set of formulas. As a set, it has no order, and so it makes no sense to talk about preceding formulas in a formal theory.

There is a deeper issue that Hilbert-style proof systems, in which a derivation is a sequence of formulas, are not the only type of formal deduction system. There are other systems in which a formal proof is not a sequence of formulas. Several of these are described at first-order logic. — Carl (CBM · talk) 15:32, 9 November 2009 (UTC)

Formal proof is the same as a derivation?

I don't think that a formal proof and derivation are the same thing. A derivation is just one representation of a formal proof. Another representation is a syntactic expression (in e.g. Martin-Löf's type theory) or a calculation in Dijkstra's style. I think the important step is that the moves made in the proofs should be so fine grained that they correspond exactly to application of the rules of the formal system, not that they actually have to be a pile of rules. I also think it is confusing to describe a derivation as a sequence (a list), it is more naturally conceived as a tree. The root of the tree is the the theorem, the nodes are applications of the inference rules of the formal system and the leaves are the axioms of the formal system.

A further example about expressions: simply-typed lambda-calculus is the term language of intuitionistic propositional logic. Hence proofs in this logic can be represented as either derivations or lambda-terms (expressions).88.196.63.146 (talk) 17:52, 9 July 2010 (UTC)

Give us an example

• Us laymen need a simple "proof" example in this article. For example, can anyone prove that 2 + 2 = 4? Engineers and experimentalists deal with the real world, and know that 2 + 2 = 4.00 +/- 0.01 (degree of uncertainty in measurement, or other experimental error in a real-world application) Proofs only exist in some surreal space.--71.245.164.83 (talk) 02:32, 7 October 2010 (UTC)
  • It only makes sense to prove 2+2=4 if you know what 2 and 4 are. One way to define them is this: 2 := 1+1. 4 := ((1+1)+1)+1. (One generally leaves 0 and 1 undefined and just postulates their most important properties.) Once you know that, it's clear that we need to prove (1+1)+(1+1) = ((1+1)+1)+1. In other words, we need to prove x+(1+1)=(x+1)+1, where x=1+1. (I have only introduced x so that the formula gets easier to read.) But this is just a special case of the associative law of addition. This is not a formal proof yet, but now you just need to press it into whatever formalism you are using. Hans Adler 07:17, 7 October 2010 (UTC)

"...and know that 2 + 2 = 4.00 +/- 0.01 ...". No! That is incorrect! 2+2 = 4. Integers have a special place in the world of significant figures. If the values are expressed conventionally, the right-most digit *should* be assumed to be accurate to within 0.5. That is 1.0 means (by convention) 1.0 ±0.5 and 2.00 means 2.00 ±0.005. So, 2.00 + 2.00 = 4.00 ±0.01 (since 'error', in this case, is additive). Integer values, probably since they represent the counting numbers, are often 'immune' from this convention. 2+2 = 4 is true when counting people, but may not be true if talking about measured quantities. ("Travel 2 miles South and 2 miles West" might be a trip of 4 miles, but no one should be much surprised if the total trip were 3.3 miles, nor if it were 5.0 miles.) Also, given 2.00 + 2.00, the convention would be to say they sum to 4.0 (reducing the number of significant digits) but in many cases, 4.00 would be more useful to convey the uncertainty. (4.0 implies ±0.05, while 4.00 implies ±0.005, and the 'actual' uncertainty is 0.01 which is closer to 0.005 than 0.05).FWIW98.21.219.152 (talk) 15:23, 31 August 2022 (UTC)

External links modified

Hello fellow Wikipedians,

I have just added archive links to one external link on Formal proof. Please take a moment to review my edit. If necessary, add {{cbignore}} after the link to keep me from modifying it. Alternatively, you can add {{nobots|deny=InternetArchiveBot}} to keep me off the page altogether. I made the following changes:

• Added archive https://web.archive.org/20090908075745/http://2piix.com:80/articles/title/Logic/ to http://2piix.com/articles/title/Logic/

When you have finished reviewing my changes, please set the checked parameter below to true to let others know.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—^{cyberbot II}_{Talk to my owner:Online} 20:34, 11 February 2016 (UTC)

Assumption

The introductory sentence states that A formal proof is a finite sequence of sentences each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence.... There should be an explanation of what assumption means in this context - the word "assumption" is never mentioned later in the article. Can somebody clarify what assumption is? In another article there is a similar definition, but nothing about assumptions is said so should we remove assumption from the definition? -- Martinkunev (talk) 15:21, 30 June 2016 (UTC)

We need an explanation of a formal proof

The sentence "For a well-formed formula to qualify as part of a proof, it must be the result of applying a rule of the deductive apparatus of some formal system to the previous well-formed formulae in the proof sequence." doesn't actually state what a formal proof is. It states one property any well-formed formula that's part of a formal proof must have. I think there's no clear definition of a formal proof because a formal proof can be a written proof in any formal system that has already been invented but we never formed a definition of a formal system because a formal system is probably just a system that got invented that people then decided to call a formal system. Maybe this article should at least state for any formal system what a formal proof of a statement in that system is as a series of well-formed formulas each of which can be deduced from 2 of the earlier formulas or in the series or from a set of axioms where the last well formed formula represents that statement. Blackbombchu (talk) 00:37, 8 September 2016 (UTC)

History

If anyone knows who first defined "formal proof" (in the logician's sense), it would be nice for the article to mention it. 31.48.245.23 (talk) 20:31, 25 January 2018 (UTC)