2

This could just be a lack of understanding on my part as I have never really properly learnt first order logic. If that is the case, then please let me know and I will delete the question. I will lead this question with an example, but that is not the focus of the question. This question will probably sound really convoluted, but I hope you read through it.


My question is, how do we know all the things that we use in writing proofs to be true. For example, do we have to prove that a proof by contradiction is a proof? How do we know for sure that if we arrive at a contradiction then our hypothesis must be false and the negation of that hypothesis must be true then? The part that the hypothesis makes sense but the part that the negation must be true is bit hard to accept.

What I am trying to get at is: Do we just use these techniques because we think that they should hold or do we have to prove that these techniques work and are true all the time?

A more familiar phrasing is how one might believe that the Collatz conjecture holds for every natural number because they tried it for a lot of numbers, but proving it holds for every natural number is a different thing. Is this is what is going on with the things that we students are taught? Another example is: Proving a statement by proving its contrapositive. It makes sense morally that this should be true, but can we prove that always proves the statement?

I am assuming this might have something to do with proof theory(although I know nothing about this) as I keep saying the word proof but I don't have a definition of what is a proof.

So my question is: Do we have to prove all the things we use to write proofs or are those things just taken for granted?

Seeker
  • 129
  • 2
  • 2
    How can you prove philosophically that the rules for constructing proofs are valid? To do so would require a proof, which would implicitly require you to accept the very rules you’re attempting to prove are valid. We can prove within ZF that the rules of first-order logic only prove true statements. But to do so requires us to use ZF, which is itself a first-order theory. So there is some fundamental philosophical circularity here. There’s also a dispute among mathematicians over whether proof by contradiction is valid, though most modern mathematicians use it without qualms. –  Oct 01 '22 at 23:45
  • @MarkSaving I see.I didn't consider the circularity of proving that something proves another thing that much. Are there any resources you could point to for any further readings in this area? –  Oct 01 '22 at 23:50
  • Perhaps I should rephrase it. You ask how we know things we prove are actually true. I could potentially prove this to you, but unless you accept that the things I prove are true, the fact that I proved “things we prove are true” does not actually mean that “things we prove are true” is true. –  Oct 02 '22 at 00:14
  • 1
    Disclaimer that I'm just an interested applied mathematician, hence why this is a comment. But logic is in a way it's own "mathematics" in that we first find some way of defining statements/propositions. We then define relationships between them such as what does it mean for $A$ and $B$ to be true? Or what would we like to define $A\to B$ to mean. Then we see what we can do. Under one set of assumptions the contrapositive may be "equal" to the implication. In others perhaps not. The question then becomes a question of philosophy: Which system of logic would we like to apply to our math? –  Oct 02 '22 at 02:07
  • @MarkSaving Proof by contradiction is too important to omit it ! Have the mathematicians denying it any good reason for this ? –  Oct 02 '22 at 13:47
  • Concerning Collatz : Surely , this has been checked upto extremely high limits (the exact current record is irrelevant here) , but that never can be a proof because infinite numbers would have to be checked. So we need other approaches , and noone has the slightest idea how it might work. We have however indications that the collatz conjecture has a good chance to be true. –  Oct 02 '22 at 13:51
  • 1
    @Peter Some schools of thought dislike proof by contradiction for the following reason: Consider the statement "this statement is false". If we assume this statement is false, we can show that this statement is not false. Does that mean it is true? Intuitively we say no. Ok so what gives? Maybe, some say, all we have to do is disallow self-referential statements. But, others argue, could there not be other reasons that some statements are similarly disallowable--admiting neither a natural interpretation as true or false? If we think this might be the case, then we should reject PbC. –  Oct 02 '22 at 16:29
  • 1
    The basic methods of proof are nothing new. They have been applied successfully across cultures in just about every field of human endeavour for centuries (millennia?). No inconsistencies have been found in them in all that time. Bottom line: To proceed with confidence, we do not need formal proof that these methods are themselves "true." – Dan Christensen Oct 02 '22 at 18:07
  • Your question really seems (to me) to be more about epistemology (how do we know?) and ontology (what is nature of reality?). I do not think that this is really a question of mathematics... –  Oct 02 '22 at 20:40
  • 1
    Logic used in math often uses Hilbert form which has axioms such as (¬q→¬p)→(p→q) (P4) with only one proof rule aka Modus Ponens, most will regard them as true except constructivists. Thus once you've completely understood Hilbert calculus you'll be confident at the logic level. Then further for mathematical theories you need other axiomatic theories such as set theory, but you can also use 2nd order PA subsystem such as powerful ACA0 to prove most theorems such as Bolzano–Weierstrass theorem in analysis. As for provability the famous Löb's theorem proves PA can only prove true propositions... – Double Knot Oct 03 '22 at 03:58
  • @Mark: Why mention ZF when it is a complete red herring? Also, although it is impossible to non-circularly *mathematically justify* classical FOL, there is no circularity in observing that the real world obeys classical FOL completely. Of course, using this as a basis for accepting classical FOL implies that you cannot justify ZF because it has no real-world meaning. – user21820 Oct 03 '22 at 09:54
  • If I understand, you’re asking about basic principles of logic used in proofs. They are for the most part taken as common sense. Weird theories would arise if we held that statements could be both true and false. There are differences in how people define common sense; for example intuitionism sees proofs differently than classical math. But there are some things that every sane person takes for granted, such as if something’s true then it’s true. I’m sure you hold such assumptions too. You imply that proving something logically makes it more reasonable, which can’t be proven non-circularly. – pastel_questions Oct 03 '22 at 16:53

