[<<][compsci][>>][..]Sun Aug 30 15:44:55 CEST 2009

A proof calculus[2] corresponds to a family of formal systems that use a common style of formal inference for its inference rules. A rule of inference[3] (also called a transformation rule) is a syntactic rule used in a formal system which is used to produce valid statements within that system. Examples of proof systems: * Hilbert-style deduction system[4], where a formal deduction is a finite sequence of formulas in which each formula is either an axiom or is obtained from previous formulas by a rule of inferences. * Natural deduction[5] is an approach to proof theory that attempts to provide a deductive system which is a formal model of logical reasoning as it "naturally" occurs. This approach is in contrast to axiomatic systems which use axioms. The sequent calculus[1] is a widely known proof calculus for first-order logic. The term "sequent calculus" applies both to a family of formal systems sharing a certain style of formal inference, and to its individual members, of which the first, and best known, is known under the name LK, distinguishing it from other systems in the family. The sequent calculus LK was introduced by Gerhard Gentzen as a tool for studying natural deduction. In the sequent calculus all inference rules have a purely bottom-up reading. In natural deduction the flow of information is bi-directional: elimination rules flow information downwards by deconstruction, and introduction rules flow information upwards by assembly. Thus, a natural deduction proof does not have a purely bottom-up or top-down reading, making it unsuitable for automation in proof search, or even for proof checking (or type-checking in type theory). [5] In Kleene's Metamathematics, Chapter V, p.86[6] ``The labour required to establish the formal provability of formulas can be greatly lessened by using metamathematical theorems concerning the existence of formal proofs.'' -- remarks The way I understand this is that natural deduction has no axioms (no primitive assumptions) but contains all its structure in the inference rules: the way propsitions can be combined to create new propositions. In contrast, a Hilbert-style deduction system has both axioms and inference rules (i.e. Modues Ponens). Reading more in [6]. It seems that meta-mathematics is quite similar to lisp macros: the meta math serves the purpose to abstract over the _construction_ of formal proofs = meaningless pure syntax. Because formal logic's composition mechanisms at the foundations of mathematics are so barbaric, a macro system makes sense to lift the tedium. What I find surprising however is that this meta system itself is _not_ formal: proofs in the meta system are not formal proofs, but are intuitive justifications of correctness. I'd say this is because of the chicken-and-egg problem: you can't use a formal system to do this, because you don't _have_ one yet (remember, your using this meta-math to _build_ a formal system). This sounds like compiler bootstrapping to me. [1] http://en.wikipedia.org/wiki/Sequent_calculus [2] http://en.wikipedia.org/wiki/Proof_calculus [3] http://en.wikipedia.org/wiki/Inference_rules [4] http://en.wikipedia.org/wiki/Hilbert_system [5] http://en.wikipedia.org/wiki/Natural_deduction [6] isbn://0720421039

[Reply][About]

[<<][compsci][>>][..]