THE LOGIC OF HYPERLOGIC. PART A: FOUNDATIONS

Abstract

Hyperlogic is a hyperintensional system designed to regiment metalogical claims (e.g., “Intuitionistic logic is correct” or “The law of excluded middle holds”) into the object language, including within embedded environments such as attitude reports and counterfactuals. This paper is the first of a two-part series exploring the logic of hyperlogic. This part presents a minimal logic of hyperlogic and proves its completeness. It consists of two interdefined axiomatic systems: one for classical consequence (truth preservation under a classical interpretation of the connectives) and one for “universal” consequence (truth preservation under any interpretation). The sequel to this paper explores stronger logics that are sound and complete over various restricted classes of models as well as languages with hyperintensional operators.

A1 Introduction

Philosophers of logic debate about metalogical claims like the following:

1. (1) Classic logic is correct.

2. (2) The law of excluded middle holds.

3. (3) Some contradiction entails everything.

Such metalogical claims can also felicitously occur in embedded environments. One illustration involves claims such as (4)–(6), which describe what holds according to certain logics.

1. (4) According to intuitionistic logic, the law of excluded middle doesn’t hold.

2. (5) In strong Kleene logic, nothing is valid.

3. (6) Everything that is intuitionistically valid is classically valid.

Other illustrations of the embeddability of metalogical claims come from attitude verbs, conditionals, and modals:

1. (7) Inej believes intuitionistic logic is correct.

2. (8) If intuitionistic logic were correct, excluded middle would fail.

3. (9) It might be that there are true contradictions.

Although such metalogical claims are loaded with theoretical terms whose nature is philosophically contentious, these are all perfectly intelligible claims of English. Given this, it is natural to investigate the semantic analysis of such claims. To do this, we need to answer two questions. First, how do we regiment metalogical claims into the object language so that they can be assigned a compositional semantic value? Second, how do we assign compositional semantic values to such regimentations?

Recently, Kocurek [30] has developed a hyperintensional system that offers answers to both questions called hyperlogic. To regiment metalogical claims, hyperlogic utilizes a combination of several different devices: a multigrade entailment operator ; propositional quantifiers and [18] to regiment laws of logic; and terms and operators borrowed from hybrid logic [1, 11], such as nominals () to regiment claims about which logic is correct, and operators $\mathop {@}\nolimits $ to regiment “according to” claims. To illustrate, here is how we could regiment (1)–(6) in hyperlogic. ¹

1. (1) Classic logic is correct.

   $$ \begin{align*} {cl} \end{align*} $$

2. (2) The law of excluded middle holds.

   

3. (3) Some contradiction entails everything.

   

4. (4) According to intuitionistic logic, the law of excluded middle doesn’t hold.

   

5. (5) In strong Kleene logic, nothing is valid.

   

6. (6) Everything that is intuitionistically valid is classically valid.

   

To assign compositional semantic values to metalogical claims, hyperlogic introduces a shiftable convention parameter—a “hyperconvention”—into points of evaluation. This parameter determines the interpretation of the logical connectives (as well as ). ² The semantic value of a formula is a set of world-hyperconvention pairs. While metalogical claims may express a trivial possible worlds proposition relative to a hyperconvention, they can have nontrivial semantic values that hyperintensional environments can exploit.

My aim in this paper is not to defend hyperlogic as a semantic theory for metalogical claims. Rather, my aim is to address the following question: given that hyperlogic is designed to reason about other logics, what, if anything, can we say about logical consequence within hyperlogic itself? In other words, what is the logic of hyperlogic?

At first, one might suspect the logic of hyperlogic is entirely uninteresting. How much could be valid in a framework with the expressive resources to talk about other logics? As it turns out, however, this initial impression is mistaken. To show this, I present a sound and complete proof system for hyperlogic. It involves two separate axiomatic systems that are recursively defined in terms of one another, each representing different kinds of consequences: one represents ordinary classical consequence (truth preservation relative to a classical interpretation of the connectives) while the other represents “universal” consequence (truth preservation relative to any interpretation of the connectives). This dual proof system contains rules for moving back and forth between these axiomatic systems. The result is an elegant, tractable, and nontrivial logic for hyperlogic.

