# Proof that the rules of logic are true

I was thinking in posting this question on the Math Stack Exchange, but it probably fits better in here. I am taking a class on euclidean and non euclidean geometries, there is a section dedicated to Logic, I assume is classical propositional logic but I am not absolutely sure. In this section we studied several rules to prove mathematical statements; Reductio Ad Absurdum proofs, negation proofs, rules of implication, proofs by cases and so on. How do we know that this rules are correct, how could one prove that this rules of logic are indeed correct, and if we can choose a set of axioms for developing several types of geometries, could we develop different types of logic by choosing different rules ?.

• You're not completely clear as to what you count as rule. Reductio ad absurdum is a kind of argumentative form, then you mention rules of inference, etc. Once we set axioms we can prove those. But like Akhil mentioned, we can't prove the axioms. As for choosing axioms: there are multiple kinds of logic resulting from different choices. For example, if you reject the law of non-contradiction you get dialetheism, a kind of logic where there are "true contradictions" (borrowing from Graham Priest). – Marc H. Nov 24 '17 at 22:22
• This is definitely the right place for this question, since this is a question of philosophy. There are different logical systems, yet one is more "standard": classical logic. Why this is so (and whether it's the "right" system in an absolute sense) is an open question, but it has interesting characteristics such as completeness (for first order logic). And of course, "proving"that this is the right system cannot be done, because any proof takes place within a logical system. – Quentin Ruyant Nov 24 '17 at 22:45

As I read your post, there are three separate but related questions:

1: How do we know that the rules of the ‘deductive calculus’ are correct?

2: How can we prove they are correct?

3: Can we construct a different logic by choosing different rules.

1) The answer to the first question is an epistemic question. Traditionally, people hold that proof rules (like e.g. ‘From (φ => χ) and φ, go to χ.’) are a priori, i.e. knowable through reflection alone. Frege held that view in his Grundlagen. He also says there that the rules are in some sense self-evident, and many philosophers agree. What we mean exactly by ‘a priori’ and ‘self-evident’ is debatable, of course; but the point is that is that (most agree that) we know the proof rules in the same way in which we know e.g. that a = a. Since you mention geometry, Frege held that it is synthetic, while logic and arithmetic are analytic.

2) Turning to the second question, the answer largely depends on what we mean by ‘proof’. In one sense, nothing is easier than proving an axiom: just cite the axiom. Yet that’s not what you mean, of course. One thing we can do is to show that the rules are sound and complete: suppose that φ is semantically entailed by a set of premises; i.e., all interpretations that make the premises true, make the conclusion true. Then we can show that this is the case if and only if φ is provable from the premises. (At least if we are dealing with 1st order logic.) This result is due to Gödel, and the proof is very complicated. Yet what the result says on a more intuitive level is that the proof rules won’t ‘lead us astray’, and won’t ‘short-change’ us, either: using the rules, we can prove all and only those consequences that we have already established by semantic means.

Of course, we can now ask how we can prove the semantics; but in a sense, that’s a moot point. If we ask: ‘are the rules correct?’, we better had a standard for deciding what does and doesn’t count as ‘correct’. Semantics does just that: it decides what sentences are true, and what arguments valid, so that our proof rules can then be checked again this truth and validity – albeit formally defined truth and validity.

3) This question is probably slightly misguided. We certainly can construct alternative logical systems (alternatives to classical logic); but changing the proof rules isn’t the best way to do it: you'll just end up proving too much or too little. Rather, you’ll want to play with the semantics. E.g., you might introduce a new truth-value besides TRUE and FALSE, so that sentences can be NEITHER. Alternatively / additionally, you could allow models with empty domains, or permit empty names. There’s a lot you can do, but it’s not normally done through the proof rules. Once you’ve made the changes, you may then want to alter the rules and see whether your system is still sound and complete.

• I am not sure about the "best way", but historically alternative logics, intuitionist, modal, paraconsistent, were constructed first by changing the "proof rules". Finding suitable semantics was a later development, and I am not sure that extensionalization of intensional logics model theory provides is really the best way to interpret what they intend, it seems more like technical convenience. And there are even technical "virtues" for logics (harmony, etc.) that do not come from semantics, Girard's "transcendental syntax" justification focuses on those. – Conifold Nov 25 '17 at 0:12
• @Conifold Point taken. I think what I meant was: if all you do is drop a rule, that doesn’t really yield a new system of logic. It’s still the same logic, with less deductive power. As you point out, Intuitionism can be characterised by its rejection of double-negation elimination and the law of excluded middle. Yet these aren’t rejected for their own sake. When Brouwer first conceived of Intuitionism, don’t you think his intentions were mostly ‘semantic’ – replacing TRUE and FALSE with something like CONSTRUCTIBLE and REFUTABLE? This isn't formal semantics, of course. – MarkOxford Nov 25 '17 at 9:43
• +1 A mention of the Agrippan/Münchhaussen trilemma might also be helpful as a reference. You touch on most of it already, but imho it would be nice to give OP some ideas of where to pursue further research. – Dennis Nov 25 '17 at 18:53
• I think that Brouwer, and anti-realists like Dummett more generally, would reject such re-interpretation. The title of Tait's book, promoting it, Against Intuitionism: Constructive Mathematics is Part of Classical Mathematics, speaks for itself. To them the classical notion of truth, and truth-conditional semantics that comes with it, is misguided, and translations into it are inherently distorting. The same goes for dialetheists and intensional modalists (w/o possible worlds). Formally, all those can be interpreted in terms of each other, classical semantics is not special in that respect. – Conifold Nov 26 '17 at 21:48