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

  • A
  • Thread starter Thread starter moriheru
  • Start date Start date
  • Tags Tags
    Formula Logic
AI Thread Summary
The discussion centers on the idea of a "proof formula" that could simplify mathematical proofs by allowing mathematicians to validate statements through a single mathematical expression related to their Gödel numbers. The possibility of such a formula is questioned, particularly in the context of first-order logic and simpler formal theories, despite the complexity of mathematics. The conversation acknowledges the ease of creating formal theories with specific axioms that yield true theorems based on their Gödel numbers. Additionally, the impact of incompleteness in formal theories, such as arithmetic, is highlighted as a significant concern. Overall, the thread explores the intersection of Gödel's incompleteness and the potential for a universal proof mechanism in mathematics.
moriheru
Messages
273
Reaction score
17
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?
 
I was reading a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema): $$\begin{align} & (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\ & (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\ & (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\ & (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\ & (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\ & (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber...

Similar threads

Replies
4
Views
190
Replies
40
Views
8K
Replies
2
Views
2K
Replies
1
Views
3K
Replies
47
Views
4K
Replies
24
Views
3K
Replies
6
Views
1K
Back
Top