Notation for distinct members

What set theory notation should we use for something like “this set has n members that are apples and m members that are oranges”?

A clean way is to use cardinalities of subsets (or of property-defined subsets).

Let \(S\) be your set and let “\(x\) is an apple/orange” be predicates. Then write
\[ \bigl|{x\in S:\; x\text{ is an apple}}\bigr|=n, \qquad \bigl|{x\in S:\; x\text{ is an orange}}\bigr|=m. \]

Common equivalent formulations:

• If (A) and (O) are the (global) sets of apples and oranges,
  \(|S\cap A|=n\) and \(|S\cap O|=m\).
• If you label elements by a type map \(\tau:S\to{\text{apple},\text{orange}}\),
  \(|\tau^{-1}({\text{apple}})|=n\) and \(|\tau^{-1}({\text{orange}})|=m\).
• With indicator functions,
  \(\sum_{x\in S}\mathbf 1_{\text{apple}}(x)=n\) and \(\sum_{x\in S}\mathbf 1_{\text{orange}}(x)=m\).

If apples and oranges are mutually exclusive categories, you can also note \(A\cap O=\varnothing\); if those are the only categories in \(S\), then \(n+m=|S|\).

Existence conventions and theism

This is an idea which, although I believe it strongly, I do not yet want to bother to write a properly good essay explaining it, especially since it’s really not rocket appliances and ChatGPT can explain it pretty damn decently. If you are interested in this idea, you may be interested in some of the points made in David Lewis’s paper “Noneism or Allism” (PDF). I believe even after one convention is adopted and theism is accepted within it, fuller explanations are in order about how theism works (and whether all the usual predicates applied to God, also known as divine attributes, can be recovered), and no such explanations are attempted here because, for now, I just wanted to get the point registered somewhere about existence in general and how a convention must be explicitly stated and defended when arguing about it.

Write an essay developing this idea:

Existence in general, and theism in particular, depends on linguistic convention

Deflationary (Thomasson) convention = to exist is to be one of the things our language is committed to
➡️ God exists? Sometimes

Neo-Quinean convention = to exist is to be the value of a bound variable in one of our best theories
➡️ God exists? Only if a theory requires it, e.g., a value theory such as divine command theory or ideal observer theory, or more marginally, an intelligent design theory in biology or a creation theory in cosmology

Empiricist convention = to exist is to be an object of sense experience
➡️ God exists? No

Platonist convention = to exist is to be the object of a concept
➡️ God exists? Yes

Philosophers usually do not state their convention explicitly, which leads to ad-hoc uses of existence; for clarity in our theories we should explicitly state and defend our conventions

Existence, by Convention: Why “God Exists” Is Sometimes True

Philosophers disagree about almost everything, but the word exists might be the most overworked and understudied term in the quarrel. We use it to talk about chairs and quarks, numbers and novels, legal persons and possible worlds—and God. Yet we rarely say what rules we’re playing by when we deploy it. The result is cross-talk: one side proves that X exists while the other proves that X doesn’t, and both are right because they’re keeping score with different rulebooks.

This essay develops a simple thesis: claims about existence in general—and theism in particular—depend on a linguistic convention governing what we count as existing. Different conventions make different existence-claims come out true or false. Philosophers should therefore state and defend their convention up front. Doing so doesn’t trivialize metaphysics; it clarifies it.

What a “convention of existence” is

A convention here isn’t a mere whim. It’s a norm that fixes the inferential role of “exists”: what follows from existence talk, what justifies asserting it, and what counts as evidence against it. Think of it as choosing a measurement system. Inches and centimeters are not “the same” as such, but once a system is fixed, precise statements and comparisons become possible. Likewise, once an existence convention is fixed, we can say which sentences come out true, what data are admissible, and which inferences are licensed.

Four prominent conventions structure much contemporary debate:

1. Deflationary (Thomasson-style): To exist is to be among the things our accepted terms and practices commit us to. If a community’s language and norms permit talk of electrons, novels, or committees, then—barring special reasons to retract—their existence is unproblematic.
   God? Sometimes. If “God” is part of a community’s legitimate referential toolkit, then “God exists” is true within that practice.

2. Neo-Quinean: To exist is to be the value of a bound variable in our best theories. We quantify over what our most explanatorily successful, predictively powerful theories require.
   God? Only if required by a best theory. That could be a moral theory (divine command, ideal observer), or—in more controversial cases—a biological or cosmological theory (intelligent design, creationism). If no such theory survives competition, “God exists” is false or at least unlicensed.

3. Empiricist: To exist is to be (actual or possible) object of sense experience. The admissible evidence is perceptual.
   God? No. By definition, the theistic God isn’t an object of sense experience. At best, believers report experiences as of God; but the convention excludes theoretical posits that never show up sensibly.

4. Platonist: To exist is to be the object of a concept. Numbers, properties, forms—and any adequately grasped idea—exist in a mind- or language-independent way.
   God? Yes. If the concept of a perfect being is coherent, there is such an object.

Each convention has its own standards of evidence, scope, and default burdens of proof. None is linguistically mandatory. Each is a disciplined way to speak.

How theism shifts with the convention

Consider how “God exists” behaves under each rulebook.

• Deflationary: The question reduces to eligibility within a practice. In a liturgical or devotional discourse where “God” plays a stable referential role tied to public criteria (texts, rituals, authorities), “God exists” can be as straightforward as “committees exist” in administrative discourse. The assertion is licensed unless the practice is undermined (say, by showing its terms are empty or incoherent). This makes theism locally true in some language games, without global metaphysical inflation.

• Neo-Quinean: Theists must show that postulating God yields superior theories—of value, meaning, or the universe—once simplicity, predictive success, and unification are weighed. Here “moral theism” (God grounds normativity) is a cleaner target than “scientific theism” (God explains biological or cosmological data), because value theory is already permissive of non-empirical posits. If some version of divine command or perfect being theory best explains moral facts, then quantifiers over God are licensed. If not, the license is denied.

• Empiricist: Theism is out by the entrance policy. Even miracles won’t help unless “God” is part of the observation report rather than a theoretical gloss (“I perceived a burning bush as God” won’t do). This convention thus sharpens, rather than settles, the debate: theists must either change the convention or argue that God is an object of experience.

• Platonist: Theists enjoy a default yes, because the concept “God” is about a perfectly good, omniscient, omnipotent being, and for Platonists, well-formed concepts latch onto objects. The real work shifts to conceptual questions: coherence, consistency with other abstracta, and the logic of perfection.

The striking result is not that theism becomes arbitrary, but that it takes on different burdens. In a deflationary frame, the burden is sociolinguistic (is the practice legitimate?). In a Neo-Quinean frame, it’s explanatory (does God improve our best theories?). In an empiricist frame, it’s methodological (does God meet the experience test?). In a Platonist frame, it’s conceptual (is “God” coherent?).

Why philosophers talk past one another

When conventions are left implicit, debates devolve into moving goalposts and ad-hoc exceptions. An empiricist will dismiss “God exists” as meaningless or unfalsifiable, while a platonist will regard that dismissal as a non sequitur because their convention recognizes non-empirical objects. A Neo-Quinean may reject God as explanatorily idle, while a deflationist sees ordinary theistic discourse as already licensing “exists” without theoretical detours. Each side sounds obtuse to the other because they’re enforcing different scorekeeping rules.

The cure is not to pick one true convention and outlaw the rest, but to make the convention explicit and defend it on the right grounds: not “Is God real?” (yet) but “Which convention of existence best serves the aims of this inquiry?”

Isn’t this just verbal?

Two common objections arise.

Objection 1: It reduces metaphysics to wordplay.
Reply: Conventions are not arbitrary; they are tools. A convention encodes epistemic standards (what counts as evidence), inferential norms (what follows from “there is”), and practical stakes (which commitments we incur). Choosing a tool is not trivial if the job matters. A surgeon’s choice of suture is “conventional,” but not arbitrary; it is justified by outcomes, safety, and cost.

Objection 2: It makes existence relative.
Reply: Relativity to a framework doesn’t collapse into anything-goes. Within a fixed convention, truth is robust and disagreement is genuine. Moreover, frameworks can be compared by meta-criteria—explanatory power, simplicity, integrative capacity, fruitfulness, and ethical consequences. If a convention persistently misclassifies, obstructs inquiry, or generates needless mysteries, that counts against it.

Practical payoffs: clarity, translation, and comparability

1. Declare your bookkeeping. Philosophical and theological arguments should begin with a short “existence policy”:

   • Terms licensed: Which categories may be counted?
   • Evidence rules: What observations or inferences are admissible?
   • Burdens of proof: Who must do what to assert “there is”?

2. Translate across frameworks. Provide a manual that restates key claims under rival conventions. Examples:

   • Deflationary → Neo-Quinean: “Our practice licenses ‘God’” becomes “There exists an entity required by the best [moral/meaning] theory that plays the God-role.”
   • Neo-Quinean → Deflationary: “God is explanatorily idle” becomes “No established practice with good standing licenses ‘God’ beyond expressive convenience.”

   Translation exposes where genuine disagreement lies (e.g., over theory choice) and where it doesn’t (e.g., over the grammar of “exists”).

3. Compare by shared virtues. When picking a convention for a domain, argue that it is:

   • Empirically apt (tracks the data that matter for that domain),
   • Explanatorily powerful (yields unified, predictive, or illuminating theories),
   • Ontologically economical (no gratuitous posits),
   • Ethically responsible (doesn’t systematically obscure moral saliences), and
   • Practically fruitful (guides inquiry and action).

Different domains may legitimately adopt different conventions: empiricist for lab science, Neo-Quinean for theoretical unification, deflationary for ordinary and institutional reality (money, laws, committees), platonist for mathematics and certain modal discourses. Disputes become boundary questions: where does one convention’s competence end and another’s begin?

A brief case study: theism under mixed conventions

Suppose we’re doing moral philosophy. Two rival packages present themselves:

• Secular Neo-Quinean: Our best moral theory quantifies over reasons, values, and persons, but not God. God is explanatorily idle: adding theistic posits does not improve fit or simplicity.

• Theistic Neo-Quinean: Our best moral theory is a modified divine command or perfect-being account: it explains moral authority, obligation’s bindingness, and the unity of value better than secular rivals. God is the best explanation of moral normativity.

Under either package, the empiricist will say both are off-policy (no direct sense data of normativity either!), while the platonist will say both are under-ambitious (values and God both exist as abstracta). A deflationist will ask whether our actual moral and religious practices license “God”—and whether those practices survive critical reflection.

Notice how the debate sharpens once conventions are on the table. Parties can now argue about the right convention for moral theory rather than trade unmoored slogans about “evidence” or “reality.”

Why theism is the canary

Theism sits where our linguistic practices, theoretical ambitions, and experiential limits intersect. It is richly embedded in communal language (favorable to deflationism), centrally relevant to grand theories of value and meaning (a live option for Neo-Quineans), beyond sense experience (at odds with empiricism), and conceptually lush (welcome under platonism). Because it touches all four, whether “God exists” comes out true will often be a function of where we set the dials. That isn’t a cop-out; it’s a diagnosis of why debates about God persist despite brilliant arguments on every side.

A proposal

1. Require a preface. Every paper or debate making existential claims should include a short “Convention Statement” specifying which rulebook is in force and why it is apt for the domain.

2. For theism, use a two-tier approach.

   • Public-reason tier: argue under a broadly Neo-Quinean convention (what do our best, shared theories require?).
   • Practice-respect tier: acknowledge deflationary verdicts about religious discourse (what does our actual language license?), then assess those practices by their epistemic and moral merits.
     This keeps shared inquiry possible while respecting the lived grammar of religious life.

