Talk:Hilbert-style deduction system

From Wikipedia, the free encyclopedia

Contents 1 Rewrite 2 Is there an error? 3 Too complicated. Kleene 1952: Development of a "formal system" 4 Availability of a forked, rewritten version 5 Three approaches I found till now 6 Possible references 7 Concept of “judgment” as a more characteristic difference among various deduction systems

[edit] Rewrite

This article reads like a cheatsheet for 3, which, I might add, is written in Hungarian. The article doesn't define any of its syntax nor explain much of anything else. I appreciate the translation work that Physis has done here, but it's so much more technical than similar articles that I think it needs a complete rewrite. Vagary 02:02, 4 February 2007 (UTC)

[edit] Is there an error?

I'm not sure I understand these entirely, but shouldn't the eight axiom be

• 

instead of

• 

? --SLi 21:52, 28 May 2007 (UTC)

• 

Thank You very much. Besides the corrected typo, I chose also a better notation: x,y for metavariables (on varables); t₁, t₂ for metavariables on terms.

Physis 10:55, 24 June 2007 (UTC)

Sorry for the other error. In fact, Axiom 8 can be weakened, while it was too strong in another aspect at the same time. It must be

where let denote a restriction of allowed substitution Sbst — the restriction says that the substituted term is a variable, not an arbitrary term: .

Physis 20:33, 28 June 2007 (UTC)

[edit] Too complicated. Kleene 1952: Development of a "formal system"

It is depressing to run into something as abstruse and inaccessible as this article. Here is the system as Hilbert and Kleene and Godel defined it, in more or less current symbolism. I'm sure what is in the article is well-done, but is there another way to present it? Here is Kleene's approach:

---

This form of number theory extends for all the real numbers: -∞, 0, +∞. Kleene 1952 starts at chapter IV A FORMAL SYSTEM then skips to Chapter VIII FORMAL NUMBER THEORY.

To develop this theory he immediately defines what he calls three "function symbols" + (plus), * (times), ' (successor). But the development is worth repeating to see what is going on. In summary:

Symbols:

His entire collection of symbols is Logical symbols: ⊃ (implies), & (and), V (or), ￢(not), ∀ (for all), ∃ (there exists). Predicate symbols: = (equals). Function symbols: + (plus), * (times), ' (successor). Individual symbols: 0 (zero). Variables: a, b, c, .... Parentheses: (, ).

Juxtaposition (concatenation):

Term: From these symbols and the notion of juxtaposition (concatenation) of these symbols he defines term.

Formula: From term he defines formula.

Scope of a variable, free variable: He develops the notions of "scope of a variable" and "free variable".

