Talk:Axiomatic system (logic)

Conjunction introduction and elimination

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)

Archived old talk page, redid much of the article

I have archived all talk page topics that were more than five years old. I moved the article because "Hilbert system" is not what axiomatic systems in logic are always called, or even usually called, or even often. I also redid its first section, changing the part that someone made up from scratch into something that is actually supported by WP:RS, but also moving some the long, unsourced consistency and completeness proofs from Propositional calculus to here, because they are too long to go there anyway, and hopefully they can be changed into properly sourced proofs at some point. I removed the old maintenance template and added other ones to reflect the article's new range of issues.Thiagovscoelho (talk) 02:32, 2 July 2024 (UTC)

Note on move

An unregistered user simply undid the move, and I simply undid it back. Even if a "Hilbert system" is just one kind of axiomatic system, this article covers axiomatic systems in general, especially since I added to it. The article's sources, even before I added to it, did not support the existence of "Hilbert system" as a distinct thing. Wikipedia reflects Reliable Sources, not your personal philosophy of logic. Thiagovscoelho (talk) 21:14, 6 August 2024 (UTC)

Your article is wrong and misleading, and the undo reason essentially provided sufficient reasoning:

"A Hilbert system is just one of several kinds of axiomatic proof systems. An axiomatic system does not even have to be a formal system, and other formal proof systems are natural deduction and sequent calculus."

It is implied that an axiomatic system is something way more general, which should also become clear from reading about axioms, since they are often not stated in formal language in philosophy. But a Hilbert system is a kind of formal system.

To address your concerns, only because someone doesn't explicitly name the a type of system (which has been established for quite some time and is named after David Hilbert who laid out its foundations), it doesn't take that type away from the system. In the same way that when a cat is never explicitly addressed as an animal, it is still an animal.

In case you want to learn some basics on the topic, here is a talk also mentioning Hilbert systems and it addresses their property of how Hilbert-style proofs are similar to Collatz sequences, which makes Hilbert systems very hard to deal with in terms of computational complexity, in contrast to some other formal proof systems, such as natural deduction.

Please do not reclassify articles on the fundamentals of proof theory when you are untrained in that area, and undo your unintentional vandalism. At this point, Hilbert systems have articles in many languages, just not in English, and they're more than relevant enough to have a dedicated article. (Almost all formal axiomatic systems in literature are Hilbert systems, but your rename mistakenly suggests it would be the only way to define formal logical systems.) There was nothing in the article that was not about Hilbert systems before you moved it.

Thanks,

your fellow logician with a research focus on Hilbert systems. 134.61.98.174 (talk) 16:10, 9 August 2024 (UTC)

There seems indeed an issue with the referenced literature being too old to address Hilbert style systems by name. Looking into more recent general introductory literature on proof theory helps, for example

• S. Buss, ed. (1998) Handbook of Proof Theory. Elsevier.

as referenced under the proof theory article. But wasn't this kind of issue declared via caption in this article before you removed it? It surely didn't mean "don't fix be but move me to a whole different topic". 134.61.96.243 (talk) 16:52, 9 August 2024 (UTC)