A2.1 Syntax

The language of hyperlogic is an extension of the language of standard propositional modal logic. We start with an infinite stock of propositional variables , the usual Boolean connectives ( $\neg $ , $\mathbin {\wedge }$ , $\mathbin {\vee }$ , $\mathbin {\rightarrow }$ ), and modal operators (, ). To reduce on clutter, we define $(\phi \mathbin {\leftrightarrow } \psi )$ as $((\phi \mathbin {\rightarrow } \psi ) \mathbin {\wedge } (\psi \mathbin {\rightarrow } \phi ))$ rather than treat $\mathbin {\leftrightarrow }$ as a primitive connective. Nothing in what follows would substantively change if we primitively introduced $\mathbin {\leftrightarrow }$ (or other sentential connectives, e.g., those from relevant logic or linear logic) into our language.

Definition A2.1 (Base language )

The full language of hyperlogic extends in three ways. I will introduce each extension separately so that fragments of the full language can be studied independently.

First, hyperlogic adds an “entailment” operator , where represents the claim that (in that order) entail $\psi $ . This operator is left-multigrade, meaning it can take any finite number (possibly zero) of arguments on the left. We could make right-multigrade as well (e.g., to represent multiple-conclusion logics) without substantively affecting the results presented in what follows. But for notational ease, we assume a fixed arity of 1 on the right.

Definition A2.2 (Entailment language )

Second, hyperlogic adds propositional quantifiers and that bind into sentence position [Reference Fine18]. When combined with the entailment operator, we can regiment laws of logic as universal entailment claims. For instance, we can regiment the law of double negation elimination as .

Definition A2.3 (Quantified language )

Finally, hyperlogic adds operators similar to those found in hybrid logic. Hybrid logic extends propositional modal logic with (i) state terms (including state variables and state “nominals”, i.e., constants), which double as terms denoting worlds and as atomic formulas that hold at their denotation; (ii) for each state term $\sigma $ , an “according to” operator $\mathop {@}\nolimits _\sigma $ , which resets the world of evaluation to the world denoted by $\sigma $ ; and (iii) for each state variable s, a binding operator $\mathop {\downarrow }\nolimits s$ , which reassigns the denotation of s to the current world of evaluation [Reference Areces, ten Cate, Blackburn, Wolter and van Benthem1, Reference Braüner and Zalta11]. Informally, we can read s as “s is actual,” $\mathop {@}\nolimits _s$ as “according to s,…,” and $\mathop {\downarrow }\nolimits s$ as “where s is the current world,….”

Instead of hybrid operators for worlds, hyperlogic introduces hybrid operators for interpretations of the base language, including the logical connectives. Thus, it introduces an infinite stock of interpretation variables and interpretation nominals . We single out a designated nominal ${cl}$ to stand for a classical ( $\textbf {S5}$ ) interpretation of the connectives. An interpretation term is a member of $\textsf {ITerm} := \textsf {IVar} \cup \textsf {INom}$ . We use $\iota , \kappa , \lambda $ , etc. as metavariables over interpretation terms.

Definition A2.4 (Hybrid language )

Informally, we can read $\iota $ as “ $\iota $ is correct,” $\mathop {@}\nolimits _\iota $ as “according to $\iota $ ,…,” and $\mathop {\downarrow }\nolimits i$ as “where i is the current interpretation,….”

The binder $\mathop {\downarrow }\nolimits $ allows us to define the following as abbreviations for the connectives under their classical interpretation.

Definition A2.5 (Rigidly classical connectives)

Where i is not in $\phi $ or $\psi $ ,

These “connectives” are interpreted classically even at nonclassical interpretations and even within the scope of “according to” operators. We will make extensive use of these rigidly classical connectives throughout, as it is in large part thanks to them that hyperlogic has a nontrivial logic.

These three extensions can be freely combined: is the quantified entailment language, is the quantified hybrid language, and is the hybrid entailment language. For convenience, we define the full language of hyperlogic as .

A2.2 Semantics

