For a long time, I used to dismiss intuitionism but more recently I've come to find it an attractive standpoint.

For one thing, you really only gain by trying to be constructive. If, in some logical system without LEM (law of excluded middle), you cannot find a proof of P without using LEM, you still have a result, namely you can prove LEM -> P. You haven't really lost anything! Furthermore, I have often been surprised just how far you can go without LEM. Very often in fact.

Finding constructive proofs can feel very much akin to removing an unnecessary dependency from a codebase. Also, even if ultimately, you do need LEM somewhere it is often possible to factor it into the "right" place in the proof rather than globally just sticking `LEM ->` at the front of the whole proof.

Lastly, though I have yet to understand this better, constructive proofs seem to be enjoy better computational properties under Curry-Howard.

maxiepoo 10 days ago [-]

Removing an unnecessary dependency is a good analogy. From a Curry-Howard perspective, intuitionistic proofs correspond to programs without side-effects, and classical proofs correspond to programs that can use continuation effects (for the unfamiliar think of a more principled version of GOTO), so in a real sense intuitionistic proofs are more direct. The double-negation translation then corresponds to implementing continuations in a pure language using continuation-passing style.

This also says why classical logic can still be useful: if I'm going to use continuations all the time, it's nicer to program with a language that supports them than to explicitly program in CPS. Pick the right language/logic for the task at hand!

gnulinux 10 days ago [-]

You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert).

Practically, intuitionistic logic has a lot of applications to computer science thanks to Curry-Howard.

Philosophically, soundness of LEM depends on where one originates the source of mathematics. If you're like Kant (or Brouwer) then LEM would make little sense since the source of mathematics, just like any other cognitive ability, is human cognition which exists independent of abstractions of the outer world. But, even without being a Platonist (like Godel) if mathematics has any sort of external source (e.g. abstracting the world or being a good abstraction of the world) then it's really hard to argue against LEM, although some epistemological arguments exist.

YorkshireSeason 10 days ago [-]

soundness of LEM depends on
where one originates the
source of mathematics

I disagree!

One of Goedel's many great contributions was the double-negation translation (later refined by others), and what it does is show that (simplifying a bit) intuitionistic logic and classical logic are equiconsistent!
In other words: any contradiction you can derive in classical logic, you can convert into a contradiction in intuitionistic logic. (The reverse direction is trivial because all intuitionistic proof principles are also classical.)

IngoBlechschmid 10 days ago [-]

> You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert).

Just wanted to chime in regarding the last sentence: There are right now ongoing efforts to eliminate any uses of LEM in algebraic geometry.

We do this not only out of academic curiosity, in order to create a more elegant setup and to be able to extract algorithms from proofs, but also to carry out a program called "relativization by internalization". The idea is that we can automatically derive some results for "relative schemes" if we have proven them for ordinary schemes without using LEM or the axiom of choice.

rntz 10 days ago [-]

This is true, but it has a problem: if you prefer constructive logic to classical because it is "finer-grained", then where do you stop?

Linear logic, for example, is finer-grained than both classical and constructive logic. Both can be embedded in it (just as classical embeds into constructive), and it makes distinctions they lack. But linear logic, too, comes in classical and intuitionistic versions, and again classical linear logic embeds into intuitionistic.

And it doesn't stop there. Linear logic can be embedded in ordered logic, and ordered logic into the logic of bunched implications. For all I know there are even finer-grained logics out there.

But doing all of mathematics in the logic of bunched implications would be an impractical nightmare, I think. I tend to prefer choosing whether to work classically or constructive (or linearly, or orderedly) according to whether it illuminates a relevant part of the problem. Sometimes you care about constructivity; sometimes you don't. If you don't, then don't waste your time trying to do the proof constructively.

The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! :)

danharaj 10 days ago [-]

> classical linear logic embeds into intuitionistic.

Wait, really? As I understand it there are things provable in LL that can't be proved in ILL. Can't find the citation though.

It should be noted that double negation translations are more complicated at the proof level even though they capture provability.

enriquto 10 days ago [-]

> The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it!

This sounds more like a motivation than like a trouble.

danbruc 10 days ago [-]