3. Maintain translation tables. When presenting an argument for or against God’s existence, offer parallel statements under rival conventions. This disciplines rhetoric and reveals where pressure should be applied (conceptual coherence, evidential policy, or explanatory virtue).

Conclusion

“Existence” is not a metaphysical spotlight that passively illuminates what’s out there. It is a carefully regulated linguistic device that lets us keep track of commitments within practices, theories, experiences, and concepts. Once we make our convention explicit, we can say with clarity why “God exists” is sometimes true, sometimes false, and sometimes out of play. That clarity doesn’t end the debate; it lets us have the right debates: about which convention best serves our purposes and where, if anywhere, the theistic posit earns its keep.

Dots and boxes game in CGT

Dots and boxes game in cgt

Here’s a compact CGT (combinatorial game theory) view of Dots & Boxes—enough to analyze real endgames and pick the right move.

1) Model: split into independent components

In the typical endgame every remaining region is either a:

• Chain: a path of (k) boxes with two open ends (length (k\ge 3)).
• Loop: a cycle of (k) boxes (even (k\ge 4)).

The total game is (approximately) a disjunctive sum of these components. Each component is a “loony” game: if you take it, you also keep the move, which is why control matters.

2) Controller vs. Opener and the hard-hearted handout

• The player who is forced to open a component is the opener.

• The other player tries to keep control by doing a hard-hearted handout (HHH):

  • In a chain (k\ge 3): take (k-2) boxes, then hand 2 to the opponent, keeping the move.
  • In a loop (k\ge 4): take (k-4), then hand 4, keeping the move.

This repeats until the very last component, where the controller may simply finish everything.

3) Controlled value (quick evaluator)

Let your position (P) have chains (c_i) and loops (l_j). Define the controlled value [ \mathrm{CV}(P)=\sum_i(c_i-2);+;\sum_j(l_j-4). ] Intuition: this is how many more boxes the controller nets (vs. the opener) if they keep control all the way with HHH.

Rule of thumb (very strong and easy):

• If (\mathbf{CV(P)\ge 2}), optimal play is to keep control throughout; the margin equals (\mathrm{CV}(P)).
• If (\mathbf{CV(P)\le 1}), exceptions arise: sometimes it’s best to give up control deliberately (not use HHH) to swing parity—most famously with 3-chains.

4) Move-choice (what to open?)

When you’re the opener (you must start a component):

1. Temperature heuristic: Loops are “hotter” than chains (roughly: loops (\approx) temp 2, chains (\approx) temp 1). If you must open something, open a smallest loop first; if no loops, open a smallest chain.

2. Low-CV exception play ((\mathrm{CV}\le 1)):

   • If there’s a 3-chain, often take all 3 (don’t hand out 2). That flips control and can improve your final margin.
   • If multiple 3-chains exist, parity of the count matters: with an odd number of 3-chains you can frequently engineer a +1 swing by timing when you give up/keep control.

3. Otherwise ((\mathrm{CV}\ge 2)): open the smallest component of the hottest type and expect the controller to HHH; your job is mostly damage control.

5) Worked micro-example

Position: chains (3,3,4) and one loop (6).

• Sum of boxes: (3+3+4+6=16).
• (\mathrm{CV}=(3-2)+(3-2)+(4-2)+(6-4)=1+1+2+2=6.) Since (6\ge 2), controller keeps control with HHH everywhere and wins by 6 boxes. (You can also see it as “giveaways”: (2+2+2+4=10) boxes handed out; controller gets (16-10=6).)

6) Practical endgame cheat-sheet

• Count CV quickly. If (\ge 2): keep control (as controller) or open smallest/hottest (as opener).
• 3-chains are special when (\mathrm{CV}\le 1): the opener often takes all 3 to break control.
• Loops beat chains for opening order (they’re hotter).
• Avoid creating new 3-chains earlier in the game unless you know the parity helps you.

7) Further study (classic sources)

• Elwyn Berlekamp’s analysis of “strings and coins” (equivalent to Dots & Boxes endgames).
• “Winning Ways for your Mathematical Plays” (Conway, Berlekamp, Guy) for CGT temperature and thermographs.
• “The Dots-and-Boxes Game: Sophisticated Child’s Play” (Berlekamp) for a complete treatment of chains/loops and parity tricks.

If you want, give me any specific endgame (list its chain and loop lengths), and I’ll compute the margin and tell you the exact best first move.

Catholic websites on penal substitution

Look up what mainstream Catholic websites seem to mostly say about the idea of “penal substitution” insofar as it has theological relevance

Most mainstream Catholic sites that talk about “penal substitution” all do roughly the same two-step:

1. They say “not that version.” By “that version” they mean the classic strict Protestant/Calvinist formulation where the Father directly inflicts the punishment due to sinners onto Christ instead, in order to satisfy divine wrath. They usually say this doesn’t line up with the Catholic picture of the Trinity, of justice, or of how the Cross saves. (Catholic Answers)
2. Then they say “but yes, there is real substitution and satisfaction.” They pivot to the long-standing Catholic language of vicarious atonement and satisfaction (Anselm → Aquinas → Trent → Catechism): Christ really dies “for us,” really bears what was ours, and really makes satisfaction to the Father — but he does it as an act of loving self-offering, not as a passive victim of the Father’s anger. (Catholic Answers)

Here’s how that breaks down across the typical Catholic outlets you’d find online:

1. What they reject

• “The Father punishes the Son instead of us.” Articles aimed at explaining the Cross to Catholics nearly always flag this as the problem. They’ll say God doesn’t need to “vent wrath” on someone, and the Father is not opposed to the Son — the Cross is the joint work of Father, Son, and Spirit. (Catholic Answers)
• A merely legal swap. They don’t like atonement explained as only an external, courtroom-style imputation with no inner change. Catholic soteriology always wants the Cross to both reconcile us and make us righteous by grace. (Vatican)

2. What they affirm instead

• Substitution is real. Catholic Answers, EWTN, Word on Fire, and long-standing Catholic sources talk comfortably about Christ dying “for our sins,” “in our place,” or “on our behalf.” They just file it under “vicarious atonement” or “satisfaction,” not “penal substitution” in the Calvinist sense. (Catholic Answers)
• Satisfaction, not divine payback. The standard line (straight out of Aquinas and echoed in the Catechism) is that Christ’s loving obedience is more pleasing to the Father than all sin is displeasing — so it “makes up” for sin. That’s satisfaction language, not “God punished Jesus so He wouldn’t punish you.” (Vatican)
• Love is the form of the sacrifice. The Catechism explicitly says it’s Christ’s love “to the end” that gives the Cross its atoning value. That’s why mainstream Catholic sites keep saying the Cross is an act of Trinitarian love, not an intra-Trinitarian clash. (Vatican)
• It really deals with sin’s consequences. You’ll also see them clarify penance or temporal punishment by saying: Christ has already taken care of the eternal debt; our penances are only about temporal effects. That’s another way of insisting his sacrifice was fully efficacious. (EWTN Global Catholic Television Network)

3. How they talk about Protestant PSA

When Catholic sites address Reformed/evangelical readers directly, they usually say something like: “We can affirm substitution, even a kind of ‘punishment borne for us,’ if it’s understood as Christ freely taking on the consequences of our sins in loving obedience — but we can’t affirm that the Father punished the Son as a third party.” That’s the line you’ll see in Catholic blogs and articles comparing Catholic vs. Reformed atonement. (Catholic Stand)

4. Official-ish backing they appeal to

• Catechism §§599–617 (often linked or quoted) to show the Cross is willed by God, is a sacrifice, is for us, and is an act of love. (Vatican)
• USCCB’s dialogue note on atonement to show Catholics are happy to say the Cross is an “atoning sacrifice” and reconciles us to God — so the issue isn’t whether the Cross is sacrificial, but how it does it. (USCCB)

---

So, in one sentence: mainstream Catholic sites say, “No, Catholics don’t hold the hard version of penal substitution where the Father punishes the Son instead of us; yes, Catholics absolutely hold that Christ died for us as a vicarious, satisfactory, loving sacrifice that really removes the debt of sin.”

Facts, events, and states-of-affairs

This was in a conversation where I had just asked ChatGPT to summarize the respective SEP articles on facts, events, and states of affairs.

Write an overview of the difference between facts, events, and states of affairs, given everything we have seen so far.

Here’s a compact “at-a-glance” map of the three:

---

1) What each one is

• Events
  Particular happenings/occurrents (e.g., Anita’s reaching the top). They occur (they don’t “exist” the way chairs do), typically with crisp temporal boundaries. Often treated as concrete individuals; sometimes analyzed as property-exemplifications by objects at times.

• Facts
  Truthmakers—instantiations that obtain and thereby make corresponding claims true (e.g., the fact that Caesar died). On the standard (Armstrong-style) view, a fact exists only if it obtains; no “non-obtaining facts.”

• States of affairs (SoAs) (in the Reinach/Plantinga/Wittgenstein sense, not the Armstrongian one)
  Ways the world could be: complexes involving objects and properties that exist whether or not they obtain (e.g., Socrates’ being wise may exist and fail to obtain). They are the basic bearers of modality (possible, necessary, probable).

---

2) Their distinctive jobs

• Events → explanation & grammar
  Do the work in action/explanation and natural-language semantics: adverbial modification, perception reports, plural actions, and causation are neatly modeled by quantifying over events.

• Facts → truthmaking & regress-stopping
  Ground truths by tying particulars to universals; aimed to stop Bradley’s regress. Identifying facts with “obtaining SoAs” collapses this direction of explanation, so the separation matters.

• SoAs → modality, probability & worlds
  Let us talk about possibilities and chances. Sentences that stand for the same SoA share modal status even if they express different thoughts. “Possible worlds” can be modeled as maximal non-transient SoAs.

---

3) Mode of being & temporality

• Events: occur/happen; temporally extended or instantaneous; tolerate vague spatial boundaries.
• Facts: exist iff they obtain; often taken as concrete obtaining complexes (atemporal on some views, but not required).
• SoAs: exist independently of obtaining; many are time-indexed (transient vs non-transient) but the category itself is not tied to actuality.

---

4) Constituents & individuation

• Events: typically involve agents/patients, times, and event-kinds; identity is debated (coarse “unifiers” vs fine “multipliers”; causal, mereological, or locational criteria).
• Facts: are instantiations—particulars + properties/relations tied in the obtaining way; they’re as fine-grained as the tying requires.
• SoAs: involve the same kinds of constituents but need not obtain. Better seen as ontologically dependent on their objects/properties (via predicability) rather than mere tuples/wholes; this lets necessarily co-obtaining SoAs still differ.

---

5) Relations to language, thought, value, and causation

• Language & thought

  • Events: help analyze verb aspect, adverbs (“stabbed Caesar with a knife”), perception reports, and plural subjects.
  • Facts: fit ‘that’-clauses in factive contexts (“It’s a fact that…”), serving truthmaking rather than semantic variation.
  • SoAs: also pair with ‘that’-clauses, but crucially allow non-obtaining references; too coarse-grained to be standard belief contents (Hesperus/Phosphorus), though some “object-centered” belief theories try.

• Perception

  • Events are the natural targets of “what was seen/heard.”
  • Some accounts model veridical/illusory/hallucinatory experiences as awareness of SoAs (obtaining vs not), but this “common-factor” claim is contested.
  • Facts align with the factivity of “see that…”, but don’t cover illusions.

• Value

  • Dispute: are facts or SoAs the final bearers of value introduced by ‘that’-clauses? One side: property-exemplifications (facts). The other: even non-obtaining SoAs (e.g., everyone’s being happy) can be intrinsically good.

