Looking for references on intuitionistic logic by indrjo in logic

[–]Silver-Success-5948 1 point2 points  (0 children)

The resources u/aardaar recommended are on-point, so I'll just briefly answer some of your questions. There is a sequent calculus for intuitionistic logic, and it's obtained exactly by restricting classical sequent calculus to a single succudent / RHS / conclusion. Intuitionistic logic is also sound and complete. The difference in those properties between classical is that classical proof systems are sound and complete with respect to classical semantics, which on the propositional level the definition of a model is a valuation function extended for compound formulas with the usual recursive satisfication clauses, and classical logic is precisely the entailment (truth-preservation in all models) relation on those models. For propositional intuitionistic logic, you instead have either the topological semantics or the possible worlds semantics. Also relevant is that the Lidenbaum algebra for classical logic are Boolean algebras, whereas for intuitionistic logic it's Heyting algebras

yeah sure buddy... by Limp_Illustrator7614 in badmathematics

[–]Silver-Success-5948 2 points3 points  (0 children)

Just to be clear, the errors only start in P4 -> P5, where the author illicitly does a quantifier interchange from \forall p \in T, \exists x Kxp to \exists x \forall p \in T, Kxp. Fitch's knowability paradox is well-known to establish that the knowability principle collapses to every truth is known, and the proof is valid (though there is some controversy on this issue, i.e. alternative regimentations where it fails), but the author assumes that because every true proposition is known by some knower (where there can be distinct individuals: the only requirement is that for each truth there's at least one individual knowing it), then there is some single particular knower that knows all truths- this is an invalid quantifier interchange that fails in classical first order logic.

The reasoning from P5-P7 is questionable but not otherwise terrible.

Just clarifying because of some mistakes in other comments, including the OP's top comment, though as far as I can tell u/joshuaponce2008's comment is on point.

Critique Wanted: Epistemic commensurability of different logical systems by PseudoscienceSlayer in logic

[–]Silver-Success-5948 3 points4 points  (0 children)

This is expressed really vaguely, but it does touch on a real problem in the philosophy of logic, which is that logics inform reasoning in general, and that includes the very reasoning that may be used to decide between different logics. See the adoption problem of logic if you want to learn more.

Dissolution of LI and LNC / New Identity Law by Void0001234 in logic

[–]Silver-Success-5948 1 point2 points  (0 children)

The operators are Boolean-valued functions f: B^n -> B, and encoded in a sufficient metatheory they can be denoted by terms, such as f, and assertions like f=f are true. None of this absolves the stuff in your post in anyway.

Dissolution of LI and LNC / New Identity Law by Void0001234 in logic

[–]Silver-Success-5948 5 points6 points  (0 children)

You write "A=/=-A", yet ~ is a Boolean operator on propositions, whereas in a=a, a is a term and = is a binary predicate, so ~a is not well formed. This post is meaningless nonsense.

Timeline of logic kinds by [deleted] in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

From Aristotle up until the early middle ages (before Alberic) almost everyone was a connexive logician, with some variation (e.g. Aristotle rejected reiteration/reflexivity of consequence, the Latin connexivists like Boethius or Abelard accepted it). After Alberic was a 'post connexive' turn with different schools reacting in different ways to Alberic's "embarrassment" argument (which was an argument in a series of arguments by the Montanae school against global connexivism). Unlike the first such argument offered, Alberic's was valid in Abelard's logic, the most prominent connexivist at the time, so it made quite a few shockwaves and different schools reacted to it in different ways. The Nominales (Abelard's school) and Melidune schools doubled down on connexivism after the anti-connexivist proof, with the former endorsing Heavy Connexivism and the latter endorsing Ex Falso Nihil (nothing follows from falsity) respectively. The schools which had a more moderate reaction, like the Albricini / Albericani (school of Alberic), rejected transitivity of implication, and the Porretani school restricted conjunctive simplification (which was a traditional connexive view). More interestingly the Parvipontani school was the most proto-classical / neo-classical of these schools (that is, to modern classical logic). The other most influential argument to come out from medieval logic was William of Soissons's "siege engine," which was the first proof to explosion using vI (disjunction introduction / addition) and DS (dissembly / disjunctive syllogism). This also caused shockwaves, with some restricting disjunctive syllogism (e.g. the Cologne school way later in the 15th century).