What exactly is the claim here with regard to the law of excluded middle? Maybe somewhat naively it seems rather obvious to me that the law of excluded middle can be true or false depending on what objects you are dealing with. Maybe not the best possible example but in classical mechanics a particle is either inside a region R or it is not inside region R while in quantum mechanics the particle may be inside region R or it may not be inside region R or it may be somewhat inside region R.

It seems rather obvious that the logic you are using has to match the behavior of the objects you are applying the logic to or you will of course end up with wrong conclusions. If we change the example a bit, the particle is in region R with probability zero or the particle is in region R with a probability larger than zero, then we again have a case where the set of possibilities is nicely partitioned into two mutually exclusive and exhaustive sets, probability zero and probability not zero. But I guess I am missing something or there wouldn't be a lot of smart people fighting over the issue.

ratmice 10 days ago [-]

I believe there are a couple of different claims being made in the above, I went ahead and just made a gist with some proofs (in lean) that try and hit some of the points about usage of law of excluded middle, double negation translation

Thanks for the effort but unfortunately for me the page just says running and nothing ever happens, especially no output at all. Not even for the small example included by default.

But besides that I did not really want to make any claims and certainly nothing that could be easily addressed by a proof, I think. My point was more that one has to take care that the type of logic one uses has to fit together with the domain one wants to reason about with that logic. If in the domain you want to reason about the law of excluded middle does not hold or only does so in a non-straight forward way, then using a logic with law of excluded middle will at least be not as easy as it could be or even painful or in the worst case lead to wrong conclusions.

ratmice 10 days ago [-]

personally, I will generally just want to construct some artifact which has some property, e.g. the proof is a program to construct something. Where a classical proof doesn't give you this program, it merely states that such a property holds. Which is perfectly fine if that is what you want to know.

protonfish 10 days ago [-]

This is fascinating, but only if you hold faith in inherent truth of mathematical symbolism. Unfortunately, this seems to be the standard dogma of mathematicians, though I haven't seen significant evidence necessary to warrant this belief.

If you understand mathematics and logic as merely a formalized language of symbols then you can judge those systems on certain qualities (complexity, clarity, expressiveness, etc.) but not "truth." The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.

jrochkind1 10 days ago [-]

Of course, the reason we invest so much in mathematics is because it is somewhat mysteriously effective for describing the observed world, not just because it's an arbitrary formalized language of symbols.

> The first point is that mathematical concepts turn up in entirely unexpected connections. Moreover, they often permit an unexpectedly close and accurate description of the phenomena in these connections. Secondly, just because of this circumstance, and because we do not understand the reasons of their usefulness, we cannot know whether a theory formulated in terms of mathematical concepts is uniquely appropriate. We are in a position similar to that of a man who was provided with a bunch of keys and who, having to open several doors in succession, always hit on the right key on the first or second trial. He became skeptical concerning the uniqueness of the coordination between keys and doors.

> Most of what will be said on these questions will not be new; it has probably occurred to most scientists in one form or another. My principal aim is to illuminate it from several sides. The first point is that the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and that there is no rational explanation for it. Second, it is just this uncanny usefulness of mathematical concepts that raises the question of the uniqueness of our physical theories.

(The article happens to mention the Brouwer-Hilbert controversy but only in a footnote).

protonfish 10 days ago [-]

That essay is a significant source of belief in the myth of inherent mathematical truth, but it has flaws and is far from proof. It focuses on cherry-picked phenomena that are easily represented by simple math, but ignores those where math struggles or appears to be inherently incapable.

Most importantly, the leap that if a medium can be used to create accurate representations, it must contain inherent, unquestioning truth about that represented phenomena, is just hogwash. Michelangelo could sculpt masterful representations of the human form, but the beauty and accuracy of the representation are the products of a skilled master, not the inherent humanness of marble.

jrochkind1 10 days ago [-]

I don't think the essay is any kind of "proof", but I think you are under-appreciating the mysteriousness it speaks of.

It's not just the medium _can_ be used to create accurate representations, by a skilled master. It's that mathematical concepts created with no regard for the natural world but purely on their formal elegance, turn out, years later, to be an elegant way to describe and predict natural phenomena.

