MHB Treatment of axioms of formal axiomatic theory

AI Thread 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.
 
Thread 'Is this public key encryption?'

Thread 'Is this public key encryption?'

I've tried to intuit public key encryption but never quite managed. But this seems to wrap it up in a bow. This seems to be a very elegant way of transmitting a message publicly that only the sender and receiver can decipher. Is this how PKE works? No, it cant be. In the above case, the requester knows the target's "secret" key - because they have his ID, and therefore knows his birthdate.
View full post »

Thread 'Who is responsible for the software when AI takes over programming?'

I tried a web search "the loss of programming ", and found an article saying that all aspects of writing, developing, and testing software programs will one day all be handled through artificial intelligence. One must wonder then, who is responsible. WHO is responsible for any problems, bugs, deficiencies, or whatever malfunctions which the programs make their users endure? Things may work wrong however the "wrong" happens. AI needs to fix the problems for the users. Any way to...
View full post »

Similar threads

Is mathematics invented or discovered?
Replies
2
Views
118
A Formal axiom systems and the finite/infinite sets
Replies
10
Views
2K
A Concrete examples of randomness in math vs. probability theory
Replies
11
Views
3K
A Is irreducibility justified as a Wightman axiom?
Replies
4
Views
2K
MHB Axioms of Set Theory .... and the Union of Two Sets ....
Replies
2
Views
2K
MHB Set Theory and ZFC - The Axiom of Replacement - Searcoid, Pages 6-7
Replies
14
Views
4K
Axiomatization of quantum mechanics and physics in general ?
5
Replies
210
Views
17K
A Choices of Axiomatic and Number Systems / Sets and Alternatives
Replies
2
Views
2K
A A "Proof Formula" for all maths or formal logic?
Replies
3
Views
2K
Why is Axiom of Induction Needed as an Axiom? (Peano's Axioms)
Replies
3
Views
5K

Hot Threads

Recent Insights

Back
Top