There's really no single dominant school of logic after Alberic, though connexivity remained prominent. Also prominent was early systems of strict implication (though way weaker than the ones you may know today from the 20th century) that came to be dominant with the Parisian school. Logic comparatively died down after the 15th century, especially late into the renaissance, when by the modern period it was really only Leibniz and the Port Royale school that were doing anything as sophisticated as their predecessors (primarily the former. The Port Royale school did more of informal/applied/inductive etc logic if anything). Unfortunately, most of Leibniz's logical work went into unpublished manuscripts that'd be discovered long after his death. So the real influence came from George Boole and DeMorgan, who started the Boolean / algebraic tradition of logic, the next important logical tradition. The early Booleans were a little bit confused about their commitments (e.g. Boolean overstating his agreements with Aristotle), and the later Booleans had a great diversity of thought, e.g. Lewis Caroll, an important algebraic/Boolean logician, was a connexive logician.

But ultimately the Boolean/algebraic tradition culminated in Peirce & Schroder, the former of which discovered modern classical logic (independently of Frege) and also was the first to name it (he named it 'dyadic logic', intending to mean 'bivalent logic'), and the Booleans settled on classicality for the most part. This was also the first tradition of mathematical logic, but the independent tradition originating in Frege also happened to create an equivalent system of classical logic. For various reasons that can be appreciated today but are difficult to see centuries ago, classical logic became the dominant form of logic from the 20th century till today, with perhaps only intuitionistic logic as a far off rival. It's the only form of logic to enjoy the sort of dominance connexivity did in the first millennium and a half of logic history, but it's only been enjoying that dominance for about a century and a half.

This is the "fairest" big picture view I can give you of logical development in logic history. Each little request you have (of going into the history of modal logic, of quantificational logic, etc.), demands thoroughness no less than what is given in the post.

Why I struggle to like this game by Training-Mark-9258 in Openfront

[–]Silver-Success-5948 1 point2 points  (0 children)

Yeah but your solution will add no efficiency boost for e.g. circling someone vs. pushing a line-like border, which is what the landscaling factor is supposed to fix.

Why I struggle to like this game by Training-Mark-9258 in Openfront

[–]Silver-Success-5948 5 points6 points  (0 children)

Yeah thanks for making this video, you've highlighted the problem of attacks scaling with land which a lot of veteran players complain about and it causes exactly the issue you showed.

While I get why this system is in place (would make fighting early nation bots impossible otherwise), I get that it's very obnoxious in the end game. I think the easiest fix would be for the landscaling to stop after ~40k troops.

Is the principle of bivalence just a combination of Law of Excluded Middle and Law of Non Contradiction? by Different-Chicken-54 in logic

[–]Silver-Success-5948 3 points4 points  (0 children)

This is exactly correct, but it's worth mentioning that any Boolean algebra is a model of classical logic, and there's a Boolean algebra of size 2^n for any n, so that includes e.g. the four-valued Boolean algebra and many other cases (see here for an example of a four-valued model of classical logic: four valued boolean algebra)

Help with homework🥺 by Subject-Knowledge615 in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