I don't think it "proves" anything, it's just... mysterious. The mystery doesn't go away if we insist that math is just an arbitrary human invented formal system. There's no a priori reason it should work to describe and predict the natural world at all, is there?

We could invent other arbitrary formal systems based on completely different axioms and rules that _weren't_ useful to describe and predict the natural world at all, could't we? I think?

protonfish 10 days ago [-]

I guess I just don't see any mystery. We've used a language of symbols to communicate and think about the world around us since language first evolved. That fact that it works well should come as no surprise to anyone. Especially since we use a language of symbols to discuss the language of symbols so things that don't fit neatly into that system are inherently undiscussable.

BeetleB 10 days ago [-]

>That essay is a significant source of belief in the myth of inherent mathematical truth, but it has flaws and is far from proof.

I don't know where this characterization of "proof" comes from. It is merely an essay, and not intended as anything other than one. When I read it years ago, I did not get the sense that Wigner was asserting inherent mathematical truth.

>It focuses on cherry-picked phenomena that are easily represented by simple math, but ignores those where math struggles or appears to be inherently incapable.

Does he assert anywhere that any phenomenon will yield easily to mathematics? I don't think so. I think his point is that there's no good reason that even the phenomena that are well explained by mathematics should yield so easily to it. It's not "All of nature is surprisingly mathematical." It's "I see no good reason that a lot of phenomena is mathematical."

I'm too lazy to reread the essay, so I may be remembering it wrong.

forkandwait 10 days ago [-]

> Of course, the reason we invest so much in mathematics is because it is somewhat mysteriously effective for describing the observed world.

Any particular "arbitrary formalized language of symbols" is validated by experiment, either explicitly or implicitly. Humanity/ culture keeps the string games that works and jettison the ones that don't; it is a slow, collaborative process. We have worked out a pretty good "arbitrary formalized language of symbols", but not because we derived these string games or intuited them, but rather because we test them daily.

To be a formalist doesn't imply that a person under-appreciates the mysterious power of mathematics, just that they don't believe in an underlying psuedo-Kantian "truth".

Also, as I understand it, advanced physics is necessarily done formally only, since our intuition is so ridiculous at the atomic scale and all the equations like Schrodingers are only postulated, then verified empirically.

Also, it is snarky and under-informed, but I think of this debate as Hilbert (Hilbert!) and Some Guy.

canhascodez 10 days ago [-]

There is no one thing called "truth". There are different systems of verification, which produce truths, but "1 + 1" is not comparable to "water boils at 100 degrees C". Mathematics fundamentally does not describe the real world. It models the real world--and many other worlds besides. Mathematical truths describe axiomatic systems. The properties of the real world are determined not by mathematics, but by measurement.

> The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.

This is usually called "physics".

dwohnitmok 10 days ago [-]

I dunno if I'd call it dogma. For the most part, most working mathematicians I've run into basically don't care either way and adaptively adopt whichever philosophy happens to match best with their intuition for a particular problem. This can change on a problem by problem basis. I wouldn't be surprised if a working mathematician hadn't heard of intuitionism or formalism.

Interestingly, your latter point is exactly formalism (the "formal" part is referring to the formalized language), i.e. Hilbert's position. Formalism basically asserts that mathematics is a fancy string manipulation game.

popnroll 10 days ago [-]

I'm really clueless about logic and mathematics theory, but isn't this the Gödel's incompleteness theorem?

undershirt 10 days ago [-]

The struggle is that the symbolic graphs we construct to explain facts become logical beasts of their own, prone to generating sentences paradoxical under our desired interpretation.

Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another.

But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning.

Gödel seems very much related to this, but I'm still lost.

cyphar 10 days ago [-]

No, this is more about the philosophy of mathematics -- the question of "to which degree is mathematics 'real'?" Gödel did have an impact on this, with formalism no longer being a particularly viable viewpoint. But this is less of a strict mathematical question and more of a philosophical one.

protonfish 10 days ago [-]

No, the incompleteness theorem only examines how formal systems relate to themselves, not to reality. It shows that no significantly expressive system can be designed that won't allow paradoxical statements.

TheRealPomax 10 days ago [-]

