Formal proof
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.
- Comment
- enIn logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.
- Has abstract
- enIn logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof. The theorem is a syntactic consequence of all the well-formed formulas preceding it in the proof. 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 formulas in the proof sequence. Formal proofs often are constructed with the help of computers in interactive theorem proving (e.g., through the use of proof checker and automated theorem prover). Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, while the problem of finding proofs (automated theorem proving) is usually computationally intractable and/or only semi-decidable, depending upon the formal system in use.
- Hypernym
- Sequence
- Is primary topic of
- Formal proof
- Label
- enFormal proof
- Link from a Wikipage to an external page
- www.ams.org/notices/200811/%7Cwork=Notices
- mizar.org/
- web.archive.org/web/20090908075745/http:/2piix.com/articles/title/Logic/
- www.isa-afp.org/
- Link from a Wikipage to another Wikipage
- Alphabet
- Automated theorem prover
- Axiom
- Axiomatic system
- Category:Formal languages
- Category:Formal systems
- Category:Logical truth
- Category:Proof theory
- Category:Syntax (logic)
- Computationally intractable
- De Bruijn Factor
- Deductive apparatus
- Effective method
- Fitch notation
- Follows from
- Formal language
- Formal semantics (logic)
- Formal system
- Formal verification
- Generalization
- Interactive theorem proving
- Interpretation (logic)
- Logic
- Mathematical proof
- Mathematics
- Meaning (linguistics)
- Natural deduction
- Proof (truth)
- Proof assistant
- Proof calculus
- Proof theory
- Proposition (philosophy)
- Reference
- Rule of inference
- Semantics
- Semi-decidable
- Sequence
- Sequence (mathematics)
- Sequent calculus
- Set (mathematics)
- String (computer science)
- Structure (mathematical logic)
- Symbol
- Theorem
- Transformation rule
- Well-formed formula
- SameAs
- 2a5Bq
- Démonstration formelle
- Derivação formal
- Dimostrazione
- Formal proof
- Formeel bewijs
- m.043v063
- Prueba formal
- Q2762418
- Доказ (логіка)
- برهان فلسفي
- Subject
- Category:Formal languages
- Category:Formal systems
- Category:Logical truth
- Category:Proof theory
- Category:Syntax (logic)
- WasDerivedFrom
- Formal proof?oldid=1113095164&ns=0
- WikiPageInterLanguageLink
- Axiomatischer Beweis
- WikiPageLength
- 5200
- Wikipage page ID
- 1197184
- Wikipage revision ID
- 1113095164
- WikiPageUsesTemplate
- Template:Authority control
- Template:Cite web
- Template:Logical truth
- Template:Main
- Template:Mathematical logic
- Template:Reflist
- Template:Short description