The main semantic innovation behind hyperlogic is to relativize truth to a “hyperconvention,” i.e., a maximally specific interpretation of the base language. More precisely, a hyperconvention specifies a space of (coarse-grained) possible worlds propositions, assigns each propositional variable to a possible worlds proposition in the space, and assigns each connective in (or ) to an operation on propositions, i.e., a function from some proposition(s) to a proposition.

At the outset, we place no constraints on which operations can be assigned to a connective by a hyperconvention. The task of exploring how things change when we impose such constraints is taken up in Part B.

Just as a proposition is typically modeled as a set of worlds, a “convention” is modeled as a set of hyperconventions.

We can think of a logic as a special type of convention that only concerns the interpretation of the connectives (and , if present). Here, we need not take a stand on what features of entailment are essential to logic: the hyperconvention semantics can accommodate a range of views on this matter.

To define our models, we need to introduce the notions of an index and an index proposition. In the hyperconvention semantics, truth is evaluated relative to an index, i.e., a world-hyperconvention pair.

As a formal semantics, hyperlogic is neutral on how to understand what an index represents. Kocurek [Reference Kocurek30, p. 13682] interprets indices as worlds “under descriptions.” On this picture, logic is not a feature of the world but a feature of our representation of it (cf. [Reference Kocurek and Jerzak32]). We could, however, instead hold that logic is genuinely part of the world. In that case, an index $\left \langle w,c \right \rangle $ represents a (perhaps logically impossible) world, where the w component determines all the nonsemantic facts while c determines the semantic facts.

Given this notion of an index, there are now three relevant notions of “proposition” to consider. First, there’s the standard, coarse-grained notion of a proposition as a set of worlds, which is what hyperconventions assign to propositional variables, and operations on which they assign to connectives. Call this the intension of a formula relative to a hyperconvention. Second, there’s a fine-grained notion of a proposition as a set of indices, which is the compositional semantic value of a formula. (Thus, semantic values are more fine-grained than intensions.) Finally, there is an intermediate notion of a “visible” index proposition, i.e., a function from hyperconventions to intensions in their proposition space. More precisely:

Since a propositional variable’s intension relative to a hyperconvention is always a world proposition from that hyperconvention’s proposition space (i.e., $c(p) \in \pi _{c}$ ), the (fine-grained) semantic value of a propositional variable is always a visible index proposition. Propositional quantifiers, therefore, range over visible index propositions (see [Reference Kocurek30, p. 13677]).

We are now ready to define our models and semantics more explicitly. A model in this semantics specifies (i) a set of states (or “worlds”), (ii) a set of conventions for interpretation terms to denote, (iii) a set of (visible) propositions for quantifiers to range over, and (iv) a valuation function.

Following [Reference Kocurek30], we only impose two minimal constraints on proposition domains at the outset (Part B will explore others). These minimal constraints effectively rule out distinct yet indiscernible hyperconventions (i.e., they ensure the soundness of PII in Table A6 in Section A4.1). It would be interesting to see how the logic of hyperlogic changes if we drop those constraints. But I have yet to find a completeness proof that does without them, so I leave that task aside.Footnote ⁷

Definition A2.12 (Semantics)

Where x is a (propositional or interpretation) variable and v is a possible value for that variable, let $V^x_v$ be the valuation like V except that $V^x_v(x) = v$ , and let $\mathcal {M}^x_v$ be $\left \langle W,D_{\mathbb {C}},D_{\mathbb {P}},V^x_v \right \rangle $ . Then

where and . If $\Gamma $ is a set of formulas, we write to mean that for all $\gamma \in \Gamma $ . When $\mathcal {M}$ is clear from context, we drop mention of it.

Note, the right-hand side of the semantic clause for should be read as requiring that is defined, i.e., each is in the proposition space of c. If for some $\phi _i$ , then regardless of w. In other words, if is undefined, then (but still defined).

Also, following [Reference Kocurek30], we interpret iterated $\mathop {@}\nolimits $ -operators as redundant. Thus, $\mathop {@}\nolimits _{\iota _1}\mathop {@}\nolimits _{\iota _2}\phi $ is equivalent to $\mathop {@}\nolimits _{\iota _2}\phi $ . This is how such operators standardly work in hybrid logic and it simplifies the semantics and logic greatly. This equivalence could be questioned, though, and it would be worth investigating a more general semantics where it doesn’t hold. Doing so is beyond the scope of this paper, however.