There are several reasons independent of the semantics of metalogical claims to be interested in the logic of hyperlogic. For one, the main semantic innovation of hyperlogic, viz., to add a shiftable convention parameter for interpreting the logical connectives, is behind several “conventionalist” approaches to hyperintensionality in the literature, which model hyperintensional environments as convention-shifting operators (cf. [32, 36, 39, 40, 59]). ³ This contrasts with approaches that introduce incomplete and/or inconsistent states (impossible worlds, truthmakers, situations, etc.) into standard possible worlds frameworks. ⁴ Even if one thinks these conventionalist approaches are ultimately mistaken, one might still wonder how many hyperintensional phenomena can be explained in terms of it. Hyperlogic presents an encouraging answer for conventionalists about hyperintensionality.

In addition, hyperlogic provides a simple logic for “according to”. For example, the following sounds fine to say:

1. (10) Pluto is not a planet, but according to the folk definition of “planet,” Pluto is a planet.

The phrase “according to the folk definition of ‘planet’” seems to, in some sense, shift the interpretation of “planet” mid-sentence so that the second “Pluto is a planet” is interpreted via the folk definition of “planet” [33, p. 8]. If so, it’s natural to ask how this operator works and what logical principles govern it. As we’ll see, hyperlogic offers a simple yet attractive answer to these questions.

Finally, hyperlogic may provide insight into the problem of logical omniscience. Stalnaker [53, 54, 56] famously analyzed the content of an agent’s mental state as a set of possible worlds, viz., those at which what the agent (actually) believes is true. While this view has its merits, it infamously predicts that agents’ beliefs are closed under logical entailment. There is a vast disagreement in the literature over how to address this problem. ⁵ Hyperlogic potentially provides a novel and attractive solution by analyzing mental content in terms of sets of world-hyperconvention pairs instead of sets of worlds. This new picture can validate certain modest closure principles without requiring beliefs be closed under classical consequence. It can thus avoid at least certain forms of logical omniscience while preserving the main features that initially motivated the Stalnakerian picture.

This paper is the first in a two-part series on the logic of hyperlogic. Part A focuses on a very general system for hyperlogic, which places no restrictions on the class of models. The logic of this system is fairly weak, and therefore constitutes a kind of minimal hyperlogic upon which stronger hyperlogics can be based. Part B explores stronger logics of this sort, as well as the logic of hyperlogic enriched further with hyperintensional operators.

Here is an outline of what is to come in this part. In Section A2, I give a brief overview of the syntax and semantics of hyperlogic. In Section A3, I present, and prove the completeness of, a proof system for the fragment of hyperlogic without propositional quantifiers. In Section A4, I extend these results to the language of hyperlogic with propositional quantifiers. I conclude in Section A5.

A2 Hyperlogic: syntax and semantics

We start by reviewing the syntax, semantics, and consequence relation(s) of hyperlogic as presented in [30]. In Section A2.1, we introduce the language of hyperlogic. In Section A2.2, we clarify the notion of a hyperconvention and use it to state a semantics for hyperlogic. In Section A2.3, we identify two notions of consequences in hyperlogic and explain their relation.

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 [18]. 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 [1, 11]. 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 .

Definition A2.6 (Substitution)

