Proof of an imbecile doctrine

[godelian]

The Curry-Howard correspondence is provable. What you say, is not provable. What is the point in saying unprovable things about proof?

I like the Moe Howard-Curly correspondence better - nyuk nyuk nyuk

-Imp

ChatGPT: A proof is a program and a program is a proof.

You're referencing the Curry-Howard Correspondence, a deep connection between logic and computation. This principle states that:

Proofs in logic correspond to programs in a programming language.

Logical propositions correspond to types in a type system.

Breaking it down:

1. A proof is a program

In constructive logic, proving a proposition means providing an explicit witness or construction of it.

In programming, writing a function of a given type is like proving a theorem: the function is the proof.

2. A program is a proof

If a program has a certain type, it can be seen as evidence that the corresponding proposition is true.

Type-checking ensures that programs correspond to valid proofs.

Example:

Consider the simple logical statement:

A → B

In logic, this means “if we have A, we can derive B.”

In programming, this is a function type A → B, meaning a function that takes an argument of type A and returns a value of type B.

Writing such a function is like proving the logical implication.

This idea is fundamental in dependently typed programming languages like Agda, Coq, and Idris, where proving theorems is the same as writing programs.

Are you interested in a particular application of this idea, like functional programming or proof assistants?

[Skepdick]

You only say that because you do not understand what the term "proof" means.

A proof is a program and a program is a proof:

https://en.m.wikipedia.org/wiki/Curry%E ... espondence

Curry–Howard correspondence

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

For somebody railing so hard against the Trinity, you sure are making great use of Computational Trinitarianism (the Curry-Howard-Lambek correspondence)

https://existentialtype.wordpress.com/2 ... y-trinity/

The Christian doctrine of trinitarianism states that there is one God that is manifest in three persons, the Father, the Son, and the Holy Spirit, who together form the Holy Trinity. The doctrine of computational trinitarianism holds that computation manifests itself in three forms: proofs of propositions, programs of a type, and mappings between structures. These three aspects give rise to three sects of worship: Logic, which gives primacy to proofs and propositions; Languages, which gives primacy to programs and types; Categories, which gives primacy to mappings and structures. The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.

And if you are ready to break your obsession with Godel's work just watch this video: https://youtu.be/Jo1TbN0M3xc?si=Xbo2uineWGzcBidX

[godelian]

And if you are ready to break your obsession with Godel's work just watch this video: https://youtu.be/Jo1TbN0M3xc?si=Xbo2uineWGzcBidX

In the video, Graham Priest proposes a genius construction: a model of arithmetic that is complete but beyond a chosen (large) number, inconsistent.

I have tried to Google for more details on the construction of this model but I couldn't find anything. It is "collapsed" or so.

Priest somewhat explains how it all fits together but the ten minutes in which he elaborates on it, are in my opinion not enough to completely elucidate how it works.

In fact, Priest is very compatible with Godel's work, which says:

Arithmetic is inconsistent or incomplete.

The more standard mainstream narrative is, however:

If arithmetic is consistent then it is incomplete.

The mainstream phrasing reflects the unwillingness to contemplate the idea that arithmetic could actually be inconsistent. This view reflects some wishful thinking.

The proof is completely neutral, however, and does not even particularly favor this view. There is nothing wrong with the idea that arithmetic could be inconsistent. In this context, there is no reason whatsoever to eliminate this possibility. In conjunction with paraconsistent logic, (controlled) inconsistent arithmetic could indeed yield some interesting results.

Paraconsistent logic allows for inconsistency but strictly controls its explosion. Without such strict control, it would be unusable. That is not the same as allowing arbitrary contradictions.

[Skepdick]

Paraconsistent logic allows for inconsistency but strictly controls its explosion.

That's the whole point. No consistent system of logic has explosion-management - e.g exception handling - because there are no exceptions in a consistent system of logic.

Without such strict control, it would be unusable.

Which is why all consistent logics are computationally vacuous - they contain no information. Any axiom-negation == False. No way to reject axioms.

not(P and not-P) is always False?!?! Well, what if it's sometimes true?

In fact, a complete system of logic must be able to handle precisely that! To make the statement not(P and not-P) decidable; and not just axiomatically false.

[Skepdick]

And if you are ready to break your obsession with Godel's work just watch this video: https://youtu.be/Jo1TbN0M3xc?si=Xbo2uineWGzcBidX

In the video, Graham Priest proposes a genius construction: a model of arithmetic that is complete but beyond a chosen (large) number, inconsistent.

I have tried to Google for more details on the construction of this model but I couldn't find anything. It is "collapsed" or so.

He's talking about these sort of systems

https://en.wikipedia.org/wiki/List_of_l ... properties

which are significantly stronger than your usual 2nd order arithmetic.

https://en.wikipedia.org/wiki/Reverse_m ... arithmetic