The soundness and completeness of logic

[@Planetarium963]

As an expert on smurgles, I can confirm that all smurgles are flumpy.

[@AllAnglesMath]

That's good to know. If you have any evidence for your claim, feel free to share it here ;-)

[@wyattsheffield6130]

Ugh yet another showboating smurgle expert 🙄 We all know smurgology is more glamorous than flumpiness theory but you simply cannot deny that the former necessarily follows from the latter. In fact I contend that flumpiness theory is more general and descriptive than smurgology. For instance, is a smurgologist such as yourself able to describe a flumpy blorbo? Yeah I thought not.

[@yuro-h7m]

I, for one, recently visited an ancient ruins 29 km North of Glorpshire and personally witnessed a tribe of non-flumpy smurgles.

[@keeperofthelight9681]

The set of experts on smurgles is not defined

[@matthewe3813]

@@wyattsheffield6130 Smurgology elegantly defines the flump transformations of smurgles in various blorbo-space manifolds, while flumpiness theory fails to do this. It follows Smurgology thus can define all transformations of any form in a blorbo-space, including flumpy blorbos

[@pedroth3]

This is one of the best explanations on this subject. For me, it was very hard to learn it from books. Thank you!

[@MusicEngineeer]

I think, for expressions like the one appearing at 4:28, parentheses would help a lot. Apparently, the expression is supposed to mean (A, A ==> B) |- B. But my first interpretation would have been more something like (A,A) ==> (B |- B). This, of course, doesn't make any sense (...or does it? ...it could be a tautology, I guess - "Given A and A, it follows that we can conclude B from B"? ....yeahhh...that sounds like it should be true, regardless of A and B 🤣 )) and was therefore confusing. Seems like one really has to know operator precedence rules here - the typographical spacing not only doesn't help but actually leads one on to the wrong way. I also often notice this effect with expressions involving the wedge product. I often get it wrong, what operand it "binds to".

[@AllAnglesMath]

Very good point. I should have added parentheses, it would have made everything much more clear. My bad.

[@MusicEngineeer]

@@AllAnglesMath Still very high quality content though. Much thanks for creating it. I'm learning a lot here. I didn't mean to come across negative. But it is something that I noticed while watching.

[@diribigal]

You seem to have confused "incompleteness" in the sense of Goedel's Incompleteness Theorems with "incompleteness" in the sense of not having syntactic proofs of everything that is true semantically. These are two unrelated ideas that confusingly have the same name. This is why the English Wikipedia page for the incompleteness theorems has a warning at the top: "for...the correspondence between truth and provability, see Goedel's completeness theorem". His completeness theorem actually says that in a first-order system (like the standard set theory axioms ZF or ZFC), the thing you're worried about towards the end of this video *can't happen* ! Every statement that's semantically true has a "blind" syntactic proof. (So unless you're a logician working with "second-order logic" or similar, all the math you do can be done on a foundation of set theory and be complete in this sense.) Goedel's *incompleteness* theorems are about something else entirely: the question of whether every statement is provable or has its negation provable (syntactically or semantically, since those are the same by completeness). For reasonably complex first-order systems, there are unsettled questions like that, but completeness still holds, so that *if* a question is settled by semantics, it's settled by syntax, too.

[@AllAnglesMath]

Thanks for the clarifications. I should probably have done more research for this one.

[@Adhil_parammel]

"If your system can classify everything as true or false, it can't resolve every contradiction. You can't know if axioms themselves are true, false, or contradictory. This applies to God too: If God can't explain contradictions, then God's knowledge is incomplete. If God can, then God is acting illogically. Either way, there's always something unexplainable within axioms or truths. In simple terms, we can't know everything. Contradictions just shift around, never fully resolved. In math, every axiom spawns systems with contradictory paths. We extend systems to handle these contradictions, but new ones always emerge. It’s about usefulness, not absolute completeness."

[@allenliao1357]