Unprovable statements. Not paradoxical statements. Paradoxes confound the reader, but can be explained as either being true or false due to rules that were implicitly used to construct the statement. Once all the steps are explicitly shown, with each rule that applies at each step, there is no more paradox.

On the other hand, unprovable statements never make it to the "but can be explained" stage: either the formal system is consistent, and these expressions by definition cannot have an answer, or they can be answered but the formal system is demonstrably inconsistent.

The formal system also needs to be a little more precise than "significantly expressive": it needs to allow for self-referential expressions. In effect, it must be possible to create an expression that can be mapped to the natural language sentence "This statement has no proof in this formal system".

While in natural language puzzles that might be a fun paradox to try to figure out, where the challenge is to determine whether, given the rules of the context, the answer is actually "true" or "false", when it comes to Godel sentences for formal systems there is never a paradox. Either they are undecidable, or the formal system is inconsistent. And we don't get an "out" by saying "but in reality, the answer is ..." because the whole point of formal systems is to be self-contained. There is nothing "outside" of them that we can use to make claims about expressions within that formal system. We only get the axioms of the formal system itself.

mietek 10 days ago [-]

> It shows that no significantly expressive system can be designed that won't allow paradoxical statements.

The above is a complete misrepresentation of Gödel’s second incompleteness theorem.

The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means.

Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8].

All of these languages are designed to be consistent. Of course, implementation bugs do happen[9].

If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11].

I like your paraphrase but I think it muddies the water. We really want to prove that axioms of a system cannot be contradicted if the system is inconsistent.

To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T.

So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system.

In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.

User23 10 days ago [-]

The invention of computing automata and the techniques required to program them, such as defining semantics, settles this issue concretely in favor of Hilbert.

joel_ms 10 days ago [-]

How so? I've always felt that intuitionism/constructivism were closer to theoretical computer science due to constructivism requiring you to produce (or compute) the what you're trying to prove.

The state space is far too large to show a program is correct by constructing all possible processes it could execute. Instead you must show that the program admits no incorrect processes whatsoever, and as far as I know mathematical formalism is the only possible way to do that.

Of course if one just wants to make money, formal correctness is observably of absolutely no importance. And there's nothing wrong with wanting to make money!

Firadeoclus 9 days ago [-]

From Wikipedia:
> Brouwer the intuitionist in particular objected to the use of the Law of Excluded Middle over infinite sets

It always seems to me that using the LEM over infinite sets is akin to claiming that all problems are decidable.

For one thing, you really only gain by trying to be constructive. If, in some logical system without LEM (law of excluded middle), you cannot find a proof of P without using LEM, you still have a result, namely you can prove LEM -> P. You haven't really lost anything! Furthermore, I have often been surprised just how far you can go without LEM. Very often in fact.

Finding constructive proofs can feel very much akin to removing an unnecessary dependency from a codebase. Also, even if ultimately, you do need LEM somewhere it is often possible to factor it into the "right" place in the proof rather than globally just sticking `LEM ->` at the front of the whole proof.

Also, if you care about, first order logic then in fact you should love intuintionistic logic: it is a finer logic that actually contains first order logic: https://en.wikipedia.org/wiki/Double-negation_translation

Lastly, though I have yet to understand this better, constructive proofs seem to be enjoy better computational properties under Curry-Howard.

This also says why classical logic can still be useful: if I'm going to use continuations all the time, it's nicer to program with a language that supports them than to explicitly program in CPS. Pick the right language/logic for the task at hand!

Practically, intuitionistic logic has a lot of applications to computer science thanks to Curry-Howard.

Philosophically, soundness of LEM depends on where one originates the source of mathematics. If you're like Kant (or Brouwer) then LEM would make little sense since the source of mathematics, just like any other cognitive ability, is human cognition which exists independent of abstractions of the outer world. But, even without being a Platonist (like Godel) if mathematics has any sort of external source (e.g. abstracting the world or being a good abstraction of the world) then it's really hard to argue against LEM, although some epistemological arguments exist.

One of Goedel's many great contributions was the double-negation translation (later refined by others), and what it does is show that (simplifying a bit) intuitionistic logic and classical logic are

