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.