# Axiomatized Formal Theory Proof

• MHB
• agapito
In summary, the conversation discusses the proof that a Consistent and Sufficiently Strong AFT (Axiomatized Formal Theory) is not decidable. This involves Church's theorem, which shows that pure first-order predicate calculus is not decidable by encoding Turing machines and their halting behavior as formulas. Additionally, Robinson's system Q (Peano Arithmetic without induction) is also proven to be undecidable by representing computable functions in Q. These results can be found in various books such as "Sets, Logic, Computation" and "Incompleteness and Computability". The conversation also mentions the use of the diagonal argument in proving Gödel's second theorem about the incompleteness of Peano Arithmetic.
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.

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.

## 1. What is an axiomatic formal theory?

An axiomatic formal theory is a mathematical system that consists of a set of axioms, logical rules, and symbols used to represent mathematical concepts. It is a deductive system that allows for the derivation of theorems and proofs based on the given axioms and rules.

## 2. What are axioms?

Axioms are statements that are assumed to be true without needing to be proven. They serve as the building blocks of a formal theory and provide the basis for logical reasoning and deduction.

## 3. How are proofs constructed in an axiomatic formal theory?

Proofs in an axiomatic formal theory follow a strict set of rules and logical steps. They begin with the given axioms and use previously proven theorems, along with logical rules, to arrive at a conclusion. The proof is complete when the conclusion is logically derived from the axioms and rules.

## 4. Can an axiomatic formal theory have multiple sets of axioms?

Yes, an axiomatic formal theory can have multiple sets of axioms. These sets may overlap or be entirely distinct, and they can be used to prove different theorems or study different mathematical concepts within the same theory.

## 5. What is the significance of an axiomatic formal theory in mathematics?

An axiomatic formal theory provides a rigorous and systematic approach to studying mathematical concepts and proving theorems. It allows for precise definitions and logical reasoning, leading to a deeper understanding of mathematics and its applications in various fields.

Replies
1
Views
1K
Replies
11
Views
1K
Replies
1
Views
1K
Replies
3
Views
801
Replies
2
Views
2K
Replies
2
Views
1K
Replies
2
Views
672
Replies
47
Views
6K
Replies
10
Views
2K
Replies
15
Views
4K