1

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?

Improve this question
12
  • 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.
    – Mark Saving
    Oct 1, 2022 at 23:45
  • 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?
    – Chessnerd321
    Oct 2, 2022 at 2:07
  • 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.
    – Chessnerd321
    Oct 2, 2022 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 2, 2022 at 18:07
  • 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 3, 2022 at 3:58

2 Answers 2

Reset to default
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.

Improve this answer
1
  • Thanks a lot for answering. You have given me a lot to think about!
    – Seeker
    Oct 3, 2022 at 22:43
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.

Improve this answer
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 3, 2022 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?” plato.stanford.edu/entries/aristotle-noncontradiction
    – J Kusin
    Oct 3, 2022 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 3, 2022 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 3, 2022 at 16:09
  • 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, 2022 at 14:36

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .