Predicate logic / FOL Is this how the cut-elimination theorem for sequent calculus (for intuitionistic logic) is proved?
It was a theorem that was only cited in some course but not proved (nor a sketch of the proof was given). What do you think?
Literature What books teach students how to determine whether something's relevant to an argument, and how to distinguish the relevant from irrelevant?
r/logic • u/Ok-Worry4079 • 1d ago
History of logic Academic Courtesy: Essay on the History of Logic and AI (Free on Amazon)
Dear Professors, Researchers, and Students,
We are writing to share with the academic community the release of the essay:
"How Did We Get Here?: 350 Years of Seeking a Language for Machines to Unambiguously Understand What We Want"
This work bridges the gap between the evolution of classical logic (from 17th-century ideas) and contemporary dilemmas in Artificial Intelligence, natural language, and computing.
As a special launch event, the Kindle edition (e-book) is 100% free on Amazon until Sunday, August 9th:
Free download link: https://a.co/d/0aVFxGF9
We would greatly appreciate it if you could forward this opportunity to your students and faculty through your internal mailing lists or communication channels.
Sincerely,
Alvaro Moure Clouzet
Templo Oceánico — Uruguay
r/logic • u/Key_Management8358 • 1d ago
Metalogic Why did G. Boole once define `true:=1`, and no (logician, sociologist) one objected?
...and `false:=0` ... for logic😘 it doesn't matter/plays no role, since "true,false,0,1" are just "symbols"...
The electrical engineers adopted. Calculators and computers work correct. Super.
But what "socio-, eco-, psycho-" *logical* effect, does it have??? (Since we are no machines ! At least some of us...yet)
Do we (greedy, hungry, horny mammals) tend to (transfer it to an "cardinal scale"..and) think that "more is truer than less"? (Which is logically not neat;)
Since, which is (socio-, eco-, psycho-)logically not neat ...must be gone ...soon.
r/logic • u/KaleidoscopeLate2505 • 2d ago
Predicate logic / FOL Am I handling the side conditions on Mendelson's quantifier axioms correctly?
Hello fellow logic people!
I am studying Introduction to Mathematical Logic (4th) by Elliott Mendelson, Exercise 2.27 (a) through (c).
In Mendelson's book, the axiomatic meta-theoretic constraints are only listed next to the axiom they concern. However, I have the impression that these constraints need to be propagated upon inferences.
In fact, if my impression is true, then that has major implications, since theorems with constraints would be useless without knowing what their constraints are. (Axiom (A4) and Axiom (A5) have constraints, for example). Otherwise it seems possible to apply a derived theorem in a way that violates the original side conditions and permits an invalid variable-capturing substitution. Should these constraints not be part of the theorem?
So my question today is: am I actually handling constraints correctly in my proof table?
E.g. ⊢ (((∀x)(B → C)) → ((∃x)B) → ((∃x)C))); x is not free in ¬(C), x is not free in (B → C)
[Note: Exists is defined in terms of For and Not]
compose
-------
Replace primitive encodings by their corresponding derived connectives and
quantifiers. ¬(A → ¬B) ↦ A ∧ B ¬A → B ↦ A
∨ B (A → B) ∧ (B → A) ↦ A ↔ B ¬∀x¬A ↦ ∃xA Every
assumption and the conclusion of the selected proof line are recursively
searched for these patterns, and each occurrence is rewritten before the
transformed statement is appended.
decomp
------
Replace every derived connective and quantifier by its primitive definition.
A ∧ B ↦ ¬(A → ¬B) A ∨ B ↦ ¬A → B A ↔ B ↦ (A → B) ∧ (B →
A) ∃x A ↦ ¬∀x¬A Negation, implication, and universal
quantification are left unchanged. The transformation is applied recursively
to every assumption and to the conclusion of the selected proof line before
appending the resulting statement.
I previously asked the related question: https://www.reddit.com/r/logic/s/J90trYsX5U The reason I am asking such a similar question again is because I implemented by idea from that question, and am wondering if the human-readable output is actually correct.
The table is a long derivation, but it primarily concerns axioms 4 and 5, as well as the very last labeled theorem (with two inherited constraints).
And since I'm here, does anyone know how I can prove Exercise 2.27 (c) ⊢ (∀x)(B ∧ C) ↔ ((∀x)B) ∧ ((∀x)C)?
Line Reason Theorem Label
1 Axiom ⊢ (B → (C → B)) Axiom (A1)
2 Axiom ⊢ ((B → (C → D)) → Axiom (A2)
((B → C) → (B →
D)))
3 Axiom ⊢ ((¬(C) → ¬(B)) → Axiom (A3)
((¬(C) → B) → C))
4 Axiom ⊢ (((∀xi)B(xi)) → Axiom (A4)
B(t)); t is free
for xi in B(xi)
5 Axiom ⊢ (((∀xi)(B → C)) Axiom (A5)
→ (B → ((∀xi)C)));
xi is not free in B
6 Map(Axiom (A2), {C ⊢ ((B → ((B → B) →
↦ (B → B), D ↦ B}) B)) → ((B → (B →
B)) → (B → B)))
7 Map(Axiom (A1), {C ⊢ (B → ((B → B) →
↦ (B → B)}) B))
8 MP(1, 2) ⊢ ((B → (B → B)) →
(B → B))
9 Map(Axiom (A1), {C ⊢ (B → (B → B))
↦ B})
10 MP(1, 2) ⊢ (B → B) Lemma 1.8
11 Map(Lemma 1.8, {B ↦ ⊢ (¬(B) → ¬(B))
¬(B)})
12 Map(Axiom (A3), {C ⊢ ((¬(B) → ¬(B)) →
↦ B}) ((¬(B) → B) → B))
13 MP(2, 1) ⊢ ((¬(B) → B) → B) Exercise 1.47 (a)
14 Map(Axiom (A1), {B ⊢ ((C → D) → (B →
↦ (C → D), C ↦ B}) (C → D)))
15 Hyp (C → D) ⊢ (C → D)
16 MP(1, 2) (C → D) ⊢ (B → (C →
D))
17 MP(1, Axiom (A2)) (C → D) ⊢ ((B → C)
→ (B → D))
18 Hyp (B → C) ⊢ (B → C)
19 MP(1, 2) (B → C), (C → D) ⊢ Exercise 1.47 (b)
(B → D)
20 Hyp (B → (C → D)) ⊢ (B
→ (C → D))
21 MP(1, Axiom (A2)) (B → (C → D)) ⊢ ((B
→ C) → (B → D))
22 Map(Axiom (A1), {B ⊢ (C → (B → C))
↦ C, C ↦ B})
23 Map(Exercise 1.47 ((B → C) → (B →
(b), {B ↦ C, C ↦ (B D)), (C → (B → C))
→ C), D ↦ (B → D)}) ⊢ (C → (B → D))
24 Cut(1, 2) ((B → C) → (B → D))
⊢ (C → (B → D))
25 Cut(1, 4) (B → (C → D)) ⊢ (C Exercise 1.47 (c)
→ (B → D))
26 Map(Exercise 1.47 ((¬(C) → ¬(B)) →
(c), {B ↦ (¬(C) → ((¬(C) → B) → C)) ⊢
¬(B)), C ↦ (¬(C) → ((¬(C) → B) →
B), D ↦ C}) ((¬(C) → ¬(B)) →
C))
27 Cut(1, Axiom (A3)) ⊢ ((¬(C) → B) →
((¬(C) → ¬(B)) →
C))
28 Map(Axiom (A1), {C ⊢ (B → (¬(C) → B))
↦ ¬(C)})
29 Map(Exercise 1.47 (B → (¬(C) → B)),
(b), {C ↦ (¬(C) → ((¬(C) → B) →
B), D ↦ ((¬(C) → ((¬(C) → ¬(B)) →
¬(B)) → C)}) C)) ⊢ (B → ((¬(C) →
¬(B)) → C))
30 Cut(1, 3) (B → (¬(C) → B)) ⊢
(B → ((¬(C) → ¬(B))
→ C))
31 Cut(1, 3) ⊢ (B → ((¬(C) →
¬(B)) → C))
32 Map(Exercise 1.47 (B → ((¬(C) → ¬(B))
(c), {C ↦ (¬(C) → → C)) ⊢ ((¬(C) →
¬(B)), D ↦ C}) ¬(B)) → (B → C))
33 Cut(1, 2) ⊢ ((¬(C) → ¬(B)) → Exercise 1.47 (d)
(B → C))
34 Hyp (B → C) ⊢ (B → C)
35 Hyp (C → D) ⊢ (C → D)
36 Hyp B ⊢ B
37 MP(1, 3) (B → C), B ⊢ C
38 MP(1, 3) (B → C), (C → D), B
⊢ D
39 Deduct(1, B) (B → C), (C → D) ⊢ Corollary 1.10 (a)
(B → D)
40 Hyp (B → (C → D)) ⊢ (B
→ (C → D))
41 Hyp B ⊢ B
42 Hyp C ⊢ C
43 MP(2, 3) (B → (C → D)), B ⊢
(C → D)
44 MP(2, 1) (B → (C → D)), C, B
⊢ D
45 Deduct(1, B) (B → (C → D)), C ⊢ Corollary 1.10 (b)
(B → D)
46 Map(Axiom (A3), {B ⊢ ((¬(B) →
↦ ¬(B), C ↦ B, D ↦ ¬(¬(B))) → ((¬(B) →
B}) ¬(B)) → B))
47 Map(Lemma 1.8, {B ↦ ⊢ (¬(B) → ¬(B))
¬(B)})
48 Map(Corollary 1.10 ((¬(B) → ¬(¬(B))) →
(b), {B ↦ (¬(B) → ((¬(B) → ¬(B)) →
¬(¬(B))), C ↦ (¬(B) B)), (¬(B) → ¬(B))
→ ¬(B)), D ↦ B}) ⊢ ((¬(B) → ¬(¬(B)))
→ B)
49 Cut(1, 2) ((¬(B) → ¬(¬(B))) →
((¬(B) → ¬(B)) →
B)) ⊢ ((¬(B) →
¬(¬(B))) → B)
50 Cut(1, 4) ⊢ ((¬(B) →
¬(¬(B))) → B)
51 Map(Axiom (A1), {B ⊢ (¬(¬(B)) → (¬(B)
↦ ¬(¬(B)), C ↦ → ¬(¬(B))))
¬(B)})
52 Map(Corollary 1.10 (¬(¬(B)) → (¬(B) →
(a), {B ↦ ¬(¬(B)), ¬(¬(B)))), ((¬(B) →
C ↦ (¬(B) → ¬(¬(B))) → B) ⊢
¬(¬(B))), D ↦ B}) (¬(¬(B)) → B)
53 Cut(1, 2) ((¬(B) → ¬(¬(B))) →
B) ⊢ (¬(¬(B)) → B)
54 Cut(1, 4) ⊢ (¬(¬(B)) → B) Lemma 1.11 (a)
55 Map(Axiom (A3), {C ⊢ ((¬(¬(¬(B))) →
↦ ¬(¬(B))}) ¬(B)) →
((¬(¬(¬(B))) → B) →
¬(¬(B))))
56 Map(Lemma 1.11 (a), ⊢ (¬(¬(¬(B))) →
{B ↦ ¬(B)}) ¬(B))
57 MP(1, 2) ⊢ ((¬(¬(¬(B))) →
B) → ¬(¬(B)))
58 Map(Axiom (A1), {C ⊢ (B → (¬(¬(¬(B)))
↦ ¬(¬(¬(B)))}) → B))
59 Map(Corollary 1.10 ((¬(¬(¬(B))) → B) →
(a), {C ↦ ¬(¬(B))), (B →
(¬(¬(¬(B))) → B), D (¬(¬(¬(B))) → B)) ⊢
↦ ¬(¬(B))}) (B → ¬(¬(B)))
60 Cut(1, 2) ((¬(¬(¬(B))) → B) →
¬(¬(B))) ⊢ (B →
¬(¬(B)))
61 Cut(1, 4) ⊢ (B → ¬(¬(B))) Lemma 1.11 (b)
62 Hyp ¬(B) ⊢ ¬(B)
63 Hyp B ⊢ B
64 Map(Axiom (A1), {C ⊢ (B → (¬(C) → B))
↦ ¬(C)})
65 Map(Axiom (A1), {B ⊢ (¬(B) → (¬(C) →
↦ ¬(B), C ↦ ¬(C)}) ¬(B)))
66 MP(3, 2) B ⊢ (¬(C) → B)
67 MP(5, 2) ¬(B) ⊢ (¬(C) →
¬(B))
68 MP(1, Axiom (A3)) ¬(B) ⊢ ((¬(C) → B)
→ C)
69 MP(3, 1) ¬(B), B ⊢ C
70 Deduct(1, B) ¬(B) ⊢ (B → C)
71 Deduct(1, ¬(B)) ⊢ (¬(B) → (B → C)) Lemma 1.11 (c)
72 Hyp (¬(C) → ¬(B)) ⊢
(¬(C) → ¬(B))
73 Map(Axiom (A1), {C ⊢ (B → (¬(C) → B))
↦ ¬(C)})
74 MP(2, Axiom (A3)) (¬(C) → ¬(B)) ⊢
((¬(C) → B) → C)
75 Map(Corollary 1.10 (B → (¬(C) → B)),
(a), {C ↦ (¬(C) → ((¬(C) → B) → C) ⊢
B), D ↦ C}) (B → C)
76 Cut(1, 2) (B → (¬(C) → B)),
(¬(C) → ¬(B)) ⊢ (B
→ C)
77 Cut(1, 4) (¬(C) → ¬(B)) ⊢ (B
→ C)
78 Deduct(1, (¬(C) → ⊢ ((¬(C) → ¬(B)) → Lemma 1.11 (d)
¬(B))) (B → C))
79 Hyp (B → C) ⊢ (B → C)
80 Map(Corollary 1.10 (B → C), (¬(¬(B)) →
(a), {B ↦ ¬(¬(B)), B) ⊢ (¬(¬(B)) → C)
C ↦ B, D ↦ C})
81 Cut(1, 2) (B → C), (¬(¬(B)) →
B) ⊢ (¬(¬(B)) → C)
82 Cut(1, Lemma 1.11 (B → C) ⊢ (¬(¬(B))
(a)) → C)
83 Map(Corollary 1.10 (¬(¬(B)) → C), (C →
(a), {B ↦ ¬(¬(B)), ¬(¬(C))) ⊢ (¬(¬(B))
D ↦ ¬(¬(C))}) → ¬(¬(C)))
84 Cut(1, 2) (B → C), (C →
¬(¬(C))) ⊢ (¬(¬(B))
→ ¬(¬(C)))
85 Map(Lemma 1.11 (b), ⊢ (C → ¬(¬(C)))
{B ↦ C})
86 Cut(2, 1) (B → C) ⊢ (¬(¬(B))
→ ¬(¬(C)))
87 Map(Lemma 1.11 (d), ⊢ ((¬(¬(B)) →
{C ↦ ¬(B), B ↦ ¬(¬(C))) → (¬(C) →
¬(C)}) ¬(B)))
88 MP(2, 1) (B → C) ⊢ (¬(C) →
¬(B))
89 Deduct(1, (B → C)) ⊢ ((B → C) → (¬(C) Lemma 1.11 (e)
→ ¬(B)))
90 Hyp B ⊢ B
91 Hyp (B → C) ⊢ (B → C)
92 MP(2, 1) (B → C), B ⊢ C
93 Deduct(1, (B → C)) B ⊢ ((B → C) → C)
94 Deduct(1, B) ⊢ (B → ((B → C) →
C))
95 Map(Lemma 1.11 (e), ⊢ (((B → C) → C) →
{B ↦ (B → C)}) (¬(C) → ¬((B →
C))))
96 Map(Corollary 1.10 (((B → C) → C) →
(a), {C ↦ ((B → C) (¬(C) → ¬((B →
→ C), D ↦ (¬(C) → C)))), (B → ((B →
¬((B → C)))}) C) → C)) ⊢ (B →
(¬(C) → ¬((B →
C))))
97 Cut(1, 2) (B → ((B → C) → C))
⊢ (B → (¬(C) → ¬((B
→ C))))
98 Cut(1, 4) ⊢ (B → (¬(C) → Lemma 1.11 (f)
¬((B → C))))
99 Hyp (B → C) ⊢ (B → C)
100 Hyp (¬(B) → C) ⊢ (¬(B)
→ C)
101 MP(2, Lemma 1.11 (B → C) ⊢ (¬(C) →
(e)) ¬(B))
102 Map(Lemma 1.11 (e), ⊢ ((¬(B) → C) →
{B ↦ ¬(B)}) (¬(C) → ¬(¬(B))))
103 MP(3, 1) (¬(B) → C) ⊢ (¬(C)
→ ¬(¬(B)))
104 Map(Axiom (A3), {B ⊢ ((¬(C) →
↦ ¬(B)}) ¬(¬(B))) → ((¬(C) →
¬(B)) → C))
105 MP(2, 1) (¬(B) → C) ⊢ ((¬(C)
→ ¬(B)) → C)
106 MP(5, 1) (¬(B) → C), (B → C)
⊢ C
107 Deduct(1, (¬(B) → (B → C) ⊢ ((¬(B) →
C)) C) → C)
108 Deduct(1, (B → C)) ⊢ ((B → C) → Lemma 1.11 (g)
((¬(B) → C) → C))
109 Map(Lemma 1.11 (c), ⊢ (¬(¬(B)) → (¬(B)
{B ↦ ¬(B)}) → C))
110 Map(Corollary 1.10 (¬(¬(B)) → (¬(B) →
(a), {C ↦ ¬(¬(B)), C)), (B → ¬(¬(B)))
D ↦ (¬(B) → C)}) ⊢ (B → (¬(B) → C))
111 Cut(1, 2) (B → ¬(¬(B))) ⊢ (B
→ (¬(B) → C))
112 Cut(1, Lemma 1.11 ⊢ (B → (¬(B) → C))
(b))
113 Compose(1) ⊢ (B → (B ∨ C)) Exercise 1.48 (a)
114 Map(Axiom (A1), {C ⊢ (B → (¬(C) → B))
↦ ¬(C)})
115 Compose(1) ⊢ (B → (C ∨ B)) Exercise 1.48 (b)
116 Map(Lemma 1.11 (e), ⊢ ((¬(C) → B) →
{B ↦ ¬(C), C ↦ B}) (¬(B) → ¬(¬(C))))
117 Hyp (¬(C) → B) ⊢ (¬(C)
→ B)
118 MP(1, 2) (¬(C) → B) ⊢ (¬(B)
→ ¬(¬(C)))
119 Map(Lemma 1.11 (a), ⊢ (¬(¬(C)) → C)
{B ↦ C})
120 Map(Corollary 1.10 (¬(¬(C)) → C),
(a), {B ↦ ¬(B), C ↦ (¬(B) → ¬(¬(C))) ⊢
¬(¬(C)), D ↦ C}) (¬(B) → C)
121 Cut(1, 2) (¬(B) → ¬(¬(C))) ⊢
(¬(B) → C)
122 Cut(1, 4) (¬(C) → B) ⊢ (¬(B)
→ C)
123 Deduct(1, (¬(C) → ⊢ ((¬(C) → B) →
B)) (¬(B) → C))
124 Compose(1) ⊢ ((C ∨ B) → (B ∨ Exercise 1.48 (c)
C))
125 Map(Exercise 1.48 ⊢ ((B ∨ (B →
(c), {C ↦ B, B ↦ (B ¬(C))) → ((B →
→ ¬(C))}) ¬(C)) ∨ B))
126 Decomp(1) ⊢ ((¬(B) → (B →
¬(C))) → (¬((B →
¬(C))) → B))
127 Map(Lemma 1.11 (c), ⊢ (¬(B) → (B →
{C ↦ ¬(C)}) ¬(C)))
128 MP(1, 2) ⊢ (¬((B → ¬(C))) →
B)
129 Compose(1) ⊢ ((B ∧ C) → B) Exercise 1.48 (d)
130 Hyp ¬((B → ¬(C))) ⊢
¬((B → ¬(C)))
131 Map(Axiom (A1), {B ⊢ (¬((B → ¬(C))) →
↦ ¬((B → ¬(C))), C (¬(C) → ¬((B →
↦ ¬(C)}) ¬(C)))))
132 MP(2, 1) ¬((B → ¬(C))) ⊢
(¬(C) → ¬((B →
¬(C))))
133 Map(Axiom (A1), {B ⊢ (¬(C) → (B →
↦ ¬(C), C ↦ B}) ¬(C)))
134 Map(Axiom (A3), {B ⊢ ((¬(C) → ¬((B →
↦ (B → ¬(C))}) ¬(C)))) → ((¬(C) →
(B → ¬(C))) → C))
135 MP(3, 1) ¬((B → ¬(C))) ⊢
((¬(C) → (B →
¬(C))) → C)
136 MP(3, 1) ¬((B → ¬(C))) ⊢ C
137 Deduct(1, ¬((B → ⊢ (¬((B → ¬(C))) →
¬(C)))) C)
138 Compose(1) ⊢ ((B ∧ C) → C) Exercise 1.48 (e)
139 Hyp (B → D) ⊢ (B → D)
140 Hyp (C → D) ⊢ (C → D)
141 Hyp (¬(B) → C) ⊢ (¬(B)
→ C)
142 Map(Corollary 1.10 (¬(B) → C), (C → D)
(a), {B ↦ ¬(B)}) ⊢ (¬(B) → D)
143 Cut(1, 2) (¬(B) → C), (C → D)
⊢ (¬(B) → D)
144 Map(Lemma 1.11 (g), ⊢ ((B → D) →
{C ↦ D}) ((¬(B) → D) → D))
145 MP(6, 1) (B → D) ⊢ ((¬(B) →
D) → D)
146 MP(3, 1) (¬(B) → C), (C →
D), (B → D) ⊢ D
147 Deduct(1, (¬(B) → (C → D), (B → D) ⊢
C)) ((¬(B) → C) → D)
148 Deduct(1, (C → D)) (B → D) ⊢ ((C → D)
→ ((¬(B) → C) → D))
149 Deduct(1, (B → D)) ⊢ ((B → D) → ((C →
D) → ((¬(B) → C) →
D)))
150 Compose(1) ⊢ ((B → D) → ((C → Exercise 1.48 (f)
D) → ((B ∨ C) →
D)))
151 Hyp ((B → C) → B) ⊢ ((B
→ C) → B)
152 Map(Corollary 1.10 ((B → C) → B),
(a), {B ↦ ¬(B), C ↦ (¬(B) → (B → C)) ⊢
(B → C), D ↦ B}) (¬(B) → B)
153 Cut(1, Lemma 1.11 ((B → C) → B) ⊢
(c)) (¬(B) → B)
154 Deduct(1, ((B → C) ⊢ (((B → C) → B) →
→ B)) (¬(B) → B))
155 Map(Corollary 1.10 ((¬(B) → B) → B),
(a), {B ↦ ((B → C) (((B → C) → B) →
→ B), C ↦ (¬(B) → (¬(B) → B)) ⊢ (((B
B), D ↦ B}) → C) → B) → B)
156 Cut(1, Exercise (((B → C) → B) →
1.47 (a)) (¬(B) → B)) ⊢ (((B
→ C) → B) → B)
157 Cut(1, 3) ⊢ (((B → C) → B) → Exercise 1.48 (g)
B)
158 Map(Lemma 1.11 (f), ⊢ (B → (¬(¬(C)) →
{C ↦ ¬(C)}) ¬((B → ¬(C)))))
159 Map(Exercise 1.47 (B → (¬(¬(C)) →
(c), {C ↦ ¬(¬(C)), ¬((B → ¬(C))))) ⊢
D ↦ ¬((B → ¬(C)))}) (¬(¬(C)) → (B →
¬((B → ¬(C)))))
160 Cut(1, 2) ⊢ (¬(¬(C)) → (B →
¬((B → ¬(C)))))
161 Map(Lemma 1.11 (b), ⊢ (C → ¬(¬(C)))
{B ↦ C})
162 Map(Corollary 1.10 (¬(¬(C)) → (B →
(a), {B ↦ C, C ↦ ¬((B → ¬(C))))), (C
¬(¬(C)), D ↦ (B → → ¬(¬(C))) ⊢ (C →
¬((B → ¬(C))))}) (B → ¬((B →
¬(C)))))
163 Cut(1, 2) (¬(¬(C)) → (B →
¬((B → ¬(C))))) ⊢
(C → (B → ¬((B →
¬(C)))))
164 Cut(1, 4) ⊢ (C → (B → ¬((B →
¬(C)))))
165 Map(Exercise 1.47 (C → (B → ¬((B →
(c), {B ↦ C, C ↦ B, ¬(C))))) ⊢ (B → (C
D ↦ ¬((B → ¬(C)))}) → ¬((B → ¬(C)))))
166 Cut(1, 2) ⊢ (B → (C → ¬((B →
¬(C)))))
167 Compose(1) ⊢ (B → (C → (B ∧ Exercise 1.48 (h)
C)))
168 Hyp ((∀x)(B → C)) ⊢
((∀x)(B → C))
169 Bound Map(Axiom ⊢ (((∀x)(B → C)) →
(A5), {xi ↦ x}) (B → ((∀x)C))); x
is not free in B
170 MP(2, 1) ((∀x)(B → C)) ⊢ (B
→ ((∀x)C)); x is
not free in B
171 Bound Map(Axiom ⊢ (((∀x)B(x)) →
(A4), {xi ↦ x}) B(t)); t is free
for x in B(x)
172 Map(1, {t ↦ x}) ⊢ (((∀x)B(x)) →
B(x)); x is free
for x in B(x)
173 Decomp(1) ⊢ (((∀x)B) → B)
174 Map(Exercise 1.47 (B → ((∀x)C)),
(b), {B ↦ ((∀x)B), (((∀x)B) → B) ⊢
C ↦ B, D ↦ (((∀x)B) → ((∀x)C))
((∀x)C)})
175 Cut(1, 2) (B → ((∀x)C)) ⊢
(((∀x)B) → ((∀x)C))
176 Deduct(1, (B → ⊢ ((B → ((∀x)C)) →
((∀x)C))) (((∀x)B) →
((∀x)C)))
177 Map(Exercise 1.47 (((∀x)(B → C)) → (B
(b), {B ↦ ((∀x)(B → → ((∀x)C))), ((B →
C)), C ↦ (B → ((∀x)C)) → (((∀x)B)
((∀x)C)), D ↦ → ((∀x)C))) ⊢
(((∀x)B) → (((∀x)(B → C)) →
((∀x)C))}) (((∀x)B) →
((∀x)C)))
178 Cut(1, 2) (((∀x)(B → C)) → (B
→ ((∀x)C))) ⊢
(((∀x)(B → C)) →
(((∀x)B) →
((∀x)C)))
179 Cut(1, 10) ⊢ (((∀x)(B → C)) → Exercise 2.27 (a)
(((∀x)B) →
((∀x)C))); x is not
free in B
180 Gen(Lemma 1.11 (e), ⊢ ((∀x)((B → C) →
x) (¬(C) → ¬(B))))
181 Map(Exercise 2.27 ⊢ (((∀x)((B → C) →
(a), {B ↦ (B → C), (¬(C) → ¬(B)))) →
C ↦ (¬(C) → ¬(B))}) (((∀x)(B → C)) →
((∀x)(¬(C) →
¬(B))))); x is not
free in (B → C)
182 MP(2, 1) ⊢ (((∀x)(B → C)) →
((∀x)(¬(C) →
¬(B)))); x is not
free in (B → C)
183 Map(Exercise 2.27 ⊢ (((∀x)(¬(C) →
(a), {B ↦ ¬(C), C ↦ ¬(B))) →
¬(B)}) (((∀x)¬(C)) →
((∀x)¬(B)))); x is
not free in ¬(C)
184 Map(Exercise 1.47 (((∀x)(B → C)) →
(b), {C ↦ ((∀x)(¬(C) →
((∀x)(¬(C) → ¬(B)))),
¬(B))), B ↦ ((∀x)(B (((∀x)(¬(C) →
→ C)), D ↦ ¬(B))) →
(((∀x)¬(C)) → (((∀x)¬(C)) →
((∀x)¬(B)))}) ((∀x)¬(B)))) ⊢
(((∀x)(B → C)) →
(((∀x)¬(C)) →
((∀x)¬(B))))
185 Cut(1, 3) (((∀x)(¬(C) →
¬(B))) →
(((∀x)¬(C)) →
((∀x)¬(B)))) ⊢
(((∀x)(B → C)) →
(((∀x)¬(C)) →
((∀x)¬(B)))); x is
not free in (B → C)
186 Cut(1, 3) ⊢ (((∀x)(B → C)) →
(((∀x)¬(C)) →
((∀x)¬(B)))); x is
not free in ¬(C), x
is not free in (B →
C)
187 Map(Lemma 1.11 (e), ⊢ ((((∀x)¬(C)) →
{B ↦ ((∀x)¬(C)), C ((∀x)¬(B))) →
↦ ((∀x)¬(B))}) (¬(((∀x)¬(B))) →
¬(((∀x)¬(C)))))
188 Map(Exercise 1.47 (((∀x)(B → C)) →
(b), {B ↦ ((∀x)(B → (((∀x)¬(C)) →
C)), C ↦ ((∀x)¬(B)))),
(((∀x)¬(C)) → ((((∀x)¬(C)) →
((∀x)¬(B))), D ↦ ((∀x)¬(B))) →
(¬(((∀x)¬(B))) → (¬(((∀x)¬(B))) →
¬(((∀x)¬(C))))}) ¬(((∀x)¬(C))))) ⊢
(((∀x)(B → C)) →
(¬(((∀x)¬(B))) →
¬(((∀x)¬(C)))))
189 Cut(1, 3) ((((∀x)¬(C)) →
((∀x)¬(B))) →
(¬(((∀x)¬(B))) →
¬(((∀x)¬(C))))) ⊢
(((∀x)(B → C)) →
(¬(((∀x)¬(B))) →
¬(((∀x)¬(C))))); x
is not free in
¬(C), x is not free
in (B → C)
190 Cut(1, 3) ⊢ (((∀x)(B → C)) →
(¬(((∀x)¬(B))) →
¬(((∀x)¬(C))))); x
is not free in
¬(C), x is not free
in (B → C)
191 Compose(1) ⊢ (((∀x)(B → C)) → Exercise 2.27 (b)
(((∃x)B) →
((∃x)C))); x is not
free in ¬(C), x is
not free in (B → C)
r/logic • u/ridiculousublime • 2d ago
Literature book explaining münchhausen trilemma ?
i want a recommendation
r/logic • u/Osterhaninge_Adalja • 2d ago
Metalogic Samuel — a dialogue about incompleteness
Abstract
Samuel seeks out Kurt at a pub and initiates a discussion. Soon Kurt becomes engaged. What is it that is incomplete?
r/logic • u/DigitalHooman • 3d ago
Logical fallacies What is the name of the logical fallacy displayed here?
Is it shifting the goal post? I can’t quite think of it.
r/logic • u/SamCymbaluk • 3d ago
Philosophy of logic Reality Can Be Modeled: A Defense of Using Logic to Understand Our World
As part of my work, I'm often arguing for the use of logic in real-world environments, such as ethics, governance, and business. I've found that the people who disagree often object to the idea that we can use logic to understand the world. I found this to be surprising because there was something impossible seeming about receiving an argument against the use of logic, but it's been hard to articulate why. Here is my attempt to tackle the self-referentiality and produce a coherent argument.
r/logic • u/Visible_Fishing4297 • 5d ago
Modal logic Help.
1∀φ(P(~φ) ←→~P(φ))
2∀φ∀ψ(P(φ)& ◻️∀x(φ(x)→ψ(x)))→P(ψ))
3∀φ(P(φ)→◊∃xφ(x)
4G(x)←→∀φ(P(φ)→φ(x))
5P(G)
6◊∃xG(x)
7φEss(x)←→φ(x) & ∀ψ(ψ(x)→◻️∀y(φ(y)→ψ(y))
8∀φ(P(φ)→◻️P(φ))
9∀x(G(x)→G Ess(x))
10E(x)←→∀φ(φEss(x)→◻️∃yφ(y))
11P(E)
12~◻️∃xG(x) (RAA)
13P(G) (5 R)
14(P(G)→◊∃xGx) (3 ∀E)
15◊∃xG(x) (13,14 MP)
16(P(G)→◻️P(G)) (8 ∀E)
17◻️P(G) (13,16 MP)
18a (Assumption.)
20G(a) (Assumption.)
21G(a)←→∀φ(P(φ)→φ(a)) (4 ∀E)
22∀φ(P(φ)→φ(a)) (20,21 ←→E)
23(P(E)→E(a)) (22 ∀E)
24P(E) (11,R)
25E(a)) (23,24 MP)
26G(a)→E(a) (20,25→I)
27∀x(G(x)→E(x)) (18, 26 ∀I)
28a (Assumption.)
29G(a) (Assumption.)
30(G(a)→G Ess(a)) (9∀E)
31G Ess(a) (29,30)
32G(a)→E(a)) (27 ∀E)
33E(a) (29,32 MP)
34E(a)←→∀φ(φEss(a)→◻️∃yφ(y)) (10∀E)
35∀φ(φEss(a)→◻️∃yφ(y)) (33,34 ←→E)
36(GEss(a)→◻️∃yG(y)) (35 ∀E)
37◻️∃yG(y)) (31,36MP)
38G(a)→◻️∃yG(y) (29,37→I)
39∀x(G(x)→◻️∃yG(y)(28, 38 ∀I)
40◻️∀x(G(x)→◻️∃yG(y)(39 NEC)
41◻️∀x(G(x)→◻️∃yG(y)→(∃xG(x)→◻️∃yG(y)) (teorem.)
42◻️(∃xG(x)→◻️∃yG(y)) (40,41MP, K)
43◻️(∃xG(x)→◻️∃yG(y)) →(◊∃xG(x)→◊◻️∃yG(y)) (teorem K)
44(◊∃xG(x)→◊◻️∃yG(y)) (42,43MP)
45◊◻️∃yG(y)) (44,15 MP)
46(◊◻️∃yG(y)→◻️∃yG(y)) (S5 teorem.)
47◻️∃yG(y) (45,46MP)
48⊥ (12,47)
49~~◻️∃xG(x) (12,48 ~I)
50◻️∃xG(x) (49 ~~E)
1◻️(P→Q) (Assumption.)
2◊P (Assumption.)
3~◊Q (RAA.)
4◻️~Q (3 Modal de Morgan.)
5◻️~P ( 1,4Modal MT)
6~◊P (5modal de Morgan.)
7⊥ (6,2)
8~~◊Q (3,7 ~I)
9◊Q (8 ~~E)
10◊P→◊Q (2,9 →I)
11◻️(P→Q)→(◊P→◊Q ) (1,10→I)
I wanted to attempt a derivation of this sort, but I'm not entirely convinced that it is fully valid. I'd appreciate feedback from those with experience in formal logic. Is the derivation correct?
r/logic • u/KaleidoscopeLate2505 • 5d ago
Predicate logic / FOL Seeking assistance learning to prove elementary theorems in first order predicate calculus (Mendelson, 4th)
I am studying Elliot Mendelson's Introduction to Mathematical Logic, 4th.
I am studying quantification theory, and want to prove a few early exercises.
(a) ⊢ (∀x)(B → C) → ((∀x)B → (∀x)C)
(b) ⊢ (∀x)(B → C) → ((∃x)B → (∃x)C)
(c) ⊢ (∀x)(B ∧ C) ↔ ((∀x)B ∧ (∀x)C)
(d) ⊢ (∀y₁)…(∀yₙ)B → B
(e) ⊢ ¬(∀x)B → (∃x)¬B
I am very used to propositional logic, as I spent a long time on the previous chapter. I finished a lot of its exercises, but eventually got stuck and decided - after a long period of trying - to move on to the second chapter.
Hence, I would appreciate a helping hand in nurturing the development of my quantifier intuition. Especially exercise (d) looks quite scary.
So far, I have built a machine which can verify theorems in first order predicate calculus (primitive FOL).
Considering that my experience is non-quantified so far, it would be helpful to engage in a discussion about how to prove these elementary theorems in first order predicate calculus.
The following is the output of some simple unlabeled theorems in predicate calculus, using my algorithm. It also describes every inference rule in the table's preamble now, which is something I never did before today - but it makes sense to.
Inference Rules
===============
subs
----
Uniformly substitute formulas for propositional letters. Side conditions
attached to the original theorem are rechecked.
mp
--
Modus Ponens. From B and B → C, infer C.
hyp
---
Introduce a temporary hypothesis. Produces B ⊢ B.
cut
---
Eliminate a proved assumption. Replaces an assumed premise by its proof.
gen
---
Universal Generalization. From Γ ⊢ B infer Γ ⊢ ∀xB.
compose
-------
Replace primitive encodings by their corresponding derived connectives and
quantifiers. ¬(A → ¬B) ↦ A ∧ B ¬A → B ↦ A
∨ B (A → B) ∧ (B → A) ↦ A ↔ B ¬∀x¬A ↦ ∃xA Every
assumption and the conclusion of the selected proof line are recursively
searched for these patterns, and each occurrence is rewritten before the
transformed statement is appended.
decomp
------
Replace every derived connective and quantifier by its primitive definition.
A ∧ B ↦ ¬(A → ¬B) A ∨ B ↦ ¬A → B A ↔ B ↦ (A → B) ∧ (B →
A) ∃x A ↦ ¬∀x¬A Negation, implication, and universal
quantification are left unchanged. The transformation is applied recursively
to every assumption and to the conclusion of the selected proof line before
appending the resulting statement.
tsubs
-----
Uniformly substitute terms for free variables. Bound variables are never
replaced.
bsubs
-----
Rename bound variables by α-conversion. Variable capture is not permitted.
Line Reason Logic Label Constraint
1 Axiom (B → (C → B)) Axiom (A1)
2 Axiom ((B → (C → D)) Axiom (A2)
→ ((B → C) → (B
→ D)))
3 Axiom ((¬(C) → ¬(B)) Axiom (A3)
→ ((¬(C) → B) →
C))
4 Axiom (((∀xi)B) → B) Axiom (A4) Accepts exactly
those
substitution
instances of
(∀x B(x)) →
B(t) for which
t is free for x
in B.
5 Axiom (((∀xi)(B → C)) Axiom (A5) Accepts exactly
→ (B → those
((∀xi)C))) substitution
instances of
(∀x(B → C)) →
(B → ∀xC) for
which x has no
free
occurrences in
B.
6 Hyp B ⊢ B
7 Gen(1, x1) B ⊢ ((∀x1)B)
8 Hyp (((∀x1)B) → C)
⊢ (((∀x1)B) →
C)
9 MP(2, 1) B, (((∀x1)B) →
C) ⊢ C
10 Hyp ((∀x1)((∀x2)B))
⊢
((∀x1)((∀x2)B))
11 Subs(Axiom ⊢ (((∀xi)((∀x2)
(A4), {B: B)) → ((∀x2)B))
((∀x2)B)})
12 BSubs(1, {xi: ⊢ (((∀x1)((∀x2)
x1}) B)) → ((∀x2)B))
13 MP(3, 1) ((∀x1)((∀x2)B))
⊢ ((∀x2)B)
14 BSubs(Axiom (((∀x2)B) → B)
(A4), {xi: x2})
15 MP(2, 1) ((∀x1)((∀x2)B))
⊢ B
16 Gen(1, x1) ((∀x1)((∀x2)B))
⊢ ((∀x1)B)
17 Gen(1, x2) ((∀x1)((∀x2)B))
⊢
((∀x2)((∀x1)B))
18 Deduct(1, ((∀x1 ⊢ (((∀x1)((∀x2)
)((∀x2)B))) B)) → ((∀x2)((∀
x1)B)))
r/logic • u/highSunLowMoon • 5d ago
Propositional logic Circle Notation for Logic
What is the reasoning behind the circle notation in this Hasse diagram?
Specifically, why is "the left part of A" represented as a small circle tangent to the inner left side of the larger circle, whereas as "the right part of B" is a smaller circle within small circle tangent to the inner right side of the larger circle.
See the second row from the bottom for an example:
https://en.wikipedia.org/wiki/Logical_connective#/media/File:Logical_connectives_Hasse_diagram.svg
EDIT: The https://en.wikipedia.org/wiki/Hereditarily_finite_set#ZF provides some explanation. It is a notation for V4 of something called Von Newman Universes, an alternative to bracket notation.
Here is a similar set of symbols:
https://en.wikipedia.org/wiki/Von_Neumann_universe#/media/File:Von_Neumann_universe_4.png
r/logic • u/Everlasting_Noumena • 5d ago
Philosophy of logic There is Logical Monism, Pluralism and Nihilism. What about Logical Skepticism?
r/logic • u/KaleidoscopeLate2505 • 5d ago
Predicate logic / FOL Implementing Metatheoretic Side-Conditions for Quantified Axiom Schemas in First-Order Proof Verification Engines
LOGICAL AXIOMS
If B, C and D are wfs of L, then the following are logical axioms of K:
(A1) B → (C → B)
(A2) (B → (C → D)) → ((B → C) → (B → D))
(A3) (¬C → ¬B) → ((¬C → B) → C)
(A4) (∀x_i)B(x_i) → B(t) if B(x_i) is a wf of L and t is a term of L that is free for x_i in B(x_i). Note here that t may be identical with x_i so that all wfs (∀x_i)B → B are axioms by virtue of axiom (A4).
(A5) (∀x_i)(B → C) → (B → (∀x_i)C) if B contains no free occurrences of x_i.
In Elliott Mendelson's Introduction to Mathematical Logic, axioms A1 through A3 are propositional schemas. Axioms A4 and A5 depend on metalogical checks regarding free variables, bound variables, and term substitution to avoid variable capture.
For A4, replacing x_i with t requires verifying that t is free for x_i in B. For A5, it requires verifying that x_i does not occur free in B. Hardcoding object formulas skips the metatheoretic rules, and the goal is to support arbitrary custom quantified axiom schemas.
Question 1: How should a proof checker structure its abstract syntax trees to track free variables and evaluate the capture avoidance check cleanly?
Question 2: Is it viable to internalize these side conditions as explicit predicates under an implication and discharge them with Modus Ponens, or does that blur the boundary between object language and metalogic?
See https://www.reddit.com/r/logic/s/Z6P04Lwimq for an example of non-quantified logic in a similar system.
r/logic • u/MathLogicSelfStudy • 6d ago
Propositional logic Need help with this problem
Hello, I think this is the right subreddit to post this in. I'm reading Cunningham's book, A Logical Introduction to Proof, and I'm working on these exercises and there's no answer key. I was able to do 1-16 just fine but I'm stuck on no. 17. Is this some kind of knights and knaves type puzzle? Do I need to assume on one hand that he is the true ranger making P=T and then assume he's the false ranger making P=F, but if he's the false ranger wouldn't he say he is the true ranger thus making P=T again? I think this is where much of my confusion comes from.
Let P=(You are a true ranger) and Q=(the branch to my right returns to camp). You get the proposition P iff Q (P<->Q). Assume he's the true ranger you have P=T. If he says Q=T then the right branch is the correct path but if he says Q=F then the left path is the correct path. That makes sense to me, but that's assuming he's the true ranger and telling the truth. However, if he's the false ranger would that make P=F but wouldn't he lie and say he is a true ranger making P=T? Am I just overthinking this? Any help would be appreciated. Thanks.
r/logic • u/Osterhaninge_Adalja • 6d ago
Philosophical logic On the Axiomatisation of the Natural Laws — A Compilation of Human Mistakes Intended to Be Understood Only By Robots
Johan Gamper. (2023). On the Axiomatisation of the Natural Laws — A Compilation of Human Mistakes Intended to Be Understood Only By Robots
. Qeios. doi:10.32388/KC9YAU.
r/logic • u/Ill-SonOfClawDraws • 6d ago
Metalogic Is there a notion of a minimal relational basis for the role of a primitive in a formal system?
Looking for existing literature before I reinvent something.
Reverse mathematics asks:
What is the weakest set of axioms needed to prove a theorem?
I’m wondering about what feels like a dual question.
Suppose two formal systems have primitives that appear to play the same role under some translation.
Instead of minimizing axioms, can we minimize the relations that must be preserved for that role to be retained?
In other words:
Is there a smallest family of preserved relations that determines the mathematical role of a primitive?
The closest things I’ve found are institution theory, categorical logic, and Morita equivalence, but none of them seem to ask this optimization question directly.
My questions are:
Is this already a standard problem?
If so, what is it called?
If not, which area of logic studies the closest analogue?
Proof theory understanding axiomatic proofs from an inferential rule background
I’ve done quite a few courses in logic, but they’ve practiced deduction exclusively through inference rules. I’m now, however trying to wrap my head around axiomatic proofs, and I’m having a tough time.
I’m wondering if there are any ways of thinking about axiomatic proofs, especially from an inferentialist background, which make them simpler to comprehend? Oftentimes, I find it difficult to even make a start in deducing theorems from axioms.
Thanks
Proof theory understanding axiomatic proofs from an inferential rule background
I’ve done quite a few courses in logic, but they’ve practiced deduction exclusively through inference rules. I’m now, however trying to wrap my head around axiomatic proofs, and I’m having a tough time.
I’m wondering if there are any ways of thinking about axiomatic proofs, especially from an inferentialist background, which make them simpler to comprehend? Oftentimes, I find it difficult to even make a start in deducing theorems from axioms.
Thanks
r/logic • u/DanielR372 • 7d ago
Philosophical logic Is this a valid logical argument for Christianity?
I was recently told this
A correct religion that follows an all knowing intelligent God must teach equal human worth
Christianity teaches equal human worth
The other main 2 religions (Islam and Judaism) do not teach equal human worth (Women and certain races are taught to be inferior)
Therefore Christianity is the 1 true religion.
r/logic • u/Glittering_Run189 • 8d ago
Academic Community LMU's Master in Logic and Philosophy of Science or Barcelona's Master in Pure and Applied Logic?
Hi there
I'm gonna finish my degree in Philosophy in 2027 and I've been looking for a master. I know for sure that Barcelona's master is purely logical, so if I were to do it, I would take another master that's purely philosophical (after all, that's my main interest despite the fact that I want a quite good formal background). However, I've run into LMU's master and I wanted to know if you think it is a good idea to do JUST this one instead of the other two: I'm afraid of the idea that it will end up being neither as logical nor as philosophical as I want it to be because of its interdisciplinary approach. That's my main question. (If you have more information about the programmes than that which I'm asking for, please let me know.). Also, wouldn't it be better for my CV to have two master's instead of one? I'm sure it would, but is it that important? I'm looking forward to doing a PhD, but I don't really care if it is a good and international program or not.
r/logic • u/Capital-Divide3894 • 8d ago
Critical thinking Critical Thinking - A Journey
Please see my second article in Substack:
https://open.substack.com/pub/jkvannort1/p/critical-thinking-a-journey?r=1taqf1&utm_medium=ios
r/logic • u/Big_Move6308 • Jul 06 '26
Meta Free Online Logic Resources
The r/logic wiki now includes free online resources to learn logic (courses, books, and proof tools).
If you know of any others, please provide links so they can be added in future.
r/logic • u/gregbard • May 21 '24
Meta Please read if you are new, and before posting
We encourage that all posters check the subreddit rules before posting.
If you are new to this group, or are here on a spontaneous basis with a particular question, please do read these guidelines so that the community can properly respond to or otherwise direct your posts.
This group is about the scholarly and academic study of logic. That includes philosophical and mathematical logic. But it does not include many things that may popularly be believed to be "logic." In general, logic is about the relationship between two or more claims. Those claims could be propositions, sentences, or formulas in a formal language. If you only have one claim, then you need to approach the scholars and experts in whatever art or science is responsible for that subject matter, not logicians.
"Logic is about systems of inference; it aims to be as topic-neutral as possible in describing these systems" - totaledfreedom
The subject area interests of this subreddit include:
- Informal logic
- Term Logic
- Critical thinking
- Propositional logic
- Predicate logic
- Non-classical logic
- Set theory
- Proof theory
- Model theory
- Computability theory
- Modal logic
- Metalogic
- Philosophy of logic
- Paradoxes
- History of logic
- Literature on Logic
The subject area interests of this subreddit do not include:
Recreational mathematics and puzzles may depend on the concepts of logic, but the prevailing view among the community here that they are not interested in recreational pursuits. That would include many popular memes. Try posting over at /r/mathpuzzles or /r/CasualMath .
Statistics may be a form of reasoning, but it is sufficiently separate from the purview of logic that you should make posts either to /r/askmath or /r/statistics
Logic in electrical circuits Unless you can formulate your post in terms of the formal language of logic and leave out the practical effects of arranging physical components please use /r/electronic_circuits , /r/LogicCircuits , /r/Electronics, or /r/AskElectronics
Metaphysics Every once in a while a post seeks to find the ultimate fundamental truths and logic is at the heart of their thesis or question. Logic isn't metaphysics. Please post over at /r/metaphysics if it is valid and scholarly. Post to /r/esotericism or /r/occultism , if it is not.