2 Answers2

3

Your question is essentially about the epistemology of mathematics. How do we know that mathematical propositions are true? This in turn depends on the metaphysics of mathematics. What is it that makes mathematical propositions true, if they are indeed true?

These are fundamental questions in the philosophy of mathematics and there is a considerable literature on them. The philpapers website has an entire section on the epistemology of mathematics. The question also relates to fundamental issues about a priori knowledge, phenomenology, analyticity, rational intuition and experience and the interplay between them. Also, if we regard mathematical propositions as necessarily true, then it raises the familiar issue of the epistemology of modality. How do we have knowledge of modal propositions? Since, as Kant put it, experience can teach us that something is thus and so, but not that it must be.

When you ask specifically about methods of proof, and how we know they work correctly, then the question becomes one of the epistemology of logic itself. A great deal has been written about whether it is possible to justify deductive logic, and if so how.

I suggest taking a look at Conifold's answers to these questions:

and my answers to these questions:

Unlike user21820's answer, I don't think it is correct to say that we accept classical FOL because the real world obeys it. The world does not obey a logic as such; rather, our choice of logic reflects how we think about the world. Also, we cannot read off a logic from our experience of the world, or at least not in any simple way. Classical FOL has plenty of limitations and some unobvious features. Also, logicians disagree about many things, including the basic rules of inference. One of the few things on which logicians concur is that A follows from "A and B", but much beyond that you are going to find disagreement.

A more pragmatic approach is to think of logics as tools that we create and use in order to organise and systematise information and render it into a computable form. Some logics are more useful than others in this respect, but it does not make sense to seek a single 'correct' one. The most we can ask is that a logic succeeds in its practical application.

Bumble
  • 20,757
  • 2
  • 27
  • 65
0

See this on proof by contradiction. In short, the reason we accept classical FOL (first-order logic) for logical reasoning is that it is completely obeyed by the real world, and hence allows us to infer facts about the real world from other known facts. There is a deductive system for classical FOL (with a finite description), meaning that you can mechanically and unambiguously deduce every classical FOL theorem. This is the syntactic side. There is also the semantic side, where we are interested in tautologies (sentences that are true in every context). Now it turns out that any (proper) deductive system for classical FOL is semantically complete, meaning that every tautology is provable. This implies that such a deductive system is all you ever need to learn in order to do all mathematics. Also, don't bother learning Hilbert-style deductive systems, since they are simply useless for doing actual mathematics. The most practical are Fitch-style deductive systems such as this one.

Of course, (classical) FOL by itself does not cover what mathematics is about. Mathematics is FOL plus some assumptions, stated in some suitable FOL-based language, that seem to make at least some sense to some people. For example, in the linked post the section "Peano Arithmetic" states the added assumptions that you need to add to FOL to get a foundational system that supports reasoning about counting numbers. Almost every real-world phenomenon that can be expressed using a sentence about counting numbers can be proven within PA. If you want to reason about real numbers as well, which are abstractions of 'real-world quantities', then you would need to expand the language and add some more assumptions. None of these assumptions (also called axioms) can be non-circularly justified to be true, but you can observe for yourself that all the axioms under PA are justifiable either empirically or philosophically (empirically for PA and philosophically for induction).