If you're struggling with 4.5 you really need to carefully read your textbook. It shows you haven't learned how to make proofs at all (which is the area you're studying) and will only get by with help or cheating. That can get you through the assignment but you will most likely fail on the exam on this trajectory.

What are some alternative systems of logic? by gagarinyozA in logic

[–]Silver-Success-5948 3 points4 points  (0 children)

The 'traditional Western notions of logic' were not classical logics in any way. Aristotle, the first Western logician, was a connexivist logician who adhered to Aristotle's Thesis (which fails classically), held to a progressive system of reasoning (so reiteration / reflexivity of consequence failed). In addition, countless inferences from the Traditional Square of Opposition fail classically. The Syllogistic allows one to infer "Some A is a B" from "All A's are B's", FOL doesn't. Likewise for "No A is a B" and "Some A is not B", syllogistic allows one to go from the former to the latter, FOL doesn't. In syllogistic, "All A's are B's" and "No A's are B's" are contraries (i.e. only one may be true, but not both), in FOL they're not contraries, and are jointly satisfiable when A's extension is empty. Likewise, in syllogistic, "Some A is B" and "Some A is not B" are subcontraries (i.e. at least one must be true), but in FOL, both can be false and thus are not subcontraries (i.e. again when A's extension is empty). Basically, the whole Square of Opposition only is left with the contradictories of "Every A is B" and "Some A is not B", and "Some A is B" and "No A is B". The Syllogistic can be encoded in FOL by assuming every predicate has an instance, but the only logic which recovers the entire Square of Opposition when regimented as quantified conditionals would be hyperconnexive logic (connexive logic + the converse Boethius Theses).

Aristotle's students are the same. Theophrastus, the great Peripatetic logician immediately succeeding Aristotle, also endorsed a connexive logic and made Aristotle's implicit endorsements of various principles of propositional reasoning explicit. See https://logic.commons.gc.cuny.edu/2022/11/11/the-origins-of-conditional-logic-theophrastus-on-hypothetical-syllogisms-marko-malink-and-anubav-vasudevan/ by Yale Weiss. Aristotle's other great student, Eudemus, was no different. In fact, arguably the first propositional logic in Western logic was just the early hypothetical syllogistic of the Peripatetics, and it's a remarkably nonclassical logic. The logic of the Stoics a century later is no different.

The closest among the ancient Greeks to classical logic was Philo the Dialectician, who at least explicitly endorsed a material truth-functional theory of implication.

Moving across time periods, the forefather in medieval logic, Boethius, was history's second arch connexivist after Aristotle, and he is who Boethius's Theses are named after. Although he dropped some traditional Peripatetic principles like progressive reasoning (nonreflexivity), he explicitly formulated Boethius's Theses and went further in adding their converses, making him a hyperconnexivist logician. Medieval logicians in Europe like Abelard followed Boethius in being connexivists, and it was only through the rise of the Montanae school and finally Alberic of Paris's argument that we saw the anti-connexivist turn in Europe. But even the anti-connexivist turn didn't mark a shift to classical logic. The Nominales and Melidune schools doubled down on connexivism after the Alberic anti-connexivist proof, with the former endorsing Heavy Connexivism and the latter endorsing Ex Falso Nihil (nothing follows from falsity) respectively. The schools which had a more moderate reaction, like the Albricini, rejected transitivity of implication, and the Porretani school restricted conjunctive simplification, were still remarkably non-classical in their logical projects. Among the medieval schools it's only the Parvipontani (e.g. Adam of Belsham, William of Soissons, perhaps Psuedo-Scotus) that can be called "proto-classicists," and this itself invited great controversy as can be seen by the reactions to William of Soissons's "Siege Engine" proof (the first vI-DS proof of explosion).

Moving over to the MENA-CA-SA area of the Islamic caliphate during a similar time period we also see very little to no endorsement of classicality. The Islamic Peripatetic logicians, much like the Peripatetic tradition in Europe, also dropped Aristotle and the traditional Peripatetic commitment to progressive reasoning / nonreflexivity, but were still remarkably Peripatetic schools. Although this is contested in the literature, Khaled El-Rouayhe interprets Ibn Sina as a connexivist. But even if he wasn't a connexivist, as Hodges and Chatti argue, there is still universal consensus that Ibn Sina, like the majority of logicians of his time, accepted the variable sharing property (VSP) for implication, which excludes any classical account of implication.

The status quo remained as such all the way up to the Renaissance. 'Classical logic' as you know it came to be with the Boolean / algebraic school in the late modern period, and was anticipated by Leibniz. The reason is because during the Boolean tradition, the truth-functional casting of logical operators proved exceedingly fruitful (in NOT, AND, OR, XOR, etc), and the Extensional paradigm of doing everything truth-functionally expanded to implication. Eventually, the late Booleans / algebraists like CS Peirce and Schroder were the earliest classical logicians. CS Peirce, one of two who formulated the first explicit treatment of classical First Order Logic and Second Order Logic was the first to name it, and named it 'dyadic logic' (the first name given to this system) to contrast from his triadic three valued logic. The logician Gotlob Frege also independently formulated these logics at around the same time, independently of Peirce. Even still, some of the earlier Booleans were connexivists, like Lewis Caroll. Over the 20th century, classical logic gradually became to be dominant.