Which logics can be represented as a hyperconvention on this semantics? Kocurek [Reference Kocurek30] proves a result that provides an answer to this question.Footnote ⁸ Say a logic $\textbf {L}$ over is a set of pairs of the form where (we allow the first element to be the empty tuple $\left \langle \right \rangle $ ). Intuitively, if , then , in that order, entail $\psi $ in $\textbf {L}$ . Say a logic $\textbf {L}$ is representable by a hyperconvention c over W if for any hyperframe $\mathcal {F} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}} \right \rangle $ where $c \in D_{\mathbb {H}}$ , there is a hypermodel $\mathcal {M} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}},V \right \rangle $ based on $\mathcal {F}$ such that

This means that so long as the state space of a hypermodel is sufficiently large, one can represent any finitary logic over that state space. This includes many of the familiar logics in the literature (intuitionistic logic, Kleene’s logic, paraconsistent logics, quantum logic, etc.).Footnote ⁹

A2.3 Consequence

There are two notions of consequences we can define in the hyperconvention semantics. First, there is a classical notion of consequence, i.e., truth-preservation relative to a classical interpretation of the connectives. Second, there is a “universal” notion of consequence, i.e., consequence no matter how we interpret the connectives.Footnote ¹⁰

To define these notions more precisely, we need to define the notion of a “classical” interpretation of the connectives.Footnote ¹¹

Note that classical hyperconventions interpret and as universal $\textbf {S5}$ modals. I suspect that the proofs of completeness presented in Sections A3 and A4 can survive if we weaken this requirement so that and can be interpreted as obeying other normal modal logics, assuming we make corresponding adjustments to the axioms (see footnote 16 for one possible strategy). But I won’t take up this question here, as the proofs are already complex enough even assuming and are universal modals.

It is straightforward to verify the following:

Proposition A2.15 (Classical connectives)

If $\mathcal {M}$ is classical, then

Henceforth, I will only consider classical hypermodels: when I say “hypermodel,” I always mean “classical hypermodel.”

Kocurek [Reference Kocurek30, theorem 8] proves the following:

Proposition A2.17 essentially gives us a method of moving back and forth between classical and universal consequences. This will be the key to developing our proof system of hyperlogic in the next section.

A3.1 Proof systems for classical and universal reasoning

The axiomatizations for classical and universal consequences in involve a kind of double recursion: they are not defined as separate systems with their own axioms and rules but rather interdefined with rules for moving between the two (cf. [Reference Curry14, Reference Indrzejczak23, Reference Indrzejczak24]; [Reference Humberstone22, sec. 7.5]).

When reasoning within hyperlogic, it is often useful to switch back and forth between classical reasoning and universal reasoning, as these notions of consequences obey different rules. Consider the rule of necessitation:

This rule is classically sound since classical hyperconventions interpret as a normal modal operator. But the rule is not universally sound: while $\mathop {@}\nolimits _{cl}(p \mathbin {\vee } \neg p)$ is universally valid, is not since a hyperconvention could interpret abnormally. By contrast, consider the corresponding rule for $\mathop {@}\nolimits $ :

$$ \begin{align*} \text{If}\ \phi\ \text{is provable, then}\ \mathop{@}\nolimits_\iota\phi\ \text{is provable}.\\[-8pt] \end{align*} $$

This rule is not classically sound: while $p \mathbin {\vee } \neg p$ is classically valid, $\mathop {@}\nolimits _\iota (p \mathbin {\vee } \neg p)$ is not since $\iota $ may denote a nonclassical convention. Yet the rule is universally sound: if $\phi $ holds on any hyperconvention, then $\phi $ holds at every hyperconvention in the convention denoted by $\iota $ , i.e., $\mathop {@}\nolimits _\iota \phi $ holds.

For this reason, we will introduce two interdefined proof systems: (for classical provability) and (for universal provability). We call the collection of these two proof systems , the minimal hyperlogic in .Footnote ¹² Before giving the axioms and rules (Tables A1 and A2), let me explain some of the notation used to state them.