We adopt the usual notions of “free” and “bound” variables (where i is bound by $\mathop {\downarrow }\nolimits i$ and p is bound by and ). We say $\iota _2$ is free for $\iota _1$ in $\phi $ if no free occurrence of $\iota _1$ in $\phi $ is in the scope of $\mathop {\downarrow }\nolimits \iota _2$ . In that case, we write $\phi [\iota _2/\iota _1]$ for the result of replacing every free occurrence of $\iota _1$ in $\phi $ with $\iota _2$ . Similarly, $\psi $ is free for p in $\phi $ if no free occurrence of p in $\phi $ is in the scope of or where q occurs free in $\psi $ , or a binder $\mathop {\downarrow }\nolimits i$ where i occurs free in $\psi $ . If $\psi $ is free for p in $\phi $ , we write $\phi [\psi /p]$ for the result of replacing every free occurrence of p in $\phi $ with $\psi $ . Simultaneous substitution $\phi [\psi _1/p_1,\dots ,\psi _n/p_n]$ is defined likewise.

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.

Definition A2.7 (Hyperconvention)

Let $W \neq \emptyset $ and $\pi _{} \mathrel {\subseteq } \mathop {\wp }W$ . A $\pi _{}$ -hyperconvention for (over W) is a function c with domain such that:

1. i. $c(p) \in \pi _{}$ for all $p \in \textsf {Prop}$ .

2. ii. for each n-ary operator .

A $\pi _{}$ -hyperconvention for (over W) adds to the domain, where:

1. iii. .

We call $\pi _{}$ the proposition space for c. We write $\pi _{c}$ for the $\pi _{}$ that c is defined over ⁶ and (with infix notation) for . A hyperconvention for $\mathcal {L}$ (over W) is a $\pi _{}$ -hyperconvention for $\mathcal {L}$ over W for some $\pi _{} \mathrel {\subseteq } \mathop {\wp }W$ . We let be the set of all hyperconventions for $\mathcal {L}$ over W. Throughout, I use “hyperconvention” to mean “hyperconvention for ” if the language under discussion contains , and “hyperconvention for ” otherwise.

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.

Definition A2.8 (Convention)

An convention is a nonempty set of hyperconventions. We let be the set of conventions (for $\mathcal {L}$ ) over W.

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.

Definition A2.9 (Index)

Given a set H of hyperconventions over W, an index over H is a pair $\left \langle w,c \right \rangle $ where $w \in W$ and $c \in H$ . We let be the set of indices over H.

As a formal semantics, hyperlogic is neutral on how to understand what an index represents. Kocurek [30, 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. [32]). 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:

Definition A2.10 (Index proposition)

Given a set of hyperconventions H over W, an index proposition over H is a set of indices . Where , let . An index proposition A is visible if $A(c) \in \pi _{c}$ for all $c \in H$ . We let $\mathbb {P}_{H}$ be the set of visible index propositions over H. We use $X,Y,Z,\dots $ for worlds propositions and $P,Q,R,\dots $ for visible index propositions.

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 [30, 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.

Definition A2.11 (Hyperframes and hypermodels)

A hyperframe is a triple of the form $\mathcal {F} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}} \right \rangle $ , where:

• • $W \neq \emptyset $ is a state space;

• • is a convention domain; we define $D_{\mathbb {H}} := \bigcup D_{\mathbb {C}}$ to be the hyperconvention domain (in other words, $D_{\mathbb {H}}$ is the set of hyperconventions that appear somewhere in $D_{\mathbb {C}}$ );

• • $D_{\mathbb {P}} \mathrel {\subseteq } \mathbb {P}_{D_{\mathbb {H}}}$ is a proposition domain such that:

  1. i. for all $p \in \textsf{Prop}$ , $P_p \in D_{\mathbb {P}}$ , where $P_p(c) = c(p)$ for all $c \in D_{\mathbb {H}}$ ;

  2. ii. for all $c \in D_{\mathbb {H}}$ and all $X \in \pi _{c}$ , there is a $P \in D_{\mathbb {P}}$ such that $P(c) = X$ .

A valuation for $\mathcal {F}$ is a mapping V such that:

• • $V(p) \in D_{\mathbb {P}}$ for each $p \in \textsf {Prop}$ ;

• • $V(l) \in D_{\mathbb {C}}$ for each $l \in \textsf {INom}$ ;