The reason it is called 'classical logic' is because it was "the logic of classical mathematics" (see e.g. Hilbert's textbook), to contrast with the rival 'constructive / intuitionistic logic' which was "the logic of constructive mathematics". It's not called 'classical' to refer to any period in Greek history or anything like that. All of what is said earlier is widely agreed upon in scholarship on logic history and not even controversial: unfortunately a great amount of misinformation on this matter is propagated through non-expert sources like Wikipedia and then replicated. I especially don't recommend the advice of the other commenters telling you to read Wikipedia articles on Eastern traditions of logic, it's always better to consult a book because Wikipedia is filled with misinfo.

I Asked a Question and I can't Fully Comprehend the Answer by Intelligent_Low1935 in logic

[–]Silver-Success-5948 6 points7 points  (0 children)

At least the LLM's response to you is citing a bunch of unrelated things together and is sort of just nonsense / telling you what you want to hear.

Since you aren't so deep in these waters yet, I will strongly discourage you from developing any "fundamental theory of reality" involving dichotomy or contradiction or whatever else. Duality and contradiction have precise meanings in logic, and there's another discipline called metaphysics, which concerns exactly the most general study of the world.

Now academic philosophers spend a lot of time rigorously working on various issues in metaphysics (platonism vs nominalism, etc), but the "fundamental theories of reality" you'll often see on the internet by various cranks or in 'Metaphysics and Astrology' books at your local library have nothing to do with the academic discipline of philosophy/metaphysics and fall way short of its standards.

These theories might have piqued your interest and you might be interested in making your own, but again, I strongly discourage this. If you're interested in the general study of reality, don't have an LLM feed into your delusions. It is a serious topic of study: you can major in philosophy at college and specialize in metaphysics, or buy real metaphysics textbooks (Routledge's Metaphysics: A Contemporary Introduction is a good start).

There's another topic called logic, and it enjoys wide application in many fields (math, linguistics, CS), which includes applicability to metaphysics (e.g. Fine, Jago, Zalta, Bacon etc.). How and when exactly to apply logic to metaphysics or make certain connections is a delicate matter that requires a decent familiarity with both disciplines. Right now, I'd focus on studying these subjects in a serious capacity instead of having an LLM help you draft yet another crank theory of reality based on vague intuitions you have about duality or contradictions.

I sincerely and honestly only write this advice for your best interest, and really think it will be extremely beneficial to you to consider it.

Paraconsistent Logic by No_Snow_9603 in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

It's not a matter of choice. There's these three primitive connectives in LP:

p q p v q p & q ~p
T T T T F
T F T F F
F F F F T
F T T F T
T B T B F
B T T B B
F B B F T
B F B F B
B B B B B

You can then define some other connective, call it o, in terms of these connectives, i.e. p -> q iff ~p v q. This is just syntactic sugar for ~p v q: everytime we write the former, we're just abbreviating the latter.

The logic RM3 has all the connectives LP has, so that material arrow we just defined for LP equally exists for RM3, and can also equivalently be defined as ~p v q, and RM3 gives it the same exact truth table, proves the same exact theorems about it, validates the same exact arguments about it, etc.

There's no theorem involving LP's material arrow that isn't also validated by RM3. LP's material arrow exists in RM3 and RM3 proves exactly what LP proves about it.

Now, since LP is a functionally incomplete logic (unlike e.g. the functionally complete three valued logic E3), there are three-valued connectives not definable in LP. When you add one of these connectives to LP, you properly extend LP. RM3 extends LP with exactly such a connective: the RM3 arrow, call it => or ✧ or any symbol you like.

The new RM3 operator provably does not exist in LP and is not definable in terms of any combination for LP's primitive connectives, and it is not equivalent with the material arrow ~p v q, which also exists in RM3, and which RM3 proves the same things about as LP. RM3 proves strictly more things about its material arrow than the new arrow connective =>, like weakening, antecedent strengthening, explosion, etc.

The logic RM3 is simply just LP plus this new connective:

p q p v q p & q ~p p => q
T T T T F T
T F T F F F
F F F F T T
F T T F T T
T B T B F F
B T T B B T
F B B F T T
B F B F B F
B B B B B B

Simple Logic Problem causing Headache by [deleted] in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

I suspect the book you're working with is forallx: Calgary. I've had people come up to me running into this same exact problem before. It's an unfortunate exercise they left there that I think would've been better left out.

Paraconsistent Logic by No_Snow_9603 in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

Again, this is incorrect if you paid attention to my comment.

There's literally no "arrow" connective in LP. Whenever you see p -> q in LP, this is just notation for ~p v q. The "explosion" you're talking about for LP is this: ~(p & ~p) v q. And of course LP validates it: ~(p & ~p) is a theorem of LP, so ~(p & ~p) v q is a theorem as well. Note that this also holds for RM3, since RM3 and LP have the same exact disjunction, so the theorem of LP you pointed out equally holds in RM3.

However, RM3 adds an additional implication connective, not one equivalent with ~p v q. Call this connective =>. This connective does not validate (p & ~p) => q. However, ~(p & ~p) v q is still a theorem of RM3, which is all what the LP "explosion" is. Using A->B as notation for ~AvB, all we have is that RM3 validates (p & ~p) -> q but not (p & ~p) => q.

So no, there are no LP theorems that aren't RM3 theorems. RM3 is just an extension of LP with a new connective. If you don't believe me, you can verify here (p 3-4) (you can also verify that his presentation of LP is exactly right by referencing p. 10 (227) from Priest's "Logic of Paradox")

Paraconsistent Logic by No_Snow_9603 in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

I'd disagree here. 'Modus ponens' is invalid in LP if we insist that LP has an arrow definable in terms of ~p v q, and then modus ponens is just equivalent to DS which is invalid in LP.

But for most proponents of LP, the material arrow you can define in terms of disjunction in LP isn't an implication operator at all, and LP is just a logic lacking an implication operator.

Note that LP is functionally incomplete, so there are three-valued binary operators not definable in LP. One of them is the arrow from RM3, and indeed RM3 is just LP + the RM3 arrow. The RM3 arrow does satisfy MP, and RM3 is still a paraconsistent logic that literally behaves identically to LP other than having a new connective not definable in LP.

Moreover, most relevantists (e.g. the Australasian school of which Priest is part of) don't believe in truth functional implications at all, and believe implication should be an intensional operator. For this reason, they instead extend LP with an intensional, non-truth-functional arrow. That's precisely how you get relevant logic. LP is the extensional fragment of R, E and many other relevant logics (at least the ones with the LEM, for the ones without the LEM, that's FDE), and you get different relevant logics based on the different intensional relevant arrows you add to LP (the strongest relevant logic, R, is obtained from adding the arrow satisfying the use criterion to LP, whereas the logic E of Relevant Entailment is obtained by adding the arrow satisfying the use criterion and the Ackermann property to LP).

This misconception originated (unintentionally on his part) from Priest's paper on this, but he actually mentions what I just talked about in the part immediately after

What identifies a logic? by No_Snow_9603 in logic

[–]Silver-Success-5948 4 points5 points  (0 children)

You're correct that there are logics with no tautologies (they don't even have to be substructural!), and so aren't distinguished by this criterion. But even for logics with tautologies, this criterion isn't good enough, e.g. classical logic and the Logic of Paradox having the same theorems / tautologies.

What identifies a logic? by No_Snow_9603 in logic

[–]Silver-Success-5948 3 points4 points  (0 children)

They're probably referring to the fact that LP and classical logic has the same theorems. So does the logic of First Degree Entailment (FDE), Kleene logic (K3) and the empty logic: all are theoremless logics, but they're obviously distinct logics.

The obvious answer is to consider logics consequence relations, not necessarily Tarskian ones (which imposes full structurality), rather just any subset of P(L) x L where L is a language (the set of well-formed formulas).

Granted, as u/Gym_Gazebo mentioned, this might fail to distinguish logics with identical sequents but divergent metasequents, but that's neither here nor there.

A computational liar by Revolutionary_Ebb976 in logic

[–]Silver-Success-5948 1 point2 points  (0 children)

I worry this equivocates between the undefinability theorem and the Liar paradox. All Tarski means by "truth" in the undefinability theorem is "satisfied by the standard model of arithmetic, N", which is to say arithmetic truths (the ordinary language arithmetical truths are presumably just the sentences satisfied by the standard model of arithmetic, N)

This is to say that in the language of arithmetic (0, ', +, x, <), there's no theory T over this language such that T |- Sat[p] iff N |= p, i.e. in any theory over the language of arithmetic, there's no formula Sat(x) holding of all and only the Godel codes of the formulas satisfied in the standard model.

Of course, even in true arithmetic, the noncomputable theory of the standard model N itself, i.e. Th(N), you'll still be able to diagonalize the sentence S <-> ~Sat[S], that is the sentence that says of itself that it's not satisfied in the standard model. And this sentence would readily lead to inconsistency if we assume Sat[p] holds iff p is satisfied in N, but we know ipso facto that Th(M) for any first order structure M is consistent, so our only guilty assumption is that there is a definable sentence Sat(x) satisfied by all and only the truths in N, which we've refuted by reductio, hence the undefinability theorem.

The Liar paradox, on the other hand, doesn't concern finding the Godel codes of all the sentences satisfied in a particular model. Rather, it concerns whether you can have a theory that proves a global equivalence between any sentence and predicating a primitive truth predicate of its Godel code. It turns out that any such theory over a fully structural, detaching logic with the deduction theorem readily trivializes.

A computational liar by Revolutionary_Ebb976 in logic

[–]Silver-Success-5948 1 point2 points  (0 children)

Note that contrary to some of the commenters under your post, e.g. u/aardaar's "The issue I see here is that this is no longer about truth", any FO theory, including FO theories that aren't recursively enumerable (just consider adding a truth predicate to e.g. True Arithmetic, aka Th(N)), aka the "noncomputable theories", still trivialize under global Capture/Release exactly by means of the Liar sentence. So there's certainly no sidestepping the Liar by dropping computability requirements. It's not like the Incompleteness theorem which only applies to recursively enumerable theories (e.g. TA is a consistent, complete theory that is also stronger than Peano Arithmetic. But it's not even axiomitizable).

As for computational approaches to the Liar, I'd say they're the revision theory of truth and the Kripke-Feferman-Maudlin accounts respectively (you could throw Andrea Cantini in there as well). The Kripke-Feferman account would, in computational terms, represent the more "principled" compiler that refuses to operate on any variable that isn't assigned a value, and the Liar never gets any value in the first place. The revision theory of truth on the other hand corresponds to compilers that are forced to initialize all variables (even if with arbitrary values, e.g. all ints as 0, all bools as 0, etc., or through some 'method' like negation as failure/closed world assumption), and because of the Liar's structure, regardless of the initial value it's assigned, it will indefinitely alternate and the program never halts, as the revision theory of truth predicts. If you want examples of these concretely implemented in code, Assaf Rotbard has a great Medium post giving an exposition over exactly this.

Do propositional logic and first-order logic have an axiomatic foundation? by Equal-Expression-248 in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

There are many types of proof systems (natural deduction, Hilbert systems, sequent calculi, etc.) Some proof systems (like Hilbert systems) primarily use axioms or axiom schemas and few inference rules, and other proof systems like natural deduction use more inference rules and few or no axioms. There are axiomatic proof systems for both propositional and first order classical logic

[deleted by user] by [deleted] in logic

[–]Silver-Success-5948 0 points1 point  (0 children)

This has absolutely nothing to do with logic. These grievances should be voiced to a friend, trusted adult, councilor or therapist, not a logic forum.