@@AllAnglesMath I think you should fix the mistake (if u can add annotations to the video), or if not, take it down. The whole video is about A but the ending + title is about B. The error is too big to ignore, and it straight up misleads the viewer in thinking that the logical system we use in math (first order logic FOL) is incomplete. The arithmetic system + FOL may be incomplete (in a different sense of completeness), but FOL certainly is complete.

[@JohnDlugosz]

1:08 Axioms for Smurgles and Flumpiness Existence of Smurgles: There exists at least one smurgle. ∃s:s is a smurgle. Flumpiness is an Inherent Property: Every smurgle is flumpy. ∀s (s is a smurgle  ⟹  s is flumpy.) Flumpiness is Transmissible: If a smurgle interacts with a non-flumpy object, that object becomes flumpy. ∀s,x (s is a smurgle∧x is not flumpy  ⟹  x becomes flumpy after interaction.) Smurgle Union: When two smurgles interact, they form a new smurgle whose flumpiness is the sum of the original smurgles' flumpiness levels. s1+s2=s3s1​+s2​=s3​, where s3 is a smurgle, and flump(s3)=flump(s1)+flump(s2). Neutral Flumpiness: There exists a smurgle s0 with neutral flumpiness that does not change the flumpiness level of another smurgle during interaction. ∃s0:∀s (s+s0=s). Inverse Smurgle: For every smurgle ss, there exists an anti-smurgle s−1 such that their interaction results in neutral flumpiness. ∀s ∃s−1:s+s−1=s0. Flumpy Symmetry: If a smurgle has flumpiness F, then its reverse smurgle has −F, and their combined flumpiness is neutral. flump(s)+flump(s−1)=0. Flumpiness Conservation: In any closed system of smurgles, the total flumpiness is conserved. ∑flump(si)=constant.

[@rafaelgostosinho3769]

First math discovery of 2025 🎉🎉

[@se7964]

“There will always be unprovable truths” is not what incompleteness actually is. This is a common misconception. Rather, any sufficiently powerful logic system (such as first-order logic plus peano’s axioms) are possessed of a degree of expressive power sufficient enough to construct ONE single self-referential statement (the liars paradox) whose inability to be evaluated by that system imbues it with a trivial aspect of being true, but unprovable. That it no way implies other statements share this property, or that the rest of mathematics is “full of holes”, anymore than the liars paradox in colloquial speak implies our grammar is “full of holes”. Rather it simply shows we have the power of self-reference in such a language.

[@samueldeandrade8535]

Why ... ? Why did you take a reasonable statement like "There will always be unprovable truths" and make an analysis about something else? You must have some condition.

[@diribigal]

Your comment makes it sound like the only statements we have in standard math systems where they and their negation can't be proved are the ones constructed using the general self-referential trick in the proof of Goedel's incompleteness. That is very much not true. For example, you might have heard about the Continuum Hypothesis being independent of standard set theory axioms (ZFC). That would be an example of a "hole" in the sense that ZFC doesn’t pin down an answer, but there's no weird self-reference trick.

[@diribigal]

​@@samueldeandrade8535there is a precise sense in which "there will always be unprovable truths" is false in standard mathematics, as shown by Goedel's completeness theorem. I think the comment was very reasonable, if perhaps misinformed about the variety of unprovable statements in math.

[@lnm3221]

@@diribigal This is incorrect. Continuum hypothesis is neither true or false in ZFC. It can be either true or false in ZFC+some other axiom.

[@lnm3221]

@@diribigal This is incorrect. Any true statement in mathematics can be proved using sufficiently strong system of logic.

[@jamaluddin9158]

During my logic course, it was actually quite satisfying to prove that First Order Logic is both complete and sound.

[@StylishHobo]

*Gödel wants your location.*

[@jamaluddin9158]

@@StylishHobo 😅

[@hossamarafa2594]

​@@StylishHobo Gödel did it first

[@anywallsocket]

Brilliant! Yes, we need a video on decidability and the connection between Tarski, Gödel, and Turing 🙏

[@jagatiello6900]

A particularly interesting issue with logic and inference models is the 'raven paradox' by Carl Hempel. Nice video, keep them coming. Have a great 2025!

[@DanielMojoli]