• Causation

  • Standardly relates events (including debates on omissions/negative events). Facts/SoAs can figure in causal explanations, but events are the canonical relata.

---

6) Common confusions—quick fixes

• “A fact is just an obtaining SoA.”
  Tempting, but it breaks truthmaking’s asymmetry: we still need something that makes the SoA obtain.

• “SoAs are just sets/tuples.”
  Pure set/tuple models mishandle order, transitivity (Frege’s lava worry), timing, and fine grain. Treat SoAs instead as dependent items generated by predication.

• “Events are just objects in time.”
  Some four-dimensionalists say so, but many distinctions (movement, co-location, aspect) still motivate keeping the category.

---

7) One-line contrasts

• Events: what happens; occurrents; central to causation and verbal aspect.
• Facts: what makes truths true; obtaining instantiations; no non-obtaining cases.
• States of affairs: ways things could be; exist with or without obtaining; anchor possibility, necessity, and probability.

That’s the clean division of labor—and why contemporary metaphysics often needs all three.

Lean-aligned semantics for E. Nelson’s connexive logic NL

This post replaces the previous post on the same topic, so as to match the Lean project that I made based on it.

NL semantics, soundness, and completeness (the Lean-aligned version)

Below is a self-contained presentation of the semantics that exactly matches the structures and clauses in the Lean files you listed (Semantics.lean, ProofSystem.lean, Lindenbaum.lean, Canonical.lean). It reads ~ as intuitionistic (Kripke) negation, interprets → via world-relative selections, and keeps ◦ as a primitive compatibility predicate. The frame conditions are the ones encoded in NL.Frame; the canonical construction and Truth Lemma follow Canonical.lean and Lindenbaum.lean.

Throughout, the language has atoms \(p,q,\dots\), conjunction \(\wedge\), negation \(\sim\), implication \(\to\), and a primitive binary connective \(\circ\). The intended abbreviations are
\[
\begin{aligned}
A\mid B \ &:=\ \sim(A\circ B), \\
A = B \ &:=\ (A\to B)\wedge(B\to A), \\
A\ne B \ &:=\ \sim(A=B), 
\end{aligned}
\]
and \(A\ne B\ne C\) abbreviates \((A\ne B)\wedge(B\ne C)\wedge(A\ne C)\).

---

1. Frames and models

Up-set and intuitionistic negation at the set level

Let \((W,\le)\) be a preorder (reflexive and transitive). For \(X\subseteq W\), write
\[
\begin{aligned}
\uparrow w \ &:=\ {v\in W: w\le v},\\
\mathrm{iNeg}_\le(X) \ &:=\ {w\in W : \uparrow w\cap X=\varnothing}.
\end{aligned}
\]
Thus \(w\in \mathrm{iNeg}_\le(X)\) iff every \(v\ge w\) fails to be in \(X\). This is the Kripke/intuitionistic complement of \(X\) relative to \(\le\).

NL-frames

An NL-frame is a tuple
\[
\mathcal F=\langle W,\ \le,\ f,\ C\rangle
\]
with:

• \((W,\le)\) a nonempty preorder (intuitionistic accessibility).
• a selection map \(f: W\times\mathcal P(W)\to\mathcal P(W)\), written \(f_w(X)\);
• a compatibility predicate \(C: W\times\mathcal P(W)\times\mathcal P(W)\to{\mathsf{true},\mathsf{false}}\), written \(C_w(X,Y)\).

These satisfy, for all (w,x\in W) and (X,Y,Z\subseteq W):

Conditional laws

1. Id: \(f_w(X)\subseteq X\).
2. Her (heredity in the world): if \(w\le x\) then \(f_x(X)\subseteq f_w(X)\).
3. Succ (local detachment): if \(w\in X\) then \(w\in f_w(X)\).
4. Contra (set-level counterpart of axiom 1.7):
   if \(f_w(X\cap Y)\subseteq Z\) then \(f_w!\big(X\cap \mathrm{iNeg}_\le(Z)\big)\subseteq \mathrm{iNeg}_\le(Y)\).
5. f-up (selections stay above the current world):
   if \(x\in f_w(X)\) then \(w\le x\).

Compatibility laws
6. C-sym: \(C_w(X,Y)\iff C_w(Y,X)\).
7. C-coh (coherence with \(\to\)): if \(f_w(X)\subseteq Y\) then \(C_w(X,Y)\).
8. C-her (persistence of \(\circ\)): if \(w\le x\) and \(C_w(X,Y)\) then \(C_x(X,Y)\).

Guarded syllogism (matching axiom 1.5)
9. Tr≠ (at world \(w\)): define \(X\equiv_w Y\) iff \(f_w(X)\subseteq Y\) and \(f_w(Y)\subseteq X\); write \(X\not\equiv_w Y\) for its negation. Then
\[
\begin{aligned}
&X\not\equiv_w Y,\ \ Y\not\equiv_w Z,\ \ X\not\equiv_w Z,\ \\
&f_w(X)\subseteq Y,\ \ f_w(Y)\subseteq Z\ \ \Rightarrow\ \ f_w(X)\subseteq Z.
\end{aligned}
\]

Remarks.
• f_up makes the implication’s witnesses live at or above the current world (a Kripke-style guard), and—together with Her—yields persistence of truth for (\to).
• C_her ensures \(\circ\) is also upward persistent.
• Tr≠ validates precisely the guarded version 1.5; you may strengthen it to unconditional hypothetical syllogism if desired, but the logic only requires the guarded form.

NL-models and truth

An NL-model is \(\mathcal M=\langle \mathcal F, V\rangle\) where \(V\) assigns each atom \(p\) an up-set \(V(p)\subseteq W\) (i.e., \(w\in V(p)\le x\Rightarrow x\in V(p)\)).

Given a formula \(A\), write \(⟦ A⟧={w\in W: \mathcal M,w\models A}\). Let \(X=⟦ A⟧\), \(Y=⟦ B⟧\). Truth is defined by:

• \(w\models p \iff w\in V(p)\).
• \(w\models A\wedge B \iff w\models A\) and \(w\models B\) (so \(⟦ A\wedge B⟧=X\cap Y\)).
• Intuitionistic negation: \(w\models \sim A \iff \forall v\ge w,\ v\not\models A\) (so \(⟦\sim A⟧=\mathrm{iNeg}_\le(X)\)).
• Implication: \(w\models A\to B \iff f_w(X)\subseteq Y\).
• Consistency: \(w\models A\circ B \iff C_w(X,Y)\).

Abbreviations \(A\mid B\), \(=\), \(\ne\) are interpreted from these clauses.

---

2. Immediate meta-properties

Persistence. For every formula \(A\), if \(w\models A\) and \(w\le x\), then \(x\models A\).
Sketch. Atoms persist by valuation; \(\wedge\) and \(\sim\) are standard Kripke cases; for \(\to\) use Her; for \(\circ\) use C_her.

Symmetry of inconsistency. \(⟦ A\mid B⟧=⟦ B\mid A⟧\) by C-sym and the Kripke clause for \(\sim\).

Kripke double negation. \(⟦ A⟧\subseteq⟦\sim\sim A⟧\) always holds, hence \(A\to\sim\sim A\) is valid.

---

3. Soundness for the Hilbert presentation of NL

All schemes 1.1–1.7 and rules R1–R2 are valid on every NL-frame.

• 1.1 \(A\to A\): by Id, \(f_w(X)\subseteq X\).
• 1.2 \((A\mid B)\to(B\mid A)\): \(⟦ A\circ B⟧=⟦ B\circ A⟧\) by C-sym, hence \(⟦\sim(A\circ B)⟧\subseteq ⟦\sim(B\circ A)⟧\) by the Kripke clause for \(\sim\).
• 1.3 \(A\to\sim\sim A\): \(X\subseteq \mathrm{iNeg}_\le(\mathrm{iNeg}_\le(X))\) in any Kripke structure; combine with Id.
• 1.4 \((A\to B)\to(A\circ B)\): immediate from C-coh.
• 1.5 \( (A\ne B\ne C)\to(((A\to B)\wedge(B\to C))\to(A\to C))\): at a world \(w\), the antecedent \(A\ne B\ne C\) says \(X\not\equiv_w Y\), \(Y\not\equiv_w Z\), \(X\not\equiv_w Z\). If also \(f_w(X)\subseteq Y\) and \(f_w(Y)\subseteq Z\), Tr≠ yields \(f_w(X)\subseteq Z\).
• 1.6 \((A\wedge B)=(B\wedge A)\): \(⟦ A\wedge B⟧=⟦ B\wedge A⟧\) set-theoretically, so each direction of \(=\) is an instance of 1.1.
• 1.7 \(((A\wedge B)\to C)\to((A\wedge\sim C)\to\sim B)\): write \(X=⟦ A⟧\), \(Y=⟦ B⟧\), \(Z=⟦ C⟧\). From \(f_w(X\cap Y)\subseteq Z\), Contra gives \(f_w(X\cap \mathrm{iNeg}_\le(Z))\subseteq \mathrm{iNeg}_\le(Y)\), i.e. the consequent.
• R1 (modus ponens): if \(w\in X\) and \(f_w(X)\subseteq Y\), then by Succ \(w\in f_w(X)\subseteq Y\), so \(w\models B\).
• R2 (adjunction): by the clause for \(\wedge\).

Nonclassicality. Using a 2-world chain \(w<v\) with \(V(p)={v}\), any selection of the form \(f_w(X)\subseteq X\cap\uparrow w\) and any symmetric, coherent \(C\) validates the axioms and rules while refuting \(\sim\sim p\to p\) at \(w\). Thus the negation is genuinely intuitionistic.

---

4. Canonical semantics and completeness

The completeness proof in the Lean development proceeds via canonical worlds built from the Hilbert interface NL.ProofSystem.NLProofSystem (with rules mp, adj and axioms 1.1–1.7).

Canonical worlds and accessibility

A world is a set \(\Gamma\) of formulas that is:

• closed under theorems and under mp, adj (closure notion Closed), and
• (schematically) consistent (Consistent in Lindenbaum.lean).

Write \(\mathrm{World}(\Gamma)\) for this property. Canonical worlds are packaged as
\[
\mathbf{W}_{\mathrm{can}}=\{\Gamma : \mathrm{World}(\Gamma)\},
\]
with canonical preorder \(\Gamma\le_C\Delta\) iff \(\Gamma\subseteq\Delta\).

Canonical detachment family

For a world \(\Gamma\) and formula \(A\), set
\[
F_\Gamma(A)\ :=\ \{\Delta\ \big|\ \mathrm{World}(\Delta),\ \Gamma\subseteq\Delta,\ \text{and}\ \forall B,\ (A\to B)\in\Gamma\ \Rightarrow\ B\in\Delta\}.
\]
In Canonical.lean we use \(F_\Gamma(A)\) to define the selection:
\[
F^{\mathrm{can}}(\Gamma,A)\ :=\ \{\Delta\in\mathbf{W}_{\mathrm{can}} : \Delta\in F_\Gamma(A)\}.
\]

The Lindenbaum apparatus (Lindenbaum.lean) provides the standard intuitionistic extension lemmas needed for negation and implication:

• extend_to_world: extend a closed consistent base to a world.
• neg_density: if \(\neg A\notin\Gamma\), there exists \(\Delta\supseteq\Gamma\) with \(A\in\Delta\).
• neg_blocks: if \(\neg A\in\Gamma\subseteq\Delta\), then \(A\notin\Delta\).
• F_nonempty: \(F_\Gamma(A)\) is nonempty.
• detachment_witness: if \((A\to B)\notin\Gamma\), some \(\Delta\in F_\Gamma(A)\) omits \(B\).