Unfortunately, there is no such justification for some stronger systems such as ZFC. But ZFC has an advantage of being an elegant foundational system that supports whatever mathematicians wanted to do, and so it stuck with us (as a sociohistorical construct). The system under "Set Theory" in the linked post has strength equivalent to that of ZFC. However, if you are concerned about the truth of what you prove, then you must first be convinced that your chosen foundational system is even meaningful, and hence you would want to limit yourself to a weaker foundational system that you can justify. See this post for some brief comments about ACA, which is the natural point you can reach with essentially the same confidence as PA. ACA is an extremely weak system, but suffices for all known real-world applications of mathematics so far. There appears to be a rather natural hierarchy of foundational systems from PA to ZFC, and it is unclear how high we can climb while still being confident that it is meaningful (even if without real-world interpretation). But logicians tend to agree that ATR0 is more or less the limit of predicative reasoning. Predicative reasoning is the best we can do to non-circularly provide clear mathematical ontology.

user21820
  • 623
  • 1
  • 7
  • 17
  • To play the devil’s advocate, the founder of the law of non contradiction, Aristotle himself didn’t even elevate the principle to “the world completely obeys it”, or at least it is open to debate. His main argument is elenchus, the Socratic method of someone who undermines their own beliefs can’t participate in a meaningful dialogue. “ Although PNC is not subject to demonstration, it is subject to “elenctic refutation” according to Aristotle. The “elenchus” refers to the Socratic method of argument. When Socrates uses the elenchus, he gets his opponent to refute himself out of his own mouth” – J Kusin Oct 03 '22 at 15:23
  • To say the world *is* actually that way is possibly another step, “ Should one conclude that the world must be a certain way or merely that we have to think that it is a certain way, in order to have the experience and thoughts at issue?” https://plato.stanford.edu/entries/aristotle-noncontradiction/ – J Kusin Oct 03 '22 at 15:24
  • @JKusin: There is absolutely no counter-examples so far. So it is reasonable to say that the world completely obeys it. Philosophical objection to this is pointless, since you can always claim that it is possible that God created the world just one second ago but inserted fake memories into you that include you reading this message. Any reasonable philosophy that can assist understanding the world would accept classical FOL as completely obeyed, regardless of any ridiculous alternative possibilities. – user21820 Oct 03 '22 at 16:02
  • Also, it's irrelevant what a 'founder of law of non-contradiction' thinks. Aristotle himself, despite being a pioneer in logical reasoning, had a poor understanding of logic, so much so that he never understood quantifiers. Finally, it is not that the world must be classical in a modal sense (i.e. that non-classical worlds are not possible), but that our world that we live in simply is classical. I'm not interested in other 'possible worlds' that don't exist, and anyone who actually desires **truth** has to define it relative to some actual entity. And, well, there is only one actual world. – user21820 Oct 03 '22 at 16:09
  • What’s this view’s relation to intuitionist mathematics, int math is either a counter example or is wrong/false? Well where is one of their theorems wrong? Until that it *is* counterexample? Now what? – J Kusin Oct 03 '22 at 23:14
  • Sorry, your last comment doesn't make grammatical sense and I can't figure out what you are even trying to ask, so I'll ignore your comment and just say a bit relevant to intuitionistic logic. If classical FOL is correct, then clearly intuitionistic FOL is also correct but inferior since it doesn't have a straightforward real-world interpretation. Also, "intuitionistic mathematics" is ill-defined; you need to specify the entire system, and then you would find that there is no philosophically sound justification for an intuitionistic system that doesn't also justify a classical one. – user21820 Oct 05 '22 at 19:20
  • Sorry my comment was very terse and left out an “a” (is a counterexample) making it even more confusing. David McCarty was an intuitionist mathematician who didn’t seem to have a problem with a realist interpretation of intuitionist theorems. I don’t know exactly what foundation and formalism he followed, but he did say that taking both classical and intuitionist theorems together realistically can result in contradiction. That seems to suggest a realist intuitionist interpretation is not default fiction/false on its own. You seem to say classical FOL is completely obeyed in the real world, – J Kusin Oct 05 '22 at 23:03
  • …that it is more universal. To me that seems parallel to an empirical situation where a better, more universal theory replaces a more narrow one, but usually that comes with cases where the old theory is demonstrably wrong. I just don’t see how intuitionist math (or any mature logic) can be shown wrong, so it seems like half the story is still left out (showing where the old theory fails). It may be less comprehensive, but is it actually wrong and where? Or do we just not need to include the "disproof" part" (unlike empirical theories I'd argue)? – J Kusin Oct 05 '22 at 23:03
  • It's simply clear that you don't actually understand foundations of mathematics. I already said very explicitly that "*intuitionistic FOL is also correct but inferior since it doesn't have a straightforward real-world interpretation*". So why do you keep trying to imply that I said intuitionistic FOL is "fiction/false"?? You're going to have to look at the actual foundational system David McCarty was referring to, and you will find that what I said in the last sentence of my last comment is 100% correct!! – user21820 Oct 06 '22 at 20:16
  • You're right, I'm trying to jump the gun. *""intuitionistic mathematics" is ill-defined; you need to specify the entire system, and then you would find that there is no philosophically sound justification for an intuitionistic system that doesn't also justify a classical one"*. I still see this as incomplete however; say we use such a sound justification to justify classical and intuitionist math, what happens when the two form contradictory theorems from it? Because I know there *are* contradictory theorems b/w the two. And according to you we justify INT only if we also justify classical. – J Kusin Oct 07 '22 at 15:38
  • I'm going to say for the last time. There is **NO** way to give a philosophically sound justification for an intuitionistic theorem that contradicts a philosophically sound classical one. You have **not** provided any example, and you **cannot**. Don't blindly believe claims that are **ill-defined**. There are **thousands** of proposed systems, whether classical or intuitionistic, and many of them were inconsistent when first proposed. Until you **specify precisely** the system you want to talk about, there's nothing to discuss. – user21820 Oct 08 '22 at 05:45
  • First I'm sorry for bending your patience. If you can stand to watch 3.5 minutes of David McCarty https://youtu.be/cLpHvZH6avg?t=30 (:30 - 4:00), he quickly builds to, "the acceptance of a general mathematical realism even in a mild form convicts one of the existence and reality of outright contradictions in mathematics" at 3:50. I don't have his specific system, but that seems almost irrelevant - he has a formal system; it is within mathematics. I firmly trust he as a mathematician did not bring an ill-defined system when invited to speak at this conference. He lists several theorems too. – J Kusin Oct 08 '22 at 15:48
  • If you firmly trust someone without knowing what they have in mind, then it's clearly pointless to continue this discussion. Not all who claim to be mathematicians make cogent arguments. There are many explicit counter-examples, but I don't think you want me to be explicit about the cranks who are professors at known universities. (I will spend my time watching iff you discard your preconceived biases first.) – user21820 Oct 11 '22 at 13:35
  • That's a very fair requirement and criticism - I do have a bias that it seems like many mathematicians don't engage in foundational, philosophical, or cross-disciplinary discussions, when it is one of the most philosophically interesting disciplines. So quite possibly I do ascribe too much to the ones who do engage. I will deeply respect and try to understand whatever conclusions you derive if you decide watch. – J Kusin Oct 11 '22 at 15:20
  • Okay. I will watch it probably by this weekend and tell you what I think. See you later! – user21820 Oct 11 '22 at 18:30
  • 1
    @JKusin: I've watched much more than the first few minutes of that video. Frankly, it's just full of junk. His notion of 'realism' is completely idiosyncratic (not mild), and his 'outright contradictions' are based on faulty assumptions (not outright). The 'several theorems' all stem from the faulty axioms. One faulty assumption is that every total function on ℕ is computable. This is just bogus, for many reasons some of which I have told you in detail before. His justification is worse, begging the question. There is simply no evidence that everything is computable. Also, did you downvote? – user21820 Oct 16 '22 at 14:36
  • Thanks for the knockdown and I’m sorry for asking of your time where you probably didn’t learn anything very worthwhile. I didn’t downvote, and I dare not waste any more of your time! – J Kusin Oct 16 '22 at 15:10