• • for each $i \in \textsf {IVar}$ .

A hypermodel based on $\mathcal {F}$ is a tuple $\mathcal {M} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}},V \right \rangle $ where V is a valuation for $\mathcal {F}$ .

Following [30], 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. ⁷

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 [30], 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 [30] proves a result that provides an answer to this question. ⁸ 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

Proposition A2.13 (Representation)

Any logic is representable by a hyperconvention over W given $\left |{W}\right | \geq \aleph _{0}$ .

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.). ⁹

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. ¹⁰

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

Definition A2.14 (Classical hyperconvention)

Given a hyperframe $\mathcal {F} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}} \right \rangle $ , a hyperconvention is classical for $\mathcal {F}$ if:

1. i. for every and every $\mathcal {M}$ based on $\mathcal {F}$ ;

2. ii. for all $X,Y \in \pi _{c}$ :

   

3. iii. for all :

   

A convention is classical for $\mathcal {F}$ if all of its member are. A (hyper)convention is classical for $\mathcal {M}$ if it’s classical for the hyperframe $\mathcal {M}$ is based on. Finally, $\mathcal {M}$ is classical if $V({cl})$ is classical for $\mathcal {M}$ .

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.”

Definition A2.16 (Consequence)

Where and :

• • $\Gamma $ classically entails $\phi $ , written , if for any (classical) hypermodel $\mathcal {M} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}},V \right \rangle $ , any $w \in W$ , and any :

  

• • $\Gamma $ universally entails $\phi $ , written , if for any (classical) hypermodel $\mathcal {M} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}},V \right \rangle $ , any $w \in W$ , and any :

  

Classical/universal validity, equivalence, etc. are defined likewise.

Kocurek [30, theorem 8] proves the following:

Proposition A2.17 (Embedding consequence)

Let and . Where l is an interpretation nominal, let .

1. a. Assume l (distinct from ${cl}$ ) does not occur anywhere in $\Gamma $ or in $\phi $ . Then iff .

2. b. iff .

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 Completeness for the quantifier-free fragments

We now present some soundness and completeness results for the quantifier-free languages and . In Section A3.1, we present an axiomatization for consequence in . In Section A3.2, we prove this system is sound and complete. In Section A3.3, we extend the axiomatization to .

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. [14, 23, 24]; [22, 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 . ¹² 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. ¹³

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

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

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 .

Lemma A3.19 (Uniform substitution)

If and $\psi $ is free for p in $\phi $ , then . Similarly for .

Tables A3 and A4 contain some useful theorems and derivable rules. Their derivations are left as exercises for the reader. ¹⁵ 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. ¹⁶ 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.

Lemma A3.20 (Unused variables)

For any $\mathcal {F} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}} \right \rangle $ , any $w \in W$ , any $c \in D_{\mathbb {H}}$ , and any $\mathcal {M}$ and $\mathcal {M}'$ based on $\mathcal {F}$ , if V and $V'$ agree on all free variables in $\phi $ (including propositional variables), then iff .

Lemma A3.21 (Partial substitution)

For any $\mathcal {M} = \left \langle W,D_{\mathbb {C}},D_{\mathbb {P}},V \right \rangle $ , if $V(\iota _1) = V(\iota _2)$ and $\iota _2$ is free for $\iota _1$ in $\phi $ , then , where $\phi '$ is the result of replacing some occurrences of $\iota _1$ with $\iota _2$ in $\phi $ .

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

Theorem A3.22 (Soundness in )

For all and :

1. a. If , then .

2. b. If , then .

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)).

Definition A3.23 (Lindenbaum set)

A set is Lindenbaum if it is a maximal consistent set satisfying the following constraints:

1. i. $\Gamma ^+$ is nominalized: there is an $l_\Gamma \in \textsf {INom}^+$ such that $l_\Gamma , \left |{l_\Gamma }\right |_1 \in \Gamma ^+$ .