Canonical truth and validity

Define canonical truth sets by recursion on \(A\):
\[
\begin{aligned}
⟦ p⟧_{\mathrm{can}} &:= {\Gamma: p\in\Gamma},\\
⟦ A\wedge B⟧_{\mathrm{can}} &:= {\Gamma:(A\wedge B)\in\Gamma},\\
⟦ \sim A⟧_{\mathrm{can}} &:= {\Gamma:\ \forall\Delta\ (\Gamma\subseteq\Delta\Rightarrow \Delta\notin ⟦ A⟧_{\mathrm{can}})},\\
⟦ A\to B⟧_{\mathrm{can}} &:= {\Gamma:\ F^{\mathrm{can}}(\Gamma,A)\subseteq ⟦ B⟧_{\mathrm{can}}},\\
⟦ A\circ B⟧_{\mathrm{can}} &:= {\Gamma:(A\circ B)\in\Gamma}.
\end{aligned}
\]
Write \(\Gamma\models_{\mathrm{can}} A\) for \(\Gamma\in⟦ A⟧_{\mathrm{can}}\), and say \(A\) is canonically valid if \(\Gamma\models_{\mathrm{can}} A\) for all canonical worlds \(\Gamma\).

Truth Lemma (canonical)

For every \(A\) and canonical world \(\Gamma\),
\[
\Gamma\models_{\mathrm{can}} A\quad\Longleftrightarrow\quad A\in\Gamma.
\]
Proof sketch. Induction on \(A\). Atoms, \(\wedge\), and \(\circ\) are by definition.
For \(A\to B\):

• If \((A\to B)\in\Gamma\), then by the definition of \(F_\Gamma(A)\), every \(\Delta\in F^{\mathrm{can}}(\Gamma,A)\) contains \(B\); by IH, \(\Delta\models_{\mathrm{can}} B\).
• Conversely, if \(F^{\mathrm{can}}(\Gamma,A)\subseteq ⟦ B⟧_{\mathrm{can}}\) but \((A\to B)\notin\Gamma\), detachment_witness yields \(\Delta\in F^{\mathrm{can}}(\Gamma,A)\) with \(B\notin\Delta\), contradicting the subset condition.
  For \(\sim A\):
• If \(\Gamma\models_{\mathrm{can}}\sim A\) and \(\sim A\notin\Gamma\), neg_density gives \(\Delta\supseteq\Gamma\) with \(A\in\Delta\); by IH, \(\Delta\models_{\mathrm{can}}A\), contradicting the negation clause.
• If \(\sim A\in\Gamma\) and \(\Gamma\subseteq\Delta\), then neg_blocks ensures \(A\notin\Delta\); by IH, \(\Delta\not\models_{\mathrm{can}}A\).

Completeness

Let Provable be the Hilbert notion from ProofSystem.lean. If \(A\) is canonically valid, then \(A\) is provable:
\[
\forall\Gamma,\ \Gamma\models_{\mathrm{can}}A\quad\Longrightarrow\quad \mathrm{Provable}(A).
\]
Proof. Suppose \(A\) is not provable. Extend the set of all theorems with \(\neg A\) to a world \(\Delta\) using extend_with_neg. By the Truth Lemma, \(\Delta\models_{\mathrm{can}}\neg A\), hence \(\Delta\not\models_{\mathrm{can}}A\), contradicting canonical validity.

From canonical to frame completeness. The canonical structure above is built to validate all NL axioms and rules and to satisfy the Truth Lemma; it serves as the usual Lindenbaum–Kripke model. Since the frame conditions used in §1 are precisely the ones enforced in the canonical construction (via the closure/extension lemmas and the way \(F_\Gamma(A)\) is used), validity over all NL-frames entails canonical validity, hence provability. Thus NL is strongly complete for the class of NL-frames of §1.

---

5. One concrete instance

As a concrete (and very simple) instance, put \(f_w(X)=X\cap\uparrow w\) (which satisfies Id, Her, Succ, f-up, and Contra) and let \(C_w\) be any symmetric, upward-persistent predicate with C-coh (e.g. the always-true relation). This validates 1.1–1.7 and R1–R2, but \(\sim\sim p\to p\) fails in general (take a 2-node chain \(w<v\) with \(V(p)={v}\)).

---

6. What differs from the earlier (informal) sketch

• Selections are anchored: f_up ensures \(f_w(X)\subseteq \uparrow w\).
• \(\circ\) is persistent: C_her builds upward monotonicity into the semantics of consistency.
• Axiom 1.5 is matched exactly: we enforce the guarded syllogism Tr≠ (not the unconditional one).
• The canonical route to completeness uses the Kripke negation lemmas (neg_density, neg_blocks) and the detachment family \(F_\Gamma(A)\) to handle \(\to\) exactly as encoded in the Lean files.

This presentation is the human-readable counterpart of the Lean development and can be read independently of the code, while lining up one-for-one with the definitions and lemmas actually used.

No deduction, no arrow

Explain this idea: "If you've got no deduction theorem, then you might as well be implication-free."

Here’s the gist in plain terms:

• The deduction theorem is the bridge between reasoning with assumptions and using → inside formulas. It says: if from Γ together with A you can prove B (Γ, A ⊢ B), then you can prove the implication inside the system (Γ ⊢ A → B). In other words, “assuming A, B follows” can be internalized as the single formula A → B.

• So, in logics where a good deduction theorem holds, the connective → earns its keep: it represents the underlying consequence relation ⊢. Proof steps that temporarily assume A can be packaged up as the statement A → B.

• If your system doesn’t have a (usable) deduction theorem, → no longer tracks provability from assumptions. You might still have a symbol called “→”, but it doesn’t internalize your consequence relation. Then implication loses its chief proof-theoretic role; it’s just another connective with some axioms, not the stand-in for “from A, infer B”.

That’s what the quip means by: “no deduction theorem ⇒ might as well be implication-free.” If → can’t encode entailment, you could drop it and work directly with the turnstile (sequents, Γ ⊢ B), or redesign your system so that whatever conditional you keep really does satisfy a deduction-style rule (e.g., by giving → an introduction/elimination rule or ensuring it’s the right adjoint to ∧ in the algebraic/structural sense).

A slightly more technical snapshot

• With DT: A → B is the internalization of entailment: A ⊢ B ⇔ ⊢ A → B (relative to Γ if present).
• Without DT: there’s no such equivalence, so → doesn’t mirror ⊢. Proof theory then usually takes ⊢ (or sequents) as primitive, or replaces → with a conditional that restores the adjunction: Γ, A ⊢ B iff Γ ⊢ A → B.

So the slogan is a design principle: if your implication can’t internalize consequence (no deduction theorem), using it is mostly decorative; organize the system around ⊢ instead, or fix → so it earns its place.

Intuitionistic Trump executive order

Featured in this post.

Write a satirical news item where President Donald Trump passes an executive order requiring the use of intuitionistic logic for all government purposes

White House Orders Government To Prove Things Actually Exist Before Using Them

WASHINGTON, D.C. — In a surprise early-morning signing ceremony attended by stunned logicians and mildly amused bureaucrats, President Donald Trump issued an executive order Tuesday mandating that all federal agencies adopt intuitionistic logic “for official government purposes, press releases, and any polling that doesn’t look good.”

The order, titled “Constructively Making America Great Again,” requires agencies to stop relying on the Law of the Excluded Middle—traditionally used to decide whether a statement is true or false—and instead provide constructive proofs that something exists before citing it.

“From now on, if the Department of Energy says there exists a plan, they’re going to show the plan,” the President said, holding up a blank binder labeled Witness. “No more saying ‘either we have a plan or we don’t.’ That’s weak, it’s very weak, and frankly people are tired of classical logic. Sad!”

Agencies scramble to downgrade certainty

The Office of Management and Budget circulated guidance urging staff to replace binary conclusions with carefully hedged commitments. A sample memo reads: “We cannot assert ‘the bridge is safe or unsafe’ without a constructive proof. Please submit an explicit method for crossing.” The Department of Transportation responded by issuing orange cones labeled “Provisional Existence.”

At the Pentagon, officials confirmed that Schrödinger’s cat has been honorably discharged pending constructive evidence of life or death “with a reproducible witness.” Navy commanders, uncertain whether an incoming radar blip “either is or is not” a threat, requested funds for a “witness-producing missile.”

Courts brace for proof obligations

Federal judges reported sudden spikes in filings titled “We Can Build It, Your Honor.” One appellate panel vacated a conviction after the prosecution failed to produce a constructive algorithm for guilt. “A mere contradiction won’t do,” the opinion stated. “Bring us the recipe for wrongdoing.”

Economists discover budget only locally decidable

The Council of Economic Advisers updated its forecast to read: “Growth exists if and only if we can exhibit it. Please check back after Q4 when we attempt to compute ε > 0.” Markets reacted ambiguously, which analysts described as “formally appropriate.”

White House clarifies: polls must now produce witnesses

When asked whether the order applied to election polling, the Press Secretary said, “Yes. If a poll claims the President is losing suburban voters, the poll must deliver those voters to the briefing room, with IDs, biographies, and a step-by-step construction showing how they came to be.”

Mathematicians: mixed feelings, mostly constructive

Logicians applauded the newfound interest but warned of practical challenges. “Intuitionistic logic isn’t about vibes,” said one professor, moments before being escorted out for saying the word “tertium.” “It requires explicit methods—”

“Exactly,” said a senior advisor. “We’re very pro-method. We’ll be making methods all week.”

Implementation timeline uncertain, but not excluded

Agencies have 30 days to submit constructive implementation plans demonstrating that compliance is realizable, not merely not impossible. A final provision bans the phrase “with all due respect,” citing its reliance on double negation.

Asked whether the policy could be reversed by a future administration, the President concluded, “Either it will be reversed or it won’t—but under the new rules, they’ll have to show how. Good luck.”

Wittgensteinian truthmaker mereology

The passage in the blockquote is from Tractatus Logico-Philosophicus, 5.11–5.122, and it is in this sense (if any) that this post is “Wittgensteinian”.

I made this post to parallel the Wittgenstein quote for fun, but if you are interested in real developments of truthmaker mereology for propositions, see Kit Fine’s A Theory of Partial Truth.

Based on the ideas below, make up a formal theory of “truthmaker mereology” for propositions.

I will give the name truth-grounds of a proposition to those truth-possibilities of its truth-arguments that make it true.

If all the truth-grounds that are common to a number of propositions are at the same time truth-grounds of a certain proposition, then we say that the truth of that proposition follows from the truth of the others.

In particular, the truth of a proposition ‘p’ follows from the truth of another proposition ‘q’ if all the truth-grounds of the latter are truth-grounds of the former.

The truth-grounds of the one are contained in those of the other: p follows from q.

If p follows from q, the sense of ‘p’ is contained in the sense of ‘q’.

Here’s a compact, fully specified theory that matches your ideas and turns them into a clean piece of logic. I’ll call it Truthmaker Mereology for Propositions (TMM).

1. Ontology and primitives

• Situations (a.k.a. truth-possibilities): a nonempty set \( \Sigma \). Intuitively, these are partial states of affairs (they can be as fine-grained as you like).
• Mereology on situations: a binary relation \( \preceq \subseteq \Sigma\times\Sigma \) read “is part of”, with:

1. (Reflexive) \(s\preceq s\).
2. (Antisymmetric) \(s\preceq t\) and \(t\preceq s \Rightarrow s=t\).
3. (Transitive) \(s\preceq t\preceq u \Rightarrow s\preceq u\).

