MHB Treatment of axioms of formal axiomatic theory

Click For Summary
The discussion centers on the treatment of results derived from outside a formal axiomatized theory, specifically regarding the "≤" relation in Robinson Arithmetic (Q). It questions whether results established through methods like induction, which are not inherent to Q, should be considered as part of Q's axioms when used in formal proofs. The consensus is that these results, referred to as Q-sentences, are not added to Q's axioms. Instead, they function similarly to other theorems within Q that do not rely on induction. The conversation highlights the need for clarity in understanding how these external results integrate into the framework of Q and encourages further elaboration on specific proofs and their implications.
agapito
Messages
46
Reaction score
0
What is the proper treatment of results about a formal axiomatized theory which are obtained from outside the theory itself? For example, there are 9 results dealing with the "≤" relation for Robinson Arithmetic, some of which are established by using induction, which is not "native" to Q.

Are these Q-sentences added to the axioms of Q when applied in some formal proof? Otherwise, where or how do they appear?

Thanks for any help.
 
Technology news on Phys.org
agapito said:
Are these Q-sentences added to the axioms of Q when applied in some formal proof?
No.

agapito said:
Otherwise, where or how do they appear?
I may have an idea about what you are asking, but I am not totally sure. It would be nice if you provided more details. Please give references to the proofs of theorems of Q that are proved by induction. And most importantly, please explain what you mean by "where or how do they appear?". They are used in exactly the same way as other theorems of Q that are proved without induction.
 
Anthropic announced that an inflection point has been reached where the LLM tools are good enough to help or hinder cybersecurity folks. In the most recent case in September 2025, state hackers used Claude in Agentic mode to break into 30+ high-profile companies, of which 17 or so were actually breached before Anthropic shut it down. They mentioned that Clause hallucinated and told the hackers it was more successful than it was...

Similar threads

  • · Replies 2 ·
Replies
2
Views
318
  • · Replies 10 ·
Replies
10
Views
2K
  • · Replies 11 ·
Replies
11
Views
3K
  • · Replies 4 ·
Replies
4
Views
2K
  • · Replies 2 ·
Replies
2
Views
2K
Replies
14
Views
4K
  • · Replies 210 ·
8
Replies
210
Views
18K
  • · Replies 2 ·
Replies
2
Views
2K
  • · Replies 3 ·
Replies
3
Views
2K
Replies
3
Views
5K