2. ii. $\Gamma ^+$ witnesses $\neg \mathop {@}\nolimits $ s: if $\neg \mathop {@}\nolimits _\iota \phi \in \Gamma ^+$ , then there is an $l_\iota \in \textsf {INom}^+$ such that $(l_\iota \in \iota ) \in \Gamma ^+$ and $\neg \mathop {@}\nolimits _{l_\iota }\phi \in \Gamma ^+$ .

3. iii. $\Gamma ^+$ differentiates terms: if $(\iota \neq \kappa ) \in \Gamma ^+$ where $\left |{\iota }\right |_1, \left |{\kappa }\right |_1 \in \Gamma ^+$ , then there is a $p^+ \in \textsf {Prop}^+$ such that $(\mathop {@}\nolimits _\iota p^+ \neq \mathop {@}\nolimits _\kappa p^+) \in \Gamma ^+$ .

Lemma A3.24 (Lindenbaum)

If is consistent, then there is a Lindenbaum set where $\Gamma \mathrel {\subseteq } \Gamma ^+$ .

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}^+$ .

Definition A3.25 (Canonical state space)

The canonical state space of $\Gamma $ is the set $W_\Gamma $ of all Lindenbaum sets $\Delta $ where for all , if , then $\phi \in \Delta $ .

Lemma A3.26 (Existence)

If , then $\phi \notin \Delta '$ for some $\Delta ' \in W_\Gamma $ .

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, .

Corollary A3.27 (Plenitude)

For all $\Delta \in W_\Gamma $ and all $\phi $ :

1. a. iff $\phi \in \Delta '$ for all $\Delta ' \in W_\Gamma $ .

2. b. iff $\phi \in \Delta '$ for some $\Delta ' \in W_\Gamma $ .

Definition A3.28 (Definable sets)

Where $X \mathrel {\subseteq } W_\Gamma $ and , we define .

Lemma A3.29 (Replacement of equivalent definitions)

Where $\left |{\iota }\right |_1 \in \Gamma $ :

1. a. If for some $\phi \in [X]_\iota $ , then for all $\phi \in [X]_\iota $ .

2. b. If for some $\phi \in [X]_\iota $ and $\psi \in [Y]_\iota $ , then for all $\phi \in [X]_\iota $ and $\psi \in [Y]_\iota $ .

Proof. We just prove (a) for illustration. Suppose $\phi \in [X]_\iota $ is such that . Let $\psi \in [X]_\iota $ . Thus, for all $\Delta ' \in W_\Gamma $ , $\mathop {@}\nolimits _\iota \phi \in \Delta '$ iff $\Delta ' \in X$ iff $\mathop {@}\nolimits _\iota \psi \in \Delta '$ . By Corollary A3.27, . By Rep (since $\left |{\iota }\right |_1 \in \Gamma $ ), . By Definition A3.25, . Hence, .

Definition A3.30 (Canonical hyperconventions)

Where $\left |{\kappa }\right |_1 \in \Gamma $ , the canonical $\kappa $ -hyperconvention $c_\kappa $ over $W_\Gamma $ is defined as follows:

1. i. $\pi _{c_\kappa } = \mathop {\wp }W_\Gamma $ .

2. ii. .

3. iii. If $\mathop {@}\nolimits _\kappa {cl} \in \Gamma $ , then each is defined as in Definition A2.14. Otherwise:

   

For any $\iota \in \textsf {ITerm}^+$ , define the canonical $\iota $ -convention as .

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

Lemma A3.31 (Identity for canonical hyperconventions)

Where $\left |{\kappa }\right |_1, \left |{\lambda }\right |_1 \in \Gamma $ , $c_\kappa = c_\lambda $ iff $(\kappa = \lambda ) \in \Gamma $ . Thus, if $c_\kappa = c_\lambda $ , then $(\kappa \in \iota ) \in \Gamma $ iff $(\lambda \in \iota ) \in \Gamma $ .

