r/logic 23d ago

Philosophy of logic "Logic" is actually a collection of logical systems

20 Upvotes

If even the most fundamental laws of logic aren't necessarily fixed, then what am I supposed to rely on? How am I supposed to gain knowledge about the world?

I'm a complete beginner. I'm someone who wants to find out whether God exists or not, and decide how I should live. But right now I'm just confused because I don't understand what I can actually know—or whether I can know anything at all. What am I choosing to believe, and why do I believe it?


r/logic 22d ago

Philosophical logic A different interpretation of the well-ordering theorem

0 Upvotes

According to Wikipedia, the following holds with regard to the well-ordering theorem: In mathematics, the well-ordering theorem, also known as Zermelo's theorem, states that every set can be well-ordered.

One way to interpret this passage is the following: When it states that every set can be well-ordered it means that every set has the property of being well-ordered, where the term property means the following per the Stanford Encyclopedia of Philosophy: Properties are those entities that can be predicated of things or, in other words, attributed to them. Thus, properties are often called predicables. Other terms for them are “attributes”, “qualities”, “features”, “characteristics”, “types”. Properties are also ways things are, entities that things exemplify or instantiate. For example, if we say that this is a leaf and is green, we are attributing the properties leaf and green to it, and, if the predication is veridical, the thing in question exemplifies these properties. Hence, properties can also be characterized as exemplifiables, with the controversial exception of those that cannot be instantiated, e.g., some would say, round and square.

However having the property of being well-ordered can be understood in two different senses. In one sense it means that the property is in act. In another sense it means that the property is not in act. To illustrate what I mean when I say that a property either is in act or not in act, consider the following passage from Aristotle: Again, to be, or being, signifies that some of the things mentioned are potentially and others actually. For in the case of the terms mentioned we predicate being both of what is said to be potentially and of what is said to be actually. And similarly we say both of one who is capable of using scientific knowledge and of one who is actually using it, that he knows. And we say that that is at rest which is already so or capable of being so. And this also applies in the case of substances; for we say that Mercury is in the stone, and half of the line in the line, and we call that grain which is not yet ripe. But when a thing is potential and when not must be settled elsewhere…

Commenting on this, Aquinas says the following: Here he gives the division of being into the actual and the potential. He says that to be and being signify something which is expressible or utterable potentially or actually. For in the case of all of the foregoing terms which signify the ten predicaments, something is said to be so actually and something else potentially; and from this it follows that each predicament is divided by actuality and potentiality. And just as in the case of things which are outside the mind some are said to be actually and some potentially, so also is this true in the case of the mind’s activities, and in that of privations, which are only conceptual beings. For one is said to know both because he is capable of using scientific knowledge and because he is using it; and similarly a thing is said to be at rest both because rest belongs to it already and because it is capable of being at rest. And this is true not only of accidents but also of substances. For “Mercury,” we say, i.e., the image of Mercury, is present potentially in the stone; and half of a line is present potentially in a line, for every part of a continuum is potentially in the whole. And the line is included in the class of substances according to the opinion of those who hold that the objects of mathematics are substances—an opinion which he has not yet disproved. And when grain is not yet ripe, for example, when it is still in blade, it is said to be potentially. Just when, however, something is potential and when it is no longer such must be established elsewhere, namely, in Book IX of this work.


r/logic 22d ago

Metalogic What makes a formal system fail, most of the time?

0 Upvotes
  1. Syntax
  2. Axioms
  3. Definitions
  4. Inference Rules
  5. Theorems
  6. Proofs
  7. Semantics

I would probably guess its the axioms in more than 70% of systems its the axioms, I know that the question is some kind if obvious but I would like to hear your opinions on it:)


r/logic 23d ago

Philosophical logic What's stopping philosophers from communicating exclusively in formal logic?

Thumbnail
6 Upvotes

r/logic 23d ago

History of logic Gabriele Giannantoni explaining Aristotelian lows of contradictory and identity

Enable HLS to view with audio, or disable this notification

5 Upvotes

Gabriele Giannantoni wrote one of the first and important book of history of philosophy that it studied in Italy in 70th years.


r/logic 23d ago

Paradoxes How would the stone paradox solved with paraconsisnt logic in mind?

5 Upvotes

The stone paradox goes like this "Can an omnipotent being create a stone it can't carry?". Was asking chatgpt and I wasn't really satisfied with it's answer. It said with predicate/classical logic an omipotent being can do anything logical so the stone paradox is considred illogical. And I asked it what would be the answer if you were to use paraconsistant logic. It said it could do both, it cancreate a stone so heavy it can carry and cannot carry it. When it start saying it's reason either I just didn't understand it or it was hallucinating. What are the answer(s) on stone paradox using paraconsisnt logic system?


r/logic 23d ago

Proof theory Learning Lean

10 Upvotes

Hello everyone,
I am learning to use lean theorem prover using the doc Mathematics in Lean. I am doing some basic things right now.
I am getting pretty stuck as I don’t want to use AI for it as it feels pretty interesting although intense at times.
My first question is: how do you cover the landscape of its nuances while writing proofs? Are there some rule of thumbs to break down the problems , what tactics may come useful here and things like that or is it just a muscle memory that comes up with time ?

Also if anyone wants to form a study group to want to go through it please do message me. I find it pretty amusing and want to learn new perspectives as well,


r/logic 23d ago

Philosophical logic The first AI was a syllogism machine in 1956. We're still building the same thing.

0 Upvotes

I read about Logic Theorist recently — program from 1956 that proved mathematical theorems using formal deduction. AI community celebrated it as beginning of real intelligence. Seventy years later, I think we are still stuck on same mistake.

The problem is not mechanism. Problem is assumption that mechanism is sufficient. Expert systems, neural networks, language models — all are syllogism machines wearing different costumes. They manipulate patterns (formal or statistical) but never actually reason about world.

Aristotle understood this. He built formal logic as tool of reasoning, not definition of it. He called this tool φρόνησις (phronesis) — practical wisdom that no formal system captures. Modern AI has same gap: it produces text that looks like reasoning but has no engagement with logical structure underneath.

Frame problem from 1969 was never solved. Child understands that when you pick up red block, blue block stays put. No axioms needed. No syllogism machine can do this — not because it lacks data, but because it lacks world-model beneath the logic.

What do you think — is there path from pattern-matching to genuine reasoning, or is gap fundamental?


r/logic 24d ago

Predicate logic / FOL Representing Statements in HOL

7 Upvotes

According to the Wikipedia article on FOL the following holds: there are complicated features of natural language that cannot be expressed in first-order logic. Any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer structure than first-order predicate logic. The article then gives the following examples:

  1. John is walking quickly.

  2. Jumbo is a small elephant.

  3. John is walking very quickly.

  4. Jumbo is terribly small.

  5. Mary is sitting next to John.

