A few thoughts, some proofs, and formalizations regarding Connection Theory.
So, apparently, some of my academic work is started to get cited (more frequently - quite a bit more in fact). That's good, since the quality, depth, and creativity of my various writings have increased quite a bit lately.
I've been struggling a bit to make sense of Connection Theory, Thinking Notation, etc. Some more recent action items of note:
Think I've made some progress.
W.R.T. Permalink 138
A straightforward, almost trivial, proof inspired by Graphic Lambda Sequences (which presents and analyzes the Lambda Calculus using familiar Graph Theoretic concepts). The key insight to this approach is that specific operations can be diagrammed in various ways without requiring the use of Graph Theory (Edges, Vertices alone). Not specific to Lambda Calculus alone, this technique focuses on symbolic relationships between syntactic terms (Keywords or Operators in programming) - a level of abstraction that's helpful to finally substantiate a claim or two more fully.
Note: this is a Representation Theorem in the vein of Cayley's Theorem (Representation of a Group by Permutations) which is typically presented as a Two-Column Proof.
The original assertion. The following:
◠ has one or many │| take || take ◠Is equivalent to the more compressed/succinct syntax:
▢ has one or many ▢▢ take ▢I'll adopt the following notational conventions:
⟳β ≡ β ← β - ⟳β is shorthand for: β ← β and represents a Function or Mapping from β to itself.← will stand for the take keyword - e.g. Φ take Φ or | take |.β ⤛ Φ stand for β has one or many Φ or ◠ has one or many │.idₐ → idₐ ≡ idₐ → idₐ → idₐ).◠, │, ▢ with Greek letters for convenience (but these are mostly interchangeable here). β will replace (top-level) ◠ and Φ will replace │.⊢ for "proves" (assuming that Deduction Theorem holds in our relevant Meta Theory per usual).Simple Proof:
β ⤛ Φ, ⟳Φ ← β (Given.)β ⤛ Φ, ⟳Φ ← β ⊢ ▢ ⤛ Φ, ⟳Φ ← ▢ (Uniform Subsitution ▢/β)▢ ⤛ Φ, ⟳Φ ← ▢ ⊢ ▢ ⤛ ▢, ⟳▢ ← ▢ (Uniform Subsitution ▢/Φ)β ⤛ Φ, ⟳Φ ← β ⊢ ▢ ⤛ ▢, ⟳▢ ← ▢ (Transitivity of ⊢)⟳▢ ← ▢ ⊢ ▢ ← ▢ ← ▢ (By the definition given above)▢ ← ▢ ← ▢ ⊢ ▢ ← ▢ (Transitivity of ←)▢ ← ▢ ⊢ ⟳▢ (By the definition given above)⟳▢ ← ▢ ⊢ ⟳▢ (Transitivity of ⊢)▢ ⤛ ▢, ⟳▢ (From 4 and 8)That reads:
▢ has one or many ▢▢ take ▢Arriving at the conclusion stated without proof many years ago.
Certain, interesting, properties:
A single synatic mark can do all the work. But it must have certain properties (described above). I've selected the squiggly mark: ⧘ since it seems to suggest a multitude of meanings that aren't fixed. Here we will make that impression explicit.
With Empty and Chiastic Sequences, a single Axiom can do all the work that the many did before.
It can be simultaneously expressed as both:
⧘ ⧘
⧘ ⧘or: ⧘ (since these are taken to be equivalent).
Generally, ⧘⧘ = ⧘ and ⧘ = ⧘⧘. This is a Self-Replicating Quine-type sequence. We'll need a few more definitions to fully flesh this idea out.
A Chiastic Sequence ς contains all elements constituting it and is the Chiastic Sequence for all elements.
I, II, III, ...III contains I and II. III isn't merely a "third" (or relative) position/index. It fully conveys the sequence up to itself (and indeed contains the sequence at that index itself). Returns (preserves) the (current) Slice or Element of the Chiastic Sequencing. Given the description above, it should be clear that each Element is a Slice (since each Chiastic index contains all prior Elements of the Sequence).
ς returns φ returns current Chiastic element φ from Sequence ς. This handles Existence and serves as an alternative to Lambda Binding. φ can be thought of as a Singleton (how Frege and Python treat True) but it needn't be. (Although, I think that if it is, the following point is more palatable.)Uₙ(n) returns Uₙ alternatively fₙ(n) returns Fₙ (to better draw out the distinction between the Function fₙ and the Set Fₙ). This handles both Type Assignment (think adding an Element Extensionally or Nominally to the Set Uₙ/Fₙ) and Typing for n (think typeof) which is given by Uₙ/Fₙ. The second component can also be thought of Chiastically (above) - Type Assignment Set Membership is Sequential and Uₙ/Fₙ is a Chiastic Element in such a Sequence (especially if φ is a Singleton).
Per the above, this will be Semantically Immured (we will wrap part of the Language into the Token itself). It's a Quine (programming), self-replicating. It's polysemantic expressing a multitude at once (in any singular occasion of use) - a polymark that at once stands for an exactly singular thing and a multitude simultaneously (akin to Unitary Evolution I suppose, it can continue in this way or be resolved to one disambiguation).
⧘ ⧘
⧘ ⧘
⧘therefore returns Slice Preservation, Empty,⧘⧘⧘⧘, or Chiastic Sequence, etc. (We can think of⧘as being "called" like a Function.) A key notion here is that through Chiasmus, the Seperator syntactic mark can be entirely omitted.
This moves the ball forward quite a bit. There are still some unwanted conceptual dependencies (reliance on Sets, Functions, etc.) that will need to be translated and omitted (some of that was already done in another paper).