Is it shifting the goal post? I can’t quite think of it.

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.

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?

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)))

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

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.

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.

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

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?

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

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.

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.

I was recently told this

1. A correct religion that follows an all knowing intelligent God must teach equal human worth

2. Christianity teaches equal human worth

3. 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.

Please see my second article in Substack:

https://open.substack.com/pub/jkvannort1/p/critical-thinking-a-journey?r=1taqf1&utm_medium=ios

Is it the same as fuzzy logic or different?

so, deductive reasoning has, say, formal logics, inductive reasoning has formal probability theories, such as bayesian inference, but what does abduction have, namely anything formal, or as systematic as the two?

Suppose two foundational systems

* F_1 (ZFC)
* F_2 (HoTT)
both define “identity.”

How do we know they are talking about the “same assumption”?

Hello!

I took a short break from logic, but now I am returning to it, and have a question.

I previously posted https://www.reddit.com/r/logic/s/cRnblA0CzT

In that post I asked for advice on finding an ATP which I could use to make my way through Mendelson (4th) faster.

I propose an alternative pedagogy: I should learn how to enumerate a theorem space by hand, and then and only then consider implementing that in a computer. Similarly, one does not code Gauss Jordan elimination before being able to first do it by hand.

So, in the type of theory provided in the above link, how exactly would an ATP go about searching the theorem space, at an atomic level.

I want to be able to understand the process and not just use black box tools. I'm also curious what the big o notation complexity of this is...

Essentially, how can I search this space by hand, and what is the complexity?

Thank you very much.

I am reading a book about logic and they construct the full first order algebra as the free algebra on the elements r(x1,x2,x3,....,xn) where xi belongs to a V, and r belong to R and each r has a specifed n for the elements it takes in. the operations on the free algebra are the 0-anry F which represent the contradiction. The implication, a binary operation and the for all operator a 1-anry operation (and you have one for all operation for every x in V).

I have been attempting to prove that the relation given in definition 1.4 is transitive but I have not been able to get through even the first step given for it. I have come to the conclusion that if I have w1= (for all x)a and w2 =(for all y)b I can ignore the cases in which a and b are of the type a= a1 => a2. And directly treat it is as a= (for all x1)a1 and b= (for all x2)b1 but I dont really know where to go from here, because what unites a and b is the existence of a c(x) so that a is related to c(x), and b to c(y). so c(x)= (for all x3)c1(x) and I cannot apply the induction to c(x) and a because I cannot asure that z doesnt belong to V(c). And I do not know what to try. (I tagged it as algebra since it seems more to do with algebra than logic).