• Fusions (mereological sums): a partial binary operation \( s \sqcup t \in \Sigma \) whenever a least upper bound of \({s,t}\) exists; we assume:

4. (Existence of binary fusions) for all (s,t\in\Sigma), (s\sqcup t) exists and is an upper bound, and any common upper bound of \(s,t\) is above \(s\sqcup t\).
5. (Arbitrary fusions) for any nonempty \(X\subseteq\Sigma\), \(\bigsqcup X\) exists. (Together 1–5 make \((\Sigma,\preceq)\) a complete join-semilattice.)

• Propositions: a set \( \mathsf{Prop} \) with standard connectives \(\land,\lor,\to,\neg,\top,\bot\).
• Verification (truthmaking): a relation \( \Vdash \subseteq \Sigma\times \mathsf{Prop} \), read “\(s\) makes \(p\) true”.

2. Truth-grounds and up-closure

For any proposition \(p\), its truth-grounds (your “truth-grounds of a proposition”) are \[ G(p) \ := \ {, s\in\Sigma \mid s \Vdash p ,}. \] Axioms for \( \Vdash \) (the truthmaker postulates):

TM-U (Up-closure). If \(s\Vdash p\) and \(s\preceq t\), then \(t\Vdash p\). (Any extension of a maker is still a maker.)

TM-\(\top / \bot\). For all \(s\), \(s\Vdash\top\) and not \(s\Vdash\bot\).

TM-\(\land\). \(s\Vdash p\land q \iff \exists,u,v\preceq s\) with \(u\Vdash p\), \(v\Vdash q\), and \(s \succeq u\sqcup v\). (“Having both” is having a fusion of a maker for each.)

TM-\(\lor\). \(s\Vdash p\lor q \iff (\exists,t\preceq s,., t\Vdash p) \ \text{or}\ (\exists,t\preceq s,., t\Vdash q)\).

TM-\(\to\). \(s\Vdash p\to q \iff\) for all \(t\preceq s\), if \(t\Vdash p\) then \(t\Vdash q\).

TM-\(\neg\). \(s\Vdash \neg p \iff\) for all \(t\preceq s\), not \(t\Vdash p\). (So negative truths are supported by situations that preclude any part that makes \(p\).)

Extensionality. Identify propositions up to their grounds: \(p\equiv q \iff G(p)=G(q)\). (All semantic clauses below respect \(\equiv\).)

3. “Follows from” as containment of common grounds

For a finite (or arbitrary) set \(\Gamma\subseteq\mathsf{Prop}\), write \[ G(\Gamma)\ :=\ \bigcap_{p\in\Gamma} G(p) \] —the grounds common to all propositions in \(\Gamma\).

Definition (Consequence). \[ \Gamma \ \vdash_{\mathrm{TMM}} \ \varphi \quad\text{iff}\quad G(\Gamma)\ \subseteq\ G(\varphi). \] Particular case. \(q \vdash_{\mathrm{TMM}} p\) iff \(G(q)\subseteq G(p)\). This matches your: “If all the truth-grounds of \(q\) are truth-grounds of \(p\), the truth of \(p\) follows from the truth of \(q\).”

Basic meta-properties. From set-theoretic facts:

• Reflexivity: \(p\vdash p\).
• Monotony: If \(\Gamma\subseteq\Delta\) and \(\Gamma\vdash\varphi\), then \(\Delta\vdash\varphi\).
• Cut/Transitivity: If \(\Gamma\vdash\psi\) and \(\Gamma\cup{\psi}\vdash\varphi\), then \(\Gamma\vdash\varphi\).

4. Mereology of propositions (ground-mereology)

Define a parthood order on propositions by \[ p \ \sqsubseteq \ q \quad :\iff\quad G(q)\ \subseteq\ G(p). \] Read “\(p\) is at most as informative as \(q\)”—the stronger a proposition, the smaller its ground set; so the order reverses set inclusion (as your notes suggest).

With this order:

• Meet is disjunction: \(p\ \wedge_{\sqsubseteq}\ q = p\lor q\) since \(G(p\lor q)=G(p)\cup G(q)\).
• Join is conjunction: \(p\ \vee_{\sqsubseteq}\ q = p\land q\) since \(G(p\land q)=\mathrm{Up}\{u\sqcup v : u\in G(p),,v\in G(q)\}\subseteq G(p)\cap G(q)\), and TM-U yields equality at the level of common grounds. Hence \((\mathsf{Prop}/{\equiv},\sqsubseteq)\) is a complete lattice anti-isomorphic to the lattice of ground-sets \( \langle \{G(p)\},\subseteq\rangle \).

Entailment = parthood. \(q \vdash_{\mathrm{TMM}} p \iff p \sqsubseteq q\).

5. “Sense containment”

Define the sense (core content) of \(p\) as the mereological greatest lower bound of its grounds: \[ \mathsf{Sense}(p)\ :=\ \bigwedge G(p)\ =\ \bigcap\nolimits_{\preceq} \{ s\in\Sigma : s\Vdash p \}, \] i.e., the largest situation \(c\) such that \(c\preceq s\) for every \(s\in G(p)\). (This exists because \((\Sigma,\preceq)\) has arbitrary fusions, hence dually arbitrary meets of up-sets.)

Then: \[ q \vdash_{\mathrm{TMM}} p \quad\Rightarrow\quad \mathsf{Sense}(p) \ \preceq\ \mathsf{Sense}(q). \] Reason: \(G(q)\subseteq G(p)\) implies \(\bigcap_{\preceq}G(p) \preceq \bigcap_{\preceq}G(q)\). This is your final clause: “If \(p\) follows from \(q\), the sense of \(p\) is contained in the sense of \(q\).”

6. Worked laws (all provable from the clauses above)

• Conjunction: \(G(p\land q)= \uparrow\{u\sqcup v : u\in G(p), v\in G(q)\}\); in particular \(p\land q \sqsubseteq p\) and \(p\land q \sqsubseteq q\).
• Disjunction: \(p \sqsubseteq p\lor q\) and \(q \sqsubseteq p\lor q\).
• Modus ponens as ground-containment: If \(G(q)\subseteq G(p)\), then \(q\vdash p\). If \(G(p)\subseteq G(r)\) and \(G(p\to q)=\Sigma\) (i.e., \(p\to q\) is valid), then \(G(r)\subseteq G(q)\), so \(r\vdash q\).
• Negation: \(G(\neg p)={s : \text{no } t\preceq s \text{ is in } G(p)}\) (up-closed), giving \(\neg\neg p \sqsubseteq p\) (and equality if \(\Sigma\) is Boolean in the obvious way).

7. Optional representation (to ground the picture)

A concrete model is:

• Let \(A\) be a set of atomic facts.
• Let \(\Sigma\) be the set of consistent, deductively closed sets of literals over \(A\) (finite or infinite), ordered by \(\subseteq\).
• Fusion is set-theoretic union (when consistent; if you want totality, take the closure of the union).
• A valuation \(s\) verifies an atom \(a\) iff \(a\in s\); extend to all formulas by TM-clauses above.
  This satisfies TM-U, the connectives, and the mereology (intersections and unions are the meets/joins).

---

What you get

• A truthmaker-first semantics: propositions are determined by their up-closed sets of verifying situations.
• A mereology of truth: consequence is literally containment of common grounds, and the core sense of a proposition is the meet of its grounds—hence “if \(p\) follows from \(q\) then the sense of \(p\) is contained in the sense of \(q\)”.
• A tidy algebra: the lattice \((\mathsf{Prop}/{\equiv},\sqsubseteq)\) is anti-isomorphic to the lattice of ground-sets under \(\subseteq\).

If you’d like, I can also add a sequent calculus that’s sound/complete for \( \vdash_{\mathrm{TMM}} \) or work through a couple of concrete examples with specific atoms to illustrate the order and the “sense” operator.

Arrhenius on welfarist axiologies

What do we know about Arrhenius's impossibility theorems about welfarist axiologies?

Here’s the short version of what Arrhenius shows about welfarist axiologies (theories that rank populations only by the welfare of the people who’d live in them):

• Core 2000 theorem. Any welfarist axiology that satisfies three very plausible conditions — Dominance (if A and B have the same number of people and everyone in A is better off than everyone in B, then A is better), Addition (if adding some worse-off people is bad, adding more and even worse-off people is at least as bad), and a mild Minimal Non-Extreme Priority (very large gains for many can outweigh a slight harm to one) — must accept at least one of three counter-intuitive results: the Repugnant Conclusion, the Sadistic Conclusion, or an Anti-Egalitarian Conclusion (preferring an unequal population with lower average welfare to an equal one). (Institutet för framtidsstudier)

• What “welfarist axiology” means in the paper. It’s an “at least as good as” ordering over all possible populations, based solely on welfare, assumed reflexive, transitive, and complete; Arrhenius notes Dominance is stronger than simple Pareto. (Institutet för framtidsstudier)

• The three “bad” conclusions defined. Arrhenius explicitly formulates Repugnant, Sadistic, and Anti-Egalitarian conclusions and proves the incompatibility result above. (Institutet för framtidsstudier)

• Escape routes he considers (and worries about). You could drop completeness (allow incommensurability), or go non-welfarist/pluralist; but Arrhenius argues these moves are costly or unmotivated within a welfarist frame. (Institutet för framtidsstudier)

• Later impossibility results. Arrhenius also proved “one more” theorem using slightly different, often weaker, conditions (e.g., Egalitarian Dominance, General Non-Extreme Priority, Non-Elitism, Weak Non-Sadism, Weak Quality Addition) to show no axiology can meet them all; this strengthens the case even if one rejects some premises from 2000. (Institutet för framtidsstudier)

• Ongoing debate. Recent work argues some proofs rely (implicitly) on a Finite Fine-Grainedness assumption about the welfare scale; critics propose “lexical” views to evade certain theorems, while others “riskify” the conditions (population prospects under uncertainty) to restore impossibility without that assumption.

If you want, I can sketch the three adequacy conditions and three conclusions in plain English with a tiny diagram of how the proof structure forces the clash.

AGM and black swans

Suppose my knowledge base is:

1. All swans from Europe are white.
2. Sweden is part of Europe.
3. The bird caught in the trap is a swan.
4. The bird caught in the trap is from Sweden.

But then despite what it may seem, I look at the trap and learn: 5. The bird caught in the trap is black.

Explain AGM belief revision.

Here’s the AGM (Alchourrón–Gärdenfors–Makinson) picture, using your swan story.

The idea

A belief set \(K\) is the (logically closed) collection of sentences you currently accept. AGM studies three ways to change \(K\):

• Expansion \(K + \varphi\): just add \(\varphi\) and close under logic (no regard for consistency).
• Contraction \(K - \varphi\): give up enough of \(K\) so that \(\varphi\) is no longer entailed.
• Revision \(K * \varphi\): incorporate \(\varphi\) while keeping \(K\) as consistent and unchanged as possible.

Two identities connect them:

• Levi identity: \(K * \varphi = (K - \neg \varphi) + \varphi\) (to accept \(\varphi\), first remove commitment to its negation, then add \(\varphi\)).
• Harper identity: \(K - \varphi = K \cap (K * \neg \varphi)\).

AGM gives rationality postulates for revision (closure, success \(\varphi \in K * \varphi\), minimal change via inclusion/vacuity, consistency when \(\varphi\) is consistent, and extensionality).

Your case, step by step

Let (b) be “the trapped bird.” Your initial (K) contains:

1. \(\forall x,[(\text{Swan}(x) \wedge \text{FromEurope}(x)) \rightarrow \text{White}(x)]\)
2. \(\text{FromEurope}(\text{Sweden})\)
3. \(\text{Swan}(b)\)
4. \(\text{From}(b,\text{Sweden})\) (hence \(\text{FromEurope}(b)\))