Crystalline. Thank you!

[@alegian7934]

is this a series? or a standalone video? i enjoy logic :)

[@AllAnglesMath]

We will publish 3 stand-alone videos about logic, type theory, and category theory. Check out the logic playlist, where you can already watch the video about Eric Hehner's unified logic system.

[@delec9665]

Will there be any on model theory too ?

[@AllAnglesMath]

@@delec9665 Sadly, no. The "mapping things to other domains" is a first step of model theory, but I won't go any deeper.

[@MusicEngineeer]

@@AllAnglesMath Great! Looking forward to these videos! 👍 Thanks for the great content!

[@markdatko4832]

Thank you for introducing Gerhard Genzen to me

[@gershommaes902]

Amazing video.

[@EvanMildenberger]

Too bad model theory wasn't mentioned in the video although a hashtag reference is made in the description. A quotation repeated in the Wikipedia article for it says: "if proof theory is about the sacred, then model theory is about the profane" and "proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature." There is an obvious duality between proof theory (how) and model theory (what) which would be nice to explore more in a future video. Related to model theory is universal algebra, which is the generalization of abstract algebra. It helped me realize that symbolic math (in contrast to the "natural" notions of geometry and topology we experience in the physical world) mainly boils down to things (the underlying sets), one or more actions that permute those things (n-ary operations from the n-fold Cartesian product to the set), and one or more properties that each of those actions always have (associativity, identity, commutativity, etc). Abstracting over the underlying set results in a "variety" of sets with the same behaviour. Relaxing the "closure" property of being a homogenous total operation to a heterogenous partial function results in a (monoidal) category, since category theory is basically just an associative, unital algebra of the composition operation between various functions. And if all those functions in the category have inverses in a way that each morphism is an isomorphism, then it results in a groupoid, which is like if a group and finite state machine had a baby.

[@hossamarafa2594]

You misinterpreted Gödel's incompleteness theorem, for you confused the semantic completeness for the syntactic or negation completness ; you see, Godel proved that if a system S is sufficiently complicated , then S is syntacticaly incomplete ie there are sentences φ of the language of S such that neither φ nor ¬φ can be proven in S ie φ is Undecidable by the axioms of S or φ is independent of S This is different from semantic completeness, for φ is not a logic consequence of S ie S⊭φ The gödel sentence is not a logical consequence of the axioms; the relation ⊨ is not total over the wffs of S

[@EvanMildenberger]

Interestingly related to what can be proven--it seems that all paradoxes have both self-reference and negation: Russel's paradox, "this sentence is false", etc. This revelation led me down a rabbit hole with associated concepts like the open vs closed world assumptions, negation as failure, and intuitionistic logic without the law of excluded middle. There's an amazing Strange Loop programming talk by Peter Alvaro called "I See What You Mean" which discusses this source of paradoxes. Now I'm always cautious when I'm dealing with something recursive when it's not fully constructive (falsehood and contradiction are not just related to the void unconstructable initial type). Also, type theory is interesting: it seems common that things are either defined recursively like a cycle with the collection of things containing its own definitions inductively, or else it's like a chain with the things being defined in terms of a collection of higher-order things. Set theory takes the first approach with being recursively defined but that leads to issues like Russel's paradox. Type theory is like the second approach in that there is always a higher order type which can define the lower order types ad infinitum. But dependent typing allows some backwards reference from higher order referring to lower order types, which gives a best of both worlds approach: it can be circularly defined when the goal is consistency but the ability to jump to a higher universe of types allows it to avoid paradoxes.

[@MarcDonis]

Lovely video, but I would take issue with your contention that physics informs mathematics. Many branches of pure maths are deliberately divorced from any physical analog. Rather, I would argue that a system of axioms must be chosen such that it constructs a system that is free from contradiction. In other words, it must not be possible to use the axioms to prove any statement to be both true and false.

[@AllAnglesMath]

It's true that many systems of axioms are not (necessarily) informed by physics. But I would argue that logic, arithmetic, calculus, and even more abstract domains like group theory and topology are definitely inspired by their usefulness for describing the universe we live in.