Proof. The left-to-right direction follows since $\Gamma $ differentiates terms. The right-to-left direction follows from SubId and Corollary A3.27.

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^+$ .

Definition A3.32 (Canonical hypermodel)

We define the canonical hypermodel of $\Gamma $ as $\mathcal {M}_\Gamma = \left \langle W_\Gamma ,{D_{\mathbb {C}}}_\Gamma ,{D_{\mathbb {P}}}_\Gamma ,V_\Gamma \right \rangle $ where:

• • (and so, );

• • ${D_{\mathbb {P}}}_\Gamma = \mathbb {P}_{{D_{\mathbb {H}}}_\Gamma }$ ;

• • for each $p \in \textsf {Prop}$ ;

• • $V_\Gamma (\iota ) = C_\iota $ for each $\iota \in \textsf {ITerm}^+$ .

Lemma A3.33 (Canonical classical convention)

$C_{cl}$ is classical.

Lemma A3.34 (Truth)

iff $\mathop {@}\nolimits _\kappa \phi \in \Delta $ .

Proof. By induction on the structure of formulas. The base cases follow from Definitions A3.32 and A3.30 and Corollary A3.27.

• IH. Suppose the claim holds for $\phi $ and $\psi $ . Observe that .

• Connectives. We just do the $\neg $ -case. Suppose first that $\mathop {@}\nolimits _\kappa {cl} \notin \Gamma $ . Then

  
  Suppose now $\mathop {@}\nolimits _\kappa {cl} \in \Gamma $ . Then
  

• $\mathop {@}\nolimits _\iota $ case. Since by Definition A3.32,

  
  For (*): Suppose first that $\mathop {@}\nolimits _\iota \phi \notin \Delta $ . Since $\Delta $ witnesses $\neg \mathop {@}\nolimits _\iota $ , $(l_\iota \in \iota ), \neg \mathop {@}\nolimits _{l_\iota }\phi \in \Delta $ for some $l_\iota $ (so $\lambda = l_\iota $ is our counterexample). Conversely, suppose $\mathop {@}\nolimits _\iota \phi \in \Delta $ . If $(\lambda \in \iota ) \in \Gamma $ , then $\mathop {@}\nolimits _\lambda \iota \in \Delta $ by Rigid, and so by Elim $_{\mathop {@}\nolimits }$ , Gen $_{\mathop {@}\nolimits }$ , and Red, $\mathop {@}\nolimits _\lambda \phi \in \Delta $ .

• $\mathop {\downarrow }\nolimits i$ case. By VE $_{\mathop {\downarrow }\nolimits }$ , we may assume WLOG that $\kappa $ is free for i in $\phi $ .

  

Theorem A3.35 (Completeness in )

Where and :

1. a. If , then .

2. b. If , then .

Proof. For (a), suppose $\Gamma \nvdash \bot $ . By Lemma A3.24, we can extend $\Gamma $ to a Lindenbaum set $\Gamma ^+$ . By Lemma A3.34, iff $\mathop {@}\nolimits _{l_\Gamma }\phi \in \Gamma ^+$ , which holds (by Intro $_{\mathop {@}\nolimits }$ and Elim $_{\mathop {@}\nolimits }$ ) iff $\phi \in \Gamma ^+$ . Hence, . By Definition A3.32, $c_{l_\Gamma } \in V_\Gamma ({cl})$ since $\mathop {@}\nolimits _{l_\Gamma }{cl} \in \Gamma $ by Intro $_{\mathop {@}\nolimits }$ and Cl. Hence, $\Gamma $ is classically satisfiable.

For (b), suppose . Introduce a new interpretation nominal l to the language. By Proposition A2.17, . By (a), . Let be such that . By Lemma A3.18, where i is fresh, . By C2U, . By Gen $_{\mathop {@}\nolimits }$ (with $\mathop {@}\nolimits _{cl}$ ), Ref, and Red, . Hence, by Gen $_{\mathop {\downarrow }\nolimits }$ and Idle $_{\mathop {\downarrow }\nolimits }$ , . Thus, .

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 Completeness with propositional quantifiers

