This project received the highest academic distinction, (“Matrícula de Honor”), during its official evaluation.
This thesis investigates the foundations and intrinsic limits of computation and formal reasoning through an algorithmic perspective, culminating in a rigorous analysis and proof of Gödel’s First Incompleteness Theorem.
The work bridges practical programming languages with classical computation models to make deep theoretical concepts accessible through computation, formal systems, and proof structures.
Problem & Motivation
Understanding the capabilities and limitations of formal reasoning systems is central to both theoretical computer science and modern machine learning — especially where questions of expressivity, decidability, and representation arise.
This work asks:
- What does it mean for a problem to be computable?
- Can practical programming languages be treated as formal mathematical systems?
- What are the fundamental limits of proof and truth?
What I Built
- Introduced a class of SISO Python programs and demonstrated they are as expressive as general Python code.
- Established a constructive equivalence between Python programs and Turing machines, enabling the use of real codebases for formal reasoning.
- Defined and classified decidable, semidecidable, and undecidable problems using a computational lens.
- Employed self-reference and reduction techniques to explain the existence of undecidable problems, with the Halting Problem as a key example.
- Formalized concepts of proof, truth, and logical systems, connecting syntactic provability with semantic truth.
- Provided a detailed proof of Gödel’s First Incompleteness Theorem in two complementary forms (semantic and syntactic).
- Discussed broader mathematical and philosophical implications of incompleteness.
Technical Highlights
- Computation Models: Equivalence between Python and Turing machines
- Problem Theory: Formal definitions and classification of computational problems
- Logic & Proof: Formal systems, truth, and syntactic vs semantic reasoning
- Incompleteness: Dual proofs of Gödel’s First Incompleteness Theorem
Impact
This thesis demonstrates the ability to:
- Reason rigorously about abstract computational systems
- Translate formal theory into executable programs
- Communicate deep theoretical insights in a structured, reproducible manner
It reflects a blend of practical programming, formal reasoning, and systems thinking — skills that extend directly into advanced ML systems, algorithmic design, and theoretical foundations of intelligent systems.
Keywords
Theoretical computation • Turing machines • Formal logic • Decidability • Incompleteness • Python computation • Computational theory