[@Velereonics]

The first one is also false technically. i don't think any planets are spheres, I think the whole thing is that, in space, nothing is spherical. In space, there's no such thing as a straight line. All planets bulge, a little bit at their poles, and you would need a really specific set up to, like counteract that I i just don't think it's possible like you'd never end up with a system that the planet is spherical, even if they were made of only one element.

[@AllAnglesMath]

I should have said "All *mathematical* planets are spherical".

[@bartbroek9695]

i see some inaccuracies have been pointed out, maybe this one as well but i haven't seen it yet. it's seemingly by the same conflation of two different concepts, you say, by the end, that at least we can rest assured everything we CAN prove, is true. but that's actually unknowable, which Gödel also proved. all systems of axioms (with basic arithmetic) are either incomplete, or inconsistent, but you can't ever prove consistency (which would imply incompleteness) from within the system itself, only can you prove inconsistency by eventually finding a contradiction. it is similar to the halting problem being unsolvable, in that we could design an algorithm that would eventually prove something halts, by just running for long enough, but before you're there you don't know there will be an end, in general. i love the topic though, and i think the presentation is great, and i could learn a lot from a series about this. i have to say i don't fully understand the notation in the introduction rule of the implication, but that could very well be due to a lack of familiarity. i think you are explaining things very well, just the content you're explaining needs some touch-ups but i'm excited about the different directions you're exploring in your content. I would like to share a verse of a song i wrote: De mysteries van mijn leven Soms ben ik het even kwijt En dan denk ik het te vinden Maar dan blijkt het tot mijn spijt Een comfortabele illusie Beslisbaar en bekend Maar alles is uiteindelijk Onvolledig Of inconsistent

[@Speed8883]

3:10 you mean the group axioms are too complicated? We haven’t even gotten to rings or fields yet 😂

[@j100j]

Spheroids*

[@MaxPicAxe]

wow very good

[@dragolov]

Bravo!

[@tanvach]

Brilliant

[@DeathSugar]

Kinda weird to see all the commas and "hence" operators instead of actual conjution/disjunctions. At first i though it was an enumeration of arguments (A,A) not sequence A & A=> B

[@RensePosthumus]

I think you should be a bit more precise in the completeness part. You cannot prove it *within* the system. You can switch to a higher order system and prove it there (assuming there is consistency).

[@rickybloss8537]

Actually all planets are oblique spheroids.🤓

[@Diez145]

This is a fantastic introduction. Your explanation of semantics of logic reminds me quite a bit of the concept of Differance by the "non-math" philosopher Derrida! When you get to the foundations of mathematics/logic, there is quite a bit of overlap with continental philosophy haha.

[@Adhil_parammel]

"If your system can classify everything as true or false, it can't resolve every contradiction. You can't know if axioms themselves are true, false, or contradictory. This applies to God too: If God can't explain contradictions, then God's knowledge is incomplete. If God can, then God is acting illogically. Either way, there's always something unexplainable within axioms or truths. In simple terms, we can't know everything. Contradictions just shift around, never fully resolved. In math, every axiom spawns systems with contradictory paths. We extend systems to handle these contradictions, but new ones always emerge. It’s about usefulness, not absolute completeness."

[@ROForeverMan]

That's because form and formless are 2 sides of the same coin. See my paper How Self-Reference Builds the World, author Cosmin Visan.

[@PauloConstantino167]

prove to me that P->Q is true when P is false and Q is true

[@diribigal]

It's true by definition. You're welcome to invent your own logical connective that doesn't act like that. However, it will be something else with a simple name, as in on the list at en.wikipedia.org/wiki/Bitwise_operation#Truth_table_for_all_binary_logical_operator or similar.

[@PauloConstantino167]

@@diribigal you lie!!! why do people always lie!!!

[@diribigal]

@@PauloConstantino167 Do you think you will convince me of my error with more exclamation points? I have a ton of textbooks on logic and they seem to back me up on this. If you have something in mind that would contradict what I said (i.e. make me a liar), I'd be curious to learn what that is.