equiconsistent! In other words: any contradiction you can derive in classical logic, you can convert into a contradiction in intuitionistic logic. (The reverse direction is trivial because all intuitionistic proof principles are also classical.)Just wanted to chime in regarding the last sentence: There are right now ongoing efforts to eliminate any uses of LEM in algebraic geometry.

We do this not only out of academic curiosity, in order to create a more elegant setup and to be able to extract algorithms from proofs, but also to carry out a program called "relativization by internalization". The idea is that we can automatically derive some results for "relative schemes" if we have proven them for ordinary schemes without using LEM or the axiom of choice.

Linear logic, for example, is finer-grained than both classical and constructive logic. Both can be embedded in it (just as classical embeds into constructive), and it makes distinctions they lack. But linear logic, too, comes in classical and intuitionistic versions, and again classical linear logic embeds into intuitionistic.

And it doesn't stop there. Linear logic can be embedded in ordered logic, and ordered logic into the logic of bunched implications. For all I know there are even finer-grained logics out there.

But doing all of mathematics in the logic of bunched implications would be an impractical nightmare, I think. I tend to prefer choosing whether to work classically or constructive (or linearly, or orderedly) according to whether it illuminates a relevant part of the problem. Sometimes you care about constructivity; sometimes you don't. If you don't, then don't waste your time trying to do the proof constructively.

The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! :)

Wait, really? As I understand it there are things provable in LL that can't be proved in ILL. Can't find the citation though.

It should be noted that double negation translations are more complicated at the proof level even though they capture provability.

This sounds more like a motivation than like a trouble.

It seems rather obvious that the logic you are using has to match the behavior of the objects you are applying the logic to or you will of course end up with wrong conclusions. If we change the example a bit, the particle is in region R with probability zero or the particle is in region R with a probability larger than zero, then we again have a case where the set of possibilities is nicely partitioned into two mutually exclusive and exhaustive sets, probability zero and probability not zero. But I guess I am missing something or there wouldn't be a lot of smart people fighting over the issue.

you should be able to copy/paste it into https://leanprover.github.io/live/latest/

https://gist.github.com/ratmice/21f069b5811d1c40911850cb690a...

But besides that I did not really want to make any claims and certainly nothing that could be easily addressed by a proof, I think. My point was more that one has to take care that the type of logic one uses has to fit together with the domain one wants to reason about with that logic. If in the domain you want to reason about the law of excluded middle does not hold or only does so in a non-straight forward way, then using a logic with law of excluded middle will at least be not as easy as it could be or even painful or in the worst case lead to wrong conclusions.

If you understand mathematics and logic as merely a formalized language of symbols then you can judge those systems on certain qualities (complexity, clarity, expressiveness, etc.) but not "truth." The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.

"The Unreasonable Effectiveness of Mathematics in the Natural Sciences" by Eugene Wigner https://www.dartmouth.edu/~matc/MathDrama/reading/Wigner.htm...

> The first point is that mathematical concepts turn up in entirely unexpected connections. Moreover, they often permit an unexpectedly close and accurate description of the phenomena in these connections. Secondly, just because of this circumstance, and because we do not understand the reasons of their usefulness, we cannot know whether a theory formulated in terms of mathematical concepts is uniquely appropriate. We are in a position similar to that of a man who was provided with a bunch of keys and who, having to open several doors in succession, always hit on the right key on the first or second trial. He became skeptical concerning the uniqueness of the coordination between keys and doors.

> Most of what will be said on these questions will not be new; it has probably occurred to most scientists in one form or another. My principal aim is to illuminate it from several sides. The first point is that the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and that there is no rational explanation for it. Second, it is just this uncanny usefulness of mathematical concepts that raises the question of the uniqueness of our physical theories.

(The article happens to mention the Brouwer-Hilbert controversy but only in a footnote).

Most importantly, the leap that if a medium can be used to create accurate representations, it must contain inherent, unquestioning truth about that represented phenomena, is just hogwash. Michelangelo could sculpt masterful representations of the human form, but the beauty and accuracy of the representation are the products of a skilled master, not the inherent humanness of marble.

It's not just the medium _can_ be used to create accurate representations, by a skilled master. It's that mathematical concepts created with no regard for the natural world but purely on their formal elegance, turn out, years later, to be an elegant way to describe and predict natural phenomena.

