Have you studied any systems of logic other than classical logic? Have you found them useful?

P1392

Already in classical mathematics, there is a difference between saying that something is true and saying that something is provable. If you adopt ZFC because you believe it correct, then presumably you believe that ZFC is consistent even though (assuming that you're aware of certain theorems) you also know that you cannot prove it so. In that case, you also believe that the continuum hypothesis (for example) is either true or false; you may or may not have an opinion on which it is, but in any case again you know that you cannot prove it either way.

A constructive mathematician can be even subtler. If you belong to the Bishop school, then you accept no classically false axioms, and anything that you can prove is valid also in classical mathematics. Even so, you can believe that the principle of excluded middle is false (even though, of course, you know that you cannot prove it false). So you can really confuse the classical mathematicians by saying, on the one hand, that they can safely accept all of your theorems as valid, and then saying, on the other hand, that you know excluded middle to be false. The resolution, of course, is that you never claimed that this was a theorem.

wot doh fohk????
looks way harder than the stuff i get for homework

P24739
no worries anon, depending on your grad level your homework just aims to teach you methodology and a certain level of rigor.
Linear logic is usually given in the terms of sequent calculus. There is a set of propositions which we construct through recursion. Each pair of lists of propositions is a sequent (written as [tex: \vdash]), some of which are valid to recursion.
As I understand it, the main point of linear logic is the restricted use of the weakening and contraction rules :
>[bold: restricted weakening rule] : If [tex: \Gamma,\Delta \vdash \Theta] then [tex: \Gamma,!A,\Delta \vdash \Theta], for any A; conversely and dually, if [tex: \Gamma \vdash \Delta,\Theta] then [tex: \Gamma \vdash \Delta,? A,\Theta] for any A.
>[bold: restricted contraction rule] : If [tex: \Gamma, !A,!A,\Delta \vdash \Theta], then [tex: \Gamma,!A,\Delta \vdash \Theta]; conversely and dually, if [tex: \Gamma \vdash \Delta,? A,? A.\Theta] then [tex: \Gamma \vdash \Delta,? A, \Theta].

P24908 tell me more about the rigour

P24908
tell me more about the train boys

P24908 tell me more about the saucepans

P24909
I can't say it better than Tao does :
>One can roughly divide mathematical education into three stages:
>1. The “pre-rigorous” stage, in which mathematics is taught in an informal, intuitive manner, based on examples, fuzzy notions, and hand-waving. (For instance, calculus is usually first introduced in terms of slopes, areas, rates of change, and so forth.) The emphasis is more on computation than on theory. This stage generally lasts until the early undergraduate years.
>2. The “rigorous” stage, in which one is now taught that in order to do maths “properly”, one needs to work and think in a much more precise and formal manner (e.g. re-doing calculus by using epsilons and deltas all over the place). The emphasis is now primarily on theory; and one is expected to be able to comfortably manipulate abstract mathematical objects without focusing too much on what such objects actually “mean”. This stage usually occupies the later undergraduate and early graduate years.
>3. The “post-rigorous” stage, in which one has grown comfortable with all the rigorous foundations of one’s chosen field, and is now ready to revisit and refine one’s pre-rigorous intuition on the subject, but this time with the intuition solidly buttressed by rigorous theory. (For instance, in this stage one would be able to quickly and accurately perform computations in vector calculus by using analogies with scalar calculus, or informal and semi-rigorous use of infinitesimals, big-O notation, and so forth, and be able to convert all such calculations into a rigorous argument whenever required.) The emphasis is now on applications, intuition, and the “big picture”. This stage usually occupies the late graduate years and beyond.
Most textbooks that you see early on are aimed at students who are in the process of moving from stage 1 to stage 2, and that's why there's less emphasis on intuition compared to rigour.
Once you get past that point, there's more of an emphasis on intuition, but it's still intuition that can be translated into rigour.

As for me, I believe intuition is not necessarily founded on the evidence of the senses; the sense would soon become powerless; for example we can not represent to ourselves ourselves a chiliagon, and yet we reason by intuition on polygons in general, which include the chiliagon as a particular case.
Thus logic and intuition have each their necessary role. Each is indispensable. Logic, which alone can give certainty, is the instrument of demonstration; intuition is the intrument of invention.
In that regard, the point of rigour is not to destroy all intuition but rather to clarify and elevating it.

http://tdx37ew3oke5rxn3yi5r5665ka7ozvehnd4xmnjxxdvqorias2nyl4qd.onion/wiki/Bloom%27s_taxonomy?lang=en

The idea of alternative systems of logic that aren't equivalent to classical logic seemed weird to me at first. Surely the fundamental rules of reasoning can't be just arbitrary choices; one of those choices ought to be right and the others wrong. But I came to realize that having multiple systems of logic around can make sense because they allow you to reason about different types of propositions. The propositions of classical logic, for example, are true/false questions.

It is philosophically debatable whether a statement like "for any natural number n, blah blah blah" is a true/false question. It can be proven true by induction; for example, "for any natural number n, n + 3 = 3 + n" can be proven that way. And the statement "for any natural number n, n * n = n" can be proven false by exhibiting the counterexample 2. If one imagines that an infinity of natural numbers already exists in some sort of Platonic realm, then it makes sense for statements about all natural numbers to be true/false questions. But if we don't accept numbers as existing until we construct them, then it's not obvious that such statement have to be true or false. They can be found true by constructing a proof, or false by constructing a counterexample, but a statement needn't have either.

Regardless of what one thinks of the above philosophical question, the new kinds of propositions that intuitionists have invented for philosophical reasons have very practical uses. You might have heard a joke where someone answers a question like "is it raining or not?" with "yes." If one uses the meaning of "or" found in classical logic, "yes" is the correct answer, but the question is clearly not meant to be a true/false question. We can deal with these sort of propositions using intuitionistic logic. In intuitionistic logic, to construct a proof of "A or B," you have to prove either A or B, so you always know which one you've proven. So an intuitionistic proof of "for any natural numbers m and n, m < n or m >= n" guarantees us a method for deciding which of the two statements is true.

With the invention of topos theory, a new sort of constructivism arose too. It was observed that any topos with a natural number object has an internal logic which is powerful enough to interpret most of mathematics, but that this logic in general fails to satisfy and excluded middle.
This means that even for a mathematician who likes to use choice and excluded middle (and a fortiori for one who believes them to be true), there is a reason to care about what can be proven without them, because only if a proof is constructive can it be interpreted in an arbitrary topos.
Even starting from a completely classical world of mathematics, many interesting toposes arise naturally whose internal logic is not classical logic. Then by internal reasoning in such a topos, one can prove various facts, which can then be reinterpreted as external statements about the behaviour of the topos itself.
By now, it is known that many of the non-classical axioms used by the early constructivists have natural models in particular toposes.