MHB Axiomatized Formal Theory Proof

[agapito]

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.

 

[Evgeny.Makarov]

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?

 

[Evgeny.Makarov]

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.

 

[agapito]

Thank you very much.