A "Proof Formula" for all maths or formal logic?

  • Context: Graduate 
  • Thread starter Thread starter moriheru
  • Start date Start date
  • Tags Tags
    Formula Logic
Click For Summary
SUMMARY

The discussion centers on the concept of a "proof formula" that could simplify the process of proving mathematical statements by correlating them with their Gödel numbers. The participant explores the feasibility of such a formula within first-order logic and simpler formal theories, while acknowledging the complexities of different mathematical languages, such as topology and order theory. The conversation also touches on the implications of Gödel's incompleteness theorem and the potential for automated theorem proving methods, including the W-Z method and tools like Isabelle.

PREREQUISITES
  • Understanding of Gödel's incompleteness theorem
  • Familiarity with first-order logic
  • Knowledge of formal theories and axiomatic systems
  • Basic concepts of automated theorem proving
NEXT STEPS
  • Research the implications of Gödel numbers in formal logic
  • Explore the capabilities of proof assistants like Isabelle
  • Learn about the W-Z method for automated proofs
  • Investigate the relationship between different formal theories and their axioms
USEFUL FOR

Mathematicians, logicians, computer scientists, and anyone interested in the foundations of mathematics and automated theorem proving.

moriheru
Messages
273
Reaction score
16
I was wondering whether or not there could be a "master formula" . What I mean by a master formula is, maybe not even a formula, some mathematical expression that would allow mathematicians to prove statements simply by plugging in some numbers into a formula.

So I guess in a way a I am talking about a " proof formula" . To be more precise: shouldn't it be possible to find for example by interpolation, a formula that relates the validity of a theorems statement to its Gödel number. I am aware that mathematics is a vast and complicated language, but would this be possible for first order logic or other simpler formal theories .

I believe the reverse process is certainly easier though. I can easily set up a formal theory in which I choose my axioms and inference rules in such a way that for example every theorem with a Gödel number divisible by 17 and 2 is true.

I am aware that I have used the term maths in a rather loose fashion. I am no expert, but there surly is no one mathematical language. Topology may have different rules than Order theory and hence be a different formal theory. Additionally, what about the incompleteness of forma, theory such as arithmetic. Any thoughts...
 
Last edited by a moderator:
Physics news on Phys.org
I am a aware of automated proofs such as the W-Z method, but that wasn't quite the point I was trying to make or inquire upon. I was more specifically asking whether a connection can be made between the validity of a statement in a formal language and it's Gödel number and how incompleteness may effect this. Nevertheless the Isabel link was very interesting thank you!
 
You can list all valid statements in a specific order. With sufficient resources, you'll find the Gödel number of every proof of length < N for large N. How does that help?
 

Similar threads

  • · Replies 4 ·
Replies
4
Views
796
  • · Replies 40 ·
2
Replies
40
Views
8K
  • · Replies 14 ·
Replies
14
Views
4K
  • · Replies 2 ·
Replies
2
Views
2K
  • · Replies 22 ·
Replies
22
Views
3K
  • · Replies 1 ·
Replies
1
Views
3K
  • · Replies 47 ·
2
Replies
47
Views
5K
  • · Replies 24 ·
Replies
24
Views
4K
  • · Replies 6 ·
Replies
6
Views
1K
  • · Replies 16 ·
Replies
16
Views
3K