Read on Twitter
so i started a thread on this where i began from a very big picture and started drilling in, but i ended up in a rather abstract place which was possibly not terribly helpful for starting with
and also not rly concrete examples
so let& #39;s try this again. https://twitter.com/johncarlosbaez/status/1300673552643809280">https://twitter.com/johncarlo...
and also not rly concrete examples
so let& #39;s try this again. https://twitter.com/johncarlosbaez/status/1300673552643809280">https://twitter.com/johncarlo...
(previous attempt: https://twitter.com/sarah_zrf/status/1301604358962974721)">https://twitter.com/sarah_zrf...
so let& #39;s work in a very pleasant and friendly category: Set.
let& #39;s use my favorite example formula φ(x) when discussing this topic (the variables range over the set R of real numbers):
∃y. x² + y² = 1
define φ₀(x, y) as x² + y² = 1, so that φ(x) is ∃y. φ₀(x, y)
let& #39;s use my favorite example formula φ(x) when discussing this topic (the variables range over the set R of real numbers):
∃y. x² + y² = 1
define φ₀(x, y) as x² + y² = 1, so that φ(x) is ∃y. φ₀(x, y)
now:
if we assign a particular value for the variable x, then the formula φ(x) has a particular truth value. for r ∈ R, let& #39;s write φ[r] for the assertion that φ(x) is true when x is set to r. so φ[10] is false, but φ[½] is true.
if we assign a particular value for the variable x, then the formula φ(x) has a particular truth value. for r ∈ R, let& #39;s write φ[r] for the assertion that φ(x) is true when x is set to r. so φ[10] is false, but φ[½] is true.
now, classically, "truth values" are elements of the set {⊥, ⊤}, and even non-classically, they coincide with subsets of a singleton. and φ(x) itself does not have a particular single truth value in this sense, in the absence of a fixed choice of x.
but we *can* assign it a single "truth value" which is (classically) an element of a boolean algebra: the algebra P(R). if φ(x) associates each possible value of x to a truth value, then it defines a characteristic function, & we can take the set {r ∈ R | φ[r]} ⊆ R.
recalling that we defined φ(x) as ∃y. x² + y² = 1, this set should be the interval [-1, 1].
now, the formula φ₀(x, y) has a single overall truth value if we give values for both x *and* y. so it defines a characteristic function on the space of possibilities of *pairs*, which gives us a "truth value" in P(R²):
{(r₁, r₂) ∈ R² | φ₀[r₁, r₂]} ⊆ R²
{(r₁, r₂) ∈ R² | φ₀[r₁, r₂]} ⊆ R²
when you look at the definition of φ₀(x, y)—i.e., x² + y² = 1—and go "oh, the unit circle", formally speaking you& #39;re recognizing *this set* as the unit circle (as a set of points in R²)—at least, unless you& #39;re doing fancy shit with schemes (:
so in general, if we have a formula ψ(x, y, ...) with free variables x, y, ... referring to elements of sets X, Y, ..., this determines a subset of X × Y × ..., and that& #39;s (classically) an element of a boolean algebra, so a kind of "overall truth value".
let& #39;s write ⟦ψ(x, y, ...)⟧ for that subset.
you can check that ⟦-⟧ turns basic propositional symbols into operations on sets—for example, ⟦ψ(x) ∧ χ(x)⟧ = ⟦ψ(x)⟧ ∩ ⟦χ(x)⟧, and similarly ∨ becomes ∪.
you can check that ⟦-⟧ turns basic propositional symbols into operations on sets—for example, ⟦ψ(x) ∧ χ(x)⟧ = ⟦ψ(x)⟧ ∩ ⟦χ(x)⟧, and similarly ∨ becomes ∪.
so you can explain the meaning of logical connectives with poset structure—formulas give elements of these posets/algebras, and the connectives correspond directly to the posets& #39; natural equipment (meets, joins)
and importantly, this is "compositional"
you can explain ⟦ψ(x) ∧ χ(x)⟧ in terms of ⟦ψ(x)⟧ and ⟦χ(x)⟧, you don& #39;t need to peek at what ψ(x) and χ(x) look like as well
you can explain ⟦ψ(x) ∧ χ(x)⟧ in terms of ⟦ψ(x)⟧ and ⟦χ(x)⟧, you don& #39;t need to peek at what ψ(x) and χ(x) look like as well
so:
what about quantification?
in our example, we know that ⟦φ(x)⟧ is [-1, 1] ⊆ R and ⟦φ₀(x, y)⟧ is S¹ ⊆ R².
since φ(x) is ∃y. φ₀(x, y), it should hopefully be possible to explain ⟦∃y. φ₀(x, y)⟧ = [-1, 1] in terms of ⟦φ₀(x, y)⟧ = S¹.
what about quantification?
in our example, we know that ⟦φ(x)⟧ is [-1, 1] ⊆ R and ⟦φ₀(x, y)⟧ is S¹ ⊆ R².
since φ(x) is ∃y. φ₀(x, y), it should hopefully be possible to explain ⟦∃y. φ₀(x, y)⟧ = [-1, 1] in terms of ⟦φ₀(x, y)⟧ = S¹.
and indeed, we can: consider π₁ : R² → R, the projection from the plane to the x-axis. then
[-1, 1] = π₁(S¹)
and indeed, you can check that it makes sense in general that ⟦∃y. ψ(y, z, w, ...)⟧ = π(⟦ψ(y, z, w, ...)⟧), where π : Y × Z × W × ... → Y × Z × W × ...
[-1, 1] = π₁(S¹)
and indeed, you can check that it makes sense in general that ⟦∃y. ψ(y, z, w, ...)⟧ = π(⟦ψ(y, z, w, ...)⟧), where π : Y × Z × W × ... → Y × Z × W × ...
what does this have to do with adjunctions?
well, for any f : X → Y, we have functions ∃_f : P(X) → P(Y) and f^* : P(Y) → P(X), the former taking image and the latter taking preimage. these are easily monotone, so theyre functors, & then it& #39;s not hard to check:
∃_f ⊣ f^*
well, for any f : X → Y, we have functions ∃_f : P(X) → P(Y) and f^* : P(Y) → P(X), the former taking image and the latter taking preimage. these are easily monotone, so theyre functors, & then it& #39;s not hard to check:
∃_f ⊣ f^*
exercise to the motivated reader: work out the right adjoint to f^* and show that ⟦∀y. ψ(y, z, w, ...)⟧ = ∀_π(⟦ψ(y, z, w, ...)⟧), where π is as above—so we have
∃_π ⊣ π^* ⊣ ∀_π
∃_π ⊣ π^* ⊣ ∀_π
ummm shit i probably should& #39;ve noted at some point the idea of like... if we have a formula ψ(z, w, ...) in which y does not occur free, then we can consider it as ψ& #39; parameterized by y but just constant in it, and then ⟦ψ& #39;(y, z, w, ...)⟧ = π^*(⟦ψ(z, w, ...)⟧)
anyway, i *really* recommend also reading the other thread i posted (here& #39;s the link again: https://twitter.com/sarah_zrf/status/1301604358962974721)">https://twitter.com/sarah_zrf... and working on paper thru how the examples in *this* thread are instances of the concepts there
this gives a fuller understanding!!!!!
this gives a fuller understanding!!!!!
...okay i think i could probably have written something a lot better if i& #39;d planned better but
such is tweets
and it couldve been a lot worse also
hope this is at all comprehensible or helpful to anyone curious???
such is tweets
and it couldve been a lot worse also
hope this is at all comprehensible or helpful to anyone curious???
anyway @silvascientist @JBeardsleyPhD hope you get anything out of these 
https://abs.twimg.com/emoji/v2/... draggable="false" alt="😅" title="Lächelndes Gesicht mit offenem Mund und Angstschweiß" aria-label="Emoji: Lächelndes Gesicht mit offenem Mund und Angstschweiß">