Table A1 Axioms and rules for classical provability in .

Table A2 Axioms and rules for universal provability in .

First, because the deduction theorem is classically sound ( iff ), we can simply define as shorthand for . However, the deduction theorem is not universally sound: does not imply since nothing of that form is universally valid. So the “axioms” for have formulas on the left.Footnote ¹³

Second, we introduce the following abbreviations (where i isn’t $\iota $ ):

The truth conditions of these abbreviations reduce to the following:Footnote ¹⁴

We’ll use $\neq $ to abbreviate $\mathop {\sim }\nolimits (\cdots = \cdots )$ (e.g., $\iota \neq \kappa $ abbreviates $\mathop {\sim }\nolimits (\iota = \kappa )$ ).

Some further notational conventions: We write and for co-provability. Where are formulas, we write $\widehat {\phi }$ for $(\en {\mathbin {\&}}{\phi })$ . We use as a metavariable over unary connectives (), over binary connectives (), and over connectives of any arity. (This will generally be clear from context.) The rigidly classical counterparts of , , and are designated as , , and respectively. (For example, if , then ; if , then ; etc.)

Tables A1 and A2 contain the basic axioms and rules for each proof system. A proof is just a list of statements of the form or , each line of which is either an axiom or follows from previous lines via a rule. By induction on the length of proofs, both proof systems satisfy the following substitution principles.

Lemma A3.18 (Term substitution)

If and $\iota '$ is free for $\iota $ in $\phi $ , where $\iota $ is any interpretation term besides ${cl}$ , then . Similarly for .

Table A3 Some useful theorems and derivable rules for in .

Tables A3 and A4 contain some useful theorems and derivable rules. Their derivations are left as exercises for the reader.Footnote ¹⁵ Throughout, I suppress mention of axioms corresponding to classical propositional reasoning (Struct, MP, and Ded) and of RE, which is implicitly used frequently. I likewise suppress mention of S5 unless the application involves specifically modal reasoning.Footnote ¹⁶ Also, by the U2C rule, all of the axioms for can be imported into , so I use the same labels for both versions.

Table A4 Some useful theorems and derivable rules for in .

A3.2 Soundness and completeness

We now set out to prove that is sound and complete in —that is, is sound and complete for classical consequence in and is sound and complete for universal consequence in . The proof of soundness is straightforward, though it requires two lemmas (established by induction on formulas), which we’ll appeal to later.

We write to mean “ is a theorem of for some ”. Similarly for .

We start by proving completeness for classical consequence via a canonical model construction. We then pair this completeness result with Proposition A2.17 to bootstrap our way to completeness for universal consequence.

Throughout, let be some new propositional variables, let be some new interpretation nominals, and let be the expansion of with these new terms. In proofs, I will use (“contradiction”) to signal the end of a reductio argument. Also, by “consistent,” I mean classically consistent, i.e., $\Gamma \nvdash \bot $ (where $\bot := (p \mathbin {\&} \mathop {\sim }\nolimits p)$ (Definition A2.5)).

Proof. Set $l_\Gamma = l_1^+$ . Enumerate the -formulas as . We define a sequence of sets . First, . Next, if $\Gamma _k, \phi _k \nvdash \bot $ ; otherwise, $\Gamma _k' = \Gamma _k$ . Lastly, let’s say $l^+$ or $p^+$ is “unused” if it is the first member of $\textsf {INom}^+$ or $\textsf {Prop}^+$ that has yet to appear in the construction. Then:

Let $\Gamma ^+ = \bigcup_{[k \geq 1]} \Gamma _k$ . The proof that $\Gamma ^+$ is maximal is standard. The fact that $\Gamma ^+$ satisfies (i)–(iii) follows from the construction of $\Gamma ^+$ . We just need to show $\Gamma ^+$ is consistent. It suffices to show that each $\Gamma _k$ is consistent. By “i is fresh,” I mean it occurs nowhere in the relevant formulas.

