Video Rembrances of Marvin Minsky

Following are videos of my rembrances of Marvin Minsky

•  https://web.media.mit.edu/~lieber/Minsky-Stanford-Memorial/Carl%20Hewitt%20Remembers%20Marvin%20Interview.mp4

 

•  https://web.media.mit.edu/~lieber/Minsky-Stanford-Memorial/Carl%20Hewitt%20Remembers%20Marvin%20Minsky%20(2).mp4

Self-Proof of Consistency

 

Basing the development of foundations on existence of a monster can lead to serious errors. For example, the [Gödel 1931] conclusion that a theory that axiomatizes is own provability cannot prove its own consistency was based on existence of the proposition I’mUnprovable (such that I’mUnprovable ⇔⊬I’mUnprovable). However, the [Gödel 1931] construction of I’mUnprovable fails in foundations because it violates restrictions on orders for propositions.

 

Nonexistence of Gödel’s proposition I’mUnprovable opened up the question of a theory being able to prove its own consistency. [Gödel 1931] included provability axioms for Russell’s system including the following:

·  ModusPonens: ⊢(Φ⋀(Φ⇒Ψ)⊢Ψ)

·  DoubleNegation: ⊢(¬¬Ψ⊢Ψ)

 

Although not included in [Gödel 1931], the incorporations of TheoremUse {⊢( (⊢Ψ)⇒Ψ)} is fundamental to foundational theories by enabling the principle that theorems can be used in subsequent proofs. As such, TheoremUse belonged in the [Gödel 1931] axiomatization of provability for Russell’s Principia Mathematica. However, its inclusion would have made [Gödel 1931] inconsistent. Not including TheoremUse made the [Gödel 1931] axiomatization of provability fundamentally incomplete.

 

Inconsistency of a theory (¬Consistent) can be formally defined as there being a proposition Ψ₀ such that  ⊢Ψ₀∧¬Ψ₀.

 

Contra [Gödel 1931], a foundational theory can prove its own consistency as shown in the following theorem:

    Theorem. ⊢Consistent

        Proof. In order to obtain a contraction, hypothesize ¬Consistent. Consequently, there is a proposition Ψ₀ such that ⊢Ψ₀∧¬Ψ₀. By the principle of TheoremUse

{((⊢Φ)⇒Φ)} with Ψ₀ for Φ, Ψ₀∧¬Ψ₀, which is the desired contradiction.

 

However, the proof does not carry conviction that a contradiction cannot be derived because the proof is valid even if the theory is inconsistent. Consistency of the mathematical theories Actors and Ordinals is established by proving each theory has a  unique-up-to-isomorphism model with a unique isomorphism.

 

See the following for more information:

    "Epistemology Cyberattacks"
         https://papers.ssrn.com/abstract=3603021