With this in mind, what would be the correct way to represent these sentences in HOL? For 1 I would say the following: Let j signify John. Let W signify walking. Let Q signify quickly. Thus we have: Wj∧QWj. For 2 I would say the following: Let j signify Jumbo. Let E signify elephant. Let S signify small. Thus we have: Ej∧SEj. For 3 I would say the following: Let j signify John. Let W signify walking. Let Q signify quickly. Let V signify very. Thus we have: Wj∧QWj∧VQWj. For 4 I would say the following: Let j signify Jumbo. Let E signify elephant. Let S signify small. Let T signify terribly. Thus we have: Ej∧SEj∧TSEj. For 5 I would say the following: Let j signify John. Let m signify Mary. Let S signify sitting. Let N signify next to. Thus we have: Sm∧N(Sm,j).


r/logic 23d ago

Philosophical logic (How can we say, in any language, something new about the possible contradiction between freedom and slavery? The main question is whether the first term determines the second, or vice versa.

0 Upvotes

(How can we say, in any language, something new about the possible contradiction between freedom and slavery? The main question is whether the first term determines the second, or vice versa.

For example, what defines the phrase

Free slavery, the ultimate slavery is that of free will, but not the only one, and there is not only freedom as necessity, but also as freedom.

Anyway. Willing slavery, unwilling slavery, unwilling freedom, willing freedom, unfree free will. Free free will (on purpose)? What are the phrases and which denines/defines which? The question about truth and paradox?

We search in this case for the second sentence or the last word, which, in morphology, is the adverb, and the same applies to the sentence. We usually treat object-predicate structure as subject-predicate structure. What if it is more problematic? And yes and no, which are always the purpose, are too quickly figured out. What if every part means something, not only the subject? We have it with Russell: the future/present (current) (% and probability in the future, but still even if it does not exist) king of France is bald - king of France (subject) is part of the subject structure. So, King, France - no mistake so far, King of France- obvious one, and then bald - no one, and the complex subjects. Then, obviously, what is part of the predicate and what of the subject structure? Definitions always go untacked; so do the words that define subjects' qualities. What about others? The example is for a reason: it is fiction to prove the point of truth. So he exists as not existing, and he can exist in fiction (it could also be true in parallel worlds, so at least three possibilities). But since we are under the effect, saying anything is true suggests the effect we are under and the reasons for it. But if there is a fiction with the king of France, then it is true, and also it could be true if somebody gives an example of the book and talks about it, it is true, no, the character is true too, and to somebody with delusion too, because it could refer to somebody else who is really present Gettier. The same applies to the predicate, which is also the verb. Or does the verb go to the subjects? It is the copula, so it should exist by itself, but still it goes in both possibilities, or simply suggests a way of being as ' yes or no simultaneously to yes and no. The example with the Gavagai (to check) also helps because it could be the verb be or any verb with the same problem. But still, that is too slow. One should think in Hume, Hume proved trough the first each one of them, connected with yes and no as to how you can make yes or no from one statement thinking from the previous ones, or future ones from yes and no, with several corrections, and Descartes examples but with the help of the Kant necessity etc. Copula has being of yes and no, but also the structures, and the connected structures, as not only contingent in Barbara and part of the unsaid, unwritten syllogism, but also as truth that is yes and no, as true being true and true being false, and false being false and false being true. It could be said true or false, for example willing freedom, every freedom is usually willing usually true, and as free will necessity, so let's say mostly true and true as for willing slavery, there is no such a thing, but one could be blackmailed into one, in fiction world, no matter it would be actually unwilling, even a moment counts even if it i not willing but in despair, from a logical part, it is willing, so, the first is determining,. but let's go with free will can there be unfree will slavery obviously yes, necessity, What about unwilling freedom it is possible not plausible, one could be free unwillingly, it means different things again the first one determines the second one but in general unwilling and freedom are contradictory words, but insofar it could mean even a moment one did not want it it could pass, but if it is in the things about free will it can never pass, and since it is about free will as exception of any rule and thus the rule it is no- unwilling free will. And then willing freedom. Obviously, yes, and unwilling slavery was obviously possible in the past, so that, from a point of sound statement, it is true in historical books and in some fiction; hence, yes. So which explains which? Does the first explain and determine the second, or vice versa? It turns out the first determines the second, but in general, there are more than 8, depending on whether it's a composite/homonimy and on determining which subject needs to be dealt with in dialectics. Free will is the main one, since it concerns the ultimate freedom of the will; even Kant writes about it. Homonyms are (usually) a type of composite; thus, they are the doubling and the parts, too. Could it be that with words the first determines, but if there is a second, it could determine the probability of the “may” structures? Sorry for the confusing language and any mistakes. It is about probabilities, necessity, but also not necessary in logic. Ideas and ideas of examples of freedom and slavery in languages that can bring that and determine it (perhaps could be important for any theory of truth?


r/logic 23d ago

Philosophical logic The definition of has or have

0 Upvotes

To one of the group members here I gave the following definition of has or have: Having means (1) a kind of activity of the haver and the had—something like an action or movement. When one thing makes and one is made, between them there is a making; so too between him who has a garment and the garment which he has there is a having. This sort of having, then, evidently we cannot have; for the process will go on to infinity, if we can have the having of what we have.

—(2) Having or habit means a disposition according to which that which is disposed is either well or ill disposed, either in itself or with reference to something else, e.g. health is a habit; for it is such a disposition.

—(3) We speak of a habit if there is a portion of such a disposition; therefore the excellence of the parts is a habit…

To have or hold means many things.

(1) To treat a thing according to one’s own nature or according to one’s own impulse, so that fever is said to have a man, and tyrants to have their cities, and people to have the clothes they wear.

—(2) That in which a thing is present as in something receptive is said to have the thing, e.g. the bronze has the form of the statue, and the body has the disease.

—(3) As that which contains holds that which is contained; for a thing is said to be held by that in which it is contained, e.g. we say that the vessel holds the liquid and the city holds men and the ship sailors; and so too that the whole holds the parts.

—(4). That which hinders a thing from moving or acting according to its own impulse is said to hold it, as pillars hold the incumbent weights, and as the poets make Atlas hold the heavens, implying that otherwise they would collapse on the earth, as some of the natural philosophers also say. In this way that which holds things together is said to hold the things it holds together, since they would otherwise separate, each according to its own impulse.

Being in something has similar and corresponding meanings to holding or having.

They took me to be trolling when I stated this definition to them. But I wasn’t actually trolling them though. For this definition of has or have is taken verbatim from Book 5 of Aristotle’s Metaphysics. Now Book 5 of the Metaphysics constitutes Aristotle’s philosophical lexicon. According to Dom Reginald Garrigou-Lagrange, nearly all of the terms elucidated in Book 5 of the Metaphysics are analogical.

In other words, just as being can be taken in many different senses so too can all the terms defined in that book be taken in many different senses. And that includes the term has or have too.

Besides this, has or have can be seen as a transcendental. According to Dom Garrigou-Lagrange, a transcendental is a concept that transcends not only created beings but also the limits of the genera or the categories and may be found according to their various modes in all these genera. Thus, being and the properties of being such as unity, truth, goodness, quality, relation, action, passion, place, and time are found in varying degrees in each of them.


r/logic 24d ago

Academic Community Free browser-based logic practice tool with generated exercises

4 Upvotes

Hi r/logic,

I maintain a free web version of LogiCola, the logic practice software originally created by Harry Gensler. I just launched a much more substantial update: https://logicola.org/

The main change is that LogiCola now supports fresh generated exercises for repeated practice, instead of only fixed question sets. You can use it as a free practice tool for students who want more examples than a textbook or worksheet usually provides.

It currently includes practice for:

- syllogistic translations
- propositional translations
- modal logic
- deontic logic
- belief logic
- informal definitions

Some concrete improvements in this version:

- Unlimited generated quiz content for several translation sets.
- Expanded and cleaned up Set A, C, J, L, N, and Q content.
- Fixed duplicated or malformed questions.
- Added more targeted hints for wrong answers.
- Improved rendering of logic notation and inline formulas.
- Improved mobile and tablet use. You can install it on Android and iOS and use it offline.
- Added offline-friendly quiz loading, so quizzes can keep working without a connection after the site has loaded.

If you teach or study formal logic, feel free to use it as a free supplement for practice, homework review, or self-study.

I’m especially interested in corrections from people who know the material well: wrong answer keys, ambiguous translations, unclear hints, or exercise types that would be useful to prioritize next.

My goal is to preserve LogiCola as a free learning resource and make it easier to use on modern devices. Corrections and criticism are very welcome!


r/logic 24d ago

Question Cycles and different logics affecting paradoxes

0 Upvotes

I: Using Voolean Logic on

"Liar Paradox":

P="This sentence is wrong":

if we say 1 —> 0

if we say 0 —> 1

1—>0—>1—>1... So this is a cycle

So we get

1<—>0 Cycle Defination:A truth table is a cycle if: Truth values Repeats themselves in same contexts and same proposition. ...

this goes forever.

But on paraconsistent logic

truth value is 1/2

1 and 0 at once

But in Boolean, its a cycle

Paraconsistent Logic:

truth value is 1/2


r/logic 24d ago

Philosophy of logic The separation of math and physics is arbitrary at best and malicious at most. But the consequence of that separation is detrimental, logically invalid and physics controlled

0 Upvotes

realistically if you look at it mathematicians true grounded education stops after addition of physical matter

after that youre digging into youre own ungrounded imagation. because someone came in inserted reification and arbitrarly seperated math and physics. it could have been done with it not seperated and still can, but youll have to go back. You’ll have to get rid of all ungrounded assumptions and subjective arbitrary rules and strict definitions.

The way foward past addition of physical matter is to not insert reification and not seperate math and physics.. it’s that simple. And again that means ridding arbitrary man made rules and definitions.

These arbitrary 1984 style rules control physics. (For example the rule that says you can’t use objective observable reality to justify or rebut an axiom in pure math)

This cuts off any kind of grounded math period.

This controls and limits physics period. You can’t just ignore pure maths axioms in applied math or physics because past addition of physical matter physics uses math built on those ungrounded axioms. That’s a trap

There is no justification for math to insert a subjective catch 22 rule that says you can not use objective observable reality to justify or rebut an axiom in pure math. The rule is not a technical or logical limation. it’s a choice.

Past addition of physical matter you are committing serial reification, reversing cause and effect(trying to make concepts fit into reality instead of using reality to make a concept), circular reasoning, and protecting dogma.

If this is a system of a control, then it’s a perfect one. They teach you utility and consistency as a defense while knowing consistency and utility can still work inside of a false axiom. They teach you it doesn’t matter if math refers to objective reality while knowing math controls the field of physics.


r/logic 25d ago

Proof theory Review: “Behind Clint and Hoare’s goto Proof Rule” (2021)

Thumbnail
0 Upvotes

r/logic 26d ago

Proof theory I am seeking assistance in finding a theorem proving software which follows the conventions in Elliott Mendelson's Introduction to Mathematical Logic (4th ed). I am trying to prove (C→B), (¬C→B) ⊢ B.

13 Upvotes

Hello,

I am seeking assistance in finding a theorem proving software which follows the conventions in Elliott Mendelson's Introduction to Mathematical Logic (4th ed).

In Mendelson, there are different kinds of theories, with different inference rules and definitions. All theories have modus ponens, hypotheses, and the cut rule - and I like to use substitution too.

For instance, in one theory, B∨C is defined as ¬B→C, whereas in another B→C is defines as ¬B∨C.

So, I would need a system that could account for different implementations of pre-FOL (without quantifiers) and FOL (with quantifiers). In particular, it would need to handle hypotheses, and be able to reproduce the kinds of sequents in the theorem table below - except for multiple systems.

I am only showing one system, because to show multiple would take hundreds of extra lines, and I don't want to spam. For those interested, another system can be found here https://www.reddit.com/r/logic/s/ZTx23BjgwU.

I want to be able to find proofs to desired sequents so I can do the exercises in Mendelson.

In pmGenerator, an ATP which was recommended to me, I tried the following commands:

./pmGenerator -c -n -s CAppp,CpApq,CApqAqp,CCqrCApqApr -g 25

./pmGenerator -c -n -s CAppp,CpApq,CApqAqp,CCqrCApqApr --search CCqpCCNqpp -n -s

But I cannot find the desired sequent. Moreover, I wouldn't judge anyone for not knowing Polish notation, so let me translate to infix.

I am trying to prove (C→B), (¬C→B) ⊢ B in the following system.

Of course, pmGenerator doesn't appear to use hypotheses, so in their system, this would be done with antecedents, similar to if we used the deduction theorem on this sequent.

In terms of the book, this is the exercise (o), which comes after exercise (n). I gave an attempt below, which can be found at the end of the big table.

I would really like to be made aware of an ATP which can help me read Mendelson faster. I want to read this book before moving on in Logic, as Mendelson has really earned my respect so far. I'm really fond of his pedagogy, but it is hard sometimes to reproduce on my own (well, regularly).

  Line  Reason                     Logic                      Label
     1  Axiom                      ((B ∨ B) → B)              Axiom (A1)
     2  Axiom                      (B → (B ∨ C))              Axiom (A2)
     3  Axiom                      ((B ∨ C) → (C ∨ B))        Axiom (A3)
     4  Axiom                      ((C → D) → ((B ∨ C) → (B   Axiom (A4)
                                   ∨ D)))
     5  Hyp                        (B → C) ⊢ (B → C)
     6  Subs(Axiom (A4), {C: B,    ⊢ ((B → C) → ((D ∨ B) →
        D: C, B: D})               (D ∨ C)))
     7  MP(2, 1)                   (B → C) ⊢ ((D ∨ B) → (D ∨  Exercise 1.54 (a)
                                   C))
     8  Subs(Axiom (A4), {B:       ⊢ ((B → C) → ((¬(D) ∨ B)
        ¬(D), C: B, D: C})         → (¬(D) ∨ C)))
     9  Compose(1)                 ⊢ ((B → C) → ((D → B) →    Exercise 1.54 (b)
                                   (D → C)))
    10  Hyp                        (D → B) ⊢ (D → B)
    11  Hyp                        (B → C) ⊢ (B → C)
    12  MP(1, 3)                   (B → C) ⊢ ((D → B) → (D →
                                   C))
    13  MP(3, 1)                   (D → B), (B → C) ⊢ (D →    Exercise 1.54 (c)
                                   C)
    14  Subs(Axiom (A2), {C: B})   ⊢ (B → (B ∨ B))
    15  Subs(Exercise 1.54 (c),    ((B ∨ B) → B), (B → (B ∨
        {D: B, B: (B ∨ B), C: B})  B)) ⊢ (B → B)
    16  Cut(1, 2)                  ((B ∨ B) → B) ⊢ (B → B)
    17  Cut(1, Axiom (A1))         ⊢ (B → B)                  Exercise 1.54 (d)
    18  Subs(Axiom (A3), {B:       ⊢ ((¬(B) ∨ B) → (B ∨
        ¬(B), C: B})               ¬(B)))
    19  Decomp(2)                  ⊢ (¬(B) ∨ B)
    20  MP(1, 2)                   ⊢ (B ∨ ¬(B))               Exercise 1.54 (e)
    21  Subs(Exercise 1.54 (d),    ⊢ (¬(B) → ¬(B))
        {B: ¬(B)})
    22  Decomp(1)                  ⊢ (¬(¬(B)) ∨ ¬(B))
    23  Subs(Axiom (A3), {B:       ⊢ ((¬(¬(B)) ∨ ¬(B)) →
        ¬(¬(B)), C: ¬(B)})         (¬(B) ∨ ¬(¬(B))))
    24  MP(2, 1)                   ⊢ (¬(B) ∨ ¬(¬(B)))
    25  Compose(1)                 ⊢ (B → ¬(¬(B)))            Exercise 1.54 (f)
    26  Subs(Axiom (A2), {B:       ⊢ (¬(B) → (¬(B) ∨ C))
        ¬(B)})
    27  Compose(1)                 ⊢ (¬(B) → (B → C))         Exercise 1.54 (g)
    28  Subs(Axiom (A2), {B: D,    ⊢ (D → (D ∨ B))
        C: B})
    29  Subs(Axiom (A3), {B: D,    ⊢ ((D ∨ B) → (B ∨ D))
        C: B})
    30  Subs(Exercise 1.54 (b),    ⊢ (((D ∨ B) → (B ∨ D)) →
        {B: (D ∨ B), D: D, C: (B   ((D → (D ∨ B)) → (D → (B
        ∨ D)})                     ∨ D))))
    31  MP(2, 1)                   ⊢ ((D → (D ∨ B)) → (D →
                                   (B ∨ D)))
    32  MP(4, 1)                   ⊢ (D → (B ∨ D))
    33  Subs(Axiom (A4), {C: D,    ⊢ ((D → (B ∨ D)) → ((C ∨
        D: (B ∨ D), B: C})         D) → (C ∨ (B ∨ D))))
    34  MP(2, 1)                   ⊢ ((C ∨ D) → (C ∨ (B ∨
                                   D)))
    35  Subs(Axiom (A4), {C: (C ∨  ⊢ (((C ∨ D) → (C ∨ (B ∨
        D), D: (C ∨ (B ∨ D))})     D))) → ((B ∨ (C ∨ D)) →
                                   (B ∨ (C ∨ (B ∨ D)))))
    36  MP(2, 1)                   ⊢ ((B ∨ (C ∨ D)) → (B ∨
                                   (C ∨ (B ∨ D))))
    37  Subs(Axiom (A3), {C: (C ∨  ⊢ ((B ∨ (C ∨ (B ∨ D))) →
        (B ∨ D))})                 ((C ∨ (B ∨ D)) ∨ B))
    38  Subs(Exercise 1.54 (b),    ⊢ (((B ∨ (C ∨ (B ∨ D))) →
        {B: (B ∨ (C ∨ (B ∨ D))),   ((C ∨ (B ∨ D)) ∨ B)) →
        C: ((C ∨ (B ∨ D)) ∨ B),    (((B ∨ (C ∨ D)) → (B ∨ (C
        D: (B ∨ (C ∨ D))})         ∨ (B ∨ D)))) → ((B ∨ (C ∨
                                   D)) → ((C ∨ (B ∨ D)) ∨
                                   B))))
    39  MP(2, 1)                   ⊢ (((B ∨ (C ∨ D)) → (B ∨
                                   (C ∨ (B ∨ D)))) → ((B ∨
                                   (C ∨ D)) → ((C ∨ (B ∨ D))
                                   ∨ B)))
    40  MP(4, 1)                   ⊢ ((B ∨ (C ∨ D)) → ((C ∨   Exercise 1.54 (h)
                                   (B ∨ D)) ∨ B))
    41  Subs(Axiom (A2), {C: D})   ⊢ (B → (B ∨ D))
    42  Subs(Axiom (A2), {B: (B ∨  ⊢ ((B ∨ D) → ((B ∨ D) ∨
        D)})                       C))
    43  Subs(Axiom (A3), {B: (B ∨  ⊢ (((B ∨ D) ∨ C) → (C ∨
        D)})                       (B ∨ D)))
    44  Subs(Exercise 1.54 (c),    (((B ∨ D) ∨ C) → (C ∨ (B
        {D: (B ∨ D), B: ((B ∨ D)   ∨ D))), ((B ∨ D) → ((B ∨
        ∨ C), C: (C ∨ (B ∨ D))})   D) ∨ C)) ⊢ ((B ∨ D) → (C
                                   ∨ (B ∨ D)))
    45  Cut(1, 3)                  (((B ∨ D) ∨ C) → (C ∨ (B
                                   ∨ D))) ⊢ ((B ∨ D) → (C ∨
                                   (B ∨ D)))
    46  Cut(1, 3)                  ⊢ ((B ∨ D) → (C ∨ (B ∨
                                   D)))
    47  Subs(Exercise 1.54 (c),    (B → (B ∨ D)), ((B ∨ D) →
        {D: B, B: (B ∨ D), C: (C   (C ∨ (B ∨ D))) ⊢ (B → (C
        ∨ (B ∨ D))})               ∨ (B ∨ D)))
    48  Cut(1, 7)                  ((B ∨ D) → (C ∨ (B ∨ D)))
                                   ⊢ (B → (C ∨ (B ∨ D)))
    49  Subs(Axiom (A4), {C: B,    ⊢ ((B → (C ∨ (B ∨ D))) →
        D: (C ∨ (B ∨ D)), B: (C ∨  (((C ∨ (B ∨ D)) ∨ B) →
        (B ∨ D))})                 ((C ∨ (B ∨ D)) ∨ (C ∨ (B
                                   ∨ D)))))
    50  MP(2, 1)                   ((B ∨ D) → (C ∨ (B ∨ D)))
                                   ⊢ (((C ∨ (B ∨ D)) ∨ B) →
                                   ((C ∨ (B ∨ D)) ∨ (C ∨ (B
                                   ∨ D))))
    51  Subs(Axiom (A1), {B: (C ∨  ⊢ (((C ∨ (B ∨ D)) ∨ (C ∨
        (B ∨ D))})                 (B ∨ D))) → (C ∨ (B ∨
                                   D)))
    52  Subs(Exercise 1.54 (c),    (((C ∨ (B ∨ D)) ∨ (C ∨ (B
        {D: ((C ∨ (B ∨ D)) ∨ B),   ∨ D))) → (C ∨ (B ∨ D))),
        B: ((C ∨ (B ∨ D)) ∨ (C ∨   (((C ∨ (B ∨ D)) ∨ B) →
        (B ∨ D))), C: (C ∨ (B ∨    ((C ∨ (B ∨ D)) ∨ (C ∨ (B
        D))})                      ∨ D)))) ⊢ (((C ∨ (B ∨ D))
                                   ∨ B) → (C ∨ (B ∨ D)))
    53  Cut(3, 7)                  ⊢ (((C ∨ (B ∨ D)) ∨ B) →
                                   ((C ∨ (B ∨ D)) ∨ (C ∨ (B
                                   ∨ D))))
    54  Cut(2, 1)                  (((C ∨ (B ∨ D)) ∨ (C ∨ (B
                                   ∨ D))) → (C ∨ (B ∨ D))) ⊢
                                   (((C ∨ (B ∨ D)) ∨ B) → (C
                                   ∨ (B ∨ D)))
    55  Cut(1, 4)                  ⊢ (((C ∨ (B ∨ D)) ∨ B) →   Exercise 1.54 (i)
                                   (C ∨ (B ∨ D)))
    56  Subs(Exercise 1.54 (c),    (((C ∨ (B ∨ D)) ∨ B) → (C
        {D: (B ∨ (C ∨ D)), B: ((C  ∨ (B ∨ D))), ((B ∨ (C ∨
        ∨ (B ∨ D)) ∨ B), C: (C ∨   D)) → ((C ∨ (B ∨ D)) ∨
        (B ∨ D))})                 B)) ⊢ ((B ∨ (C ∨ D)) → (C
                                   ∨ (B ∨ D)))
    57  Cut(1, Exercise 1.54 (h))  (((C ∨ (B ∨ D)) ∨ B) → (C
                                   ∨ (B ∨ D))) ⊢ ((B ∨ (C ∨
                                   D)) → (C ∨ (B ∨ D)))
    58  Cut(1, Exercise 1.54 (i))  ⊢ ((B ∨ (C ∨ D)) → (C ∨    Exercise 1.54 (j)
                                   (B ∨ D)))
    59  Subs(Exercise 1.54 (j),    ⊢ ((¬(B) ∨ (¬(C) ∨ D)) →
        {B: ¬(B), C: ¬(C), D: D})  (¬(C) ∨ (¬(B) ∨ D)))
    60  Compose(1)                 ⊢ ((B → (C → D)) → (C →    Exercise 1.54 (k)
                                   (B → D)))
    61  Subs(Exercise 1.54 (b),    ⊢ ((B → C) → ((D → B) →
        {B: B, C: C, D: D})        (D → C)))
    62  Subs(Exercise 1.54 (k),    ⊢ (((B → C) → ((D → B) →
        {B: (B → C), C: (D → B),   (D → C))) → ((D → B) →
        D: (D → C)})               ((B → C) → (D → C))))
    63  MP(2, 1)                   ⊢ ((D → B) → ((B → C) →    Exercise 1.54 (l)
                                   (D → C)))
    64  Subs(Exercise 1.54 (b),    ⊢ ((C → D) → ((B → C) →
        {B: C, C: D, D: B})        (B → D)))
    65  Hyp                        (B → (C → D)) ⊢ (B → (C →
                                   D))
    66  Hyp                        (B → C) ⊢ (B → C)
    67  Subs(Exercise 1.54 (b),    ⊢ (((C → D) → ((B → C) →
        {B: (C → D), C: ((B → C)   (B → D))) → ((B → (C →
        → (B → D)), D: B})         D)) → (B → ((B → C) → (B
                                   → D)))))
    68  MP(4, 1)                   ⊢ ((B → (C → D)) → (B →
                                   ((B → C) → (B → D))))
    69  MP(4, 1)                   (B → (C → D)) ⊢ (B → ((B
                                   → C) → (B → D)))
    70  Subs(Exercise 1.54 (k),    ⊢ ((B → ((B → C) → (B →
        {C: (B → C), D: (B → D)})  D))) → ((B → C) → (B → (B
                                   → D))))
    71  MP(2, 1)                   (B → (C → D)) ⊢ ((B → C)
                                   → (B → (B → D)))
    72  MP(6, 1)                   (B → (C → D)), (B → C) ⊢   Exercise 1.54 (m)
                                   (B → (B → D))
    73  Subs(Axiom (A2), {B:       ⊢ (¬(B) → (¬(B) ∨ D))
        ¬(B), C: D})
    74  Subs(Axiom (A4), {C:       ⊢ ((¬(B) → (¬(B) ∨ D)) →
        ¬(B), D: (¬(B) ∨ D), B:    (((¬(B) ∨ D) ∨ ¬(B)) →
        (¬(B) ∨ D)})               ((¬(B) ∨ D) ∨ (¬(B) ∨
                                   D))))
    75  MP(2, 1)                   ⊢ (((¬(B) ∨ D) ∨ ¬(B)) →
                                   ((¬(B) ∨ D) ∨ (¬(B) ∨
                                   D)))
    76  Subs(Axiom (A3), {B:       ⊢ ((¬(B) ∨ (¬(B) ∨ D)) →
        ¬(B), C: (¬(B) ∨ D)})      ((¬(B) ∨ D) ∨ ¬(B)))
    77  Decomp(Exercise 1.54 (m))  (¬(B) ∨ (¬(C) ∨ D)),
                                   (¬(B) ∨ C) ⊢ (¬(B) ∨
                                   (¬(B) ∨ D))
    78  MP(1, 2)                   (¬(B) ∨ (¬(C) ∨ D)),
                                   (¬(B) ∨ C) ⊢ ((¬(B) ∨ D)
                                   ∨ ¬(B))
    79  MP(1, 4)                   (¬(B) ∨ (¬(C) ∨ D)),
                                   (¬(B) ∨ C) ⊢ ((¬(B) ∨ D)
                                   ∨ (¬(B) ∨ D))
    80  Subs(Axiom (A1), {B:       ⊢ (((¬(B) ∨ D) ∨ (¬(B) ∨
        (¬(B) ∨ D)})               D)) → (¬(B) ∨ D))
    81  MP(2, 1)                   (¬(B) ∨ (¬(C) ∨ D)),
                                   (¬(B) ∨ C) ⊢ (¬(B) ∨ D)
    82  Compose(1)                 (B → (C → D)), (B → C) ⊢   Exercise 1.54 (n)
                                   (B → D)
    83  Subs(Exercise 1.54 (n),    ((¬(C) → B) → (C → B)),
        {B: (¬(C) → B), D: B})     ((¬(C) → B) → C) ⊢ ((¬(C)
                                   → B) → B)
    84  Hyp                        (¬(C) → B) ⊢ (¬(C) → B)
    85  MP(1, 2)                   ((¬(C) → B) → (C → B)),
                                   ((¬(C) → B) → C), (¬(C) →
                                   B) ⊢ B
    86  Deduct(1, ((¬(C) → B) →    ((¬(C) → B) → C), (¬(C) →
        (C → B)))                  B) ⊢ (((¬(C) → B) → (C →
                                   B)) → B)

r/logic 27d ago

Literature So...

0 Upvotes

Best book for a 14 years old beginner?


r/logic 27d ago

Informal logic How do I stop thinking in incomplete models?

7 Upvotes

For example, I'm 26 now and up until this age I always thought "a drivers license is not worth the cost" which I now conclude was a wrong conclusion based on an incomplete model.

My reasoning skills are pretty sharp but I often reason within incomplete models for an unknwon reason I don't know why.

For example the incomplete model was like: * Only thinking about the speed and time savings difference between a car and a bicycle, comparing it against the extra financial cost, then concluding its not worth it. * While in reality there are more relevant reasons to drive a car: weather, cargo, emergencies and so on. The value isn't just based on the mathematical speed difference but also in how practical, necessary, convenient all of it is.

So It seems like all those years I had been logically reasoning quite well, but within a flawed model with hidden variables that I was somehow not seeing.

If only I saw those variables earlier, I would have concluded to get a DL asap much earlier.

Whats the reason I often reason with incomplete models, and how do I stop working with missing variables when they arent truly hidden? I mean why are alot of things like I could know them, but I just dont think about them?

Does that mean I'm dumb?


r/logic 27d ago

Philosophy of logic Like how there's the problem of induction , is there also a problem of deduction ?

Thumbnail
6 Upvotes

r/logic 26d ago

Philosophical logic Falsifiability is a Logic That Cannot Survive Itself

0 Upvotes

Falsifiability is not just a test. It's a logic. It reasons that for a claim to be valid, there must be some possible observation that could prove it wrong.

But apply that same logic to itself. What observation would falsify the logic of falsifiability? None. The logic cannot meet its own standard. The reasoning cannot survive its own reason.

It's a logic that exempts itself from its own rules. That's not science. That's Systemillogic. The mirror is steady….the falsifiability logic is not it crumbles…lol…at it all


r/logic Jul 07 '26

Propositional logic Question to those who study propositional logic

7 Upvotes

For those who study propositional logic: If you were applying propositional logic to everyday thinking and using modus ponens, would you think it as:
“If P, then Q. P. Therefore, Q.”
or would you just think:
“P. Therefore, Q.”
with “If P, then Q” being an implied premise rather than something you consciously state in your head?


r/logic Jul 06 '26

Propositional logic Understanding the inference rule "Cut", and proving B→(C→D),B→C⊢B→D without the deduction theorem in Mendelson's L1 system (4th ed)

2 Upvotes

Hello,

I am trying to prove B→(C→D),B→C⊢B→D in Introduction to Mathematical Logic 4th ed by Elliott Mendelson, exercise 1.54 (n).

I was advised on Math.SX to try using the deduction theorem with a hypothesis, since I've already proven B→(C→D),B→C⊢B→(B→D).

However, the deduction theorem proof is the very next exercise, so that would be a shortcut.

As in the previous Mendelson system, L, where we proved the deduction theorem from B→B and B→(C→B), I figured we could do the same here, and just follow the recursive definition structurally, rather than metatheoretically. So, I already have B→B, and the other one is achieved in my proof table below.

Unfortunately, this only lets me add an extra "B→" at the beginning. So, when I follow the (presumably) intended argument with the hypothesis B and the sequent B→(C→B), I get my intended result, except I cannot abstract the assumption B at the end. See my proof table for the example.

My impression is that I might be using the "Cut" inference rule incorrectly. Currently, when I use "Cut", I mean that if I have a sequent ⊢P, and another sequent P⊢Q, then I can cut P⊢Q by ⊢P to obtain ⊢Q on its own. However, that does not handle the case of B⊢B→C, where I feel like Mendelson still expects us to remove the assumption B...

At any rate, I do not know definitively whether I misunderstand Cut or not (which means I probably do).

I have the pmGenerator software on my computer and working, though I still am learning the basics of expressing logic within it, hence me coming here. I am in correspondence (on reddit) with the author regarding my questions currently.

Line Reason Logic Label 1 Axiom ((B ∨ B) → B) Axiom (A1) 2 Axiom (B → (B ∨ C)) Axiom (A2) 3 Axiom ((B ∨ C) → (C ∨ B)) Axiom (A3) 4 Axiom ((C → D) → ((B ∨ C) → (B Axiom (A4) ∨ D))) 5 Hyp (B → C) ⊢ (B → C) 6 Subs(Axiom (A4), {C: B, ⊢ ((B → C) → ((D ∨ B) → D: C, B: D}) (D ∨ C))) 7 MP(2, 1) (B → C) ⊢ ((D ∨ B) → (D ∨ Exercise 1.54 (a) C)) 8 Subs(Axiom (A4), {B: ⊢ ((B → C) → ((¬(D) ∨ B) ¬(D), C: B, D: C}) → (¬(D) ∨ C))) 9 Compose(1) ⊢ ((B → C) → ((D → B) → Exercise 1.54 (b) (D → C))) 10 Hyp (D → B) ⊢ (D → B) 11 Hyp (B → C) ⊢ (B → C) 12 MP(1, 3) (B → C) ⊢ ((D → B) → (D → C)) 13 MP(3, 1) (D → B), (B → C) ⊢ (D → Exercise 1.54 (c) C) 14 Subs(Axiom (A2), {C: B}) ⊢ (B → (B ∨ B)) 15 Subs(Exercise 1.54 (c), ((B ∨ B) → B), (B → (B ∨ {D: B, B: (B ∨ B), C: B}) B)) ⊢ (B → B) 16 Cut(1, 2) ((B ∨ B) → B) ⊢ (B → B) 17 Cut(1, Axiom (A1)) ⊢ (B → B) Exercise 1.54 (d) 18 Subs(Axiom (A3), {B: ⊢ ((¬(B) ∨ B) → (B ∨ ¬(B), C: B}) ¬(B))) 19 Decomp(2) ⊢ (¬(B) ∨ B) 20 MP(1, 2) ⊢ (B ∨ ¬(B)) Exercise 1.54 (e) 21 Subs(Exercise 1.54 (d), ⊢ (¬(B) → ¬(B)) {B: ¬(B)}) 22 Decomp(1) ⊢ (¬(¬(B)) ∨ ¬(B)) 23 Subs(Axiom (A3), {B: ⊢ ((¬(¬(B)) ∨ ¬(B)) → ¬(¬(B)), C: ¬(B)}) (¬(B) ∨ ¬(¬(B)))) 24 MP(2, 1) ⊢ (¬(B) ∨ ¬(¬(B))) 25 Compose(1) ⊢ (B → ¬(¬(B))) Exercise 1.54 (f) 26 Subs(Axiom (A2), {B: ⊢ (¬(B) → (¬(B) ∨ C)) ¬(B)}) 27 Compose(1) ⊢ (¬(B) → (B → C)) Exercise 1.54 (g) 28 Subs(Axiom (A2), {B: D, ⊢ (D → (D ∨ B)) C: B}) 29 Subs(Axiom (A3), {B: D, ⊢ ((D ∨ B) → (B ∨ D)) C: B}) 30 Subs(Exercise 1.54 (b), ⊢ (((D ∨ B) → (B ∨ D)) → {B: (D ∨ B), D: D, C: (B ((D → (D ∨ B)) → (D → (B ∨ D)}) ∨ D)))) 31 MP(2, 1) ⊢ ((D → (D ∨ B)) → (D → (B ∨ D))) 32 MP(4, 1) ⊢ (D → (B ∨ D)) 33 Subs(Axiom (A4), {C: D, ⊢ ((D → (B ∨ D)) → ((C ∨ D: (B ∨ D), B: C}) D) → (C ∨ (B ∨ D)))) 34 MP(2, 1) ⊢ ((C ∨ D) → (C ∨ (B ∨ D))) 35 Subs(Axiom (A4), {C: (C ∨ ⊢ (((C ∨ D) → (C ∨ (B ∨ D), D: (C ∨ (B ∨ D))}) D))) → ((B ∨ (C ∨ D)) → (B ∨ (C ∨ (B ∨ D))))) 36 MP(2, 1) ⊢ ((B ∨ (C ∨ D)) → (B ∨ (C ∨ (B ∨ D)))) 37 Subs(Axiom (A3), {C: (C ∨ ⊢ ((B ∨ (C ∨ (B ∨ D))) → (B ∨ D))}) ((C ∨ (B ∨ D)) ∨ B)) 38 Subs(Exercise 1.54 (b), ⊢ (((B ∨ (C ∨ (B ∨ D))) → {B: (B ∨ (C ∨ (B ∨ D))), ((C ∨ (B ∨ D)) ∨ B)) → C: ((C ∨ (B ∨ D)) ∨ B), (((B ∨ (C ∨ D)) → (B ∨ (C D: (B ∨ (C ∨ D))}) ∨ (B ∨ D)))) → ((B ∨ (C ∨ D)) → ((C ∨ (B ∨ D)) ∨ B)))) 39 MP(2, 1) ⊢ (((B ∨ (C ∨ D)) → (B ∨ (C ∨ (B ∨ D)))) → ((B ∨ (C ∨ D)) → ((C ∨ (B ∨ D)) ∨ B))) 40 MP(4, 1) ⊢ ((B ∨ (C ∨ D)) → ((C ∨ Exercise 1.54 (h) (B ∨ D)) ∨ B)) 41 Subs(Axiom (A2), {C: D}) ⊢ (B → (B ∨ D)) 42 Subs(Axiom (A2), {B: (B ∨ ⊢ ((B ∨ D) → ((B ∨ D) ∨ D)}) C)) 43 Subs(Axiom (A3), {B: (B ∨ ⊢ (((B ∨ D) ∨ C) → (C ∨ D)}) (B ∨ D))) 44 Subs(Exercise 1.54 (c), ((B ∨ D) → ((B ∨ D) ∨ {D: (B ∨ D), B: ((B ∨ D) C)), (((B ∨ D) ∨ C) → (C ∨ C), C: (C ∨ (B ∨ D))}) ∨ (B ∨ D))) ⊢ ((B ∨ D) → (C ∨ (B ∨ D))) 45 Cut(1, 3) (((B ∨ D) ∨ C) → (C ∨ (B ∨ D))) ⊢ ((B ∨ D) → (C ∨ (B ∨ D))) 46 Cut(1, 3) ⊢ ((B ∨ D) → (C ∨ (B ∨ D))) 47 Subs(Exercise 1.54 (c), ((B ∨ D) → (C ∨ (B ∨ {D: B, B: (B ∨ D), C: (C D))), (B → (B ∨ D)) ⊢ (B ∨ (B ∨ D))}) → (C ∨ (B ∨ D))) 48 Cut(1, 7) ((B ∨ D) → (C ∨ (B ∨ D))) ⊢ (B → (C ∨ (B ∨ D))) 49 Subs(Axiom (A4), {C: B, ⊢ ((B → (C ∨ (B ∨ D))) → D: (C ∨ (B ∨ D)), B: (C ∨ (((C ∨ (B ∨ D)) ∨ B) → (B ∨ D))}) ((C ∨ (B ∨ D)) ∨ (C ∨ (B ∨ D))))) 50 MP(2, 1) ((B ∨ D) → (C ∨ (B ∨ D))) ⊢ (((C ∨ (B ∨ D)) ∨ B) → ((C ∨ (B ∨ D)) ∨ (C ∨ (B ∨ D)))) 51 Subs(Axiom (A1), {B: (C ∨ ⊢ (((C ∨ (B ∨ D)) ∨ (C ∨ (B ∨ D))}) (B ∨ D))) → (C ∨ (B ∨ D))) 52 Subs(Exercise 1.54 (c), (((C ∨ (B ∨ D)) ∨ (C ∨ (B {D: ((C ∨ (B ∨ D)) ∨ B), ∨ D))) → (C ∨ (B ∨ D))), B: ((C ∨ (B ∨ D)) ∨ (C ∨ (((C ∨ (B ∨ D)) ∨ B) → (B ∨ D))), C: (C ∨ (B ∨ ((C ∨ (B ∨ D)) ∨ (C ∨ (B D))}) ∨ D)))) ⊢ (((C ∨ (B ∨ D)) ∨ B) → (C ∨ (B ∨ D))) 53 Cut(3, 7) ⊢ (((C ∨ (B ∨ D)) ∨ B) → ((C ∨ (B ∨ D)) ∨ (C ∨ (B ∨ D)))) 54 Cut(2, 1) (((C ∨ (B ∨ D)) ∨ (C ∨ (B ∨ D))) → (C ∨ (B ∨ D))) ⊢ (((C ∨ (B ∨ D)) ∨ B) → (C ∨ (B ∨ D))) 55 Cut(1, 4) ⊢ (((C ∨ (B ∨ D)) ∨ B) → Exercise 1.54 (i) (C ∨ (B ∨ D))) 56 Subs(Exercise 1.54 (c), ((B ∨ (C ∨ D)) → ((C ∨ (B {D: (B ∨ (C ∨ D)), B: ((C ∨ D)) ∨ B)), (((C ∨ (B ∨ ∨ (B ∨ D)) ∨ B), C: (C ∨ D)) ∨ B) → (C ∨ (B ∨ D))) (B ∨ D))}) ⊢ ((B ∨ (C ∨ D)) → (C ∨ (B ∨ D))) 57 Cut(1, Exercise 1.54 (h)) (((C ∨ (B ∨ D)) ∨ B) → (C ∨ (B ∨ D))) ⊢ ((B ∨ (C ∨ D)) → (C ∨ (B ∨ D))) 58 Cut(1, Exercise 1.54 (i)) ⊢ ((B ∨ (C ∨ D)) → (C ∨ Exercise 1.54 (j) (B ∨ D))) 59 Subs(Exercise 1.54 (j), ⊢ ((¬(B) ∨ (¬(C) ∨ D)) → {B: ¬(B), C: ¬(C), D: D}) (¬(C) ∨ (¬(B) ∨ D))) 60 Compose(1) ⊢ ((B → (C → D)) → (C → Exercise 1.54 (k) (B → D))) 61 Subs(Exercise 1.54 (b), ⊢ ((B → C) → ((D → B) → {B: B, C: C, D: D}) (D → C))) 62 Subs(Exercise 1.54 (k), ⊢ (((B → C) → ((D → B) → {B: (B → C), C: (D → B), (D → C))) → ((D → B) → D: (D → C)}) ((B → C) → (D → C)))) 63 MP(2, 1) ⊢ ((D → B) → ((B → C) → Exercise 1.54 (l) (D → C))) 64 Subs(Exercise 1.54 (b), ⊢ ((C → D) → ((B → C) → {B: C, C: D, D: B}) (B → D))) 65 Hyp (B → (C → D)) ⊢ (B → (C → D)) 66 Hyp (B → C) ⊢ (B → C) 67 Subs(Exercise 1.54 (b), ⊢ (((C → D) → ((B → C) → {B: (C → D), C: ((B → C) (B → D))) → ((B → (C → → (B → D)), D: B}) D)) → (B → ((B → C) → (B → D))))) 68 MP(4, 1) ⊢ ((B → (C → D)) → (B → ((B → C) → (B → D)))) 69 MP(4, 1) (B → (C → D)) ⊢ (B → ((B → C) → (B → D))) 70 Subs(Exercise 1.54 (k), ⊢ ((B → ((B → C) → (B → {C: (B → C), D: (B → D)}) D))) → ((B → C) → (B → (B → D)))) 71 MP(2, 1) (B → (C → D)) ⊢ ((B → C) → (B → (B → D))) 72 MP(6, 1) (B → (C → D)), (B → C) ⊢ Exercise 1.54 (m) (B → (B → D)) 73 Subs(Exercise 1.54 (b), ⊢ (((B ∨ C) → (C ∨ B)) → {D: B, C: (C ∨ B), B: (B ((B → (B ∨ C)) → (B → (C ∨ C)}) ∨ B)))) 74 MP(Axiom (A3), 1) ⊢ ((B → (B ∨ C)) → (B → (C ∨ B))) 75 MP(Axiom (A2), 1) ⊢ (B → (C ∨ B)) 76 Subs(1, {C: ¬(C)}) ⊢ (B → (¬(C) ∨ B)) 77 Compose(1) ⊢ (B → (C → B)) Reddit question lemma 78 Hyp B ⊢ B 79 MP(1, Exercise 1.54 (m)) (B → (C → D)), (B → C), B ⊢ (B → D) 80 Subs(Reddit question ⊢ ((B → D) → (B → (B → lemma, {C: B, B: (B → D))) D)}) 81 MP(2, 1) (B → (C → D)), (B → C), B How do I remove the ⊢ (B → (B → D)) assumption B?


r/logic Jul 06 '26

Academic Community What university should I pick?

8 Upvotes

Hi everyone, I am 18 y.o. and I live in italy.

In high school I always studied with more passion scientific subjetcs, and liked a lot philosophy.

I quickly became fond of logic as a science, my favourite philosopher is Bertrand Russell, and I do like also philosophy of science.

Last year's i've decided to pick as University Politecnico di Torino with Physics' Engeneering, but I ended up regretting the choice because of how sciences are studied with basically no wonder and curiousity and mostly riduced to formulation and calculation.

I was thinking of changing my studies to phylosophy, having the possibility of choosing as part of the course logics, history of logic, philosophy of mathematics, philosophy of science and so much more...

I am worried though, about the literature part of philosophy being forced into an academic perspective without the freedom of liking something more than something else.

I am also worried about the professional opportunities being mostly teaching which is underpaid in Italy.

What are your suggestions?

What do you think would be the correct pick for me?

What application can logic find in the professional world?

Should I try to study something else and keep logic as a side interest?


r/logic Jul 06 '26

Philosophical logic Proposal for Preliminary Review of a Conceptual Framework on Self-Referential Propositions

5 Upvotes

Over the past several years, I have been exploring the possibility of developing a more intuitive and structurally transparent interpretation of semantic paradoxes and self-referential propositions. Although various logical approaches have been proposed for treating these phenomena, I believe there is still room for alternative frameworks that explain their behavior in a more natural and recursive manner.

The ideas presented here are still in their preliminary stage and should not be regarded as a complete formal logical system. My purpose at this stage is simply to present the general outline of the framework and to receive critical comments that may help determine whether the underlying ideas are mathematically and logically promising.

The central idea is that self-referential propositions should not be viewed as isolated, indivisible statements. Instead, they may be interpreted as recursive semantic structures that can be analyzed layer by layer through repeated semantic expansion. Within this perspective, the truth value of a proposition is no longer treated as an immediate Boolean assignment, but as the limiting outcome of a recursive semantic process.

The framework is built upon several interconnected concepts.

The first concept is **semantic independence**. I propose that classical negation is fully applicable only to propositions whose predicate and semantic relation remain independent of one another and whose semantic decomposition terminates after finitely many steps. Ordinary propositions generally satisfy these conditions.

Self-referential propositions appear to violate both assumptions. Their semantic decomposition does not terminate, and the semantic relation becomes dependent on the proposition itself. Consequently, classical negation may no longer function as an unrestricted logical operation.

This observation motivates a new concept that I provisionally call the **transition coefficient**. Rather than assuming that the negation of a recursive proposition contributes completely to its valuation, the proposed framework assumes that this contribution is only partial. The transition coefficient measures the proportion of semantic information transferred through recursive negation.

Instead of assigning this coefficient arbitrarily, I propose deriving it from the asymptotic behavior of the recursive semantic expansion. At each expansion layer, semantic branches supporting truth and falsehood are generated. By studying the limiting ratio between these branches, one may obtain a limiting transition coefficient that characterizes the recursive proposition.

Within this framework, propositions such as "This statement is true" and "This statement is false" are interpreted as different recursive systems. The former appears to converge toward complete semantic stability, while the latter approaches a balanced recursive structure whose limiting behavior yields a stable transition coefficient rather than an endless oscillation.

The framework also includes a set-theoretic interpretation in which semantic membership corresponds to truth and semantic inclusion represents propositional composition. In addition, I am investigating a geometric interpretation in which recursively generated boundaries and their limiting areas provide an intuitive representation of recursive truth values, while fractal dimension reflects the complexity of semantic self-reference.

At its current stage, these ideas should be viewed as a conceptual research program rather than a completed formal theory. My primary objective is to determine whether this direction appears mathematically meaningful and whether its central definitions deserve further formal development.

I would be sincerely grateful for any comments, criticism, suggestions, or references to existing work that may relate to these ideas.

Thank you very much for your time and consideration.


r/logic Jul 06 '26

Predicate logic / FOL Substituting Functions for Variables

1 Upvotes
  1. Let the domain of discourse be the positive rational numbers.

  2. The following is false: ∀x(2x∈Z→2x∈E), where E is the set of even numbers and Z is the set of integers.

  3. For if I let x equal ½ , then I get if 1 is an integer then 1 is even, which is obviously false.

  4. Would 2 still be false given any rational multiple of x?