I don't think it "proves" anything, it's just... mysterious. The mystery doesn't go away if we insist that math is just an arbitrary human invented formal system. There's no a priori reason it should work to describe and predict the natural world at all, is there?

We could invent other arbitrary formal systems based on completely different axioms and rules that _weren't_ useful to describe and predict the natural world at all, could't we? I think?

I don't know where this characterization of "proof" comes from. It is merely an essay, and not intended as anything other than one. When I read it years ago, I did not get the sense that Wigner was asserting inherent mathematical truth.

>It focuses on cherry-picked phenomena that are easily represented by simple math, but ignores those where math struggles or appears to be inherently incapable.

Does he assert anywhere that any phenomenon will yield easily to mathematics? I don't think so. I think his point is that there's no good reason that even the phenomena that are well explained by mathematics should yield so easily to it. It's not "All of nature is surprisingly mathematical." It's "I see no good reason that a lot of phenomena is mathematical."

I'm too lazy to reread the essay, so I may be remembering it wrong.

Any

particular"arbitrary formalized language of symbols" is validated by experiment, either explicitly or implicitly. Humanity/ culture keeps the string games that works and jettison the ones that don't; it is a slow, collaborative process. We have worked out a pretty good "arbitrary formalized language of symbols", but not because we derived these string games or intuited them, but rather because we test them daily.To be a formalist doesn't imply that a person under-appreciates the mysterious power of mathematics, just that they don't believe in an underlying psuedo-Kantian "truth".

Also, as I understand it, advanced physics is necessarily done formally only, since our intuition is so ridiculous at the atomic scale and all the equations like Schrodingers are only postulated, then verified empirically.

Also, it is snarky and under-informed, but I think of this debate as Hilbert (Hilbert!) and Some Guy.

modelsthe real world--and many other worlds besides. Mathematical truths describe axiomatic systems. The properties of the real world are determined not by mathematics, but by measurement.> The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.

This is usually called "physics".

Interestingly, your latter point is exactly formalism (the "formal" part is referring to the formalized language), i.e. Hilbert's position. Formalism basically asserts that mathematics is a fancy string manipulation game.

Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another.

But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning.

Gödel seems very much related to this, but I'm still lost.

On the other hand, unprovable statements never make it to the "but can be explained" stage: either the formal system is consistent, and these expressions by definition cannot have an answer, or they can be answered but the formal system is demonstrably inconsistent.

The formal system also needs to be a little more precise than "significantly expressive": it needs to allow for self-referential expressions. In effect, it must be possible to create an expression that can be mapped to the natural language sentence "This statement has no proof in this formal system".

While in natural language puzzles that might be a fun paradox to try to figure out, where the challenge is to determine whether, given the rules of the context, the answer is actually "true" or "false", when it comes to Godel sentences for formal systems there is never a paradox. Either they are undecidable, or the formal system is inconsistent. And we don't get an "out" by saying "but in reality, the answer is ..." because the whole point of formal systems is to be self-contained. There is nothing "outside" of them that we can use to make claims about expressions within that formal system. We only get the axioms of the formal system itself.

> It shows that no significantly expressive system can be designed that won't allow paradoxical statements.The above is a complete misrepresentation of Gödel’s second incompleteness theorem.

The theorem holds for any

sufficiently expressivesystem, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressiveconsistentsystem canprove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means.Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8].

All of these languages are designed to be consistent. Of course, implementation bugs do happen[9].

If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11].

[1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co...

[2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...

[3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type

[4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming

[5] Agda programming language, http://agda.readthedocs.io

[6] Coq proof assistant, http://coq.inria.fr

[7] Idris programming language, http://www.idris-lang.org

[8] Lean theorem prover, http://leanprover.github.io

[9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408

[10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer

[11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming

To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T.

So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system.

In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.

The state space is far too large to show a program is correct by constructing all possible processes it could execute. Instead you must show that the program admits no incorrect processes whatsoever, and as far as I know mathematical formalism is the only possible way to do that.

Of course if one just wants to make money, formal correctness is observably of absolutely no importance. And there's nothing wrong with wanting to make money!

It always seems to me that using the LEM over infinite sets is akin to claiming that all problems are decidable.