[@diribigal]

On the off chance you or someone else is interpreting "true by definition" as something like "obviously true from everyday logic", I meant the opposite. I meant that it's true by fiat by the mathematical community, and we all have to live with that fairly arbitrary decision.

[@AllAnglesMath]

@@diribigal In our video about Hehner logic, there's a strong analogy between logic and order theory. In that context, the '=>' operator is interpreted as "less than or equal to", which makes it a lot less arbitrary. But this analogy is still by fiat as you point out.

[@maynardtrendle820]

I regargus this kleb.

[@MultiversalGoat]

here

[@j4BnSPUgdu]

It is distressing to me that this video here before us today tells us we must simply accept a thing as true (Goedel's incompleteness theorem, in this case) without this video providing any pretence whatsoever of justification for this claim. We should accept a thing as true merely by fiat, just because a slick video is telling us? That sets a regrettable precedent for educational videos. That would be unremarkable if this were, for instance, a gossipy news video. But the title of this video makes it clear that it intends to be telling us something about logic. Isn't logic supposed to refrain from making claims without attempting to justify them? In fairness, the video was extremely well organized and produced. You can tell a lot of thought, work, and care went into constructing and producing it. I just wish if a video about logic isn't going to give any justification for a statement, leave it out. If you're going to make a video in the future explaining the incompleteness theorem, fine. Talk about it there. Making categorical pronouncements concerning the truth or falsity of claims with no justification is the opposite of constructing and extending the network of human knowledge: it fosters and encourages the growth of human ignorance and error. Please don't do it. Please refrain from digressing into claims about a subtopic unless you intend to offer support for the claim. Thank you for taking the time to read this.

[@kyay10]

If you want a proof, the proof exists out there. Have you ever been in a mathematics or science class before? Things are stated constantly without proof if they're well-known results. Godel's incompleteness needs its own video to explain its mechanism in detail. In fact, such videos exist already, even one by Veritasium I think that's intended for the general public. Not every video needs to regurgitate proof details when they're so well known and would deter from the greater point.

[@diribigal]

Your "justify every claim" desires puts an unreasonable bar that would make basically any video unwatchable. If you were to watch a video targeted towards primary school students about basic properties of even and odd numbers, would you require the video to justify 1+1=2 via a proof using the Peano axioms for natural numbers? Of course not. Similarly, this video is targeting people who have not learned about the basics of this stuff in a class about mathematical logic, and so it would be a digression to turn the video into, say, a many-hours-long video building up a semester's worth of material on the proofs of soundness and the incompleteness theorems. Soundness, Completeness, and Incompleteness are just about the most famous theorems in mathematical logic, and there are a ton of free readings, proofs, and videos everywhere about them.

[@j4BnSPUgdu]

@@diribigal only for videos that make it plain in the title and in the content that they're about logic. This video was almost perfect. The fact that it was so nearly perfect made the defect of introducing a new subtopic without any justification more distressing than it otherwise would have been. Less do as we say, not as we do, and more show us, give us good role models to pattern our thinking after, and less gossip and anecdotes when making videos about logic or science. I get that people want to make videos entertaining. My own preference is for less entertainment and higher quality information.

[@diribigal]

@j4BnSPUgdu I would hardly call "mentioning-without-proof a very famous theorem that basically takes a whole book to prove" gossip or anecdote, but I don't know what I can say to convince you. All I can say is that for me, the fact that the cited results are so famous as to have expositions everywhere makes the difference. And if it were some niche thing, then I'd still be fine with a video that cites a published paper for me to read on my own.

[@j4BnSPUgdu]

@@kyay10 My own copy of the incompleteness proof is well-thumbed, I assure you. It's this video I was talking about. It was experience by me a bit like a slap in the face and rather insulting to talk in a relatively rigorous manner, as this video did, about topics in logic such as soundness and completeness and then have the same video manifestly demonstrate the opposite of good logical practice. Of course this is the opinion of one person sharing a subjective reaction. One data point, and maybe not a very representative or generalizable one.