MHB Axiomatized Formal Theory Proof

  • Thread starter Thread starter agapito
  • Start date Start date
  • Tags Tags
    Proof Theory
AI Thread Summary
The discussion centers around the undecidability of a Consistent and Sufficiently Strong Axiomatized Formal Theory (AFT), with references to the Diagonal Argument and its application. Participants clarify that AFT refers to Axiomatized Formal Theory and emphasize the importance of formal proofs, particularly those verified by proof assistants like Coq and Isabelle. Key points include Church's theorem, which establishes that pure first-order predicate calculus is undecidable by demonstrating that Turing machines can be encoded within it, and the undecidability of Robinson's system Q, which shows that computable functions can be represented in Q. The diagonal argument is highlighted as crucial for proving Gödel's second theorem regarding the incompleteness of Peano Arithmetic. Recommended resources for further reading include the Open Logic Project books and "Computability and Logic" by Boolos et al.
agapito
Messages
46
Reaction score
0
Can someone please direct me to ,or show, a proof that a Consistent and Sufficiently Strong AFT is not decidable. It presumably involves the Diagonal Argument, but I can't figure out how to apply it.

Many thanks.
 
Technology news on Phys.org
What is AFT?

Also, "formal" in the context of proof lately means proofs that have been verified by a computer program (proof assistant, such as Coq, Isabelle, Agda and so on). Do you have a formalized proof in mind or simply a proof from a textbook?
 
I realized that AFT stands for Axiomatized Formal Theory.

There is Church's theorem that says that pure first-order predicate calculus is not decidable. This is proved by showing that Turing machines can be encoded in predicate calculus and the fact that a machine halts can be expresses as a formula. There is also a theorem that Robinson's system $Q$ (Peano Arithmetic without induction) is undecidable. This is proved by showing that computable functions are representable in $Q$. Again, for each machine and input there exists a formula saying that the machine halts on that input, and the machine indeed halts iff that formula is provable.

These two results can be found, for example, in the Open Logic Project books "Sets, Logic, Computation" and "Incompleteness and Computability". Another comprehensive book that deals with this is Computability and Logic by Boolos et al.

The diagonal argument is used, in particular, in the proof of second Gödel's theorem about incompleteness of Peano Arithmetic.
 
Thank you very much.
 
Thread 'Star maps using Blender'
Blender just recently dropped a new version, 4.5(with 5.0 on the horizon), and within it was a new feature for which I immediately thought of a use for. The new feature was a .csv importer for Geometry nodes. Geometry nodes are a method of modelling that uses a node tree to create 3D models which offers more flexibility than straight modeling does. The .csv importer node allows you to bring in a .csv file and use the data in it to control aspects of your model. So for example, if you...
Back
Top