We now extend these results to languages with propositional quantifiers. In Section A4.1, we state the additional axioms and rules governing quantifiers. In Section A4.2, we revise the proof of completeness from Section A3.2. In Section A4.3, we consider how these results are affected when is introduced.

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. ¹⁷

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 }$ ):

Lemma A4.36 (Propositional relabeling)

If q is free for p in $\phi $ , then . Similarly for simultaneous substitution.

Theorem A4.37 (Soundness in )

Where and :

1. a. If , then .

2. b. If , then .

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 . ¹⁸ Instead, only a restricted form of Lemma A3.19 holds (fortunately, this suffices):

Table A7 Some useful theorems and derivable rules in .

Lemma A4.38 (Propositional substitution)

If and q is free for p in $\phi $ , then .

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”).

Definition A4.39 (Henkin set)

A set is Henkin if it is a maximal consistent set that is nominalized, witnesses $\neg \mathop {@}\nolimits $ s, and:

1. iii. $\Gamma ^+$ witnesses s: if , then there is a $p \in \textsf {Prop}^+$ not in $\phi $ such that $\phi [p^+/p] \in \Gamma ^+$ .

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 .

Lemma A4.40 (Henkin)

If is consistent, then there is a Henkin set where $\Gamma \mathrel {\subseteq } \Gamma ^+$ .

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,

Lemma A4.41 (Existence (revised))

Suppose . Then there is a $\Delta ' \in W_\Gamma $ such that $\phi \notin \Delta '$ .

Proof. As before, is guaranteed to be consistent and nominalized. Enumerate all sentences of the form $\neg \mathop {@}\nolimits _\iota \psi $ or of the form as . We define a sequence of formulas as before except the definition depends on the form of $\chi _{n+1}$ . If $\chi _{n+1} = \neg \mathop {@}\nolimits _\iota \psi $ , define $\delta _{n+1}$ as in Lemma A3.26. If , then define $\delta _{n+1} := \chi _{n+1} \mathbin {\rightarrow } \psi [p^+/q]$ , where $p^+$ is the first propositional variable such that . As before, it suffices to show that there always is such a $p^+$ . Suppose are defined but there is no $p^+$ meeting the above condition. Reasoning as before, this means that and for all $p^+$ . Once again, it must be that . Let p be fresh. By VE $_{\forall }$ , . By VDist, . By BF and Bool, . Since $\Delta $ witnesses s, there is a $p^+$ such that , contradicting the fact that , .

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).

Definition A4.42 (Canonical hyperconventions (revised))

Let $\left |{\kappa }\right |_1 \in \Gamma $ . Define the canonical $\kappa $ -hyperconvention $c_\kappa $ over $W_\Gamma $ as follows:

1. i. .

2. ii. .

3. iii. is defined as follows (regardless of whether $\mathop {@}\nolimits _\kappa {cl} \in \Gamma $ ):

   

The definition of $C_\iota $ is as before.

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 }$ .

Lemma A4.43 (Canonical hyperconventions are hyperconventions)

Let $\left |{\kappa }\right |_1 \in \Gamma $ .

1. a. If $\mathop {@}\nolimits _\kappa {cl} \in \Gamma $ and $[X]_\kappa \neq \emptyset $ , then $X \in \pi _{c_\kappa }$ .

2. b. $c_\kappa (p) \in \pi _{c_\kappa }$ .

3. c. for any .

Proof. For (a), let $\phi \in [X]_\kappa $ . By ClEx and C2U, . By Gen $_{\mathop {@}\nolimits }$ and Ref, . By U2C, . Thus, $\mathop {@}\nolimits _\kappa {\mathop {\textsf {E}}}\phi \in \Gamma $ . By BF $_{\mathop {@}\nolimits }^+$ , . By -witnessing, there is a $p^+ \in \textsf {Prop}^+$ such that $(p^+ =_\kappa \phi ) \in \Gamma $ . By Dist $_{\mathop {@}\nolimits }$ , $(\mathop {@}\nolimits _\kappa p^+ = \mathop {@}\nolimits _\kappa \phi ) \in \Gamma $ . By Corollary A3.27, $p^+ \in [X]_\kappa $ . Hence, $X \in \pi _{c_\kappa }$ .