• Base case. Suppose $\Gamma _1$ is inconsistent. Thus, by Elim $_{\mathbin {\&}}$ , for some . By Lemma A3.18, where i is fresh, . By Gen $_{\mathop {\downarrow }\nolimits }$ , . By Vac $_{\mathop {\downarrow }\nolimits }$ , .

• Inductive step. Suppose $\Gamma _k$ is consistent. By construction, $\Gamma _k'$ is consistent. Suppose for reductio $\Gamma _{k+1}$ is inconsistent. That means $\Gamma _{k+1} \neq \Gamma _k'$ , which means $\phi _k \in \Gamma _{k+1}$ where either $\phi _k = \neg \mathop {@}\nolimits _\iota \psi $ or $\phi _k = (\iota \neq \kappa ) \mathbin {\wedge } \left |{\iota }\right |_1 \mathbin {\wedge } \left |{\kappa }\right |_1$ . Assume throughout that the contradiction is derivable from .

  Suppose $\phi _k = \neg \mathop {@}\nolimits _\iota \psi $ . Let $l^+$ be the witness introduced into $\Gamma _{k+1}$ . Observe that by Red (recall: $\left |{l^+}\right |_1 := \mathop {@}\nolimits _{l^+}\mathop {\downarrow }\nolimits i.\mathop {@}\nolimits _{l^+}i$ ). Thus, where i is fresh,

  

  Suppose $\phi _k = (\iota \neq \kappa ) \mathbin {\wedge } \left |{\iota }\right |_1 \mathbin {\wedge } \left |{\kappa }\right |_1$ . Where $p^+$ is the witness introduced into $\Gamma _{k+1}$ ,

  

Throughout, let $\Gamma $ be a Lindenbaum set, and let $\textsf {ITerm}^+ = \textsf {ITerm} \cup \textsf {INom}^+$ .

Proof. Let . Observe is consistent by RK. By Rigid and S5, is also nominalized (since $l_\Gamma \in \Gamma $ ) and differentiates terms (since $\Gamma $ differentiates terms). Moreover, any will continue to have these properties (for differentiation of terms, note that either or for any $\iota $ and $\kappa $ ). So we just need to show can be consistently extended to witness $\neg \mathop {@}\nolimits $ s. One can then extend this set into a maximal consistent one.

Enumerate all formulas of the form $\neg \mathop {@}\nolimits _\iota \psi $ as . Define the formulas as follows: $\delta _0 := \neg \phi $ ; given $\delta _n$ is defined so that , let $\delta _{n+1} := \chi _{n+1} \mathbin {\rightarrow } (l^+ \in \iota \mathbin {\wedge } \neg \mathop {@}\nolimits _{l^+}\psi )$ where $\chi _{n+1} = \neg \mathop {@}\nolimits _\iota \psi $ and $l^+$ is the first from $\textsf {INom}^+$ such that . Given there always is such an $l^+$ , will consistently witness $\neg \mathop {@}\nolimits $ s.

Suppose for reductio that are defined but there is no $l^+$ meeting the above condition. Thus, for all $l^+$ , there are some such that . By RK, . Since , that means . So if , then , and so . Hence, , i.e., . Now, where $l_\Delta ,\left |{l_\Delta }\right |_1 \in \Delta $ , the following are -provable from $l_\Delta ,\left |{l_\Delta }\right |_1$ :

Since $\Delta $ witnesses $\neg \mathop {@}\nolimits $ s, there is an $l^+$ such that . Reversing the provable equivalence above, we get . But , so $\Delta $ is inconsistent, .

Note that $C_\iota $ is well-defined by the following lemma:

Finally, $C_\iota $ is always nonempty: if $\left |{\iota }\right |_1 \in \Gamma $ , then $(\iota \in \iota ) \in \Gamma $ ; and if $\neg \left |{\iota }\right |_1 \in \Gamma $ , i.e., $\neg \mathop {@}\nolimits _\iota \mathop {\downarrow }\nolimits i.\mathop {@}\nolimits _\iota i \in \Gamma $ , then since $\Gamma $ witnesses $\neg \mathop {@}\nolimits $ s, $(l^+ \in \iota ) \in \Gamma $ for some $l^+$ .

A3.3 Axioms for