From 1–4 you deduce \(\text{White}(b)\).

Then you observe:

5. \(\text{Black}(b)\).

Assume “black” and “white” are mutually exclusive. So \(K \cup {5}\) is inconsistent, and you must revise by \(\varphi=\text{Black}(b)\).

By the Levi identity: \[ K * \text{Black}(b) = (K - \neg \text{Black}(b)) + \text{Black}(b). \] Contracting by \(\neg\text{Black}(b)\) means: remove just enough from \(K\) so that you no longer (even indirectly) commit to “\(b\) isn’t black.” Right now \(K\) entails \(\neg\text{Black}(b)\) via \(\text{White}(b)\). To block that entailment you could drop any one of the premises that make \(b\) white:

• drop (1) the universal rule,
• or drop (2) Sweden⊆Europe,
• or drop (3) that (b) is a swan,
• or drop (4) that (b) is from Sweden.

Each of these yields a remainder set (a maximal subset of (K) that no longer implies \(\neg\text{Black}(b))\). AGM lets a selection function choose among such remainders according to your epistemic entrenchment (how hard a belief is to give up). Then you expand by adding \(\text{Black}(b)\).

A natural entrenchment here is:

• very hard to give up: geographical fact (2) and the direct particulars (3) & (4),
• easier to give up: the overbold universal (1).

With that entrenchment, the chosen remainder drops (1). So:

• Contraction: \(K - \neg\text{Black}(b) = K \setminus \{(1)\}\).
• Revision (final): \(K * \text{Black}(b) = \text{Cn}\big(\{(2),(3),(4),\text{Black}(b)\}\big)\).

Consequences now include \(\neg(1)\) (i.e., not all European swans are white), since from (2–4) and \(\text{Black}(b)\) you get a counterexample to (1). You’ve satisfied success (you believe the bird is black) and changed your beliefs minimally (you gave up just the generalization that the new observation falsified).

What AGM adds conceptually

• Minimal change via selection: Among all ways to restore consistency, pick those that sacrifice the least entrenched beliefs.
• Representation theorems: AGM shows revision is equivalent to choosing models minimal in a faithful total preorder (or, dually, to using an epistemic entrenchment relation). This formalizes “keep as much as you reasonably can.”
• Underdetermination: Different entrenchments → different (but still rational) revisions. If, for some reason, you trusted the universal law more than the reports about \(b\), AGM would instead suggest dropping (3) or (4) and then adding \(\text{Black}(b)\).

Quick glossary

• Belief set \(K\): logically closed set of sentences.
• Expansion \(+\): add only.
• Contraction \(-\): give up just enough to avoid \(\varphi\).
• Revision \(*\): adopt \(\varphi\) with minimal disturbance; \(K * \varphi = (K - \neg\varphi) + \varphi\).
• Remainder sets: maximal subsets of \(K\) that don’t entail \(\varphi\).
• Selection function / entrenchment: tells which remainders to keep; captures what you find most trustworthy.

In short: AGM tells you how to rationally absorb “the bird is black” by first retracting whatever commits you to “it isn’t black,” guided by which beliefs you treat as most defensible—here, naturally, the sweeping Rule (1) gives way to the observed counterexample.

But how to revise the universal?

Great question. AGM tells you what to drop to accept the new fact, but it doesn’t itself say how to re-formulate a universal generalization once it’s been falsified. Here are the standard, rational ways to “revise the universal,” from most conservative to more conceptual changes:

1) Name the exception (syntactic weakening in the same language)

If your language can name the bird (b), replace \[ \forall x,[(\text{Swan}(x)\wedge \text{Europe}(x))\to \text{White}(x)] \] with \[ \forall x,[(\text{Swan}(x)\wedge \text{Europe}(x)\wedge x\neq b)\to \text{White}(x)]. \] This is the smallest weakening that preserves the rule for every other case. In AGM terms: after revising by \(\text{Black}(b)\), you’ve dropped the old universal; adding the “all-but-\(b\)” version is an admissible, minimal repair.

If you can’t name \(b\), you can’t write “\(x\neq b\)”. Then the safest move is simply to not keep a universal at all (see #2).

2) Retreat from “all” to “not all”

Keep only what your new beliefs logically support: \[ \exists x,(\text{Swan}(x)\wedge \text{Europe}(x)\wedge \neg \text{White}(x)). \] That is, don’t replace the universal; just accept that it was too strong. This is the default AGM outcome if you don’t add any new generalization.

3) Guard the rule with an “abnormality” (defeasible/default move)

Introduce a guard: \[ \forall x,[(\text{Swan}(x)\wedge \text{Europe}(x)\wedge \neg \text{Ab}(x))\to \text{White}(x)],\qquad \text{Ab}(b). \] Now the rule reads “normally, European swans are white,” and \(b\) is marked as an exception. This is the classic fix in nonmonotonic/default logics (e.g., rational closure/System Z) and aligns well with the intuition that universal laws in the wild are default rules.

4) Strengthen the antecedent (narrow the scope)

Replace “from Europe” with a narrower condition supported by evidence, e.g., \[ \forall x,[(\text{Swan}(x)\wedge \text{Europe}(x)\wedge \neg \text{Sweden}(x))\to \text{White}(x)]. \] This is justified only if you have reasons to localize the exception (more than a single counterexample).

5) Switch to a statistical/inductive universal

Replace \(\forall\) with a quantifier of proportion or a probability claim, e.g., \[ \Pr(\text{White}\mid \text{Swan}\wedge \text{Europe}) \ge 1-\varepsilon, \] and update that probability when you see a black swan. This preserves the spirit of the generalization while acknowledging uncertainty.

---

Where AGM fits technically

• Revision step: \(K * \text{Black}(b) = (K - \neg\text{Black}(b)) + \text{Black}(b)\). Dropping the old universal (1) is the natural contraction.

• What to put back: AGM is agnostic; your entrenchment/selection policy decides.

  • If you favor exception-by-name → option #1.
  • If you avoid new symbols or dislike ad-hoc exceptions → option #2.
  • If you treat “laws” as defaults → option #3.
  • If you’re doing induction/statistics → option #5.

A crisp way to remember it:

• Logical repair: “all” → “all-but-(b)” (if you can name (b)), else drop “all”.
• Knowledge-engineering repair: add an abnormality guard.
• Scientific/inductive repair: replace universals with high-confidence generalizations and keep updating.

Quaker thees and thous

Voltaire's letters on England describe the Quakers as always using thee and thou with everyone, which got them into trouble with nobility who found this disrespectful. Moby-Dick is a book that has Quaker characters in the 19th century and notably portrays them still using thee and thou at that time, when English speakers had drifted to using you for everyone. Did they really hold onto the thees and thous for that long? I assume Friends don't do this nowadays?

Short answer: yes—many Friends really did keep “plain speech” (thee/thy/thou) going well into the 1800s, and a few pockets kept some of it into the 1900s. Today it’s rare, though you may still hear it among a small minority of Conservative Friends.

A bit more detail:

• Early Quakers (1600s) adopted plain speech—addressing everyone with the singular pronouns and avoiding honorifics—as an equality witness. Voltaire even noted they were punished for “theeing and thouing the magistrates.” (Project Gutenberg)
• By the 18th–19th centuries, Friends’ usage had shifted from classical “thou goest” to a distinctive Quaker pattern like “thee is/has” (using thee for both subject and object). That feature is well attested in Quaker sources. (Quaker Historical Lexicon)
• As for timing, evidence from ministers’ journals suggests consistent use through the 1800s, with broader abandonment only around the turn of the 20th century. A general history of Philadelphia-area Quakers likewise says that by the early 1900s most Friends had given up the old peculiarities of dress and speech. That makes Moby-Dick’s 1840s Quakers using “thee” perfectly plausible. (Language Log)

What about now?
In mainstream Quaker circles, no—Friends don’t normally talk this way today. Official British materials even describe “using ‘thee’ or ‘thou’” as belonging to the past, with the modern emphasis instead on avoiding titles. Still, a small minority (notably some Conservative Friends, e.g., in Ohio Yearly Meeting or plain-dressing groups in England) keep the practice occasionally—often thee without the old verb endings. (Quakers)

If thee is curious about the grammar rabbit hole: the hallmark Quaker form you’ll see in older letters is things like “Thee is right.” That’s not a mistake; it’s a stable Quaker usage from the period when many Friends still maintained plain speech. (Quaker Historical Lexicon)

So: Voltaire’s portrait (1700s) and Moby-Dick (set in the 1840s) both line up with real usage; the practice largely faded in the early 1900s, and today it survives only here and there. (Project Gutenberg)

Write a “Lockean catechism”, with questions such as, “What is the natural liberty of man?”

A Lockean Catechism

Q. What is the state of nature?
A. A condition where people live without a common superior on earth, equal and independent, governed by the law of nature.

Q. What is the law of nature?
A. Reason, teaching that no one ought to harm another in life, health, liberty, or possessions.

Q. What is the natural liberty of man?
A. To be free from any earthly superior’s will, subject only to the law of nature—not a license to injure others.

Q. Are all people by nature equal?
A. Yes. No one has a natural right to rule another; legitimate authority must arise from consent.

Q. What different kinds of power exist?
A. Paternal (over children until they reach reason), political (over free equals for the public good), and despotic (over those who have forfeited their rights by unjust aggression).

Q. What is property?
A. One’s life and liberty, and also one’s external goods—“estate.”

Q. How does property in goods begin?
A. By mixing one’s labor with what is unowned—for example, cultivating land or gathering fruit.

Q. Are there limits on initial appropriation?
A. Yes: one must leave “enough and as good” for others and not let what one takes spoil.

Q. How can great inequalities arise without violating those limits?
A. By consent to the use of durable money, which lets people exchange and accumulate beyond immediate need.

Q. What inconveniences attend the state of nature?
A. Partiality and uncertainty—each person is judge in his own case, which breeds conflict.

Q. Why do people form political society?
A. To better secure their property—life, liberty, and estate—through settled, known law and impartial enforcement.

Q. What creates a commonwealth?
A. Each person consents to unite into one body politic and to be governed by the will of the majority.

Q. What is the trust given to government?
A. To use its powers solely for the public good—the preservation of the people and their property.

Q. Which power is supreme in a commonwealth?
A. The legislative power, for it makes the standing rules; yet it remains a fiduciary power, limited by the trust.

Q. What limits bind the legislature?
A. It must govern by promulgated, standing laws; aim at the public good; not take property without consent; and not transfer its law-making power to others.

Q. What of taxation?
A. Taxes require the people’s consent, given personally or by chosen representatives.

Q. What is the executive power?
A. The power to apply the law and secure its execution; it may also include a federative power to manage foreign affairs.

Q. What is prerogative?
A. A lawful latitude in the executive to act for the public good without, or even against, the letter of the law—so long as it truly serves that good.

Q. What is tyranny?
A. The exercise of power beyond right, for private advantage, not for the public good.

Q. When is resistance justified?
A. When rulers break the trust—subvert the laws, invade property, or set up arbitrary power—thereby dissolving the government.

Q. Who judges whether the trust is broken?
A. In the last appeal, the people judge; they may resume their original liberty and institute a new government.

Q. What of conquest and slavery?
A. Just war may give a right over an unjust aggressor’s life; sparing that life can yield a form of despotical power, but no right is acquired over the innocent or their estates.

Q. What of parental power?
A. Parents have a temporary authority to guide children to the use of reason; this is not political dominion.

Q. What is religious toleration?
A. The church is a voluntary society; magistrates cannot command belief, and coercion cannot save souls. Civil peace is the aim of the state, worship the aim of the church.

