Skip to content

Minimal Type Theory (MTT)

Minimal Type Theory.pdf

Author peteolcottPosted on March 16, 2017March 16, 2017

Post navigation

Previous Previous post: Formalizing Self-Reference Paradox using Predicate Logic (PDF)

Next Next post: Simple English refutation of the Incompleteness Theorem

Recent Posts

Simple formal refutation of the Liar Paradox
Proof that Wittgenstein is correct about Gödel
Deductively sound formal proofs of mathematical logic
Tarski Undefinability Theorem Terse Refutation
Converting Formal Proofs to Sound Deduction
Links to Various Papers
Provable_Mendelson.pdf
Prolog already refutes the Tarski Undefinability Theorem
Eliminating Undecidability in Formal Systems
Tarski Undefinability Theorem Succinctly Refuted
Expressing Truth directly within a formal system with no need for model theory
Gödel Sentence from 1931 Incompleteness Theorem
An Introduction to Formal Languages and Automata (1990) by Peter Linz (Pages 315-320)
Sound deduction and formal proof are necessarily isomorphic
Principle of Explosion rejected by formalized semantic constraints
Liar Paradox refuted with Olcott universal Truth predicate
Liar Paradox formalized as Prolog
(error now unequivocally shown)
Halting decidability decider defined
Formal Proof defined
Gödel’s 1931 Incompleteness Theorem Refutation
Minimal Type Theory (MTT) parsed output
Sketch of Solution to the Halting Problem
Tarski 1936 Undefinability Proof Simplified
Gödel’s 1931 Incompleteness Theorem (as simple as possible)
Refutation of Rice’s Theorem
The ultimate foundation of
[a priori] Truth
Removing all extraneous complexity from the 1931 GIT
Simple refutation of the 1931 Incompleteness Theorem
Defining a Halt Decider’s Inference Chain
The Nature of Truth in Plain English
Simple English Refutation of Gödel’s 1931 Incompleteness Theorem
True(X) and ~Provable(X) is Impossible
1931 Incompleteness Theorem Refutation
Refutation of Halting Problem Proof
Terminology of Minimal Type Theory
State Transition Diagram Halting Problem Proof
Reformulating the notions of Truth and formal provability
1931 Incompleteness Theorem Refutation Strategy
Provability Predicate as simple as possible
Simple tutorial on Propositional Logic
Forming a Bridge between Proof Theory and Model Theory
Fulfilling Tarski’s ∀x True(x) ↔ φ(x)
1931 Incompleteness Theorem is only undecidable because it is not a sentence expressing Boolean
Concise Formalization of the Liar Paradox
Quick recap of the Liar Paradox Error
Refuting the conclusion of Gödel’s 1931 Incompleteness Theorem
Provability according to Mendelson
Defining Tarski’s 1933 ∀x True(x) ↔ φ(x)
Detecting and Rejecting Pathological Self-Reference (in Prolog and MTT)
Gödel’s 1931 Incompleteness Theorem summed as a single line of Minimal Type Theory
Gödel’s Proof Revised Edition Nagel, Newman, and Hofstadter (pages 96-98)
1931 Incompleteness Theorem simplified
Provability with Minimal Type Theory
Simple English refutation of the Incompleteness Theorem
Minimal Type Theory (MTT)
Formalizing Self-Reference Paradox using Predicate Logic (PDF)
Liar Paradox Proof (PDF)
Significance of the Liar Paradox