It is straightforward to extend into . The two additional axioms needed are stated in Table A5. The resulting system is called . To prove the completeness of , we simply amend Definition A3.30 so that is defined as:

The proof goes through as in Section A3.2, adding the relevant inductive steps for .

Table A5 Axioms and rules for provability in .

A4.1 Axiomatizing quantifiers

The new axioms and rules for the quantifiers are stated in Table A6. We call the resulting system . This axiomatization makes use of the following abbreviations (where p is not free in $\phi $ ):

If and , the truth conditions reduce to the following:

Intuitively, ${\mathop {\textsf {E}}}\phi $ says that $\phi $ denotes a world proposition that “exists” according to the current hyperconvention. This formula is not trivially satisfied: if, say, $W \notin \pi _{c}$ , then $\mathcal {M},w,c \nVdash {\mathop {\textsf {E}}}(p \mathbin {\supset } p)$ since for no $Q \in D_{\mathbb {P}}$ does $Q(c) = W$ .

Table A6 Axioms and rules for provability in .

Note that Elim $_{\forall }$ does not allow substituting any $\psi $ for p (even if p is free for $\psi $ ), since $\psi $ need not denote an existent proposition according to a hyperconvention. For example, if $\emptyset \notin \pi _{c}$ , then (since $P(c) \in \pi _{c}$ for any $P \in \mathbb {P}_{D_{\mathbb {H}}}$ ) even though (since regardless of c). However, since $V(p)$ is always a visible proposition ( $V(p)(c) \in \pi _{c}$ ), instantiation with other propositional variables is allowed. Note also the PII axiom, which is effectively the principle of the identity of indiscernibles for hyperconventions: if $c_1$ and $c_2$ have the same proposition space, and interpret the propositional variables and connectives the same way, then $c_1 = c_2$ . The soundness of PII is ensured by the two minimal constraints on proposition domains in Definition A2.11.Footnote ¹⁷

The proofs of Lemmas A3.20 and A3.21 remain unchanged. In addition, we have the following (which is needed to prove the soundness of Elim $_{\forall }$ ):

Table A7 contains some useful derivable theorems and rules. The proof of Lemma A3.18 still goes through. However, Lemma A3.19 no longer holds in : e.g., yet .Footnote ¹⁸ Instead, only a restricted form of Lemma A3.19 holds (fortunately, this suffices):

Table A7 Some useful theorems and derivable rules in .

A4.2 Completeness

Now for completeness. The lemmas from Section A3.2 whose proof need revision are Lemmas A3.24, A3.26, A3.31, A3.33, and A3.34. Throughout, let $\textsf {Prop}^+$ and $\textsf {INom}^+$ be as before, and let be the expansion of with these new terms but without propositional quantifiers binding elements of $\textsf {Prop}^+$ (so members of $\textsf {Prop}^+$ are treated as propositional “constants”).

Note that Henkin sets do necessarily not differentiate terms in the sense of Definition A3.23. We don’t want to assume that if $(\iota \neq \kappa ) \in \Gamma ^+$ , then $(\mathop {@}\nolimits _\iota p^+ \neq \mathop {@}\nolimits _\kappa p^+) \in \Gamma ^+$ for some $p^+$ since $\Gamma ^+$ might contain . In that case, $\Gamma ^+$ would have to contain for some .

Proof. Proof is as before except we revise the definition of $\Gamma _{k+1}$ :

We need to show that if $\Gamma _k'$ is consistent and , then $\Gamma _{k+1}$ is consistent. Suppose otherwise. That means for some , where $q \in \textsf {Prop}$ is fresh,

The proofs of the intermediate lemmas through Lemma A3.29 remain intact. To continue, we revise the definition of a canonical hyperconvention (Definition A3.30).

Since $\pi _{c_\kappa }$ is no longer the full powerset, we must ensure that this does define a hyperconvention in that the outputs of $c_\kappa $ are always within $\pi _{c_\kappa }$ .

We must also verify Lemma A3.31 still holds in order for $C_\iota $ to be well-defined.

Lemma A4.44 (Identity for canonical hyperconventions (revised))