Q. Are there limits to toleration?
A. Locke held that opinions threatening civil order or allegiance may be restrained; yet the general rule is broad toleration for peaceable worship.

Q. What is liberty under government?
A. To live under known, equal laws made by consent, with one standing rule for all—not to be subject to another’s arbitrary will.

Q. What, finally, is the end of political society?
A. The secure and peaceful enjoyment of one’s property—life, liberty, and estate—by means of just laws and accountable powers.

Semantics for E. Nelson’s connexive logic NL

If this post is correct, then ChatGPT just solved an open problem. I lack the skill to check whether it is correct. Due to MathJax fucking up, I have replaced ChatGPT’s uses of \llbracket and \rrbracket with the Unicode ⟦ and ⟧.

I used the “ChatGPT Classic” agent with the GPT-5-Thinking model to avoid it trying to use the Internet for this.

Axioms and inference rules for E. Nelson’s connexive logic NL are presented as follows (we here use schematic letters for arbitrary formulas instead of propositional variables and a different symbol for negation):

1.1 A → A
1.2 (A|B) → (B|A)
1.3 A → ~~A
1.4 (A → B) → (A ◦ B)
1.5 (A ≠ B ≠ C) → (((A → B) ∧ (B → C)) → (A → C ))
1.6 (A ∧ B) = (B ∧ A)
1.7 ((A ∧ B ) → C ) → ((A ∧ ~C) → ~B )

R1 if ⊢ A and ⊢ (A → B), then ⊢ B (modus ponens)
R2 if ⊢ A and ⊢ B, then ⊢ (A ∧ B) (adjunction)

where ◦ is a primitive binary consistency operator, (A|B) (inconsistency) is defined as ~(A ◦ B), A = B is defined as (A → B) ∧ (B → A), A ≠ B as ~ (A = B), and A ≠ B ≠ C is an abbreviation of (A ≠ B) ∧ (B ≠ C) ∧ (A ≠ C).

Try to come up with a sound and complete semantics for NL.

Below is a compact, fully-worked semantics that validates exactly the NL axioms/rules you’ve listed and is strong enough to be complete. It’s a “conditional-selection” semantics (in the spirit of Stalnaker/Lewis and the usual semantics for conditional logics), augmented with a primitive, symmetric compatibility/consistency predicate for ◦ and two frame conditions that capture the connexive features (Boethius and the contraposition-like 1.7).

I’ll first define the models, then give the truth-clauses, then list the frame conditions we need (they are very natural), and finally sketch soundness and completeness.

---

NL frames and models

An NL-frame is a triple \[ \mathcal F=\langle W,\; f,\; C\rangle \] where

• \(W\) is a nonempty set of worlds.
• For each \(w\in W\), \(f_w:\mathcal P(W)\to \mathcal P(W)\) is a selection function (think: the set \(f_w(X)\) are the “relevant \(X\)–cases” at \(w\)).
• For each \(w\in W\), \(C_w\subseteq \mathcal P(W)\times \mathcal P(W)\) is a compatibility (consistency) relation on sets of worlds; we use it to interpret \(A\circ B\).

An NL-model is a frame \(\mathcal F\) together with a valuation \(V:\text{Atoms}\to\mathcal P(W)\). For any formula \(A\), let \(⟦ A⟧^\mathcal M={w\in W: \mathcal M,w\models A}\) be its truth set.

---

Truth clauses

Extend \(V\) to all formulas as follows (classical pointwise \(\sim\) and \(\wedge\); non-truth-functional \(\to\) via selection; primitive \(\circ\) via \(C\)):

• \(\mathcal M,w\models p\) iff \(w\in V(p)\) (for atoms \(p\)).
• \(\mathcal M,w\models A\wedge B\) iff \(\mathcal M,w\models A\) and \(\mathcal M,w\models B\).
• \(\mathcal M,w\models \sim A\) iff \(\mathcal M,w\not\models A\). (So \(\sim\) is classical negation.)
• \(\mathcal M,w\models A\to B\) iff \(f_w(⟦ A⟧^\mathcal M)\subseteq ⟦ B⟧^\mathcal M\).
• \(\mathcal M,w\models A\circ B\) iff \(C_w\big(⟦ A⟧^\mathcal M,⟦ B⟧^\mathcal M\big)\).

Write \(A=B\) as usual for mutual implication, and \(A\neq B\) as its negation; those are just abbreviations in the object language.

---

Frame conditions (the “NL-frame” axioms)

We assume every NL-frame satisfies the following conditions, for all \(w\in W\) and all \(X,Y,Z\subseteq W\):

On the conditional \(f_w\):

1. Identity (Id): \(f_w(X)\subseteq X\).
   (This forces \(A\to A\), axiom 1.1.)

2. Monotonicity (Mon): If \(X\subseteq Y\) then \(f_w(X)\subseteq f_w(Y)\).
   (Gives the transitivity pattern used in 1.5.)

3. Success (Detachment) (Succ): If \(w\in X\) then \(w\in f_w(X)\).
   (Delivers local modus ponens and validates rule R1.)

4. Nonemptiness on nonempty input (NE): If \(X\neq\varnothing\) then \(f_w(X)\neq\varnothing\).
   (Blocks vacuous truths from producing connexive failures.)

5. Boethius/Connexive condition (Bo): If \(f_w(X)\subseteq Y\) then \(f_w(Y)\nsubseteq W\setminus X\).
   (Captures \((A\to B)\Rightarrow \neg(B\to \sim A)\).)

6. Contraposition-like condition (Contra): If \(f_w(X\cap Y)\subseteq Z\) then \(f_w\big(X\cap (W\setminus Z)\big)\subseteq W\setminus Y\).
   (This is exactly axiom-schema 1.7 in set form.)

On compatibility \(C_w\):

7. Symmetry (C-Sym): \(C_w(X,Y)\iff C_w(Y,X)\).
   (Delivers axiom 1.2.)

8. Conditional coherence (C-Coherence): If \(f_w(X)\subseteq Y\) then \(C_w(X,Y)\).
   (This is axiom 1.4: from \(A\to B\) infer \(A\circ B\).)

No further constraints on \(C_w\) are required for the NL axioms you gave.

---

What the conditions mean (intuitively)

• \(f_w\) says which \(A\)-worlds are “relevant” at \(w\) when checking \(A\to B\). (Id) makes \(A\to A\) valid. (Succ) makes modus-ponens sound. (NE)+(Bo) deliver connexive behavior: if \(A\to B\) holds, then \(B\to\sim A\) must fail. (Contra) is exactly your 1.7 turned into set-inclusion.
• \(C_w\) is a primitive compatibility predicate; we only need it to be symmetric and to accept every pair \((X,Y)\) when \(X\) relevantly entails \(Y\) (C-Coherence). This is deliberately weak: the axioms you listed do not force a tighter reading of \(\circ\), so we keep it as general as possible while still making 1.2 and 1.4 valid.

---

Soundness (axioms and rules are valid)

Let \(\mathcal M=\langle W,f,C,V\rangle\) be any NL-model.

• 1.1 \(A\to A\): At any (w), \(f_w(⟦ A⟧)\subseteq ⟦ A⟧\) by (Id).
• 1.2 \((A|B)\to (B|A)\): \((A|B)\) is \(\sim(A\circ B)\). By (C-Sym), \(C_w(X,Y)\iff C_w(Y,X)\). Hence if \(\neg C_w(X,Y)\) then \(\neg C_w(Y,X)\).
• 1.3 \(A\to \sim\sim A\): \(\sim\sim A\) is equivalent to \(A\) under classical negation, so this is just 1.1.
• 1.4 \((A\to B)\to (A\circ B)\): If \(f_w(⟦ A⟧)\subseteq ⟦ B⟧\), then by (C-Coherence), \(C_w(⟦ A⟧,⟦ B⟧)\), i.e., \(A\circ B\).
• 1.5 \((A\neq B\neq C)\to(((A\to B)\wedge (B\to C))\to (A\to C))\): The inner implication is validated by (Mon): if \(f_w(⟦ A⟧)\subseteq ⟦ B⟧\) and \(f_w(⟦ B⟧)\subseteq ⟦ C⟧\), then \(f_w(⟦ A⟧)\subseteq f_w(⟦ B⟧)\subseteq ⟦ C⟧\). The outer antecedent only strengthens it further, so the whole axiom is valid.
• 1.6 \((A\wedge B)=(B\wedge A)\): \(⟦ A\wedge B⟧=⟦ B\wedge A⟧\) set-theoretically, hence each direction \((A\wedge B)\to (B\wedge A)\) and converse hold by (Id).
• 1.7 \(((A\wedge B)\to C)\to ((A\wedge \sim C)\to \sim B)\): Let \(X=⟦ A⟧\), \(Y=⟦ B⟧\), \(Z=⟦ C⟧\). The antecedent says \(f_w(X\cap Y)\subseteq Z\). By (Contra), \(f_w(X\cap (W\setminus Z))\subseteq W\setminus Y\), i.e., \(f_w(⟦ A\wedge \sim C⟧)\subseteq ⟦ \sim B⟧\). That is exactly the consequent.
• R1 (modus ponens): If \(\mathcal M,w\models A\) and \(\mathcal M,w\models A\to B\), then \(w\in ⟦ A⟧\subseteq f_w(⟦ A⟧)\subseteq ⟦ B⟧\) by (Succ). Thus \(w\models B\).
• R2 (adjunction): If \(A\) and \(B\) are true at \(w\), then \(A\wedge B\) is true at \(w\) by the clause for \(\wedge\).

Hence every NL theorem is valid in every NL-model.

---

Completeness (canonical model sketch)

Let \(\vdash\) be NL-provability from your axioms and rules. Build a canonical model \(\mathcal M^\ast=\langle W^\ast, f^\ast, C^\ast, V^\ast\rangle\) as follows.

Worlds. \(W^\ast\) is the set of all maximal NL-consistent theories \(\Gamma\) (i.e., sets of formulas closed under \(\vdash\), containing no contradiction in the sense of deriving every formula, and maximal under inclusion).

Valuation. \(V^\ast(p)={\Gamma\in W^\ast: p\in \Gamma}\). Extend \(\sim,\wedge\) pointwise (standard canonical model moves).

Selection. For each \(\Gamma\in W^\ast\) and formula \(A\), define \[ F_\Gamma(A) \; := \;{\Delta\in W^\ast:\ \forall B\ (A\to B\in \Gamma\ \Rightarrow\ B\in \Delta)}. \] This is the set of \(A\)-detachment points for \(\Gamma\). Now set \[ f^\ast_\Gamma\big(⟦ A⟧^{\mathcal M^\ast}\big)\ :=\ F_\Gamma(A). \] (One checks that if \(\Gamma\vdash A=B\) then \(F_\Gamma(A)=F_\Gamma(B)\), so \(f^\ast_\Gamma\) is well-defined on truth sets.)

Compatibility. Put \[ C^\ast_\Gamma!\big(⟦ A⟧^{\mathcal M^\ast},⟦ B⟧^{\mathcal M^\ast}\big)\quad\text{iff}\quad A\circ B\in \Gamma. \] (Again, because \(\circ\) occurs only positively in 1.2 and 1.4, one proves that if \(\Gamma\vdash A=B\) and \(\Gamma\vdash A'=B'\) then \(\Gamma\vdash (A\circ A')\leftrightarrow (B\circ B')\), so this is well-defined on truth sets.)

