0

Primarily, this a request to check Fitch-style derivations in the file,

https://drive.google.com/file/d/1du-EIZG3CSdrcfDbldlzwgRftDzeVc8K/view?usp=drivesdk

This is not trivial. The reflexiveness derivation contains over 300 steps.

It is fine if no one steps up. I ask only because it is often difficult to see one's own errors in such detailed work.

As for "the philosophy" involved, the stackexchange community has little love for my views. For me, at least, this is a simple fact. Others may not recognize my writing style.

I will only retain a membership for a short time.

Nevertheless, the topic is one which has been of interest to category theorists (or, perhaps, to homotopy type theorists more specifically). In 2019 Quanta published the article,

https://www.quantamagazine.org/with-category-theory-mathematics-escapes-from-equality-20191010/

making great claims concerning the nature of mathematics relative to equality statements. The article illustrates the basic idea behind the work using a pretty graphic. The graphic is based upon a straightforward theorem from algebraic topology about the contractibility of sets in real spaces where every two points can be joined by a straight line segment.

By analogy, the "terms" of an equivalence relation correspond to the endpoints of line segments. The line segments essentially encode how the terms of its endpoints are substitutable for one another.

Essentially, this is a "topological gluing." Recognized as such, it becomes ubiquitous across mathematics. Differential manifolds, for example, are often described as "gluing" small patches of real spaces together with coordinate charts.

The technical details of such gluings always involve transitivity in termwise descriptions.

By contrast, my work lies effectively within the symbolic domain. Hence, the Fitch-style derivations.

I am an autodidact without many resources. Verification --- or any constructive suggestions --- would be appreciated.

Thank you.

Improve this question
11
  • There is an error on page 45, in that line 314 is incorrectly indicated as line 313. Hope this helps.
    – Joseph_Kopp
    Jul 25 at 0:34
  • You should learn a proof verification software , this is exactly what they were designed for. coq in particular is used heavily by ppl in HTT.
    – emesupap
    Jul 25 at 4:29
  • Having someone review your work (never mind the 77 pages) is unfortunately not really appropriate for a Q&A. There's probably some less structured discussion forum somewhere, where this would fit (although you're still asking a lot, and I'd probably suggest asking about one part at a time, if nothing else, or trying to get a formal peer review somehow). Also, pure symbolic logic may also be more in the maths domain, rather than philosophy.
    – NotThatGuy
    Jul 25 at 8:55
  • @Joseph_Kopp Thank you. I found it. Even typos like this are helpful.
    – user66875
    Jul 25 at 22:47
  • @emesupap Do you have a proof of program correctness for any proof assistant software and the compilers/interpreters that generate their machine-readable code? If you wish to ridicule that question, know that I had the privilege of studying topology with Wolfgang Haken many years ago.
    – user66875
    Jul 25 at 23:38

1 Answer 1

Reset to default
0

The first formula you use in 1.1 is somewhat complicated, so let's simplify it. The formula is:

∀x∀y(xRy <-> [ ∀z ¬(¬x=z <-> (x=z ∧ zRy)) ∧ ∀z ¬(¬y=z <-> (y=z ∧ xRz))])

As part of this, you write ¬x=z <-> x=z ∧ zRy. Let's draw a truth table for that.

x=z   zRy   |  ¬x=z <-> x=z ∧ zRy
T     T        F
T     F        T
F     T        F
F     F        F

So this is equivalent to x=z ∧ ¬zRy. So let's replace that, and the other similar part of the expression:

∀x∀y(xRy <-> [ ∀z ¬(x=z ∧ ¬zRy) ∧ ∀z ¬(y=z ∧ ¬xRz)])

DeMorgan:

∀x∀y(xRy <-> [ ∀z (¬x=z ∨ zRy) ∧ ∀z (¬y=z ∨ xRz)])

Introduce implications:

∀x∀y(xRy <-> [ ∀z (x=z -> zRy) ∧ ∀z (y=z -> xRz)])

This is clearer, and now by inspection I can see this is a tautology. Because xRy, we already know that x=z -> zRy, and same for y=z, and the reverse is clear as well.

So what's the purpose of complicating the formula like that? I don't understand what you hope to gain.

Improve this answer
7
  • Thank you causitive. Since you took the time to look at it, I will accept the answer and add to your reputation. In several places, David Hilbert states that formal axiomatics presupposes decidable equality. The use of the exclusive disjunction makes this explicit. The form of the formula is intended to condition relations to decidable equality as the language signature is expanded. When the signature is expanded with further relations, the new relation is associated with a second formula intended to formally constrain its interpretation. You can see this with any Step 3 and Step 5 at end.
    – user66875
    Jul 25 at 23:02
  • @causitive: For the equality relation, the formula (Step 1 in the systems at the end) relates equality to the usage of the universal quantifier. Other systems I work on relate equality to the usage of the existential quantifier. This syntax is precisely the transitivity axiom (C6) from Tarski's cylindric algebra (see the second listing of axioms at en.m.wikipedia.org/wiki/Cylindric_algebra ) This embeds the existential quantifier into equality statements. In turn, this admits a capacity for implementing the management of existential import as in free logic.
    – user66875
    Jul 25 at 23:15
  • Naturally, the inference rules must be different. Constants and functions are introduced with descriptive syntax, although not Russell's. And the "discernibility relation" from Step 5 on page 62 of the given file must also be used to accommodate the possibility of "non-existents." The inference rules are such that no term for a non-existent shall ever enter a proof. But, the axioms must accomodate the possibility. The methodolgy is directly comparable to what one finds in recursive function theory. But, this is work that no one will ever see. (Kafka's "Letter for the king")
    – user66875
    Jul 25 at 23:26
  • Setting all of the previous comments aside, consider various notions of reductionism for a moment. It may be out of vogue, but, in principle, if someone proposes axioms from which extant "essential" axioms are derived, they "ought" to be intrinsically interesting. I have accepted that this is not the case. I have asked for assistance simply to know whether or not I have made a fatal mistake that I am missing.
    – user66875
    Jul 25 at 23:33
  • @mls Hilbert states that formal axiomatics presupposes decidable equality? But equality is not decidable in the sense of "able to be decided by a Turing machine." There are many relations of equality that a Turing machine cannot decide. And yet this is not a fatal flaw in foundations of mathematics. Hilbert asked whether theorem-proving was decidable, but the answer given by Godel and Turing was "no."
    – causative
    Jul 26 at 0:49

You must log in to answer this question.