For (b), by Intro. Since $\Gamma $ witnesses s, there is a $p^+ \in \textsf {Prop}^+$ such that . By Corollary A3.27, . Hence, $p^+ \in [c_\kappa (p)]_\kappa $ , i.e., $c_\kappa (p) \in \pi _{c_\kappa }$ .

For (c), we just show the -case. Let $X \in \pi _{c_\kappa }$ . Suppose first $\mathop {@}\nolimits _\kappa {cl} \in \Gamma $ . Then for some , $\phi \in [X]_\kappa $ , i.e., . Thus, by Lemma A3.29, . Suppose instead $\mathop {@}\nolimits _\kappa {cl}\notin \Gamma $ . So for some $p^+ \in \textsf {Prop}^+$ , $p^+ \in [X]_\kappa $ , i.e., . By Lemma A3.29, . By OpEx, BF $_{\mathop {@}\nolimits }^+$ , and Dist $_{\mathop {@}\nolimits }$ , . By witnessing s, there is a $q^+ \in \textsf {Prop}^+$ such that . Hence, .

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. We show $c_\kappa (\neg )(X) = \overline {X}$ for illustration. Suppose $p^+ \in [X]_\kappa $ . By Lemma A3.29 and Dist $_{\mathop {@}\nolimits }$ , . By maximal consistency, . Hence, $c_\kappa (\neg )(X) = \overline {X}$ by Definition A3.28.

Lemma A4.47 (Truth)

iff $\mathop {@}\nolimits _\kappa \phi \in \Delta $ .

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.

Lemma A4.48 (Closure for canonical classical convention)

Let $c_\kappa \in C_{cl}$ . Then for any and any $\mathcal {M}$ based on $\left \langle W_\Gamma ,{D_{\mathbb {C}}}_\Gamma ,{D_{\mathbb {P}}}_\Gamma \right \rangle $ .

Proof. Let $c_\kappa \in C_{cl}$ , let , and let $\mathcal {M} = \left \langle W_\Gamma ,{D_{\mathbb {C}}}_\Gamma ,{D_{\mathbb {P}}}_\Gamma ,V \right \rangle $ . Let be the free propositional variables in $\phi $ . By definition of ${D_{\mathbb {P}}}_\Gamma $ , there are some such that for all $c_\kappa \in {D_{\mathbb {H}}}_\Gamma $ . By Lemmas A4.36 and A4.47, . Hence, , and so .

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

Theorem A4.49 (Completeness in )

Where and :

1. a. If , then .

2. b. If , then .

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. ¹⁹ Over such classes, completeness can be restored.

A5 Conclusion

Hyperlogic is a hyperintensional system that is designed to regiment, and facilitate reasoning about, metalogical claims within the object language. This is achieved by introducing a multigrade entailment operator, propositional quantifiers, and modified hybrid operators into the language. To interpret these claims, we introduced hyperconventions, i.e., maximally specific interpretations, into points of evaluation. While one might suspect that the logic of hyperlogic is uninteresting, as we’ve seen, this suspicion is incorrect. We presented dual axiomatic systems for both classical and universal consequences in a number of fragments of hyperlogic and proved their soundness and completeness.

The minimal logic of hyperlogic explored in this paper is fairly weak and assumes next to nothing about the possible interpretations of the connectives. It also does not yet include hyperintensional operators like belief operators or counterfactuals. In Part B of this series, we begin to fill these gaps by exploring stronger logics that can be obtained by imposing various restrictions on the class of hypermodels and also by adding hyperintensional operators to the language.