Substitution: Then he introduces the notion of substitution (everywhere there's an occurrence), also replacement (selectively for e.g. one occurrence but not all ... this is confusing).

Transformation rules: in particular the three deductive schema. In the following the symbol ⇒ is being used in place of a long line under the expression, and indicates "yields" in the tautological or derivational sense. The symbols A, B are formulas, A(x), A(t) indicate a formula with a free variable:

Rules of inference: Immediate consequence :

• 2. A, (A ⊃ B) ⇒ B [here A is the first premise and (A ⊃ B) is the second premise, and B is the conclusion
• 9. C ⊃ A(x )⇒ (C ⊃ ∀xA(x) )
• 12. ( A(x) ⊃ C) ⇒ (∃xA(x) ⊃ C)

Postulates: These transformation rules are three of 21 postulates that he divides into three categories:

• GROUP A1: Postulates for the propositional calculus (formulas with no free variables)

• 1a A ⊃ (B ⊃ A). [Hilbert's #1, introduction of an assumption]
• 1b (A ⊃ B) ⊃ ((A ⊃ (B ⊃ C)) ⊃ (A ⊃ C).
• 2. A, A ⊃ B ⇒ B [Modus ponens: which I've always written and worked with as (A & (A ⊃ B)) ⊃ B, cf Kleene 1952:88 ]
• 3. A ⊃ (B ⊃ A & B). [As ⊃ has seniority over &, this is A ⊃ ( (B) ⊃ (A & B) ) ]
• 4a. A & B ⊃ A. [ (A & B) ⊃ A ]
• 4b. A & B ⊃ B. [ (A & B) ⊃ B ]
• 5a. A ⊃ A V B. [ A ⊃ (A V B) ]
• 5b. B ⊃ A V B. [ B ⊃ (A V B) ]
• 6. (A ⊃ C) ⊃ ((B ⊃ C) ⊃ ((A V B) ⊃ C)).
• 7. (A ⊃ B) ⊃ ((A ⊃ ~B) ⊃ ~A). [here ~ instead of the bent bar only because it's easier for me to write]
• 8^o. ~~A ⊃ A. [^o indicates that this "~-elimination" is intuitionistically unacceptable]
• 8^I. ~A ⊃ (A ⊃ B). ["weak ~-elimination" acceptable to intuitionists]

• GROUP A2: (Additional) Postulates for the predicate calculus (incorporating formulas A(x) with a free variable x)

• 9. C ⊃ A(x) ⇒ C ⊃ ∀xA(x)
• 10. ∀xA(x) ⊃ A(t)
• 11. A(t) ⇒ ∃xA(x)
• 12. ( A(x) ⊃ C ) ⇒ ( ∃xA(x) ⊃ C )

• GROUP B: (Additional) Postulates for number theory

It is in the last group B that the predicate symbol " = " and the "function symbols" + and * appear. As these are axioms, they are worth repeating:

• 13. A(0) & ∀x(A(x)⊃A(x') ⊃ A(x). (axiom of induction, cf Peano axioms)
• 14. a'=b' ⊃ a=b. (Peano axiom)
• 15. ￢a' = 0. (Peano axiom)
• 16. a=b ⊃ (a=c ⊃ b=c). (Peano axiom)
• 17. a=b ⊃ a'=b' (Peano axiom)
• 18. a+0=a (additive identity defined)
• 19. a+b'=(a+b)' (addition function-symbol defined in a recursive sense, cf Kleene 1952:186)
• 20. a*0=0 (multiplicative identity defined, an axiom)
• 21. a*b'=a*b+a (multiplication function-symbol defined in a recursive sense, cf Kleene 1952:186)

Finally, he defines the notion of immediate consequence of the premise(s) by the rules.

In his Chapter V Formal Deduction Kleene introduces the metamathematical sign ⊦ ("yields", deducibility relation) as in, for example:

modus ponens: A, A ⊃ B ⊦ B

In the final chapter he introduces the INDUCTION RULE over formulas with variables i.e. A(x). From all of this he deduces (proves) the familiar "arithmetic laws", including "association", "distribution", and "commutation" for + and *, the notions of additive identity and multiplicative identity, and the notions of multiplicative and additive inverses, the order properties (<, ≤, >, ≥), other more unusual properties such as "connexity, irreflexiveness, asymmetry, inequalities under addition and multiplication), but in particular interest the existence and uniqueness of quotient and remainder.

From this follows the notion of formally provable and we have, in a nutshell the same development used by Kurt Gödel in his Incompleteness theorems (1931) (which is fact where Kleene's development stops until he introduces the notion of primitive recursive functions. wvbailey Wvbailey 16:03, 11 November 2007 (UTC)

---

The reference David Hilbert (1927) The Foundations of Mathematics is a famous exerpt from Sahotra Sarkar (ed.) 1996, The Emergence of Logical Empiricism: From 1920 to the Vienna Circle, Garland Publishing Inc. Wherein Hilbert lays out his formal axiomatic system. This can be found at

reference: http://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm

Hilbert 1927:

Symbols of the system: { ⊃ , &, V, ~, ∀x, ∃x, =, (, ) }

I. Axioms of implication:

• 1. A ⊃(B ⊃ A) (introduction of an assumption)
• 2. (A ⊃(A ⊃ B)) ⊃ (A ⊃ B) (omission of an assumption)
• 3. (A ⊃(B ⊃ C)) ⊃ (B ⊃ (A ⊃ C)) (interchange of assumptions)
• 4. (B ⊃ C) ⊃ ((A ⊃ B) ⊃ (A ⊃ C)) (elimination of a propostion)

II. Axioms about & and V:

• 5. A & B ⊃ A
• 6. A & B ⊃ B
• 7. A ⊃(B ⊃ A & B)
• 8 A ⊃ A V B
• 9. B ⊃ A V B
• 10. ((A ⊃ C) & (B ⊃ C) ⊃ ((A V B) ⊃ C)

III. Axioms of negation:

• 11. ((A ⊃ B) & ~B) ⊃ ~A (principle of contradiction)
• 12. ~(~A) ⊃ A (principle of double negation)

IV. The logical e-axiom:

• 13. A(a) ⊃ A(e(A)), where e(A) is an object about which the proposition A(a) holds if it holds for any object at all (here ≡ is "logically equivalent" i.e. ←→ )

• 13.1 Definition: ∀(a)A(a) ≡ A(e(~A))
• 13.2 Definition: (∃a)A(a) ≡ A(e(A))

Axioms of equality:

• 14. a = a
• 15. (a = b) ⊃ (A(a) ⊃ A(b))

Axioms of number:

• 16. a' ≠ 0; ( ≠ for "not=")
• 17. ( A(0) & ∀(a)(A(a)⊃ A(a')) ) ⊃ A(b) (principle of mathematical induction)

He also cites the "explicit definitions", which introudce the notions of mathematics and have the character as axioms, as well as certain recursion axioms).

[etc.] Wvbailey 17:59, 15 November 2007 (UTC)

---

[edit] Availability of a forked, rewritten version

I tried to reply these concerns with writing a new approach to introduce the topic. I kept this on a subpage. I shall follow Carl's proposal and will not develop this subpage any more, but contribute to the article indirectly. If the subpage contains anything that can be usable in any way, please feel free to use it. Physis 16:18, 15 November 2007 (UTC)

[edit] Three approaches I found till now

Till now, I have found the following three approaches:

Relying on Extension by definition I

R1.

R2.

R3. (reductio ad absurdum)

R4. where t may be substituted for x in α

R5.

R6. where x is not a free variable of α.

R7. for variable where the notation is not meant as a metavariable, but it is directly part of object language: any fixed variable selected from the object language. Thus, R7 need not be an axiom scheme: it can be a standalone axion instance of its own. Of course, we could use a x metavariable ranging over variables of the object language, but it can be proven that doing so would be superfluous.

R8.

Relying on extension by definition II

D1.

D2.

D3. , mentioning that instead of this (contraposition), also reductio ad absurdum can be used, as at the above approach (R3).

D4.

D5.

D6. where x is not a free variable in α₀

D7. t = t where t is a metavariable ranging over terms

D8. where f is a metavariable ranging over function symbols, and are metavariables ranging over terms.

D9. where P is a metavariable ranging over predicate symbols, and are as above

Conservative extension

The approach I found is not a mere superset of any of the former approaches, because the most interesting axiom for universal quantifier differs: instead of

it postulates

where x is not a free variable in α₀

In details:

C01.

C02.

C03.

C04. . (In both "extension by definition" former approach, this was lacking.)

Conjunction and disjunction

C05.

C06.

C07.

C08.

C09.

C10.

Universal

C11. where x is not a free variable in α₀

C12. where x is a metavariable ranging over variables of the object language, t is also a metavariable ranging over terms of the object language

C13 where x is not a free variable in α₀

Existential

C14. where x is not a free variable in β₀

C15.

C16. where x is not a free variable in α₀. The reference does not use it, I put it here only becauase I think it fits here, forming a kind of dual pair with C13.

Identity

C17. t = t where t is a metavarable ranging over terms

C18. where f is a metavariable ranging over function symbols, and are metavariables ranging over terms.

C19. where P is a metavariable ranging over predicate symbols, and are as above

Questions

Unfortunatelly, I lack the knowledge and overview. which could be needed to write a good summary article. The most interesting thing for me in the differences and common parts in the above approaches:

• In the "conservative extension" approach, can reduction ad absurdum be postulated in a from, so that it resembes more to -introduction? (while double negation axiom would playing the role of -elimination.) Thus, instead of

could we postulate

because I think, so it would form a nice -introduction / -elimination pair with

• Why is the most interesting axiom for universal quantifier in "conservative extension" treatment:

where x is not a free variable in α₀

different from the corresponding axiom in "extension by definition" treatment:

Maybe these questions are not really important here, thus, if they are not really relevant for the article and the topic itself, please do not waste time for them.

Physis 13:56, 15 November 2007 (UTC)

[edit] Possible references

In a book by Stolyar,

Abram Aronovich Stolyar 1970 Introduction to Elementary Mathematical Logic, Dover Publications Inc, NY ISBN 0-486-64561-4,

I found a reference to Alonzo Church 1956 'Introduction to Mathematical Logic, I [?? sic], Princeton University Press, 1956, and also David Hilbert and William Ackermann, Principles of Mathematical Logic, Chelsea, New York, 1950 (translation of 1928 German edition.)

On p. 102 Stolyar writes that "In one of Hilbert's systems, one takes the symbols for disjunction and implication" to form an axiom system for the propositional calculus. On page 167 Stolyar introduces the four formulas of the predicate calculus that appear in Kleene 1952:82, i.e. the same four that appear in the section above, in "Group A2". Bill Wvbailey (talk) 19:01, 18 November 2007 (UTC)

[edit] Concept of “judgment” as a more characteristic difference among various deduction systems

Maybe I have made an error as I wrote in the lead that an essential feature Hilbert-style deduction system (distinguishing it from other ones) is the specific trade-off between logical axioms versus rules of inference. I should have grasped the essence better. What is the main motivation? What is the most essential feature that sort of "defines" what can be regarded as a [variant of the many] Hilbert style deduction systems?

Two things could be explained in lead:

1. The main motivation. I lack the knowledge to undertake it.
2. Motivations, trade-offs are things that we can move along a continuous scale. But there is also a very clear, sharp, not-blurrable border that separates the various deduction systems, manifesting itself even in use of metasigns. This clear distinguishing (maybe defining?) characteristic feature is the way they define (and exploit) the auxiliary concept of “judgment”.

In Sequent calculus article, I read an approach that grasps the differences among deduction systems in the way they define the auxiliary concept of "judgment". Hilbert-style (HS), natural deduction (ND) and sequent calculus (SC) seem fro me increasingly exploiting this concept:

• from coinciding with a standalone formula (HS),
• through asserting deduction explicitly from a given context (ND),
• to reaching a sophisticated form (SC).

A standalone article could be written for Judgment (mathematical logic), detailing the roles of "judgment" in each of all the three deduction systems, in a similar way as it is worked out in Sequent calculus article. I lack the necessary sincerity of knowledge, thus I only have only written a stub (and extended also Judgment (disambiguation) slightly).

As for the other characteristics of Hilbert-style deduction system (trade-off between logical axioms and rules of inference, metatheorems that are not explicitly declared as building blocks, but can be demonstrated): are they only secondary phenomena following from the way judgments are defined? Theoretically, the number of rules of inference (or logical axioms) can be augmented (with declaring both-side rules for conjunction, disjunction, both quantifiers), but the resulting system will still be not the same as natural deduction, because judgments will still coincide with standalone formula themselves, lacking the explicit mentioning of context. Thus, it seems to be for me an independent feature, a casual coincidence, not giving the defining essence of Hilbert-style deduction systems (albeit tradition may suggest so).

In summary: how do these many things join to each other, and which are primary factors, which are of secondary nature, which are independent?

• motivation
• metatheorems
• trade-off between logical axioms and rules of inference
• exploiting auxiliary concept of "judgment"

Physis (talk) 23:45, 2 January 2008 (UTC)

I have began some changes. The way I have rewritten the lead of Hilbert-style deduction system, and initiated Judgment (mathematical logic) itself, can have serious flaws, of couse it can be reverted or rewritten. But I hope this way the proposal can be judged better, because it can be seen explicitly what changes it suggests.

Physis (talk) 01:18, 3 January 2008 (UTC)

Could you give a reference for this? I don't think I've seen it in, for example, the Handbook of Proof Theory, but I might have missed it. The "party line" is that Hilbert-style systems trade fewer inference rules for more axiom schemes. — Carl (CBM · talk) 02:42, 3 January 2008 (UTC)

Thank You very much for the quick feedback. I admit I cannot provide a reference it yet (except for article Sequent calculus, of couse I know Wikipedia cannot not be referenced by Wikipedia). But I remember vaguely a book that discusses the topic in a similar way, unfortunately I had to return it to the library, I try to take it again tomorrow. I hope I can provide exact references and more details then. Best wishes, Physis (talk) 03:42, 3 January 2008 (UTC)

Everything has also an article about "judgment" in formal theories], I shall check its references tomorrow (e.g. Pfenning, Frank and Rowan Davies. A Judgmental Reconstruction of Modal Logic. In Mathematical Structures in Computer Science, 11(4):511--540, August 2001). I shall check tomorrow if I can avail this article or someting refered by it. Physis (talk) 04:00, 3 January 2008 (UTC)

Dear Carl,

I have taken the book, its approach (pp. 168, 185, 193) seems to fit here. I shall summarize it tomorrow (the book is Hungarian language).

I shall try to look for English sources on the weekend. Till now, I have found Pfenning, Frank (2004 Spring). "Natural Deduction", 15-815 Automated Theorem Proving.  As far as I can grasp it now, it supports exactly this approach, but shall have to read through it thoroughly yet. I shall check also Kneale & Kneale The Development of Logic, and Curry Combinatory Logic tomorrow.

Best wishes,

Physis (talk) 04:25, 4 January 2008 (UTC)

Thank you very much. I'll need some time to look through those before I can comment sensibly here. My main concern is first to understand what is being referred to as a judgement. A secondary concern is judging the correct amount of weight our articles should give to the concept. I'll be away for a few days, as well. — Carl (CBM · talk) 12:59, 4 January 2008 (UTC)

---

I don't know what is the best way to explain Hilbert-style logic, natural deduction and sequent calculus in the most intelligible way but the distinction between proofs as simple derivations of formulas and proofs as derivations of formulas relative to a given context is probably rather difficult to justify.

Hilbert-style logic is not strictly free of assumptions. Typically, how could we state the deduction theorem if derivations in Hilbert-style logic were not relative to a context of assumptions? Especially the rule (from paragraph Formal deductions) that states that φ holds if φ is an assumption of the context requires a notion of context.

I don't think that considering Hilbert-style logic as a logic that maximizes the ratio axioms/inference rules is a wrong view as Physis wonders at the beginning of the talk.

I'm not sure that there is a so clear and sharp border that separates the various deduction systems. For instance, even sequent calculus, in some recent formulations, has been formalized as a system for deriving formulas, leaving away the need for explicit sequents. In practice, all of the three kinds of systems can be presented as systems of sequents of the form , and all of the three kinds of systems can also be presented as systems for deriving formulas from an implicit context "hanging in the air". --Hugo Herbelin (talk) 20:55, 5 January 2008 (UTC)

---

Dear Hugo Herbelin,

The idea has was instilled into me originally by article Sequent calculus, but later

• Pfenning, Frank (2004 Spring). "Natural Deduction", 15-815 Automated Theorem Proving. 

seemed for me to reinforce it, and

• Martin-Löf, Per (1983). On the meaning of the logical constants and the justifications of the logical laws. Siena Lectures.

suggested me that Judgment (mathematical logic) is not only something capable of helping in the classification of various deduction systems, but something important examining it on its own as well.

(The whole reference list is being collected on Judgment (mathematical logic)#External links.)

I admit I have not read them through yet, just judged by the intoductory parts of both. Please forgive me if I had misunderstood them in a serious way, in that case please help me show the main track these papers want to say.

Thank You very for Your these information. The last sentence You wrote was especially novelty to me.

• Is the "simpler direction" (formalizing HS with explicit mentioning of contexts) solved in the trivial way (using contexts in an idle way)?
• And how is the "more interesting" direction (formalizing ND or SC without explicit contexts) solved? (I think techniques like "dischargement of hypothesis" is a "cheating" in this question: something of "context-changing" nature is hiding behind it.) Can You help me to find some works about this, or summarize the main ideas?

Similarly, it was novelty to me that there are recent treatments of sequent calculus without referring to given context. Can You write some details (or sources) about it (or about the analogous achievement for natural deduction)? What I am interested in most: how are those rules of inferences conveyed, which are inherently of "context-changing" nature (most importantly, implication-introduction). Are these recent approaches You wrote about really a way which can be compared to the way HS acts? Does it not "cheatingly" "bring back" context-changing in a disguised form? For example, I think, the technique of "discharging hypotheses" in the proof tree is a "cheating" (from the point of vies of this this problem): HS does not even need referring to any dischargment.

As for summarizing my conjecture: I think HS is something that is free from any kind of "context-changing rules of inference (of course metatheroems about context or even context-changing can be posed "on top of it"), while ND is something that incorporates something context-changing in its very kernel: it has context-changing rules of inference, at least that of implication-introduction (it corresponds to deduction theorem in HS, but HS has DT not incorporated in its kernel, but built on top of it, "in the shell"). I suppose that's why ND relies so heavily on a more sophisticated form of concept "judgment", while for HS such a minimalistic jdugment concept suffices.

• Of course natural deduction can be formalized also without -like rules, e.g. using techniques like discharging hypotheses in a proof tree. But I think that is "cheating" (from the point of viw of this problem): dischargement is an open admitting that something of context-changing nature is taking place. That is why I am very interested in Your message: a non-cheating way of approaching natural deduction without any context-changing rules of inference.
• On the other side, of course HS can be formalized via contexts, but (at least in the trivial solution I can think of now), this contexts will be idle, conveying no context-changing. Please summarize the main idea if the solution You have thought of is not this trivial one.

To express it in images:

In Hilbert-style deduction system,	For contrast, in natural deduction,
judgments are of minimalistic form	judgment is of a more sophisticated form, playing significant role in the machinery.
DT is not connected to the notion judgment	(implication-introduction, the correspondent of DT in HS) relies directly on the notion of judgment
DT is on the shell, built on top of the machinery as a metatheorem.	is in the very kernel, incorporated as rule of inference, not just dropped onto the top of the already-built machinery.

I did not understand Your second paragraph (debating the claim that HS is free of notion of context). Of cause HS is as powerful as ND or SC, thus, we can define concept of derivation, introduce turnstyle symbol in the metalanguage, we can say metatheroems using it, posing things about context, even about context-changing. Deduction theorem surely holds for HS, but I did not really understand why DT (expressed as metatheroem) would contradict the claim that HS uses a minimalistic form of judgment. In short: after we have already built the machinery of HS, we can define deduction via it, and on top of all this, we can say (and prove) metatheorems about context-changing (including DT). But HS does not incorporate DT as a rule of inference, thus, it does not have anything of "context-changing" nature its very kernel, thus, concept of "judgment" can be of minimalistic form. In short, HS has DT in the "shell", while ND has it in the "kernel".

I know there are principal questions I could not answer yet: for example, as Talk:Judgment (mathematical logic) shows, I know almost nothing about "ontology" of the notion of judgment. The references I can find are being collected on Judgment (mathematical logic)#External links.

Physis (talk) 04:50, 6 January 2008 (UTC)

---

Dear Physis,

I now understand what you mean. Yes, HS is the only kind of deduction system (among HS, ND and SC) for which the context is never modified by the inference rules and hence, HS is the only system that, in the case one is interested in only tautologies (i.e. ) and not in hypothetical judgments (i.e. the more general form ), one can formulate the notion of provability without introducing a notion of contexts.

That derivability of tautologies in HS can be defined more easily is certainly the reason why HS has come first, historically. Nevertheless, I would not restrict HS to this property. The most general form of HS needs to refer to judgements of the form (again I'm thinking about DT) in its definition and the restricted, simplest form, that does not require to mention explicit contexts, addresses only the derivability of pure tautologies.

Especially, I agree that the property that contexts are never changed by the inference rules is an essential property of HS and I have no objection against saying that the not-changing nature of contexts in the definition of provability is the essence of HS.

Still, I would not consider that HS relies on a different kind of judgment than ND or SC do. In all three kinds of systems, judgments are predicates of the metalanguage that are characterized by a set of inference rules and a judgment is by no way reducible to a formula. A judgment asserts the provably of a formula, it is not itself a formula. The only difference with ND and SC is that in ND and SC, judgments in the empty context (i.e. judgements asserting the provability of a tautology) cannot be defined without referring to non-empty contexts while in HS, judgments in the empty context can be defined without referring to any kind of context.

DT is indeed not an inference rule of HS but DT is a statement about derivability, and it cannot be formulated without introducing the notion at some point of the definition of HS.

From a didactic point of view, it may be indeed interesting to first define the judgments and to define the more general notion (so that DT can be stated) only in a second step.

Regarding SC in implicit context form (i.e. as a tree of formulas, like ND), the trick is the following: Instead of having just a "judgment" of the form "A true" as in Natural deduction, we use three kinds of judgments which are "A true", "A false" and "contradiction". The inference rules (for classical logic), then, are the following:

This is somehow a presentation which is standard for the introduction rules in the proof search community and that has additional rules for cut and reasoning by contradiction. I don't know how far this is an original presentation, it is taken from a work of mine (page 7).

I'm afraid not to be of great help regarding the "ontology" of the notion of judgments. I believe I generally use it in a rather naive way as a generic name for the kind of inductively defined predicates used in metatheory when talking about logic as an object of study. In its more general view, definitions like "φ is a formula", "φ and ψ are isomorphic", "φ is provable", "φ is provable in the empty context", "φ is true", "t is a term built from symbols f₁,...,f_n", "the variable x occurs in formula φ", etc. are considered by some authors as judgments.

PS: It could be interesting to look at how metatheory is formalized in practice. For instance the Coq proof assistant is a software in which the notions of provability in HS, ND or SC can be defined in a rather simple way. If I find time I may elaborate on the use of such software as a metalanguage for talking about logic. --Hugo Herbelin (talk) 13:30, 6 January 2008 (UTC)

---

Dear User:Hugo Herbelin,

Thank You very much the kind and detailed answer. It helped to me to unify several disjointed bits, I did not grasped such an overview before.

I lacked overview, now thank You for illuminating

• "judgment" is not an especially distinguished entity, it is not separated from other predicates in the metaheory. I thought previously that judgments are sort of "lower lever", "standing closer to the kernel", than "other" metatheoretic assertions, moreover, other metatheoretic assertions are built on top of them.
• HS can be formalized also in style rules of inference. Although they are not context-changing, but this approach has still advantages, because in this way, we can define the concept of deduction in one go. The only solution I knew till now was to say axioms and rules in a context-less form, then build on top of it a concept, using auxiliary techniques (e.g. sequence)
• Sequent calculus can be approached also by the discharging technique.

I shall modify my changes in both affected articles

• lead of Hilbert-style deduction system
• Judgment (mathematical logic)

accordingly to what You have written.

Thank You also for about writing about Coq. I read about it somewhere in the materials provided by the Haskell community, but I have to learn yet much about proof theoretic aspects of functional programming. The thing I did in Haskell was to write an untyped combinatory logic interpreter (augmented with some computer algebra capabilities), then with its help to write a quine in pure combinatory logic: an expression that is equivalent to its own quotation (i.e term tree representation).

Best wishes,

Physis (talk) 12:41, 7 January 2008 (UTC)