Where $\left |{\kappa }\right |_1 \in \Gamma $ and $\left |{\lambda }\right |_1 \in \Gamma $ ,

$$ \begin{align*} c_\kappa = c_\lambda {\quad{\mathbin{\Leftrightarrow}}\quad} (\kappa = \lambda) \in \Gamma. \end{align*} $$

Proof. The right-to-left direction is as before. For the left-to-right direction, suppose $(\kappa \neq \lambda ) \in \Gamma $ . By PII, either (i) or (ii) for some . We’ll show that either way, $c_\kappa \neq c_\lambda $ .

Suppose (i). By Dual $_{\forall }$ and witnessing s, there is a $p^+$ such that $(\mathop {@}\nolimits _\kappa p^+ \neq \mathop {@}\nolimits _\lambda p^+) \notin \Gamma $ . Thus, $c_\kappa (p^+) \neq c_\lambda (p^+)$ , since

Suppose instead (ii). I’ll just do the case to illustrate. By Dual $_{\forall }$ and witnessing s, for some $p^+$ and $q^+$ . Hence, $(\mathop {@}\nolimits _\kappa p^+ = \mathop {@}\nolimits _\lambda q^+) \in \Gamma $ , and so $c_\kappa (p^+) = c_\lambda (q^+)$ . Moreover, . Thus, by Lemma A3.29,

Hence, .

Definition A4.45 (Canonical hypermodel (revised))

The canonical hypermodel of $\Gamma $ is the hypermodel $\mathcal {M}_\Gamma = \left \langle W_\Gamma ,{D_{\mathbb {C}}}_\Gamma ,{D_{\mathbb {P}}}_\Gamma ,V_\Gamma \right \rangle $ is defined as in Definition A3.32, except where $\textsf {Prop}^* = \textsf {Prop} \cup \textsf {Prop}^+$ :

It is easy to check that ${D_{\mathbb {P}}}_\Gamma $ satisfies conditions i and ii from Definition A2.11. Note also that $V_\Gamma (p) \in {D_{\mathbb {P}}}_\Gamma $ by Lemma A4.43(b).

Lemma A4.46 (Canonical classical convention (Revised))

Where $c_\kappa \in C_{cl}$ ,

Proof. The proof is the same as before, except now we must tweak the connectives case and also deal with the quantifier cases. For the connectives, I’ll just do the $\neg $ -case. The proof is the same except when . In that case, $\Delta ,c_\kappa \nVdash \neg \phi $ (see page 8). Thus, we must show that $\mathop {@}\nolimits _\kappa \neg \phi \notin \Delta $ . Since , there is no , i.e., no $p^+$ such that . By -witnessing, . By Bool, Dist $_{\mathop {@}\nolimits }$ , and BF $_{\mathop {@}\nolimits }^+$ , $\neg \mathop {@}\nolimits _\kappa {\mathop {\textsf {E}}} \phi \in \Gamma $ . By OpEx, $\neg \mathop {@}\nolimits _\kappa {\mathop {\textsf {E}}}\neg \phi \in \Gamma $ . By NecEx, . By TrEx and RK, . Hence, $\neg \mathop {@}\nolimits _\kappa \neg \phi \in \Delta $ , and so $\mathop {@}\nolimits _\kappa \neg \phi \notin \Delta $ .

For the quantifiers, here’s the -case (the -case is similar):

The left-to-right direction of the (*) step follows from -witnessing, while the right-to-left direction follows from Intro and VE.

From here, the proof of completeness is the same. (In particular, Lemmas A4.46 and A4.48 show that $C_{{cl}}$ is classical.) Thus:

A4.3 Axioms for

In adding to the language, the main complication involves PII. Since can take any number of arguments on the left, we cannot state “” as a single formula. In fact, completeness is not possible in as it stands, since consequence is not compact in . In particular, , where . Yet $\Gamma _0 \nvDash (\iota = \kappa )$ for each finite $\Gamma _0 \mathrel {\subseteq } \Gamma $ . Still, as we’ll see in Part B, there are natural restricted classes of hypermodels on which PII is sound as is.Footnote ¹⁹ Over such classes, completeness can be restored.