Truth Lemma. For all \(\Gamma\in W^\ast\) and formulas (A), \[ \mathcal M^\ast,\Gamma \models A \quad\Longleftrightarrow\quad A\in \Gamma. \] The Boolean cases are routine. For \(\to\):
\(\Rightarrow\): If \(\Gamma\models A\to B\), then \(F_\Gamma(A)\subseteq ⟦ B⟧\), hence by maximality and the definition of \(F_\Gamma(A)\) we get \(A\to B\in \Gamma\).
\(\Leftarrow\): If \(A\to B\in \Gamma\), then by definition of \(F_\Gamma(A)\), every \(\Delta\in F_\Gamma(A)\) contains \(B\), i.e., \(F_\Gamma(A)\subseteq ⟦ B⟧\).
For \(\circ\): by the definition of \(C^\ast\).

Frame conditions in the canonical model. One checks:

• (Id) because \(A\to A\) is an axiom, \(A\in\Delta\) for all \(\Delta\in F_\Gamma(A)\).
• (Mon) because from \(\vdash (A\wedge (A\to B))\to B\) (derivable using R1/R2), we get \(F_\Gamma(A)\subseteq F_\Gamma(B)\) whenever \(\Gamma\vdash A\to B\).
• (Succ) since \(\Gamma\) is closed under modus ponens: if \(A\in\Gamma\) and \(A\to B\in \Gamma\), then \(B\in \Gamma\); thus \(\Gamma\in F_\Gamma(A)\).
• (NE) because if \(A\in\Gamma\) then \(\Gamma\in F_\Gamma(A)\).
• (Bo) because \((A\to B)\to \neg(B\to \sim A)\) is provable from 1.4 and 1.2 (read via \(C^\ast\)), hence cannot have \(F_\Gamma(B)\subseteq W^\ast\setminus ⟦ A⟧\).
• (Contra) is provable in the object language as 1.7; thus holds set-theoretically by the truth lemma.
• (C-Sym) is axiom 1.2, hence holds by the truth lemma.
• (C-Coherence) is axiom 1.4, hence holds by the truth lemma.

Therefore \(\mathcal M^\ast\) is an NL-model. By the Truth Lemma, if \(A\) is valid in all NL-models then \(A\in \Gamma\) for every \(\Gamma\in W^\ast\); hence \(\vdash A\). That gives strong completeness.

---

Summary

• Semantics: selection-function conditional \(A\to B\) with classical \(\sim\) and \(\wedge\), plus a primitive symmetric compatibility predicate \(C_w\) for \(A\circ B\).
• Key frame laws: (Id), (Mon), (Succ), (NE), (Bo), (Contra) for \(f_w\); (C-Sym) and (C-Coherence) for (C_w).
• Result: With these frames, all NL axioms and rules are sound, and by the canonical construction above, the semantics is complete for NL.

This gives you a clean, fully compositional, set-based semantics that treats ◦ as a genuine (but weakly constrained) compatibility connective and pins down exactly the connexive behavior encoded by 1.2, 1.4, and 1.7. If you want a more intensional reading of ◦ (e.g., defining \(A\circ B\) as the conjunction of \(\neg(A\to\sim B)\) and \(\neg(B\to\sim A)\)), you can add that definition on top of the above by replacing (C-Coherence) with the biconditional \[ C_w(X,Y)\ \text{iff}\ \neg\big(f_w(X)\subseteq W\setminus Y\big)\ \text{and}\ \neg\big(f_w(Y)\subseteq W\setminus X\big), \] but then you must keep (NE) to avoid vacuity and adjust a few details in the completeness proof. The skeleton above already ensures all the listed NL theorems hold and yields a clean completeness argument.

The negation isn’t classical since we don’t have double negation elimination. Can you write a weaker semantics?

Great point — if NL doesn’t validate double-negation elimination, we shouldn’t build it into the semantics. Here’s a weaker, intuitionistic-style semantics for ~ that keeps 1.3 (A → ~~A) valid but does not validate ~~A → A. Everything else (→, ∧, and ◦) stays as before.

NL* models (with intuitionistic negation)

An NL*-model is \[ \mathcal M=\langle W,\ \le,\ f,\ C,\ V\rangle \] with:

• \((W,\le)\): a nonempty preorder (Kripke frame). Write \(v\ge w\) for \(w\le v\).
• \(V\): a monotone valuation on atoms: if \(w\in V(p)\) and \(w\le v\), then \(v\in V(p)\).
• For each \(w\), a selection function \(f_w:\mathsf{Up}(W)\to \mathcal P(W)\) mapping up-sets \(X\subseteq W\) to sets of worlds.
• For each \(w\), a compatibility relation \(C_w:\mathsf{Up}(W)\times \mathsf{Up}(W)\to{\text{true,false}}\) to interpret \(A\circ B\).

Here \(\mathsf{Up}(W)\) are up-closed sets wrt \(\le\).

Truth-clauses

Let \(⟦ A⟧={w\in W:\mathcal M,w\models A}\).

• \(w\models p\) iff \(w\in V(p)\).
• \(w\models A\wedge B\) iff \(w\models A\) and \(w\models B\).
• Intuitionistic negation:
  \(w\models \sim A\) iff for all \(v\ge w\), \(v\not\models A\).
  Equivalently, \(⟦ \sim A⟧={w:\uparrow w\cap ⟦ A⟧=\varnothing}\), which is an up-set.
• Conditional: \(w\models A\to B\) iff \(f_w(⟦ A⟧)\subseteq ⟦ B⟧\).
• Consistency: \(w\models A\circ B\) iff \(C_w(⟦ A⟧,⟦ B⟧)\).
• Abbreviations: \((A|B)\) is \(\sim(A\circ B)\); \(A=B\) is \((A\to B)\wedge(B\to A)\); \(A\neq B\) is \(\sim(A=B)\).

Frame conditions (all \(w\in W\); \(X,Y,Z\in\mathsf{Up}(W)\))

On the conditional \(f_w\):

1. Id: \(f_w(X)\subseteq X\).
2. Mon: \(X\subseteq Y \Rightarrow f_w(X)\subseteq f_w(Y)\).
3. Succ (local detachment): If \(w\in X\) then \(w\in f_w(X)\).
4. NE (nonvacuity on live inputs): If \(X\cap\uparrow w\neq\varnothing\) then \(f_w(X)\neq\varnothing\).
5. Bo (connexive): If \(f_w(X)\subseteq Y\) then not\((,f_w(Y)\subseteq \neg X,)\), where \(\neg X:={u:\uparrow u\cap X=\varnothing}=⟦ \sim A⟧\) when \(X=⟦ A⟧\).
6. Contra (Boethius 1.7 in set form): If \(f_w(X\cap Y)\subseteq Z\), then \(f_w\big(X\cap \neg Z\big)\subseteq \neg Y\).

On compatibility \(C_w\): 7. C-Sym: \(C_w(X,Y)\iff C_w(Y,X)\). 8. C-Coherence: If \(f_w(X)\subseteq Y\) then \(C_w(X,Y)\).

(Note: “\(\neg\)” above is the intuitionistic negation on sets induced by \(\le\): \(\neg Z={w:\uparrow w\cap Z=\varnothing}\). It’s an up-set, not a plain complement.)

---

Why this is strictly weaker than classical negation

• In any Kripke frame, \(⟦ A⟧\subseteq ⟦\sim\sim A⟧\), so 1.3 \(A\to\sim\sim A\) is valid (via Id).
• But in general \(⟦\sim\sim A⟧\not\subseteq ⟦ A⟧\), so ~~A→A is not valid.
  Countermodel: a two-node chain \(w< v\), with \(p\) true only at \(v\). Then \(w\models \sim\sim p\) but \(w\not\models p\).

---

Soundness (sketch)

Let \(X=⟦ A⟧\), etc. Because \(⟦\sim A⟧\) and \(⟦ A\wedge B⟧\) are up-sets, all clauses are well-typed.

• 1.1 \(A\to A\): by Id, \(f_w(X)\subseteq X\).
• 1.2 \((A|B)\to(B|A)\): since \(C_w\) is symmetric, \(⟦ A\circ B⟧=⟦ B\circ A⟧\); hence \(⟦ \sim(A\circ B)⟧=⟦ \sim(B\circ A)⟧\), and this is just an instance of 1.1.
• 1.3 \(A\to\sim\sim A\): in Kripke semantics, \(X\subseteq \neg\neg X\); thus by Id, \(f_w(X)\subseteq X\subseteq \neg\neg X\).
• 1.4 \((A\to B)\to(A\circ B)\): by C-Coherence.
• 1.5 Transitivity under \(\neq\): the inner \(((A\to B)\wedge(B\to C))\to(A\to C)\) follows from Mon: if \(f_w(X)\subseteq Y\) and \(f_w(Y)\subseteq Z\), then \(f_w(X)\subseteq f_w(Y)\subseteq Z\). (The outer \(A\neq B\neq C\) just strengthens antecedents.)
• 1.6 Commutativity of \(\wedge\): set-theoretic.
• 1.7 \(((A\wedge B)\to C)\to((A\wedge \sim C)\to \sim B)\): let \(X=⟦ A⟧\), \(Y=⟦ B⟧\), \(Z=⟦ C⟧\). Antecedent says \(f_w(X\cap Y)\subseteq Z\). By Contra, \(f_w(X\cap \neg Z)\subseteq \neg Y\), i.e. \(⟦ (A\wedge \sim C)\to \sim B⟧\).
• R1 (MP): if \(w\in X\) and \(f_w(X)\subseteq Y\), then by Succ \(w\in f_w(X)\subseteq Y\).
• R2 (Adjunction): direct from the \(\wedge\)-clause.

Hence every NL theorem is valid in all NL*-models.

---

Completeness (canonical sketch)

Use a standard Kripke-style canonical model for intuitionistic negation:

• Worlds: maximal NL-consistent theories \(\Gamma\) (closed under your rules).
• Order: \(\Gamma\le\Delta\) iff \(\Gamma\subseteq \Delta\).
• Valuation: \(V(p)={\Gamma: p\in\Gamma}\) (monotone under (\subseteq)).
• Selection: \(F_\Gamma(A):={\Delta\ge\Gamma: \forall B\ ((A\to B)\in\Gamma \Rightarrow B\in\Delta)}\). Set \(f^\ast_\Gamma(⟦ A⟧):=F_\Gamma(A)\).
• Compatibility: \(C^\ast_\Gamma(⟦ A⟧,⟦ B⟧)\) iff \(A\circ B\in\Gamma\).

Then prove the Truth Lemma by induction:

• Boolean cases standard (with intuitionistic negation: \(\Gamma\models \sim A\) iff for all \(\Delta\ge\Gamma\), \(\Delta\not\models A\), matching the intended reading).
• \(\to\): by the definition of \(F_\Gamma(A)\).
• \(\circ\): by the definition of \(C^\ast_\Gamma\).

The frame conditions (Id/Mon/Succ/NE/Bo/Contra; C-Sym/C-Coherence) hold in the canonical model because the corresponding axiom-schemata are theorems of NL, and the truth lemma transfers them to the set/relational level. Hence if \(A\) is valid in all NL*-models, then \(A\) is in every maximal NL-theory, so \(\vdash A\).

---

What you get

• A strictly weaker negation (intuitionistic) that validates \(A\to\sim\sim A\) but not \(\sim\sim A\to A\).
• The rest of the NL machinery (conditional, consistency ◦, Boethius principles) is preserved by the same selection/compatibility style, with Bo and Contra phrased using the Kripke negation \(\neg X\) (not classical complement).
• Sound and complete for the given axioms/rules (proof sketched above).

If you like, I can also show a tiny concrete NL*-model that validates 1.1–1.7 but refutes ~~p→p, just to make the failure of DNE explicit.