This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | |||||||||||
|
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)
I'm not sure I understand these entirely, but shouldn't the eight axiom be
instead of
? -- SLi 21:52, 28 May 2007 (UTC)
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 :
Postulates: These transformation rules are three of 21 postulates that he divides into three categories:
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:
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:
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
Hilbert 1927:
Symbols of the system: { ⊃ , &, V, ~, ∀x, ∃x, =, (, ) }
I. Axioms of implication:
II. Axioms about & and V:
III. Axioms of negation:
IV. The logical e-axiom:
Axioms of equality:
Axioms of number:
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)
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)
Till now, I have found the following three approaches:
Relying on Extension by definition I
Relying on extension by definition II
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
In details:
Conjunction and disjunction
Universal
Existential
Identity
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:
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)
In a book by Stolyar,
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)
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:
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:
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?
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)
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. {{
cite book}}
: Check date values in: |year=
(
help); External link in
(
help); Unknown parameter |chapterurl=
|chapterurl=
ignored (|chapter-url=
suggested) (
help) 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)
---
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
{{
cite book}}
: Check date values in: |year=
(
help); External link in |chapterurl=
(
help); Unknown parameter |chapterurl=
ignored (|chapter-url=
suggested) (
help)seemed for me to reinforce it, and
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.
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.
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 f1,...,fn", "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
I shall modify my changes in both affected articles
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)
The article uses ϕ in LaTeX formulas and φ in the text itself, as if they are the same symbol. It should be consistent and use only one of them. -- salty-horse ( talk) 22:44, 3 January 2009 (UTC)
Why is the frequently used Hilbert system a redirect to the infrequently used Hilbert-style deduction system? I propose to reverse this redirect. — Charles Stewart (talk) 10:01, 26 February 2009 (UTC)
...and some of it is my fault. I'll slap on a Template:Contradict notice on it. The main issues are:
1. Doesn't really recognise the differences between different sorts of Hilbert system. The most important distinction is the threefold distinction between (i) systems that have schemes that are short for infinite sets of axioms, (ii) systems with axioms that contain schematic variables, which have a special rule, typically combined into axiom instantiation and rule unification, and (iii) systems with a rule of uniform substitution.
2. Has a straightforward contradiction: the lede asserts that systems for predicate logic needs a generalisation rule, the body asserts that generalisation is a meta-theorem. The contradiction is introduced by me; which claim is true depends on which kind of Hilbert system one uses.
3. Has a convoluted reference section whose contents do not obviously provide sources to the article.
4. Has some rather glib claims, e.g. the asserted difference between Hilbert systems and natural deduction. In fact the inference system that takes a Hilbert system and extends its notion of inference by allowing such metatheorems as the deduction theorem as steps is widely called natural deduction.
5. Oh, and I also introduced -ise spelling into an article that was using -ize spelling. Trivial, but still an issue.
The article is clearly in need of intensive care. I haven't time in the next few days; it would be wonderful if on my return some kind soul had done the edits, otherwise I will get around to it... — Charles Stewart (talk) 08:36, 16 April 2009 (UTC)
---
Well here it's almost 2 years later. So I've forgotten all this stuff. That means I'm looking at this with newbie eyes. I scanned the article and was left clueless. I figured I'd just blow this one off, but then I slept on it and woke up curious.
My first, most important, question: Is there a reliable source that I trust and I can comprehend (key concepts) that actually uses the words "Hilbert system"? (Yes, after a long search, exactly 1 book.)
Second question: And is a "Hilbert system" a "Hilbert-style deductive system"? (Haven't a clue.)
Third question: In fifty words or less, what is it? (It's an antidote to model theory called "proof theory" of which there are a number of alternates that includes the "Gentzen-type system" and has variants due to guys like von Neumann. Model theory is t and f and truth tables. Proof theory (I surmise) is how to get from INPUT (assertions) to OUTPUT (a derived formula) via manipulation of abstract symbols per rules defined at the outset (44 words).)
Fourth question: Does it include the four categories described in Hilbert 1927, or just the first one? Or just the first and second ones? (Haven't a clue):
Fifth question: This is related to Question 6. Is this just some archaic, historically-interesting backwater? (Kleene shows how to analyze arguments. But does anyone use this stuff anymore?)
Sixth question: What's the relationship between this stuff and the theory of abstract machines [Turing machine or a counter machine]? At every instance of a conditional instruction and combinatorial line(s) (such as A ← A + B), "symbol manipulation" and modus ponens (detachment) is at work. That's how the computation proceeds: given that A + B, we detach the sum and put it in location A. It's all Markovian, once its been derived, we move on. And clearly we have replacement (substitution).
I hunted through all my books on logic (including Kleene 1952) and came up with only one "hit" re "Hilbert system"-- actually indexed that way in Kleene 1967 Mathematical Logic, republished 2002 by Dover Publications, Inc., Mineola, NY, ISBN 0-486-42339 (pbk.). In his 1952 he derives all the following stuff but doesn't actually call it a "Hibert system" that I could see.
Who called it a "Hilbert system"? Haven't a clue except it looks like Kleene can be implicated in the crime:
So what is the little symbol ⊧ mean? It means "is valid" [cf p. 14 from an exhaustive truth-table investigation]. In a footnote he expands the notion:
Okay, so what are his "axioms"? Well, it depends. I believe we are talking only about the propositional calculus. But if we're going to inlcude the Predicate calculus, and Equality, then there are more. And for number theory, even more. For the propositional calculus:
For the predicate calculus (additional, pp. 107, 94-96, 150):
For the use of Equality (additional, p. 154)
At least in my mind, the symbolisms etc need further expansion: what's a P() and a f()?
⊧⊃¬∼∾∀∃⇒ Anyway, he goes on in section 9 to discuss the notion of (formal) deduction from assumption formulas (page 35). In section 10 appears "The deduction theorem" which he blames on Herbrand 1930:
The proof is sufficiently opaque. Section 11 is Introduction and Elimination Rules. Section 12 is Completeness., Section 13 is Use of Derived Rules. This is sufficiently overwhelming. So I'm going to stop now.
Anyway, this may provide some background that I can pull from. Bill Wvbailey ( talk) 17:43, 3 February 2011 (UTC)
Answers:
Cheers, — Charles Stewart (talk) 18:35, 3 February 2011 (UTC)
Thanks. I got the same request you did. But last time I looked at this was 2 years ago and I didn't clearly understand then that this is a topic in "proof theory" (as distinct from its extension via the extra axioms, into number theory). Which brings me to . . .
Some clarifications RE question #5, and a new question #7 re proof theory vs recursion.
Thanks again, Bill Wvbailey ( talk) 19:58, 3 February 2011 (UTC)
Ben Ari [1] calls it "Hilbert system" --Anonymous 14:52, 1 September 2011 (UTC) — Preceding unsigned comment added by 84.58.201.140 ( talk)
from A. S. Troelstra in “basic proof theory”:
"2.5.3. Hilbert systems. Kleene [1952a] uses the term “Hilbert-type system”; this was apparently suggested by Gentzen [1935], who speaks of “einem dem Hilbertschen Formalismus angeglichenen Kalkiil”. Papers and books such as Hilbert [1926,1928], Hilbert and Ackermann [1928], Hilbert and Bernays [1934] have made such formalisms widely known, but they date from long before Hilbert; already Frege [1879] introduced a formalism of this kind (if one disregards the enormous notational differences). We have simplified the term “Hilbert-type system” to “Hilbert system”. There is one aspect in which our system differs from the systems used by Hilbert and Frege: they stated the axioms, not as schemas, but with proposition variables and/or relation variables for A, B, C, and added a substitution rule. As far as we know, von Neumann [1927] was the first to use axiom schemas."
Even in Hilbert and Ackermann [1928], they mentioned that this was first done by Frege. I think we should change the subject to something like "Hilbert-style system" or "Hilbert-type system" but I should take a look at A. Church’ Great Book for more information on history. — Preceding unsigned comment added by Mrmusavi ( talk • contribs) 12:08, 8 October 2012 (UTC)
I believe that the axioms listed for the Hilbert system have a small error. The logical axioms each need to be preceded by a list of arbitrary universal quantifiers. E.g., instead of
it should read
where denotes a sequence of arbitrarily many universal quantifiers over arbitrary variables. And so forth for all the other axioms. Otherwise you can't infer, e.g., (supposing that is a unary relation). (The universal introduction rule requires that the quantified variable not be free in the formula of interest.) See, e.g., https://cs.uwaterloo.ca/~david/cs245/cs-firstorder.pdf.
Nick Thomas <nwthomas@asu.edu> — Preceding unsigned comment added by 68.230.67.135 ( talk) 10:06, 22 November 2012 (UTC)
And I think, in the equality axioms I8, I9, there should also be universal quantifiers at the beginning. 128.176.181.5 ( talk) 16:41, 18 February 2013 (UTC)
The page says: "Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on Metatheorems), in which case the rules Q6 and Q7 are redundant."
I can't see how this can be the case. It is easy to prove Q6 and Q7 using universal generalisation and the deduction theorem, but proving the deduction theorem as a metatheorem with universal generalisation as a rule (as well as modus ponens) requires Q6 and Q7.
Conversely, I don't see how you could do anything without universal generalisation as a rule. How would you prove something as simple as ? You can't use substitution of equivalents because contains x free.
Is there perhaps a mistake here?
The page also says: "US. Let be a formula with one or more instances of the propositional variable , and let be another formula. Then from , infer ."
This also seems wrong to me. Let be and let be .
Then we have from , infer , which is clearly wrong.
I think what it's meant to be is:
"US. Let be a theorem with one or more instances of the propositional variable , and let be a formula. Then is also a theorem."
In other words, if then
AndreRD ( talk) 11:50, 16 June 2016 (UTC)
Am I reading this right?
A -> B -> A ^ B
I'm not seeing any mention of the branching rule used. This should be explicitly mentioned somehow. I'm assuming left branching and reading it this way: "(A implies B) implies (A and B)"
This would mean that if we accept that A implies B we have to accept B. What? And it means that if we accept that A implies B we have to accept A. What? Something seems to be wrong here.
If we assume some sort of right branching scheme it could be: "A implies (B implies (A and B))"
Which seems fine. But right branching schemes require reading all the way to the end of a potentially very long expression before you can even figure out how to group terms, and then going back to the beginning of the expression and employing the previously discovered grouping while reading the expression. Could this really be how a standard notation for a Hilbert system works? It seems to me there must be something wrong here. Perhaps the expression in question was formulated incorrectly. But either way, to avoid confusion, some convention should be employed to allow a reader to figure out notation conventions. Perhaps a section on notation should be included in each article that covers a logical system. If Wikipedia employs certain agreed upon conventions about logical notations, then one or more articles about those conventions should be crafted and those articles could be linked to in a sufficiently prominent way from articles about logical systems. Readers should not have to guess, and notation systems used should be made explicit somehow. Comiscuous ( talk) 19:48, 19 December 2021 (UTC)