A general framework for consistent logical reasoning in Wigner's friend scenarios: subjective perspectives of agents within a single quantum circuit

It is natural to expect a complete physical theory to have the ability to consistently model agents also as physical systems of the theory. In [Nat. Comms. 9, 3711 (2018)], Frauchiger and Renner (FR) claim to show that when agents model each other as quantum systems while reasoning about each other's knowledge in a certain Wigner's friend scenario, they arrive at a logical contradiction. In light of this, Renner often poses the challenge: provide a set of reasoning rules that can be used to program future quantum computers that may act as agents, which are (a) logically consistent (b) generalise to arbitrary Wigner's friend scenarios (c) efficiently programmable and (d) consistent with the temporal order of the protocol. Here we develop a general framework where we show that every logical Wigner's friend scenario (LWFS) can be mapped to a single temporally ordered quantum circuit, which allows agents in any LWFS to reason in a way that meets all four criteria of the challenge. Importantly, our framework achieves this general resolution without modifying classical logic or unitary quantum evolution or the Born rule, while allowing agents' perspectives to be fundamentally subjective. We analyse the FR protocol in detail, showing how the apparent paradox is resolved there. We show that apparent logical contradictions in any LWFS only arise when ignoring the choice of Heisenberg cut in scenarios where this choice does matter, and taking this dependence into account will always resolve the apparent paradox. Our results establish that universal applicability of quantum theory does not pose any threat to multi-agent logical reasoning and we discuss the implications of these results for FR's no-go theorem. Moreover, our formalism suggests the possibility of a truly relational and operational description of Wigner's friend scenarios that is consistent with quantum theory as well as probability theory applied to measurement outcomes.

V. Vilasini
Institute for Theoretical Physics, ETH Zurich, 8093 Zürich, Switzerland
Mischa P. Woods
Institute for Theoretical Physics, ETH Zurich, 8093 Zürich, Switzerland

§ INTRODUCTION

When we apply quantum theory to describe the world around us, we often give a preferred role to “agents” or “observers” who we regard as macroscopic, classical systems which are outside the full purview of the theory.
Quantum theory provides a very accurate description of microscopic phenomena and there continue to be experimental efforts towards observing quantum phenomena in larger and more complex systems, both for the purpose of quantum technologies and tests of fundamental physics. In light of this, it is natural to consider the (theoretical) consequences of the universal applicability of quantum theory, in particular where agents can be modelled as quantum systems and subject to quantum mechanical laws, noting that a future quantum computer could in-principle play the role of an agent.

Wigner was among the first to point out that extending quantum theory in this manner can have puzzling consequences [1]. To this effect, Wigner proposed a thought experiment where he considered an agent (the friend) who measures a quantum system in their lab, while another agent (Wigner) models the friend's lab as a closed quantum system. The crucial feature at play in a Wigner's friend scenario is the tension between two types of quantum evolutions. On the one hand, from the perspective of the friend who performs the measurement, the measurement induces an irreversible “collapse” and produces a definite classical measurement outcome that can be recorded on a database (their memory). On the other hand, Wigner regards the friend's lab (which includes their system and memory) as a closed quantum system, which would evolve unitarily, according to the laws of quantum theory. He would therefore describe the friend's measurement as a unitary evolution of their lab that does not generate any classical records.

How do we reconcile these two very different accounts of a quantum measurement which provide apparently conflicting views regarding the status of a measurement outcome? This question is at the heart of the infamous quantum measurement problem.

Frauchiger and Renner in [2] (which we will call FR for short) considered a more sophisticated Wigner's friend setup with two friends and two Wigners, where they claim to show that when agents who can model each other's labs as quantum systems reason about each other's knowledge using simple rules of classical logic, they arrive at an apparent logical contradiction or a paradox. In FR, the main claimed result is a no-go theorem that three seemingly reasonable assumptions which they call $Q$, $C$ and $S$ cannot be simultaneously satisfied in a physical theory that can consistently describe the predictions of a thought experiment that they propose. The assumption $Q$ relates to the universal applicability of quantum theory while $C$ and $S$ can be thought of as basic rules of logical reasoning (these assumptions are reviewed in <ref>).
A conclusion suggested by this is that universal applicability of quantum theory is at conflict with the axioms of classical (modal) logic [3].

Taken at face value, this appears to be a grave problem. With global efforts towards observing quantum effects in meso and macroscopic systems, it is not entirely unreasonable to fathom a situation where a quantum computer plays the role of a reasoning agent— performs measurements on other quantum systems, and based on the observed outcome, draws inferences about past and future measurement outcomes obtained by other quantum computers. How then should such quantum agents reason about each other's knowledge without reaching paradoxical conclusions? What are the concrete reasoning rules for such agents that are compatible with universal quantum theory? Does the FR theorem require us to abandon our classical logical intuitions and if so, how far must we venture from these intuitions? These questions inspired by the FR claimed no-go theorem are relevant for a deeper fundamental understanding of the role of agents and measurements in quantum theory, as well as for gauging the implications for future quantum technologies, and will be the subject of the current paper.

In light of the Frauchiger-Renner paper, Renner often poses the following challenge.[An initial version of this challenge was posted by Renner in the comments section of Scott Aaronson's blog post [4], and more detailed versions are often quoted in Renner's talks on the topic of Wigner's friend. The version quoted here is what we understand to be the main criteria of this challenge.] Provide a set of reasoning rules that can be used to program hypothetical quantum computers that may act as reasoning agents, which are (a) logically consistent (b) generalise to arbitrary quantum protocols (c) efficiently programmable and (d) consistent with the temporal order of the protocol. Conditions (a) and (b) require that these rules must not only avoid the paradox that arises in the particular set-up that FR considered, but also generalise to arbitrary quantum mechanical (thought-)experiments where reasoning agents can model each other as quantum systems. Condition (c) requires that the rules should be computationally efficient, for instance the computer should not have to check an arbitrarily large list of conditions at every step of the reasoning.  Finally, condition (d) requires that in order for an agent to reason about the outcome of a measurement performed at time $t$, they must not have to consider operations performed at later times $t'>t$.
This also relates to computational efficiency, if a computer has to take into account all possible future operations on itself and other computers before reasoning about the present, then this would certainly not be efficient.

There are several previous works discussing and analysing the FR apparent paradox, that suggest possible directions or partial solutions to Renner's challenge. These works can be divided into three broad categories. A first set of works [5, 6, 7, 8, 9] provide fundamental reasons for rejecting one of the assumptions of the FR no-go theorem. Note that this is a natural response to any no-go theorem which establishes the impossibility of satisfying a set of assumptions, as it forces us to identify a subset of the assumptions that we are willing to give up. There are then a second set of papers [3, 10, 11] which (possibly after noting inexplicit assumptions beyond $Q$, $C$ and $S$) conclude that there is indeed a paradox in the FR thought experiment. Some of these papers go on to suggest possible resolutions of the paradox by proposing additional reasoning rules. Finally, a third  set of works [4, 12, 13, 14, 15, 16, 17] question the correctness of the theorem itself. They have argued that the reasoning employed in the original paper includes additional implicit assumptions, one or more of which are not valid, and conclude that there is no real paradox as FR claim.[The cited works are only representatives of the enormous volume of research generated by the FR paper, for a detailed discussion of the current state of the debate, as well as further references, we refer the reader to [18].]

Among the first set of works, [5, 6, 7, 8] argue that it is the assumption $Q$ (regarding the universal applicability of quantum theory) that must be rejected in light of FR's claimed no-go result, because any physical measurement model induces decoherence. Interpretations of quantum mechanics such as collapse theories and hidden variable theories are likely to subscribe to this point of view. The assumption $C$ of the FR theorem relates to the agreement between the perspectives of different agents. Frameworks that adopt a fundamentally relational point of view on physics have argued that this is the assumption that must be rejected. This argument is elucidated by the distinguishing between stable and relative facts [9].

Among the second set of works, one of the earliest analyses of the logical structure of the FR thought experiment was carried out in [3]. They note two additional assumptions, $U$ and $D$ which are needed to establish the FR no-go result, but were not stated explicitly before. $U$ allows agents to model the measurements of other agents as unitary evolutions of their labs while $D$ is the distributive axiom of classical logic. They claim to prove a refined version of the FR theorem to the effect that $Q$, $U$, $C$, $D$ and $S$ cannot be simultaneously satisfied in a physical theory that consistently describes the FR thought experiment, and go on to discuss possible ways to modify logic such that there is no contradiction, but no concrete model for resolving the paradox in quantum theory was proposed here.

More recently, [10, 11] have proposed concrete reasoning principles or rules which could be added to quantum theory in order to avoid FR type paradoxes when the theory is applied to agents (typically these are interpreted as a modification to either the assumption $Q$ or $C$ of the FR theorem). While these works meet condition (a) and possibly also condition (b) of Renner's challenge, namely logical consistency and generality, the status of conditions (c) and (d), which relate to computational efficiency and causality remain unclear. In particular, [11] proposes a parsing rule for determining when an operation performed by an agent can be regarded as a measurement whose outcome can be reasoned about. While this rule is sufficient to avoid logical paradoxes, it appears that this rule must also consider the operations performed by future agents in order to determine whether a given operation at time $t$ can count as a measurement and therefore it is unclear whether condition (d) is satisfied. As we noted before, the validity of condition (c) is related to that of (d) and therefore its validity is also a priori unclear. Another recent proposal [19] for resolving the apparent FR paradox suggests that agents whose memories are subject to incompatible measurements cannot make reliable predictions about events that take place after this measurement. Due to similar reasons as above, the temporal consistency and efficiency aspects of this resolution are unclear.

To the best of our knowledge, a concrete resolution that is proven to meet all four conditions is unknown. In particular, there are no concrete examples of FR-type (apparent) logical paradoxes in quantum theory other than the original FR scenario. Therefore, in order to fully justify condition (b), one also requires a constructive definition of what constitutes a general, logical Wigner's friend scenario. Furthermore while these additional reasoning rules are sufficient for logical consistency, an interesting question is whether they are also necessary or can a weaker set of reasoning rules already resolve the apparent paradox.

Finally, a third set of works [4, 12, 13, 14, 15, 16, 17] object to FR's conclusion by arguing that there is no real paradox in the FR scenario. They argue that the derivation of the contradiction involves unformalised assumptions that allow FR to combine statements arising from incompatible measurement contexts, and that such combinations are not valid within quantum theory.
In particular, such arguments were made in a popular blog post by Scott Aaronson [4] where he argues that the statements made by all agents are not valid at the end of the experiment as the brains of the friends get Hadamarded in the process, and that the FR reasoning involves an additional unformalised assumption relating to the combination of statements from incompatible measurement contexts. Renner responded to this post noting that the agents in their thought experiment only think and reason before any Hadamarding of their brains and their paradox does not require the validity of the statements after the Hadamarding, and he posed an initial version of the above mentioned challenge in response. He interpretted Aaronson's objection as giving up the assumption about the universal applicability of quantum theory (i.e., either $Q$ or $U$), in response to their no-go theorem (also see [18] for a justification of this interpretation). At the end of this interesting discussion, the formalisation of what Aaronson refers to as FR's “unformalised assumption” and its role in the resolution of the apparent paradox still appear to remain open.

Further, the FR analysis involves a post-selection on the two “Wigners” obtaining a certain outcome, and the reasoning of all agents is only considered in the run of the experiment where this post-selection succeeds.
Araujo [12] argues that some of their reasoning steps make certain additional assumptions about whether or not the wavefunction is collapsed by the friends' measurements, which affects the post-selection success probability, and suggests that taking this into account appears to resolve the apparent paradox. Another work in this category is that of Healey [14], where a heuristic assumption called intervention insensitivity is identified. [14] argues that this is implicitly assumed in FR's reasoning but fails to hold in their set-up when accounting for the necessary post-selections.

While all these works provide significant insights into the assumptions and possible resolution of the apparent FR paradox, a general framework that provably meets all the conditions of Renner's challenge while allowing for a concrete formalisation of these unstated assumptions and objections in an interpretation-independent manner is still lacking. Such a framework would also clarify the status of the FR no-go theorem (and any potential generalisations) in light of the objections raised in the third set of papers.
Here we propose such a concrete mathematical framework. Importantly, we prove that our framework meets the conditions of Renner's challenge without modifying quantum theory or classical logic. It therefore allows us to demonstrate that universal applicability of unitary quantum theory is not at conflict with classical logic applied to outcomes of performed measurements, as long as agents make explicit all the assumptions that go into the reasoning (such as the choices of the Heisenberg cuts[The Heisenberg cut of a hypothetical experiment distinguishes between the set of systems to which a full quantum mechanical treatment may be applied (inside the cut), and those which are regarded as macroscopic, classical systems (outside the cut). Note that in a Wigner's friend scenario, different agents in general have different Heisenberg cuts. In particular, each agent would regard their own memory (where they store the classical outcome of their measurement) as a system that is outside their own Heisenberg cut as it only stores classical values from their perspective, but the memory of one agent (e.g., the friend) may be inside another agents' (e.g., Wigner) Heisenberg cut.] for different agents).

Importantly, this framework allows for different agents to make fundamentally subjective statements while reasoning about each others' knowledge of measurement outcomes using a single temporally-ordered quantum circuit, and without running into logical contradictions. This demonstrates that even in the lack of an objective and agent-independent notion of measurement events, users of quantum theory, in any measurement scenario, can reason about each others' knowledge in an efficient, logically and temporally consistent manner. This makes our resolution fundamentally distinct and more general than previous “resolutions” that simply require an objective fixing of the Heisenberg cut for all agents or declare that measurements must not be modelled unitarily.

Our framework also demonstrates that the resolution of the apparent FR paradox does not necessarily invoke inherently quantum features such as incompatible measurements, wavefunction collapse, Bell non-locality or contextual correlations as suggested by previous works. Instead, the solution can already be understood in terms of classical probability theory and rules for conditional probabilities. We summarise the main contributions of this paper below.

Summary of the paper

* In <ref>, we provide a more concrete overview of the Wigner's friend scenario and then review the assumptions $Q$, $C$ and $S$ of the claimed Frauchiger-Renner no-go theorem as well as the additional assumptions $U$ and $D$ noted by Nurgalieva and del Rio [3].

* Then, in <ref>, we proceed to set out our general framework which has the features outlined above. We do so by first defining a general form of logical Wigner's friend scenarios (of which the FR scenario is a special case) and show that every such scenario can be mapped to a single standard quantum circuit (the augmented circuit) from which the predictions of the original Wigner's friend scenario for all agents can be derived.

* Within this framework, we define more formal versions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$, $\mathbf{D}$, and $\mathbf{S}$ of the FR assumptions $Q$, $U$, $C$, $D$ and $S$. We then prove the completeness, logical and temporal consistency of the framework and show that agents can simultaneously reason using the assumptions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$, $\mathbf{D}$, and $\mathbf{S}$ without running into contradictions. This establishes that our framework meets all the conditions of Renner's challenge, without modifying the reasoning rules of classical logic or the unitary quantum evolution or the Born rule.

* Having established the consistency of our framework, we show that in order to recover an apparent paradox in any LWFS, it is necessary to impose an additional assumption $\mathbf{I}$ in a situation where the assumption actually fails to hold. $\mathbf{I}$ is effectively the assumption that predictions in an LWFS are independent of the choice of Heisenberg cut.
The implications for the claimed FR no-go theorem then depend on the relations between our assumptions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$, $\mathbf{D}$, $\mathbf{S}$, $\mathbf{I}$ and FR's (and [3]'s) assumptions $Q$, $U$, $C$, $D$, $S$, and we discuss this in section <ref>.

* We then apply our general framework to analyse in detail, both the entanglement version (in <ref>) as well as the original prepare and measure version (in <ref>) of the FR thought experiment showing that in both cases our framework resolves the apparent paradox without giving up any rule of classical logic or the assumption regarding the universal applicability of quantum theory.

* We show that the FR protocol does indeed satisfy all five assumptions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$, $\mathbf{D}$ and $\mathbf{S}$ but violates the assumption $\mathbf{I}$ and does not lead to any inconsistencies within our framework.
Our results imply that the FR apparent paradox and any apparent logical Wigner's Friend paradox can be resolved without rejecting the universal validity of quantum theory or classical logic, but only by acknowledging that predictions in Wigner's friend scenarios do depend on the choice of Heisenberg cut.
We argue that this dependence is unsurprising although important to keep track of, and show that the independence assumption $\mathbf{I}$ also fails in Wigner's original thought-experiment (as Wigner himself pointed out). We also provide an example of a simple classical protocol (in <ref>) where making a mathematically analogous assumption would lead to an apparent logical contradiction.

* In <ref>, we discuss the connections between FR's claimed no-go theorem and Hardy's logical proof of Bell non-locality. In <ref> we provide a more unified view of the relations between our framework and the three categories of previous works outlined above, and we also illustrate how different interpretations of quantum theory might apply our framework (which highlights its interpretation-independence).

We conclude by outlining the salient features of our framework, possible interpretations of FR's claimed theorem in light of our results, along with a discussion of open questions and future directions stemming from our work.

What can be skipped in the first read We acknowledge that this is a rather long and detailed paper, as it aims to formally address and unify many different perspectives and arguments on this topic. However, many of the details could be skipped in a first read of this paper and may not be of interest to every reader. For readers already familiar with the set-up of Wigner's friend scenarios and the FR assumptions, but who are interested in how our framework meets Renner's challenge and guarantees consistency of quantum theory with classical logic, <ref> covers this aspect. For those interested in the specific case of the FR protocol with a step-by-step analysis of the paradox resolution there, we refer to <ref> (for the entanglement version) and <ref> (for the prepare and measure version). For those interested in a detailed discussion on the relation(s) to previous works, interpretations of the FR theorem, and the outlook of our work for other philosophical debates and open questions, we refer to <ref> and <ref>.

§ WIGNER'S FRIEND SCENARIOS: A TALE OF TWO EVOLUTIONS

Suppose an agent, Alice, measures a quantum system $\Ss$ prepared in the state $\ket{\psi}=\alpha\ket{0}_\Ss+\beta\ket{1}_\Ss$ in the computational basis and obtains a classical measurement outcome $a\in \{0,1\}$. She stores the result of this outcome in her memory $\A$, which was initialised to the state $\ket{0}_\A$. In the case she obtains $a=0$, she describes the evolution of her lab as $\ket{\psi}_\Ss\ket{0}_\A\mapsto \ket{0}_\Ss\ket{0}_\A$ and in the case she obtains $a=1$, she describes the evolution of her lab as $\ket{\psi}_\Ss\ket{0}_\A\mapsto \ket{1}_\Ss\ket{1}_\A$. In case she made a measurement and then forgot about the outcome, she would tend to describe the evolution as

\begin{align}
\label{eq:M_mixture}
\begin{split}
M^{\A}_{mixture}&\big(\proj{\psi}_{\Ss}\otimes \proj{0}_\A\big)=\\
& |\alpha|^2 \ketbra{00}{00}_{\Ss\A}+|\beta|^2 \ketbra{11}{11}_{\Ss\A}
\end{split}
\end{align}

Another agent Bob who treats Alice's memory $A$ as a classical system (in the computational basis) and is aware that she performed a measurement but not of the measurement outcome, would also tend to describe the evolution as above. This is the case in the standard use of quantum theory, where we apply the theory to systems under study but treat all agents (and in particular, their memories) as classical systems. Note that this is also the evolution one would ascribe to the measurement in a theory with decoherence, where $\Ss$ and $\A$ become entangled with other systems (the measuring apparatus or the environment), such that the reduced state on $\Ss\A$ is the above mixed state.

On the other hand, if we consider a more universal use of quantum theory where agents model each other's labs as closed quantum systems, we can have the following scenario.
If an agent Bob situated outside Alice's lab, models Alice's lab (consisting of her system $\Ss$ and memory $\A$) as a closed quantum system, he would describe Alice's computational basis measurement as a unitary evolution

\begin{equation}
\label{eq:M_unitary}
M^{\A}_{unitary}(\ket{\psi}_{\Ss}\otimes \ket{0}_\A)= \alpha \ket{00}_{\Ss\A}+\beta \ket{11}_{\Ss\A}
\end{equation}

We will refer to such a Bob as a super-agent. Bob can perform further measurements on $\Ss\A$, he will however model his own measurements in an irreversible manner, even though a further sup(super)-agent, Charlie situated outside both Alice and Bob's lab would model these labs as evolving unitarily, if they believe in the universal applicability of quantum theory. Notice that when the memory is initialised to $\ket{0}_\A$, the unitary perspective $M^\A_{unitary}$ of the computational basis measurement on $\Ss$ is simply a CNOT with $\Ss$ as control and $\A$ as target.

In the standard use of quantum theory where all agents are treated classically, all agents unaware of the outcome of Alice's measurement would associate the post-measurement state given by the evolution $M^{\A}_{mixture}$ with her measurement. On the other hand, in the universal use of quantum theory there is an ambiguity on how to model the post-measurement state of Alice's lab, as an agent who is unaware of Alice's outcome may either use the evolution $M^{\A}_{mixture}$ or the evolution $M^{\A}_{unitary}$. These two evolutions lead to observably different predictions for the probabilities of subsequent measurements on $\Ss\A$. Note that in both the standard and universal use of quantum theory, any agent who knows the outcome of Alice (say to be $a=0$) would agree on the post-measurement state of Alice (in this case $\ket{00}_{\Ss\A}$). Thus the ambiguity in how a measurement is modelled only arises in the universal use of quantum theory where an agent is unaware of the outcome of the said measurement. We note that the memory system $\A$ essentially plays the role of the rest of Alice's lab, excluding the system $\Ss$ she measures i.e., $\Ss\A$ constitutes a simplistic model of Alice's lab in discussions relevant to Wigner's friend type thought experiments.

The above is a version of Wigner's original thought-experiment [1] with Alice playing the role of the friend and Bob playing the role of Wigner. FR's paper [2] elevates this ambiguity into an apparent logical paradox. They propose a no-go theorem which claims that any physical theory satisfying a set of assumptions $Q$, $C$ and $S$ would yield contradictory results when applied to their thought experiment. We review these assumptions in the following section.

§ THE FRAUCHIGER-RENNER NO-GO THEOREM AND APPARENT PARADOX

Here we review the assumptions $Q$, $C$ and $S$ of the FR claimed no-go theorem, as well as the additional assumptions $U$ and $D$ that are also relevant to the FR analysis, as pointed out in [3]. The FR protocol and formal statement of their no-go theorem will be reviewed in <ref>.

Assumption ($Q$): it asserts that an agent can be certain that a given proposition holds whenever the quantum-mechanical Born rule assigns probability 1 to it. Specifically:

Suppose that agent A has established that

Statement A$^\textup{(i)}$: “System $\Ss$ is in state $\ket{\psi}_\Ss$ at time $t_0$.”

Suppose furthermore that agent A knows that

Statement A$^\textup{(ii)}$: “The value $x$ is obtained by a measurement of $\Ss$ w.r.t. the family $\{\pi_x^{t_0}\}_{x\in\chi}$ of Heisenberg operators relative to time $t_0$, which is completed at time $t$.”

If $\braket{\psi|\pi_\xi^{t_0}|\psi}=1$ for some $\xi\in\chi$, then agent A can conclude that

Statement A$^\textup{(iii)}$: “I am certain that $x=\xi$ at time $t$.”

Assumption ($C$):
It asserts that one agent can inherit the knowledge of another agent who uses the same theory as them to arrive at their conclusions.

Suppose that agent A has established that

Statement A$^\textup{(i)}$: “I am certain that agent A', upon reasoning within the same theory as the one I am using, is certain that $x=\xi$ at time $t$”

Then agent A can conclude that

Statement A$^\textup{(ii)}$: “I am certain that $x =\xi$ at time $t$”.

Assumption ($S$): from the viewpoint of an agent who carries out a particular measurement, this measurement has one single outcome. Specifically:

Suppose that agent A has established that

Statement A$^\textup{(i)}$: “I am certain that $x=\xi$ at time $t$”

The agent A must necessarily deny that

Statement A$^\textup{(ii)}$: “I am certain that $x\neq \xi$ at time $t$”.

Note that a violation of $S$ can itself be interpreted as a logical paradox, as it would imply that the outcome $x$ is both $\xi$ and not $\xi$ with certainty.

In [3], the authors also identify additional assumption $U$ (unitarity) that FR use (as part of $Q$) but did not explicitly state in their set of assumptions.

Assumption ($U$):

An agent $\A$ can model measurements performed by

any other agent $\B$ as reversible unitary evolutions
in $\B$'s lab.

Furthermore they also note that the FR reasoning involves another basic rule of classical logical inference namely the distributive axiom.

Assumption ($D$):

If an agent $\A$ knows a statement $s_1$ and also knows that $s_1$ implies another statement $s_2$ then agent $\A$ can conclude that they know $s_2$.

They formulate this in terms of a knowledge operator which formally keeps track of which agent knows which statement [3]. We will also introduce said notation later. Assumption $D$ is implicitly used in FR when the statements $s_1$ and $s_2$ correspond to measurement outcomes, e.g. $s_1$ could be “I am certain that $x =\xi$ at time $t$', $s_2$ could be “$x'=\xi'$ at time $t'$”. Then if agent $\A$ also knowns “If I am certain that $x =\xi$ at time $t$, then I am certain that $x'=\xi'$ at time $t'$”,  they would use $D$ to conclude that agent $A$ is certain of the  statement “I know that $x' =\xi'$ at time $t'$”.

As already mentioned, the assumptions $U$ and $D$ were implicitly assumed in FR. In [3], a refined version of the claimed FR theorem is claimed which makes explicit these additional assumptions. It thus has the implication that the assumptions $Q$, $U$, $C$, $D$ and $S$ cannot be simultaneously satisfied in the protocol proposed by FR. We note that this result is proven by formalising these assumptions using the Kripke structure of epistemic modal logic (which is the branch of logic that refers to knowledge of agents) and we refer the reader to [3] for the formal statement of this theorem in this mathematical language. We will not review the full modal logic framework here but will refer to aspects of it wherever necessary.

At a broad level, the proof proceeds by considering the FR thought experiment where agents reason about each other's knowledge using assumptions $Q$, $U$, $C$ and $D$ and claims to show that such agents would always arrive at a violation of $S$, which as we have explained above can be interpreted as a paradox.

§ A GENERAL RESOLUTION TO LOGICAL WIGNER'S FRIEND PARADOXES

[->] (6,-8)–(9,-8); at (9.5,-8) time;

[ultra thick,decorate,
decoration = calligraphic brace] (-0.2,-2.2)–(-0.2,0.2); at (-1,-1) $\rho_{\Ss_1,\ldots,\Ss_m}$; at (-0.5,-3) $\ket{0}_{\M_1}$;  at (-0.5,-4) $\ket{0}_{\M_2}$;  at (-0.5,-5) $\ket{0}_{\M_3}$;  at (-0.5,-7) $\ket{0}_{\M_N}$;

(0,0)–(1,0); at (0.5,0.2) $\Ss_1$; (0,-2)–(1,-2); at (0.5,-1.8) $\Ss_m$; at (0.5,-1) $\cdot$; at (0.5,-1.3) $\cdot$; at (0.5,-0.7) $\cdot$; (1,0.3) rectangle node$\mathcal{M}^{\A_1}$ (2,-3.2);
(0,-3)–(1,-3); at (0.5,-2.8) $\M_1$;

(2,0)–(3,0); at (2.5,0.2) $\Ss_1$; (2,-2)–(3,-2); at (2.5,-1.8) $\Ss_m$; at (2.5,-1) $\cdot$; at (2.5,-1.3) $\cdot$;
(2,-3)–(3,-3); at (2.5,-2.8) $\M_1$; (3,0.3) rectangle node$\mathcal{E}^1$ (4,-3.2);

(4,0)–(5,0); at (4.5,0.2) $\Ss_1$; (4,-2)–(5,-2); at (4.5,-1.8) $\Ss_m$; at (4.5,-1) $\cdot$; at (4.5,-1.3) $\cdot$;
at (4.5,-0.7) $\cdot$; (4,-3)–(5,-3); at (4.5,-2.8) $\M_1$;
(0,-4)–(5,-4); at (2.5,-3.8) $\M_2$; (5,0.3) rectangle node$\mathcal{M}^{\A_2}$ (6,-4.2);

(6,0)–(7,0); at (6.5,0.2) $\Ss_1$; (6,-2)–(7,-2); at (6.5,-1.8) $\Ss_m$; at (6.5,-1) $\cdot$; at (6.5,-1.3) $\cdot$; at (6.5,-0.7) $\cdot$;
(6,-3)–(7,-3); at (6.5,-2.8) $\M_1$;  (6,-4)–(7,-4); at (6.5,-3.8) $\M_2$; (7,0.3) rectangle node$\mathcal{E}^2$ (8,-4.2);

(8,0)–(9,0); at (8.5,0.2) $\Ss_1$; (8,-2)–(9,-2); at (8.5,-1.8) $\Ss_m$; at (8.5,-1) $\cdot$; at (8.5,-1.3) $\cdot$; at (8.5,-0.7) $\cdot$;
(8,-3)–(9,-3); at (8.5,-2.8) $\M_1$;  (8,-4)–(9,-4); at (8.5,-3.8) $\M_2$; (0,-5)–(9,-5);at (4.5,-4.8) $\M_3$;

(11,0)–(12,0); at (11.5,0.2) $\Ss_1$; (11,-2)–(12,-2); at (11.5,-1.8) $\Ss_m$; at (11.5,-1) $\cdot$; at (11.5,-1.3) $\cdot$; at (11.5,-0.7) $\cdot$;
(11,-3)–(12,-3); at (11.5,-2.8) $\M_1$;  (11,-4)–(12,-4); at (11.5,-3.8) $\M_2$; (11,-5)–(12,-5); at (11.5,-4.8) $\M_3$;

at (10,-3.5) $\dots$;

at (0.5,-6) $\cdot$; at (0.5,-6.3) $\cdot$; at (0.5,-5.7) $\cdot$;
(0,-7)–(12,-7); at (5.5,-6.8) $\M_N$;  at (11.5,-6) $\cdot$; at (11.5,-6.3) $\cdot$; at (11.5,-5.7) $\cdot$;
(12,0.3) rectangle node$\mathcal{M}^{\A_N}$(13,-7.3);

(13,0)–(14,0); at (13.5,0.2) $\Ss_1$; (13,-2)–(14,-2); at (13.5,-1.8) $\Ss_m$; at (13.5,-1) $\cdot$; at (13.5,-1.3) $\cdot$; at (13.5,-0.7) $\cdot$;
(13,-3)–(14,-3); at (13.5,-2.8) $\M_1$;  (13,-4)–(14,-4); at (13.5,-3.8) $\M_2$; (13,-5)–(14,-5); at (13.5,-4.8) $\M_3$;
at (13.5,-6) $\cdot$; at (13.5,-6.3) $\cdot$; at (13.5,-5.7) $\cdot$; (13,-7)–(14,-7); at (13.5,-6.8) $\M_N$;  (14,0.3) rectangle node$\mathcal{E}^N$(15,-7.3);

Circuit illustrating the general form of a LWFS involving $N$ agents and $m$ systems described in the main text. All agents agree on the initial state $\rho_{\Ss_1,\ldots,\Ss_m}$ of the systems and initialise their memories to $\ket{0}$. Each agent $\A_i$ performs a measurement on some subset of the systems and on a subset of the memories of all agents who acted before, and they store the outcome of the measurement in their own memory $\M_i$. After the measurement, each agent may perform a fixed transformation $\mathcal{E}^i$ (that is previously agreed upon by all agents) before the next agent measures. However, the agents need not necessarily agree on how each measurement is modelled, depending on their perspective some agents may describe a measurement as a purely unitary evolution as in <ref> while others may describe the same measurement as a decoherent process by assigning projectors as in <ref>.

Having motivated the assumptions of the FR scenario, in this section, we develop a framework which allows agents in any such logical Wigner's friend protocol to consistently reason within a single quantum circuit that we call the augmented circuit, while assuming the universal validity of quantum theory as well as the validity of classical logic applied to performed measurement outcomes. In particular, this framework resolves the apparent paradox of FR (we discuss the implications for the validity of FR claimed theorem in section <ref>).
The results of this section are general and apply to arbitrary Wigner's friend scenarios. For completeness, we also apply this framework to analyse the original FR protocol in detail in <ref> to highlight precisely how it resolves the original (apparent) paradox. We first develop the framework, and then formulate rigorous versions of the FR assumptions here before proving the completeness and consistency of our framework.

§.§ Mapping a Wigner's friend scenario to a single quantum circuit

Before we formally consider logical reasoning in Wigner's friend scenarios, it is useful to state the following definition of what we mean by predictions, logical predictions and logical statements associated with a prediction.

Given any quantum protocol involving $N$ measurements $\mathcal{M}^{\A_1}$,...,$\mathcal{M}^{\A_N}$ with associated measurement outcomes $a_1$,...,$a_N$, we define a prediction to be the probability $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q})$ of obtaining outcomes $a_{j_1}$,...,$a_{j_p}$ for a subset $\mathcal{M}^{\A_{j_1}}$,...,$\mathcal{M}^{\A_{j_p}}$ of the measurements, given that the outcomes $a_{l_1}$,...,$a_{l_q}$ are obtained for a disjoint subset $\mathcal{M}^{\A_{l_1}}$,...,$\mathcal{M}^{\A_{l_q}}$ of the measurements. Here $p\in\{1,2,...,N\}$ and $q\in \{0,1,...,N-1\}$, where $q=0$ denotes the case where the set of outcomes being conditioned on is empty.

A logical prediction is a prediction $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q})$ taking values in $\{0,1\}$. Each logical prediction is associated with a corresponding logical statement (that could be made by any agent using that prediction). The logical predictions $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q})=0$ and $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q})=1$  are associated with the following statements respectively

Statement $\textup{S}^0$: “If the outcomes $a_{l_1},...,a_{l_q}$ are obtained in the measurements of the agents $\A_{l_1},...\A_{l_q}$, then it is certain that the outcomes $a_{j_1},...a_{j_p}$ cannot be obtained in the measurements of the agents $\A_{j_1},...\A_{j_p}$.”

Statement $\textup{S}^1$:  “If the outcomes $a_{l_1},...,a_{l_q}$ are obtained in the measurements of the agents $\A_{l_1},...\A_{l_q}$, then it is certain that the outcomes $a_{j_1},...a_{j_p}$ are obtained in the measurements of the agents $\A_{j_1},...\A_{j_p}$.”

In the case that $q=0$, these become definitive statements, i.e. the statements start with “it is certain that...” with the previous part of the statement starting with “If...” omitted.

We now proceed with setting out the general form of a logical Wigner's friend scenario (LWFS), of which the FR scenario is a special case, and we will specify how predictions are calculated here. Broadly speaking, a LWFS corresponds to any quantum mechanical (thought-)experiment that consists of a set of agents, each performing a measurement on a set of systems and reasoning about each others' knowledge of measurement outcomes, while modelling each other's labs as quantum systems. Agents in an LWFS apply the Born rule to evaluate quantum mechanical probabilities, and can in principle model the evolution of other agents' laboratories as unitary evolutions. In specific LWFS, such as the FR scenario one may wish to consider specific reasoning rules such as $C$, $D$ and $S$. We now set out the notation needed to formally define a LWFS.

Suppose we have a set of $N$ agents $\mathtt{A}=\{\A_1,\ldots,\A_N\}$ and a set of $m$ systems $\mathtt{S}=\{\Ss_1,\ldots,\Ss_m\}$ under study and a set $\mathtt{M}:=\{\M_1,\ldots,\M_N\}$ of systems, one for each agent $\A_i$ which models their memory where they store the outcomes of measurements that they perform. In this paper, $N$ and $m$ are both natural numbers $\geq 1$.
For simplicity but without loss of generality, we take the lab of each agent $\A_i$ to consist of the system $\mathtt{S}_i$ that they measure, along with their memory $\M_i$.
Each agent $\A_i\in \mathtt{A}$ performs a measurement $\mathcal{M}^{\A_i}$ on some subset $\mathtt{S}_i\subseteq \mathtt{S}\cup \mathtt{M} \backslash \{\M_i\}$ of systems, which can include the memories of other agents, and stores the outcome of the measurement in their memory $\M_i$.[The memory $\M_i$ of an agent $\A_i$ is chosen to be a system of at least the same dimension as the system $\mathtt{S}_i$ that the agent $\A_i$ measures.] Note that $\mathtt{S}_i$ is a subset of systems and memories of other agents, which allows each agent to possibly act as a super-agent to any subset of the other agents by measuring their memories. We have no loss of generality in assuming that each agent performs one measurement, because any scenario where one agent performs multiple measurements can be bought to this form by modelling them as multiple agents, each performing one measurement.

Further, also without loss of generality, we can assume that each agent $\A_i$ acts at a distinct time step $t^i$ with $t^i<t^j$ for $i<j$ and that each measurement $\mathcal{M}^{\A_i}$ acts on the whole set $\mathtt{S}$ of systems and the set of all memories $\M_1,\ldots,\M_{i-1}$ of previous agents (since any operation on a subset $\mathtt{S}_i$ of systems can be trivially enlarged into an operation on all systems by appending the identity on the complementary set of systems). Agent $\A_i$ may also perform certain fixed transformations (corresponding to quantum channel $\mathcal{E}^i$ on $\mathtt{S}\cup \mathtt{M}$) in between time steps $t_i$ and $t_{i+1}$, for instance, agent $\A_1$ may measure the system $\Ss_1\in \mathtt{S}$ and  depending on their measurement outcome, could perform a different transformation on some initial state of $\Ss_2$ which they send to agent $\A_2$ who could then measure $\Ss_2$.

The circuit of <ref> illustrates this general form of a LWFS that we consider, where $\{\mathcal{E}^i\}_{i=1}^N$ are fixed transformations that all agents agree on as part of the protocol while $\{\mathcal{M}^{\A_i}\}_{i=1}^N$ denote the measurements, one for each agent, which agents could model as unitary evolutions or as yielding particular classical outcomes, depending on whose perspective they are reasoning from.

More specifically, suppose that an agent $\A_i$ measures a subset $\mathtt{S}_i$ of the systems through a measurement $\mathcal{M}^{\A_i}$. Let $a_i$ be the measurement outcome, which takes values in the set $\mathtt{O}_i:=\{0,1,...,d_{\mathtt{S}_i}-1\}$, where $d_{\mathtt{S}_i}$ is the Hilbert space dimension (assumed to be finite) of the system $\mathtt{S}_i$ measured by $\A_i$.
Without loss of generality, we model this as a projective measurement[Since any measurement on finite dimensional systems can be purified to a projective measurement involving rank 1 projectors on a larger set of systems through Naimark dilation; see e.g. <cit.>.] $\{\pi_{a_i}^{\mathtt{S}_i}=\proj{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$, where $\{\ket{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ forms an orthonormal basis of $\mathtt{S}_i$.[While this looks like a computational basis due to the choice of outcome labels $\mathtt{O}_i:=\{0,1,...,d_{\mathtt{S}_i}-1\}$, the choice of which basis to associate with these labels is arbitrary and therefore the measurement may correspond to an arbitrary orthonormal basis.]
In this general case, $\mathcal{M}^{\A_i}_{unitary}$ corresponds to a CNOT from $\mathtt{S}_i$ to the memory $\M_i$ (chosen to be of appropriate dimensions) in the $\{\ket{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ basis, i.e., we have the following for any state $\ket{\psi}_{\mathtt{S}_i}=\sum_{a_i} c_{a_i} \ket{a_i}_{\mathtt{S}_i}$ expressed in this basis[In the following equation, we have used a pure initial state $\ket{\psi}_{\mathtt{S}_i}$ to make the equations more concise, but it is easy to verify that analogous equations and the same arguments hold for mixed initial states $\rho_{\mathtt{S}_i}$.]

\begin{equation}
\label{eq:M_unitary_gen}
\mathcal{M}^{\A_i}_{unitary}: \ket{\psi}_{\mathtt{S}_i}\otimes \ket{0}_{\M_i} \mapsto \sum_{a_i} c_{a_i} \ket{a_ia_i}_{\mathtt{S}_i \M_i}.
\end{equation}

While agents can in-principle model the measurements of other agents unitarily in a LWFS, when they wish to calculate the probability of an outcome $a_i$, they calculate the probabilities associated with the corresponding projectors $\{\pi_{a_i}^{\mathtt{S}_i}=\proj{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ using the Born rule (for instance, as in assumption $Q$ of FR, which applies a special case of the Born rule). We summarise the above in the following general definition of a LWFS.

A LWFS is a quantum protocol that consists of

* A set $\mathtt{S}:=\{\Ss_1,...,\Ss_m\}$ of systems,

* A set $\mathtt{A}:=\{\A_1,...,\A_N\}$ of agents,

* A set $\mathtt{M}:=\{\M_1,...,\M_N\}$ of memory systems, one for each agent $\A_i$ where they store the outcome of their measurement.

* For each agent $\A_i$, a subset $\mathtt{S}_i\subseteq \mathtt{S}\cup \mathtt{M} \backslash \{\M_i\}$ of systems (which can include the memories of other agents) that they measure at time $t_i$ according to a measurement $\mathcal{M}^{\A_i}$, obtaining a measurement outcome $a_i$ that they store in their memory system $\M_i$. Here, $t_i<t_j$ for $i<j$.

* For each agent $\A_i$, a finite set $\mathtt{O}_i:=\{0,1,...,d_{\mathtt{S}_i}-1\}$ in which their outcome $a_i$ takes values.

* For each agent $\A_i$, a fixed operation $\mathcal{E}^i$ acting on their measured system and memory $\mathtt{S}_i\cup \{\M_i\}$ that captures the possibility of performing a further operation on the system $\mathtt{S}_i$ after the measurement, depending on the measurement outcome.

* A joint initial state $\rho_{\Ss_1,...,\Ss_m}$ of all the systems $\mathtt{S}$ at time $t_0<t_i$ for all $i\in\{1,...,N\}$

The protocol takes the form of <ref>, and we can consider projective measurements $\mathcal{M}^{\A_i}=\{\pi_{a_i}^{\mathtt{S}_i}=\proj{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ without loss of generality (as shown in the main text).

In any given LWFS, a prediction $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q})$ is evaluated through the following procedure. In the circuit of <ref>, the measurement $\mathcal{M}^{\A_i}$ of all agents $\A_i\in \mathtt{A}\backslash \big(\{\A_{j_1},...,\A_{j_p}\}\bigcup \{\A_{l_1},...,\A_{l_q}\}\big)$ is modelled as unitary evolutions of their labs (according to <ref>). For each agent $\A_i\in \{\A_{j_1},...,\A_{j_p}\}\bigcup \{\A_{l_1},...,\A_{l_q}\}$, the projective measurement $\{\pi_{a_i}^{\mathtt{S}_i}=\proj{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ is applied on their system $\mathtt{S}_i$, followed by a CNOT in the same basis from the system $\mathtt{S}_i$ to the memory $\M_i$ which models the procedure of making the measurement on the system and storing the outcome in the memory. The joint probability $P(a_{j_1},...,a_{j_p},a_{l_1},...,a_{l_q})$ is calculated by applying the Born rule to these projectors and the required prediction $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q})$ is obtained using the conditional probability rule.

Note that by default, the measurements of all agents, except those appearing in the prediction, are modelled unitarily in a LWFS, and agents whose measurements we calculate probabilities for are assigned projectors whose probabilities are calculated through the Born rule. Clearly, an LWFS goes beyond standard quantum theory as it allows agents to model each other's labs (consisting of the system $\mathtt{S}_i$ they measure, and their memory/rest of the lab $\M_i$) as quantum systems. We now explain how every LWFS can nevertheless be mapped to a standard quantum circuit which we call the augmented circuit of the LWFS.

For this, recall that in the universal use of quantum theory, agents can describe a measurement (whose outcome they do not know) through two possible evolutions, either unitarily or decoherently. For the measurement $\mathcal{M}^{\A_i}$ described above, associated with the projectors $\{\pi_{a_i}^{\mathtt{S}_i}=\proj{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$, the unitary description is as given in <ref>. The corresponding decoherent evolution $\mathcal{M}^{\A_i}_{mixture}$ is given by

\begin{equation}
\label{eq:M_mixture_gen}
\mathcal{M}^{\A_i}_{mixture}(\proj{\psi}_{\mathtt{S}_i}\otimes \proj{0}_{\M_i})=\sum_{a_i} |c_{a_i}|^2 \proj{a_ia_i}_{\mathtt{S}_i\M_i}.
\end{equation}

Notice that $ \mathcal{M}^{\A_i}_{mixture}(\proj{\psi}_{\mathtt{S}_i}\otimes \proj{0}_{\M_i})$ above can be equivalently expressed as

\begin{equation}
\label{eq:M_mixture_gen_proj}
\sum_{a_i} \pi_{a_i}^{\mathtt{S}_i \M_i}  \Big( \mathcal{M}^{\A_i}_{unitary}\big(\proj{\psi}_{\mathtt{S}_i}\otimes \proj{0}_{\M_i}\big)  \mathcal{M}^{\A_i \dag}_{unitary}\Big) \pi_{a_i}^{\mathtt{S}_i \M_i},
\end{equation}

where $\{\pi_{a_i}^{\mathtt{S}_i \M_i}:=\proj{a_ia_i}_{\mathtt{S}_i \M_i}\}_{a_i\in \mathtt{O}_i}$, and we still have a one-to-one correspondence between the measurement outcomes $a_i\in \mathtt{O}_i$ and an element from the above set of projectors. Therefore the two possible evolutions associated with a measurement $\mathcal{M}^{\A_i}$ are now given by <ref> and <ref>. We can explicitly model this choice by introducing a classical binary variable for each agent that takes values $x_i\in\{0,1\}$ (which we call the setting), such that when $x_i=0$, the measurement is modelled purely as unitary evolution $\mathcal{M}^{\A_i}_{unitary}$ on the system $\mathtt{S}_i$ and memory $\M_i$, and when $x_i=1$, the measurement is modelled as the unitary $\mathcal{M}^{\A_i}_{unitary}$ followed by the projective measurement $\{\pi_{a_i}^{\mathtt{S}_i \M_i}=\proj{a_ia_i}_{\mathtt{S}_i \M_i}\}_{a_i\in \mathtt{O}_i}$. This is captured through the following enlarged set of projectors, obtained by appending a trivial value $\perp$ to the outcome set $\mathtt{O}_i$.

\begin{equation}
\label{eq: proj_settings}
\mathtt{\Pi}_{x_i}^{\A_i}:=\begin{cases}
\{\pi_{a_i,x_i}^{\A_i}\}_{a_i\in\{ \perp\}}= \{\pi_{\perp,0}^{\A_i}:=\id_{\mathtt{S}_i \M_i}\}  &\text{ if } x_i=0\\
\{\pi_{a_i,x_i}^{\A_i}\}_{a_i\in \mathtt{O}_i}= \{\pi_{a_i,1}^{\A_i}:=\pi_{a_i}^{\mathtt{S}_i \M_i}\}_{a_i\in \mathtt{O}_i} &\text{ if } x_i=1.
\end{cases}
\end{equation}

That is, for $x_i=0$ the value $a_i$ is fixed uniquely to $a_i=\perp$ and the corresponding projector is the identity operator $\id_{\mathtt{S}_i \M_i}$.  Meanwhile, for $x_i=1$, $a_i$ takes values in the set $\mathtt{O}_i$ (reflecting the different possible classical outcomes of the measurement). We will only use the terminology outcome, to refer to the value of $a_i$ when $x_i=1$. In the case $x_i=0$, $a_i=\perp$ and we will not regard this as an outcome (we will sometimes refer to this case as the trivial outcome).

Then we can model each measurement $\mathcal{M}^{\A_i}$ as the corresponding unitary $\mathcal{M}^{\A_i}_{unitary}$, followed by a (setting-dependent) projective measurement $\mathtt{\Pi}_{x_i}^{\A_i}$. The pure unitary picture is always recovered by setting $x_i=0$, in which case only $\mathcal{M}^{\A_i}_{unitary}$ $\mathcal{M}^{{\A_i}^A}_{{unitary}_y}$ unitary is applied. The set of choices of settings for all $N$ agents can be represented by a vector $\vec{x}=(x_1,\ldots,x_N)$. With this explicit model, we can transform any LWFS into a standard temporally ordered quantum circuit parametrized by the settings $\vec x$ such that all the predictions made by different agents having different perspectives can be derived from the single circuit by fixing the settings $\vec x$ (as shown in <ref>). This circuit is obtained by replacing each measurement $\mathcal{M}^{\A_i}$ of the original circuit of <ref> with $\mathcal{M}^{\A_i}_{unitary}$ followed by a projective measurement of $\mathtt{\Pi}_{x_i}^{\A_i}$, which explicitly depends on the setting, such that the overall operation reduces to pure unitary evolution for $x_i=0$. We call this the augmented circuit of the LWFS. This is illustrated in <ref>, and summarised in the following definition.

Given a LWFS of the form of <ref>, we can associate with it an augmented circuit of the form of <ref> which is obtained from the LWFS by replacing each measurement $\mathcal{M}^{\A_i}$ by the corresponding unitary description $\mathcal{M}^{\A_i}_{unitary}$  (<ref>), followed by the setting-dependent enlarged set of projectors $\mathtt{\Pi}^{\A_i}_{x_i}$ (<ref>). The setting takes binary values $x_i\in \{0,1\}$, where we have only the trivial outcome $a_i=\perp$ whenever $x_i=0$ and the non-trivial measurement outcome $a_i\in \mathtt{O}_i$ whenever $x_i=1$. We will simply refer to this as an augmented LWFS, in short.

Keeping in mind the discussion of <ref>, note that <ref> respectively correspond to the two possible descriptions of a measurement $\mathcal{M}^{\A_i}$ from the perspective of an agent who is unaware of the outcome of the measurement.
Any agent who knows the outcome of $\A_i$'s measurement (on an initial state $\ket{\psi}_{\mathtt{S}_i}$) to be a particular value $a_i$ (or reasons about the case where it takes this particular value), would assign the post-measurement state $\ketbra{a_ia_i}{a_ia_i}_{\Ss_i\M_i}$, which can equivalently be written as

\begin{equation}
\label{eq:M_outcome_gen_proj}
\frac{ \pi_{a_i,1}^{\A_i}  \Big(\mathcal{M}^{\A_i}_{unitary}\big(\proj{\psi}_{\mathtt{S}_i}\otimes \proj{0}_{\M_i}\big)  \mathcal{M}^{\A_i \dag}_{unitary}\Big) \pi_{a_i,1}^{\A_i}}{\tr\Big(\pi_{a_i,1}^{\A_i}  \Big(\mathcal{M}^{\A_i}_{unitary}\big(\proj{\psi}_{\mathtt{S}_i}\otimes \proj{0}_{\M_i}\big)  \mathcal{M}^{\A_i \dag}_{unitary}\Big) \pi_{a_i,1}^{\A_i}\Big)}.
\end{equation}

Thus we have three cases: 1) the outcome of the measurement is known (or one is reasoning about a particular measurement outcome), 2) the outcome of the measurement is unknown (or not being reasoned about) and the measurement is modelled as in <ref>, and 3) the outcome of the measurement is unknown (or not being reasoned about) and the measurement is modelled as in <ref>. All three cases are fully covered by our augmented circuit framework using the projectors defined in <ref>. The measurement of each agent $\A_i$ is modelled using the set

\begin{equation}
\resizebox{0.48\textwidth}{!}{$\Bigg\{  \pi_{a_i,x_i}^{\A_i}  \Big(\mathcal{M}^{\A_i}_{unitary}\big(\proj{\psi}_{\mathtt{S}_i}\otimes \proj{0}_{\M_i}\big)  \mathcal{M}^{\A_i \dag}_{unitary}\Big) \pi_{a_i,x_i}^{\A_i} \Bigg\}_{a_i},$}
\end{equation}

where the setting $x_i$ takes values in $\{0,1\}$ and the outcomes take the singleton value $a_i=\perp$ when $x_i=0$ and can take multiple values $a_i\in\mathtt{O}_i$ when $x_i=1$. Case 1) is fully specified by taking $x_i=1$ and choosing the appropriate element of this set corresponding to the obtained outcome $a_i\in \mathtt{O}_i$. Case 2) is covered by choosing $x_i=0$ and Case 3) by choosing $x_i=1$ and summing over the outcomes $a_i\in \mathtt{O}_i$.

We now make a crucial observation. While we have so far given each agent full freedom in choosing how to model the measurements of other agents (i.e., unitarily by choosing setting $x_i=0$ or by assigning non-trivial projectors by choosing setting $x_i=1$), this freedom naturally becomes constrained when an agent $\A_i$ chooses to reason about the classical measurement outcome of another agent $\A_j$, based on their own outcome. This is because the unitary evolution $  \mathcal{M}^{\A_i}_{unitary}$ maps to a coherent, pure superposition state as the post-measurement state and is not associated with any classical record. On the other hand, in order to reason about a classical measurement outcome, we must assign certain projectors in order to identify that very outcome. For instance, in order to reason about the outcome $a_i\in \mathtt{O}_i$ of agent $\A_i$, we must consider the projectors $\{\pi_{a_i}^{\mathtt{S}_i}=\proj{a_i}_{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ or equivalently $\pi_{a_i}^{\mathtt{S}_i \M_i}:=\{\proj{a_ia_i}_{\mathtt{S}_i \M_i}\}_{a_i\in \mathtt{O}_i}$ as we have seen above. Whenever an agent chooses to reason about the outcome of some agent $\A_i$, they cannot model $\A_i$'s measurement through $\mathcal{M}^{\A_i}_{unitary}$ alone, they must identify the classical outcome $a_i\in \mathtt{O}_i$ being reasoned about through the corresponding projector $\pi_{a_i}^{\mathtt{S}_i\M_i}$ which is only possible when $x_i=1$ (cf. <ref>). They are however free to model $\A_i$'s measurement purely unitarily in situations where they do not reason about $\A_i$'s measurement outcomes. This free choice of whom to reason about, and how to model the measurements of agents who are not being reasoned about, is captured explicitly by the settings $\vec{x}$ in our framework. For instance, if $\A_i$ reasons about $\A_j$'s outcome based on their own outcome, they must necessarily choose $x_i=x_j=1$ in order to identify the outcomes they are reasoning about, but they may choose $x_k=0$ for all $k\neq i,j$ and model all other agents unitarily.

In particular, when reasoning about a particular outcome of $\A_i$, we apply Case 1) to $\mathcal{M}^{\A_i}$, but at the same time, we have a choice of whether we apply Case 2) or Case 3) to the measurement of another agent $\A_j$ who's outcome is unknown and not being reasoned about. The default choice in an LWFS is to choose the setting to be 0 i.e. Case 2 for all agents who are not being reasoned about. That is Case 3 is in principle not used in LWFS such as the FR scenario, as we will see later. However our framework is more general and also allows for this choice, where agents who are not being reasoned about are also assigned the setting 1. This generality will become relevant when discussing the different responses to FR's no-go theorem (<ref>).

Having defined and explained the augmented circuit, which is a standard quantum circuit, we can calculate the predictions here. This can be done by applying the Born rule along with the conditional probability rule, as long as we are given a prior $P(\vec{x})$ over the settings as this is required for the full specification of the circuit. Apart from the predictions $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q})$ , the augmented LWFS also allows us to consider probability distributions that involve the setting $\vec{x}$. Of particular interest in our analysis, will be conditional probabilities of the form $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q}, \vec{x})$ and we therefore define these below.

Given an augmented LWFS, we define a setting-conditioned prediction as a probability $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q}, \vec{x})$ assigned to a set of agents $\{\A_{j_1}, \A_{j_2},\ldots, \A_{j_p}\}$ obtaining outcomes $\{a_{j_1}, a_{j_2},\ldots, a_{j_p}\}$, given another disjoint set of agents $\{\A_{l_1}, \A_{l_2},\ldots, \A_{l_q}\}$ obtaining outcomes $\{a_{l_1}, a_{l_2},\ldots, a_{l_q}\}$ and given a setting choice $\vec{x}$. Here $p\in\{1,2,\ldots, N\}$ while $q\in\{0,1,\ldots, N\}$ where $q=0$ denotes the case where the conditioning is only on $\vec x$.

A logical setting-conditioned prediction is a setting-conditioned prediction $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q},\vec{x})$ taking values in $\{0,1\}$. Each logical setting-conditioned prediction is associated with a corresponding logical statement (that could be made by any agent using that prediction). The logical setting-conditioned predictions $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q},\vec{x})=0$ and $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q},\vec{x})=1$  are associated with the following statements respectively

Statement $\textup{S}^0_{\vec{x}}$: “If the outcomes $a_{l_1},...,a_{l_q}$ are obtained in the measurements of the agents $\A_{l_1},...\A_{l_q}$ and the settings are chosen to be $\vec{x}$, then it is certain that the outcomes $a_{j_1},...a_{j_p}$ cannot be obtained in the measurements of the agents $\A_{j_1},...\A_{j_p}$.”

Statement $\textup{S}^1_{\vec{x}}$:  “If the outcomes $a_{l_1},...,a_{l_q}$ are obtained in the measurements of the agents $\A_{l_1},...\A_{l_q}$ and the settings are chosen to be $\vec{x}$, then it is certain that the outcomes $a_{j_1},...a_{j_p}$ are obtained in the measurements of the agents $\A_{j_1},...\A_{j_p}$.”

In the case that $q=0$, then the “if” part of these statements only includes the setting choice.

Apart from setting-conditioned predictions $P(a_{j_1},...,a_{j_p}|\vec{x},a_{l_1},...,a_{l_q})$, we can also calculate predictions $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q})$ in the augmented circuit.
Predictions $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q})$ for an augmented LWFS are calculated by choosing a prior distribution $P(\vec{x})$ over the settings to calculate the joint probability $P(a_1,...,a_N,\vec{x})$ using the enlarged set of projectors of <ref> (as shown in the appendix, <ref>). Writing this as
$P(a_1,...,a_N,\vec{x})=P(a_1,...,a_N|\vec{x})P(\vec{x})$, and then marginalising gives $P(a_{j_1},...,a_{j_p},a_{l_1},...,a_{l_q})=\sum_{\vec{x},a_i\not\in \{a_{j_1},...,a_{j_p}\}\cup \{a_{l_1},...,a_{l_q}\}}P(a_1,...,a_N|\vec{x})P(\vec{x})$. We can then use the conditional probability rule to obtain $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q})$ by dividing $P(a_{j_1},...,a_{j_p},a_{l_1},...,a_{l_q})$ by $P(a_{l_1},...,a_{l_q})$.

Notice that in the particular case where we choose a deterministic prior $P(\vec{x})$, we obtain $P(a_{j_1},...,a_{j_p},a_{l_1},...,a_{l_q})=P(a_{j_1},...,a_{j_p},a_{l_1},...,a_{l_q}|\vec{x})$, and consequently the prediction $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q})$ becomes equivalent to a setting-conditioned prediction $P(a_{j_1},...,a_{j_p}|\vec{x},a_{l_1},...,a_{l_q})$, conditioned on a particular value $\vec{x}$ of the setting (given by the deterministic prior). This shows that the setting-conditioned prediction can be seen as a special type of a prediction that can be obtained in an augmented LWFS. Further, recall that the outcomes $a_i$ in augmented circuit take on the trivial value $\perp$ whenever $x_i=0$. In order to calculate a non-trivial prediction, i.e., a prediction where  $a_i\in \mathtt{O}_i$ for all $i\in\{j_1,...,j_p,l_1,...,l_q\}$, we must choose a prior $P(\vec{x})$ that has support on the setting values $x_i=1$ for $i\in\{j_1,...,j_p,l_1,...,l_q\}$.

Finally, we can define the set of all statements of interest in an LWFS. These include not only the logical inferences that agents make from predictions but also their own observations or observations of other agents (which may be publicly announced at the end or shared between subsets of agents as part of the protocol). We refer to all such statements as observational statements.

The set of all statements in an LWFS, denoted $\Sigma$ consists of all the logical statements that are associated with logical setting-conditioned predictions that can be made in the corresponding augmented circuit, as well as observational statements i.e., statements of the following form

Statement $\textup{S}$: “The outcomes $a_{l_1},...,a_{l_q}$ are obtained in the measurements of the agents $\A_{l_1},...\A_{l_q}$.”

For every LWFS, we have provided a method to assign an augmented circuit. Given an augmented circuit, we can calculate all possible predictions that the agents can make in the scenario by applying the Born rule to the augmented circuit. We derive an explicit expression for said predictions and setting-dependent predictions in <ref>. We now proceed to formally define the assumptions $Q$, $U$, $C$, $D$ and $S$ and then prove the completeness and consistency of our framework.

Although we do not do this here, we note that one can further enlarge the set $\Sigma$ of statements in our framework (and consequently generalise all the following results) by also considering statements associated to predictions in the augmented LWFS that are not setting-conditioned. We have already explained that these predictions come about from making a choice of prior over the settings and recover setting-conditioned predictions for the case of deterministic priors. Therefore in logical statements associated with logical predictions in an augmented LWFS, the choice of prior must also be specified in the conditions as this must be implicitly assumed to calculate the said prediction.

[->] (6,-6)–(9,-6); at (9.5,-6) time;

[ultra thick,decorate,
decoration = calligraphic brace] (-0.2,-2.2)–(-0.2,0.2); at (-1,-1) $\rho_{\Ss_1,\ldots,\Ss_m}$; at (-0.5,-3) $\ket{0}_{\M_1}$;  at (-0.5,-5) $\ket{0}_{\M_N}$;  at (0.5,-4) $\cdot$; at (0.5,-4.3) $\cdot$; at (0.5,-3.7) $\cdot$;

(0,0)–(1.3,0); at (0.5,0.2) $\Ss_1$; (0,-2)–(1.3,-2); at (0.5,-1.8) $\Ss_m$; at (0.5,-1) $\cdot$; at (0.5,-1.3) $\cdot$; at (0.5,-0.7) $\cdot$;  (0,-3)–(1.3,-3);at (0.5,-2.8) $\M_1$;
[dashed] (1,1.4) rectangle  (5,-3.5); (1.3,0.2) rectangle node$\mathcal{M}^{\A_1}_{unitary}$ (2.8,-3.2);
(0,-3)–(1,-3); [blue] (3.8,1.2) rectangle node$\mathtt{\Pi}^{\A_1}_{x_1}$ (4.8,-3.2); [blue] (0,1)–(3.8,1); [blue] at (-0.9,1) $x_1\in\{0,1\}$; [blue] (4.8,1)–(5.8,1); [blue] at (6.5,1.3) $a_1\in\{\perp,0,1,...\}$;
at (3,1.8) $\mathcal{M}^{\A_1}$;

(2.8,0)–(3.8,0); at (3.3,0.2) $\Ss_1$; (2.8,-2)–(3.8,-2); at (3.3,-1.8) $\Ss_m$; at (3.3,-1) $\cdot$; at (3.3,-1.3) $\cdot$;    at (3.3,-0.7) $\cdot$; (2.8,-3)–(3.8,-3); at (3.3,-2.8) $\M_1$;

(4.8,0)–(6,0); at (5.5,0.2) $\Ss_1$; (4.8,-2)–(6,-2); at (5.5,-1.8) $\Ss_m$; at (5.5,-1) $\cdot$; at (5.5,-1.3) $\cdot$;
at (5.5,-0.7) $\cdot$; (4.8,-3)–(6,-3); at (5.5,-2.8) $\M_1$; (6,0.3) rectangle node$\mathcal{E}^1$ (7,-3.2);

(7,0)–(8,0); at (7.5,0.2) $\Ss_1$; (7,-2)–(8,-2); at (7.5,-1.8) $\Ss_m$; at (7.5,-1) $\cdot$; at (7.5,-1.3) $\cdot$;
at (7.5,-0.7) $\cdot$; (7,-3)–(8,-3); at (7.5,-2.8) $\M_1$;

at (9,-1.5) $\dots$;

(0,-5)–(11.3,-5); at (5.5,-4.8) $\M_N$;  (10,0)–(11.3,0); at (10.5,0.2) $\Ss_1$; (10,-2)–(11.3,-2); at (10.5,-1.8) $\Ss_m$; at (10.5,-1) $\cdot$; at (10.5,-1.3) $\cdot$;
at (10.5,-0.7) $\cdot$; (10,-3)–(11.3,-3); at (10.5,-2.8) $\M_1$; at (10.5,-4.3) $\cdot$; at (10.5,-3.7) $\cdot$; at (10.5,-4) $\cdot$;

[dashed] (11,2.9) rectangle  (15,-5.5); (11.3,0.2) rectangle node$\mathcal{M}^{\A_N}_{unitary}$ (12.8,-5.2);
[blue] (13.8,2.7) rectangle node$\mathtt{\Pi}^{\A_N}_{x_N}$ (14.8,-5.2); [blue] (0,2.5)–(13.8,2.5); [blue] at (-0.9,2.5) $x_N\in\{0,1\}$; [blue] (14.8,2.5)–(15.8,2.5); [blue] at (16.5,2.8) $a_N\in\{\perp,0,1,...\}$;
at (13,3.3) $\mathcal{M}^{\A_N}$;

(12.8,0)–(13.8,0); at (13.3,0.2) $\Ss_1$; (12.8,-2)–(13.8,-2); at (13.3,-1.8) $\Ss_m$; at (13.3,-1) $\cdot$; at (13.3,-1.3) $\cdot$; at (13.3,-4.3) $\cdot$; at (13.3,-3.7) $\cdot$; at (13.3,-4) $\cdot$;

at (13.3,-0.7) $\cdot$; (12.8,-3)–(13.8,-3); at (13.3,-2.8) $\M_1$; (12.8,-5)–(13.8,-5); at (13.3,-4.8) $\M_N$;

(14.8,0)–(16,0); at (15.5,0.2) $\Ss_1$; (14.8,-2)–(16,-2); at (15.5,-1.8) $\Ss_m$; at (15.5,-1) $\cdot$; at (15.5,-1.3) $\cdot$; at (15.5,-4.3) $\cdot$; at (15.5,-3.7) $\cdot$; at (15.5,-4) $\cdot$;
at (15.5,-0.7) $\cdot$; (14.8,-3)–(16,-3); at (15.5,-2.8) $\M_1$; (14.8,-5)–(16,-5); at (15.5,-4.8) $\M_N$; (16,0.3) rectangle node$\mathcal{E}^N$ (17,-5.2);

[blue] at (-0.8,1.75) $\cdot$;  [blue] at (-0.8,2.05) $\cdot$;  [blue] at (-0.8,1.45) $\cdot$;

Augmented circuit for the general form of a LWFS illustrated in <ref>
that makes explicit the implicit setting choices needed to model the measurement of each agent. This circuit makes it clear that each agent has a choice in how they describe each measurement in the scenario, when the setting $x_i=0$, the corresponding measurement $\mathcal{M}^{\A_i}$ is modelled as a unitary evolution $\mathcal{M}^{\A_i}_{unitary}$ (in this case the projector in the blue box implements an identity operation and $a_i=\perp$ deterministically) and when $x_i=1$, the same measurement is modelled as the unitary $\mathcal{M}^{\A_i}_{unitary}$ followed by non-trivial projectors that identify the classical measurement outcome $a_i\in\{0,1,...d_{\mathtt{S}_i}-1\}:=\mathtt{O}_i$. In order for any agent to reason about the measurement outcome $a_i\in \mathtt{O}_i$ of an agent $\A_i$, they must necessarily choose $x_i=1$ in order to identify and calculate probabilities for the classical outcome that they are reasoning about. They may however choose to model all other agents $\A_j$ unitarily by choosing $x_j=0$.

§.§ Completeness, logical and temporal consistency

The following definitions apply to all agents in an LWFS who use the corresponding augmented circuit to make predictions and reason about each others' knowledge. In order to distinguish the following formal version of the FR assumptions from their original formulation, we denote them in boldface. In the following, recall that the mentioned predictions are construction-obtained by applying the Born rule to the augmented circuit.

Given a logical prediction (or logical setting-conditioned prediction), agents can take the corresponding logical statement defined in <ref> and <ref> to be true.

Agents can choose the setting $x_i=0$ for the measurement of any agent $\A_i$ whose outcome they are not logically reasoning about i.e., for every logical setting-conditioned prediction $P(a_{j_1},...,a_{j_p}|a_{l_1},...,a_{l_q},\vec{x})$, both choices $x_i\in\{0,1\}$ are allowed for all $a_i\not\in \{a_{j_1},...,a_{j_p}\}\cup \{a_{l_1},...,a_{l_q}\}$.

In [3], the assumption $C$ of the FR paper was formalised within the framework of modal logic.
This formulation is useful as it makes explicit whose knowledge is being referred to in each statement $s$. We will use $K_{\A_i}(s)$ to denote that “agent $\A_i$ knows that the statement $s$ is true”, where $K^{\A_i}$ is known as a knowledge operator (see [3] for a formal definition of the knowledge operators in terms of Kripke structures in modal logic). The assumption $C$ can then be succinctly expressed as an inference of the form

\begin{equation}
\label{eq: C_logic}
K_{\A_i}K_{\A_j}(s) \Rightarrow K_{\A_i}(s),
\end{equation}

where an agent $\A_i$ inherits the knowledge of another agent $\A_j$. More specifically, it is pointed out in [3] that such an inference only needs to be made when the agent $\A_i$ trusts the agent $\A_j$ (for otherwise $\A_i$ may not believe in everything that $\A_j$ claims to know, and may not want to inherit $\A_j$'s knowledge as their own). In a Wigner's friend scenario, not all pairs of agents are required to be able to inherit knowledge in this way, for instance if Wigner would eventually measure the memory of his friend in a complementary basis to the one in which the friend measured, often colloquially referred to as “Hadamarding the friend's brain”[4], then we cannot in general demand that $K_WK_F(s) \Rightarrow K_W(s)$ where $s$ is a statement about the classical measurement outcome of the friend, because from Wigner's perspective, no such classical outcome exists, even though he knows that it does from the perspective of the friend. We will later explain the trust structure of the FR protocol (which is also discussed in [3, 21]) but this will not be relevant for the general solution that we propose here. This is because, as we will show (cf. <ref>), the inclusion of the settings in our framework removes the need to specify a trust structure and ensures the general validity of <ref> in an augmented LWFS.

For any two agents $\A_i$ and $\A_j$, <ref> holds for all statements $s\in \Sigma$.

For any two statements $s_1, s_2 \in \Sigma$, if an agent $\A_i$ knows $s_1$ and also that $s_1$ implies $s_2$, then the agent knows $s_2$ i.e.,

\begin{equation}
\label{eq: logic_axiom1}
K_{\A_i}(s_1\land (s_1\Rightarrow s_2))\Rightarrow K_{\A_i}(s_2),
\end{equation}

For any subset of agents $\{\A_{j_1},...,\A_{j_p}\}$, denoting the corresponding set of outcomes as the vector $\vec{a}_j:=(a_{j_1},...,a_{j_p})$, if $P(\vec{a}_j)=1$ holds, then it is impossible to have $P(\vec{a}'_j)=1$, where $\vec{a}_j\neq \vec{a}'_j:=(a'_{j_1},...,a'_{j_p})$.

Note that imposing the above assumption $\mathbf{S}$ in an augmented LWFS ensures that the same property holds also for setting-conditioned predictions $P(a_{j_1},...,a_{j_p}|\vec{x})$ for every value $\vec{x}$ of the settings, since we have already shown that predictions reduce to setting-conditioned predictions whenever we choose a deterministic prior distribution $P(\vec{x})$ over the settings.

Firstly, we note that our assumptions $\mathbf{Q}$ and $\mathbf{U}$, just like FR's assumptions $Q$ and $U$ also relate to the universal validity of the quantum mechanical Born rule and unitary evolution. $\mathbf{Q}$ in our framework encompasses the full Born rule (for the augmented circuit) while FR's $Q$ only requires a deterministic version thereof (in their framework without the settings). $\mathbf{U}$ allows agents to freely choose for agents whom they are not reasoning about, whether or not to model their measurement unitarily which is the same condition captured by $U$. As explained in [18], this is indeed part of what FR originally intended with the assumption $Q$. Further, the logical assumptions $\mathbf{C}$, $\mathbf{D}$ and $\mathbf{S}$ formalised here are very similar to previous formalisations and take exactly the same form. Thus $\mathbf{C}$ in our framework can still be understood as a knowledge inheritance rule, $\mathbf{D}$ as the distributive axiom and $\mathbf{S}$ as the single-outcome assumption.

We note however that at the mathematical level of the Kripke structure of modal logic, the set of statements $\Sigma$ on which these rules are applied within our framework is different from the set considered in the original model logic formulation of the FR claimed theorem given in [3] since $\Sigma$ includes additional structure given by the setting labels. We will return to a discussion of the relationship between our formalisation and previous versions of the FR assumptions in <ref> where we will discuss the FR claimed theorem in light of our resolution of the apparent  paradox. At a physical level, it is important to note that the formal version of these assumptions in our framework still capture exactly the same physical requirements as FR namely the universal validity of quantum theory, inheritance of knowledge and validity of classical logic applied to knowledge of measurement outcomes.

We are now ready to state our main results, the proofs of which can be found in <ref>.

If any two agents use the same choice of settings $\vec x$ for all measurements $\{\mathcal{M}^{\A_i}\}_i$ in an augmented LWFS or more generally, use the same prior distribution $P(\vec{x})$ over the settings, then they make all the same predictions in that scenario.

In the following by contradiction we mean two distinct agents derive distinctions values of the same prediction.

If all agents $\A_1,\ldots,\A_N$ in an augmented LWFS use the same choice of settings $\vec x$ for all measurements $\{\mathcal{M}^{\A_i}\}_i$ or more generally, use the same prior distribution $P(\vec{x})$ over the settings, then they can never arrive at a contradiction when reasoning about each other's knowledge using the assumptions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$, $\mathbf{D}$ and $\mathbf{S}$.

* Completeness:  All predictions and all logical statements that agents can make in an LWFS can be derived within the augmented circuit for the LWFS. More specifically, each prediction $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q})$  in an LWFS corresponds to a particular setting-conditioned prediction $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q}, \vec{x})$ of the augmented LWFS with the setting choice $x_i=1$ for all $i\in \{a_{j_1},...,a_{j_p}\}\cup \{a_{l_1},...,a_{l_q}\}$ and $x_i=0$ for all $i\in \{1,...,N\}\backslash \big( \{a_{j_1},...,a_{j_p}\}\cup \{a_{l_1},...,a_{l_q}\}\big)$.

* Logical consistency:
If agents in a LWFS reason about each other's knowledge using the augmented circuit for the scenario, then they can never arrive at a logical contradiction even if they reason using all five assumptions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$, $\mathbf{D}$ and $\mathbf{S}$.

* Temporal consistency: When agent $\A_i$ makes a prediction about a set of agents $\{\A_{j_1}, \A_{j_2},\ldots, \A_{j_p}\}$, it is sufficient for $\A_i$ to specify only those components $x_1,\ldots,x_k$ of the settings $\vec{x}$ where $k=\max(j_1, j_2, \ldots, j_p, i) \leq N$. What's more, the prediction is also independent of channels $\mathcal{E}^j$ and measurements $M^{j}$ for which $j>k$. In other words, the reasoning is consistent with the temporal order of the augmented circuit and future operations do not affect the validity of inferences made at a given time.

The above theorem establishes that our framework meets all the conditions of Renato Renner's challenge, namely logical consistency, generality, computational efficiency and temporal consistency. The computational efficiency follows from the fact that we have mapped the original LWFS with $N$ measurements (and $N$ intermediate operations) to a standard quantum circuit with $N$ operations with a binary setting choice each and $N$ fixed operations, where each prediction depends on the binary setting choice only of operations in the past. In particular, we have avoided the problem of having to consider all possible future operations while reasoning about an outcome in the present, by establishing the temporal consistency of the circuit which means that adding additional operations later in the circuit have no effect on earlier predictions. Note also that each prediction and logical statement (where one set of agents infers with certainty the outcome values of another set of agents) of the original LWFS corresponds exactly to one setting-conditioned prediction and logical statement (of the same form) in the augmented LWFS and involves exactly the same number of reasoning steps.

In the previous literature, apparent logical paradoxes such as the FR paradox are often associated with the failure of logical transitivity (see for instance [3, 22]), which asserts that if $a$ implies $b$ and $b$ implies $c$, then $a$ implies $c$. This class of literature suggests that in light of the FR result, one must replace logical transitivity a more general reasoning rule in quantum theory. Note however that logical transitivity follows from the distributive axiom $\mathbf{D}$,[Assume that $a$ is true, then using $a$ implies $b$ and the assumption $\mathbf{D}$, we obtain that $b$ is true. Again using $b$ implies $c$ and the assumption $\mathbf{D}$, we obtain that $c$ is true. That is, assuming $a$ implies $b$ and $b$ implies $c$ and using $D$, we have shown that if $a$ is true, so is $c$ or equivalently, $a$ implies $c$ as required.] which we have shown to be satisfied in our framework. It follows that logical transitivity also holds in our framework. The key concept is the introduction of the settings in our framework which make explicit all the assumptions made during the agents' reasoning and break any FR-like chain that could potentially lead to paradoxes recursive application of the reasoning rule $\mathbf{D}$, as such chains would necessarily be associated with different setting labels.

Thus the framework proposed here allows agents in any LWFS to reason about each other using quantum theory ($\mathbf{Q}$, $\mathbf{U}$) as well as classical logic applied to measurement outcomes ($\mathbf{C}$, $\mathbf{D}$, $\mathbf{S}$ as well as other rules of classical logic such as transitivity) without running into logical contradictions and while preserving consistency with the temporal order of their operations. Agents' perspectives can nevertheless be subjective within our framework; for instance they need not agree on the setting choice $\vec{x}$ that specifies which measurements are described unitarily. Furthermore, the settings in our framework do not correspond to choices of actual operations that are performed in the protocol, but to choices that agents must make when reasoning about the protocol. This means that an agents' choice of settings can vary with time, as they gain more knowledge about other agents' outcomes in the protocol. Thus the proposed framework ensures that even quantum mechanical agents with different subjective perspectives can never run into a logical paradox as long as they keep the choice of settings explicit in their reasoning, and it is sufficient for them to only keep track of past settings, the validity of their predictions is unaffected by setting choices for future measurements or by updates to their setting choices made in light of new knowledge acquired in the future. We will discuss the relationship between different perspectives and consistency with experiments in <ref> and <ref>.

Given that our framework is logically consistent despite satisfying a formal version of each of the FR assumptions, one might naturally wonder what assumption is additionally required in order to reproduce logical contradictions such as the apparent FR paradox in our framework. The main difference between our framework and previous analyses of LWF scenarios is in the explicit introduction of the settings (we say “explicit” since the settings were present in the FR protocol in the sense that they do choose a particular measurement and channel in every statement they make which corresponds to a particular setting in our framework. The difference if that this choice while present in the maths, it is not specified at the level of the logical probabilities or statements they derive|see <ref> for details). And it is precisely an assumption regarding the ability to ignore the setting choice that is required to reproduce the apparent paradox. We formalise this assumption below.

A logical setting-conditioned prediction $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q}, \vec{x})\in \{0,1\}$ is said to be setting-independent if  $P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q}, \vec{x})=P(a_{j_1},...a_{j_p}|a_{l_1},...,a_{l_q})$.

In the following, when we say that $\mathbf{I}$ is assumed or imposed, we mean that atleast one setting-conditioned prediction is assumed to be setting-independent.

We can then immediately obtain the following corollary of our results.

In order to obtain an apparent logical contradiction (i.e., a violation of $\mathbf{S}$) in an augmented LWFS where agents reason using assumptions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$ and $\mathbf{D}$, it is necessary to assume $\mathbf{I}$ on at least one logical setting-conditioned prediction that is not setting-independent.

This corollary follows from the results because using <ref> we know that in the absence of $\mathbf{I}$, the augmented LWFS is perfectly consistent with all five assumptions $\mathbf{Q}$, $\mathbf{U}$, $\mathbf{C}$, $\mathbf{D}$ and $\mathbf{S}$. Further, <ref> implies that any apparent violation of $\mathbf{S}$ (i.e., $P(\vec{a}_j)=1$ and $P(\vec{a}'_j)=1$ for $\vec{a}'_j\neq \vec{a}_j$) that might be obtained in a LWFS (for instance, the violation obtained by FR [2]), necessarily arises by computing the probability of the outcomes under two distinct choices of settings and then ignoring this choice by identifying the two predictions as the same (which is equivalent to applying $\mathbf{I}$ to the two setting-conditioned predictions). In other words, an apparent violation of $\mathbf{S}$ such as $P(\vec{a}_j)=1$ and $P(\vec{a}'_j)=1$ when formulated explicitly within our framework, always translates to $P(\vec{a}_j|\vec{x})=1$ and $P(\vec{a}'_j|\vec{x}')=1$ (where $\vec{x}$ and $\vec{x}'$ are two distinct setting values), which is not paradoxical as it refers to two distinct conditional probability distributions. Note however that this necessarily violates $\mathbf{I}$ since the predictions are indeed dependent on the setting, which is why the apparent paradox is recovered when $\mathbf{I}$ is imposed.

We note that a violation of $\mathbf{I}$ is not so surprising. In <ref> we show that it is indeed violated in the FR protocol, as well as Wigner's original thought experiment. In <ref> we show that we can have simple classical protocols where imposing an analogous assumption leads to an apparent paradox.

§.§ Recovering standard quantum theory

(-1,1.5)–(0,1.5); (-1,0.5)–(0,0.5);
(0,0) rectangle node$\mathcal{M}^{\A_i}_{unitary}$(1.5,2);  (1.5,1.5)–(2.5,1.5); (1.5,0.5)–(2.5,0.5);
[blue] (2.5,0) rectangle node$\mathtt{\Pi}^{\A_i}_{x_i}$ (3.5,3);
(3.5,1.5)–(4.5,1.5); (3.5,0.5)–(4.5,0.5);
[blue] (-1,2.75)–(2.5,2.75); [blue] (3.5,2.75)–(4.5,2.75); [dashed] (-0.5,-0.5) rectangle (4,3.5); at (1.75,3.9) $\mathcal{M}^{\A_i}$;
[blue] at (-1.8,2.75) $x_i\in\{0,1\}$;
[blue] at (5.7,2.75) $a_i\in\{\perp,0,1,...\}$;
at (-0.8,1.7) $\mathtt{S}$;
at (-1.5,0.5) $\ket{0}_{\M_i}$;
at (4.3,1.7) $\mathtt{S}$;
at (4.3,0.7) $\M_i$;
[->, line width=0.5mm] (7.3,2)–(8.3,2);

(0,0) rectangle node$\mathcal{M}^{A_i}$ (1,1.5); (-1,0.75)–(0,0.75); (1,0.75)–(2,0.75); [blue] (1,1.3)–(2,1.3);
at (-0.8,0.95) $\mathtt{S}$;  at (1.8,0.95) $\mathtt{S}$; [blue] at (3,1.3) $a_i\in\{0,1,...\}$;

In an LWFS where an agent $\A_i$'s memory $\M_i$ is not acted upon after their measurement $\mathcal{M}^{\A_i}$, we can replace their setting-dependent measurement in the augmented LWFS (dashed box on the left hand side) with the simpler, setting-independent measurement of the right hand side. On both sides, $\mathtt{S}=\{S_1,...,S_m\}$ denotes the set of all systems. Recall that each agent's mesurement acts non-trivially only on some subset $\mathtt{S}_i\subseteq \mathtt{S}$. Here the simplified measurement on the right hand side is simply a projective measurement of $\{\pi_{a_i}^{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$, noting that $\mathtt{O}_i=\{0,1,...,d_{\mathtt{S}_i}-1\}$.

Here we explain how the general framework developed above for Wigner's friend type scenarios recovers our intuitions about standard quantum theory, when agents do not measure each other's memories/labs. Recall that in our framework, the memory $\M_i$ of each agent $\A_i$ plays the role of “their entire lab except the system that they measure” i.e., the quantum system $\mathtt{S}_i$ which $\A_i$ measures together with their memory $\M_i$ constitute an idealised model of $\A_i$'s lab that is relevant to the discussion on LWFS.

The main distinction between standard quantum measurement scenarios and LWFS is in the introduction of the settings which are not choices of actually performed operations but of choices made during the reasoning, that specify whether or not a measurement is modelled as a purely unitary evolution. We have seen that in the universal use of quantum theory, this creates an ambiguity in how measurements are modelled. In the standard use of quantum theory, we do not consider scenarios where the labs of agents (other than the quantum systems they measure and manipulate) are further measured by other agents. Here we show that under such a constraint on the LWFS, we indeed recover the familiar intuitions of standard quantum theory where we need not explicitly consider the state of the agents' labs (other than the quantum systems that they measure and manipulate) and there is no longer an ambiguity in how a measurement is described i.e., the settings become irrelevant in this case. This establishes that our general framework is consistent with all quantum experiments performed till date (at least for cases where the approximation of finite dimensional quantum mechanics safely holds).

If there are no operations in a LWFS that act on an agent $\A_i$'s memory $\M_i$ (except the measurement $\mathcal{M}^{\A_i}$ of that agent), then the predictions of the augmented LWFS are independent of the setting $x_i\in\{0,1\}$ of the agent $\A_i$. Futher, the predictions of the augmented circuit (<ref>) are invariant under replacing the measurement $\mathcal{M}^{\A_i}$ of $\A_i$ with a projective measurement of $\{\pi_{a_i}^{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ on the system $\mathtt{S}_i$, without introducing the setting $x_i$ or the memory $\M_i$, as shown in <ref>.

Applying the above theorem to each agent $\A_i$, we immediately obtain the following corollary.

If there are no operations in an LWFS that act on the memory $\M_i$ of any agent $\A_i$ (except the measurement $\mathcal{M}^{\A_i}$ of that agent), then all predictions in the augmented LWFS are independent of all settings $\vec{x}=(x_,...,x_N)$. Furthermore, the predictions of the augmented LWFS (and hence the LWFS) are equivalent to the predictions that can be obtained in the circuit of <ref> which includes no memory systems or settings.

One may consider further generalisation of these results in our framework. For instance, one would expect that even if an agent $\A_i$'s memory is subsequently operated upon  through operations that are compatible with the basis of measurement of that agent, then the setting $x_i$ can be ignored as well. We leave these generalisations for future work as they are not required for our results and conclusions.

[->] (6,-3.5)–(9,-3.5); at (9.5,-4) time;

[ultra thick,decorate,
decoration = calligraphic brace] (-0.2,-2.2)–(-0.2,0.2); at (-1,-1) $\rho_{\Ss_1,\ldots,\Ss_m}$;

(0,0)–(1,0); at (0.5,0.2) $\Ss_1$; (0,-2)–(1,-2); at (0.5,-1.8) $\Ss_m$; at (0.5,-1) $\cdot$; at (0.5,-1.3) $\cdot$; at (0.5,-0.7) $\cdot$; (1,0.3) rectangle node$\mathcal{M}^{\A_1}$ (2,-2.3);

(2,0)–(3,0); at (2.5,0.2) $\Ss_1$; (2,-2)–(3,-2); at (2.5,-1.8) $\Ss_m$; at (2.5,-1) $\cdot$; at (2.5,-1.3) $\cdot$; at (2.5,-0.7) $\cdot$;

(3,0.3) rectangle node$\mathcal{E}^1$ (4,-2.3);

(2,0)–(3,0); at (2.5,0.2) $\Ss_1$; (2,-2)–(3,-2); at (2.5,-1.8) $\Ss_m$; at (2.5,-1) $\cdot$; at (2.5,-1.3) $\cdot$; at (2.5,-0.7) $\cdot$;

(5,0.3) rectangle node$\mathcal{M}^{\A_2}$ (6,-2.3);

(2,0)–(3,0); at (2.5,0.2) $\Ss_1$; (2,-2)–(3,-2); at (2.5,-1.8) $\Ss_m$; at (2.5,-1) $\cdot$; at (2.5,-1.3) $\cdot$; at (2.5,-0.7) $\cdot$;

(7,0.3) rectangle node$\mathcal{E}^2$ (8,-2.3);
(2,0)–(3,0); at (2.5,0.2) $\Ss_1$; (2,-2)–(3,-2); at (2.5,-1.8) $\Ss_m$; at (2.5,-1) $\cdot$; at (2.5,-1.3) $\cdot$; at (2.5,-0.7) $\cdot$;

at (10,-1) $\dots$;

(2,0)–(3,0); at (2.5,0.2) $\Ss_1$; (2,-2)–(3,-2); at (2.5,-1.8) $\Ss_m$; at (2.5,-1) $\cdot$; at (2.5,-1.3) $\cdot$; at (2.5,-0.7) $\cdot$;

(12,0.3) rectangle node$\mathcal{M}^{\A_N}$ (13,-2.3);

(2,0)–(3,0); at (2.5,0.2) $\Ss_1$; (2,-2)–(3,-2); at (2.5,-1.8) $\Ss_m$; at (2.5,-1) $\cdot$; at (2.5,-1.3) $\cdot$; at (2.5,-0.7) $\cdot$;

(14,0.3) rectangle node$\mathcal{E}^N$ (15,-2.3);

Equivalent circuit for an LWFS where memories of agents are discarded after measurement. If the memory $\M_i$ of each agent $\A_i$ in an LWFS is never operated upon by other agents after their measurement, the augmented circuit for such an LWFS can be replaced with the simple circuit shown here which does not include any memories or settings. Here, each measurement $\mathcal{M}^{\A_i}$ is a projective measurement of some set of projectors $\{\pi_{a_i}^{\mathtt{S}_i}\}_{a_i\in \mathtt{O}_i}$ on a subset $\mathtt{S}_i\subseteq \mathtt{S}$ of all the systems $\mathtt{S}=\{\Ss_1,...,\Ss_m\}$ i.e., there is no ambiguity in how a measurement is modelled, as is the case in the standard use of quantum theory. This circuit is obtained by performing the replacement of <ref> for each measurement in the augmented circuit of <ref>. Here, we have supressed the blue outcome wire $a_i$ for each measurement for simplicity. The ambiguity characteristic of Wigner's friend type thought experiments can only become relevant when one or more agents measure or operate upon the memories (or labs) of other agents.

§ ANALYSIS OF THE FRAUCHIGER-RENNER PROTOCOL

We now review and analyse within our framework, two versions of the FR protocol namely a simplified entanglement version and the more involved, original prepare and measure version showing that no paradox arises in either case.

§.§ Entanglement version

§.§.§ Review of the scenario

We are now ready to review the entanglement-based version of the FR paradox that is originally attributed to Lluis Masanes, and was also mentioned in [23]. This version makes the important/salient features of the FR protocol more readily accessible, and thus allow for a more succinct explanation of where the reasoning fails. For completeness, we also provide an analysis of every step in the reasoning of the original FR protocol in <ref>. The conclusions are the same.

In this section we follow the notation and agent naming conventions of [3, 21] for clarity. Here we have two agents Alice and Bob who measure individual subsystems of a bipartite system while two super-agents Ursula and Wigner measure the labs (system and memory) of Alice and Bob respectively. The protocol can be broken down into three steps: a bipartite state preparation (pre-selection) at an initial time $t=1$, intermediate local measurements by Alice and Bob on the state at time $t=2$, a final measurement and post-selection by two super-agents Ursula and Wigner at time $t=3$.

* Pre-selection at time $t=1$: An initial state $\ket{\psi^{t=1}}_{\R\Ss}:=\frac{1}{\sqrt{3}}(\ket{00}_{\R\Ss}+\ket{10}_{\R\Ss}+\ket{11}_{\R\Ss})$ is prepared and shared between Alice and Bob where $\R$ and $\Ss$ label the subsystems belonging to Alice and Bob respectively. Alice and Bob's memories $\A$ and $\B$ are initialised to $\ket{0}_\A$ and $\ket{0}_\B$. Hence the initial preparation (i.e., pre-selected state) on $\R\A\Ss\B$ is given by

\begin{equation}
\ket{\psi^{t=1}}_{\R\A\Ss\B}:=\frac{1}{\sqrt{3}}(\ket{0000}+\ket{1000}+\ket{1010})_{\R\A\Ss\B}
\end{equation}

* Intermediate operations at time $t=2$: Alice and Bob measure their respective systems in the computational basis $\{\ket{0},\ket{1}\}$ and store the outcomes $a$ and $b$ of their respective measurements in their memory systems. From the outside perspective, Alice's measurement is modelled as a unitary $M^{\A}_{unitary}:=(CNOT)_{\R\A}$ on the joint system $\R\A$ which performs a CNOT operation with $\R$ as control and $\A$ as target, while Bob's measurement is similarly modelled as a unitary $M^{\B}_{unitary}:=(CNOT)_{\Ss\B}$.

* Post-selection at time $t=3$: The super-observers Ursula and Wigner post-select on the following final state $\ket{\phi^{t=3}}_{\R\A\Ss\B}:=\ket{\textup{ok}}_{\R\A}\ket{\textup{ok}}_{\Ss\B}$, which they achieve by measuring $\R\A$ and $\Ss\B$ respectively in the basis $\{\ket{\textup{ok}}:=\frac{1}{\sqrt{2}}(\ket{00}-\ket{11}),\ket{\textup{fail}}:=\frac{1}{\sqrt{2}}(\ket{00}+\ket{11})\}$ and halting when both of them obtain the outcome $u=\textup{ok}$, $w=\textup{ok}$ (where $u$ and $w$ denote Ursula's and Wigner's outcomes, the halting condition is checked by announcing these measurement outcomes in each run).

When modelling both measurements as unitaries, the joint state of $\R\A\Ss\B$ just after time $t=2$ is given by

\begin{align}
\label{eq: state_main}
\begin{split}
&\ket{\psi^{t=2}}_{\R\A\Ss\B}=(M^{\A}_{unitary}\otimes M^{\B}_{unitary})  \ket{\psi^{t=1}}_{\R\A\Ss\B}\\
\end{split}
\end{align}

The super-observers can then calculate the probability of success of the post-selection given the pre-selection and intermediate unitary evolution as

\begin{align}\label{eq:prob u Ok, w Ok in FR}
\begin{split}
&P(u=w=\textup{ok}|\psi^{t=2})\\&=|\braket{\phi^{t=3}|\psi^{t=2}}|^2\\&=|\bra{\phi^{t=3}}(M^{\A}_{unitary}\otimes M^{\B}_{unitary})  \ket{\psi^{t=1}}|^2\\&=\frac{1}{12}.
\end{split}
\end{align}

By this, they establish that they have a non-zero probability of obtaining $u=w=\textup{ok}$ and can thus repeat the protocol until they succeed. Upon successfully obtaining the desired outcomes, the protocol is halted and the agents reason about each others' knowledge as follows.

* Upon obtaining $u=\textup{ok}$ on measuring $\R\A$, Ursula reasons using the joint state $\ket{\psi^{t=2}}$ (<ref>) that Bob must have certainly obtained the outcome $b=1$ upon measuring $\Ss$, since  $\bra{\textup{ok}}_{\R\A}\bra{00}_{\Ss\B} \ket{\psi^{t=2}}_{\R\A\Ss\B}=0$. This gives

\begin{equation}
\label{eq: chain1}
K_U(  u=w=\textup{ok} \Rightarrow b=1)
\end{equation}

* Using the same state, Ursula knows that if Bob obtained $b=1$ on measuring $\Ss$, he would have concluded with certainty that Alice obtained $a=1$ on measuring $\R$ since $\bra{00}_{\R\A}\bra{11}_{\Ss\B}\ket{\psi^{t=2}}_{\R\A\Ss\B}=0$.

\begin{equation}
\label{eq: chain2}
K_U K_B(  b=1 \Rightarrow a=1)
\end{equation}

* Again using the same state, Ursula further reasons that Bob knows that if Alice had obtained $a=1$, she would have concluded with certainty that Wigner would obtain $w=\textup{fail}$, since  $\bra{11}_{\R\A}\bra{\textup{ok}}_{\Ss\B}\ket{\psi^{t=2}}_{\R\A\Ss\B}=0$. This gives

\begin{equation}
\label{eq: chain3}
K_U K_B K_A(  a=1 \Rightarrow w=\textup{fail}).
\end{equation}

As shown in [3], the above three statements can be combined using the assumption $C$ of the FR paper (in the form of <ref>) and the distributive axiom $D$ to yield the following paradoxical chain of statements. To obtain this result, the assumption $C$ in the form of <ref> only needs to be used between the following pairs of agents: Alice and Bob, Alice and Wigner, Ursula and Bob, Ursula and Wigner, as other pairs of agents need not trust each other [3, 21].[In [3], the assumption C is replaced by what they call the trust axiom which asserts that an agent $A^i$ can inherit the knowledge of another agent $A^j$ as per <ref> only if $A^i$ trusts $A^j$. In the FR setup, it is precisely these pairs of agents who can be said to trust each other. Other pairs such as Alice and Ursula need not trust each other as one agent Hadamard's the memory of the other.]

\begin{equation}
\label{eq: chain4}
K_U( u=w=\textup{ok} \Rightarrow b=1 \Rightarrow  a=1 \Rightarrow w=\textup{fail}),
\end{equation}

or in short $K_U(u=w=\textup{ok} \Rightarrow w=\textup{fail})$. This argument claims to establish that agents reasoning using $Q$, $U$, $C$ and $D$ will arrive at a contradiction with $S$ as they conclude through such a reasoning that $w=\textup{ok}$ and $w=\textup{fail}$ must both hold with certainty, and is therefore regarded as a proof of the FR no-go theorem (and its refinement as given in [3]) regarding the incompatibility of $Q$, $U$, $C$, $D$ and $S$.

§.§.§ Resolution of apparent paradox

(-1.5,0)–(4,0);  (-1.5,-1)–(4,-1);  (-1.5,-3)–(4,-3); (-1.5,-4)–(4,-4); [ultra thick,decorate,
decoration = calligraphic brace] (-1.7,-3.2)–(-1.7,-0.8);

at (-2,0) $\ket{0}_\A$;
at (-2.5,-2) $
\ket{\psi}_\textup{RS}$;
at (-2,-4) $\ket{0}_\B$;

(1.5,-1) circle [radius=3pt]; (1.5,0) circle (3mm); (1.5,-1)–(1.5,0.3);
(1.5,-3) circle [radius=3pt]; (1.5,-4) circle (3mm); (1.5,-3)–(1.5,-4.3);

[dashed] (1,-1.5) rectangle (2,0.5); at (1.5,1.2) Alice's
of $\textup{R}$;

[dashed] (1,-4.5) rectangle (2,-2.5); at (1.5,-5.2) Bob's
of $\textup{S}$;

(4,-1.5) rectangle nodeUrsula's
measurement (6,0.5); [->] (6,-0.5)–(7,-0.5); at (8.2,-0.5) $u\in \{\textup{ok},\textup{fail}\}$;
(4,-4.5) rectangle nodeWigner's
measurement (6,-2.5);  [->] (6,-3.5)–(7,-3.5); at (8.2,-3.5) $w\in \{\textup{ok},\textup{fail}\}$;

at (-2,-6.5) $t=1$;  at (1.5,-6.5) $t=2$;  at (5,-6.5) $t=3$;

Circuit that describes the entanglement version of the FR protocol, from the view of the super-agents Ursula and Wigner who describe the measurement of Alice and Bob as unitary evolutions. Alice and Bob share a bipartite state $\ket{\psi}_{\R\Ss}$, measure their half of the state in the computational basis and store the outcome of the measurement in their memories $\A$ and $\B$ respectively (which when modelled as a unitary corresponds to a CNOT). Ursula and Wigner then jointly measure Alice and Bob's system and memories to obtain the outcomes $u,w\in\{\textup{ok},\textup{fail}\}$. Note that this circuit by itself does not allow the super-agents to reason about the classical measurement outcome of Alice and Bob as no such outcome has been identified.

We first formulate the entanglement version of the FR protocol reviewed above within our framework by giving its augmented circuit. A typical circuit associated with this scenario, also found in the previous literature, is shown in <ref>. It is one which models the measurements of the agents Alice and Bob purely unitarily. As these are computational basis measurements, the corresponding unitary is the CNOT. However, this circuit alone does not allow us to calculate the probabilities of Alice and Bob's classical outcomes. In the previous literature (see for instance [18]), multiple different circuits are considered for calculating the probabilities from the perspective of each agent. In our framework, we have shown that all such reasoning can in fact be captured with a single circuit, the augmented circuit. This circuit includes a setting $x_i$ for each agent $\A_i$, which when set to $x_i=0$ models their measurement as the unitary $\mathcal{M}^{\A_i}_{unitary}$ and when set to $x_i=1$ models the measurement as the unitary $\mathcal{M}^{\A_i}_{unitary}$ followed by a set of projectors associated with the measurement outcome $a_i\in \mathtt{O}_i$.

In the present case, we have four agents, but it will suffice to assign settings $x_1$ and $x_2$ only to the agents Alice and Bob. We need not assign settings to the super-agents Ursula and Wigner in this case because they announce their classical outcomes $u$ and $w$ in each run of the protocol and halt when all agents know that $u=w=\textup{ok}$. This means that all agents model Ursula and Wigner's measurements as though their settings are always 1. We need not consider the case where Ursula and Wigner's measurements are modelled unitarily (setting 0) as this is only the case if there were further super-super agents who measured Ursula and Wigner's labs. Thus the only relevant settings in our augmented circuit as $x_1$ and $x_2$, for Alice and Bob respectively.

We can now write the enlarged set of projectors $\mathtt{\Pi}^A_{x_1}$, and $\mathtt{\Pi}^B_{x_2}$ (cf. <ref>) as

\begin{align}
\label{eq: FR_aug_proj}
\begin{split}
\mathtt{\Pi}^A_{0}&:=\{\pi_{0,\perp}^A=\id_{\R\A}\},\\
\mathtt{\Pi}^A_{1}&:=\{\pi_{1,0}^A=\proj{00}_{\R\A},\pi_{1,1}^A=\proj{11}_{\R\A}\}\\
\mathtt{\Pi}^B_{0}&:=\{\pi_{0,\perp}^B=\id_{\Ss\B}\},\\
\mathtt{\Pi}^B_{1}&:=\{\pi_{1,0}^B=\proj{00}_{\Ss\B},\pi_{1,1}^B=\proj{11}_{\Ss\B}\}\\
\end{split}
\end{align}

These capture the fact that when Alice's setting $x_1=0$, her measurement is modelled as a unitary evolution and the $a$ is set deterministically to the trivial value $\perp$. When $x_1=1$, Alice's measurement is first modelled unitarily and then her measurement outcomes $a=0$ and $a=1$ are identified by the projectors $\pi_{1,0}^A$ and $\pi_{1,1}^A$.

With this we obtain the augmented circuit for the entanglement version of the FR protocol which is illustrated in <ref>. Note that here Alice and Bob act at the same time $t=2$ and Ursula and Wigner act at $t=3$, but we could always have the agents' operations occur at different times without affecting the circuit structure, such that this circuit fits within the general form of <ref>. We do not do this here for simplicity, but it is easy to see that this transformation would not affect any of the arguments.

(-1.5,0)–(4,0);  (-1.5,-1)–(4,-1);  (-1.5,-3)–(4,-3); (-1.5,-4)–(4,-4); [ultra thick,decorate,
decoration = calligraphic brace] (-1.7,-3.2)–(-1.7,-0.8);

at (-2,0) $\ket{0}_\A$;
at (-2.5,-2) $
\ket{\psi}_\textup{RS}$;
at (-2,-4) $\ket{0}_\B$;

at (-2,-6.5) $t=1$;  at (2.5,-6.5) $t=2$;  at (7,-6.5) $t=3$;

(1.5,-1) circle [radius=3pt]; (1.5,0) circle (3mm); (1.5,-1)–(1.5,0.3);
(1.5,-3) circle [radius=3pt]; (1.5,-4) circle (3mm); (1.5,-3)–(1.5,-4.3);

[dashed] (1,-1.5) rectangle (2,0.5); at (1.5,1.2) Alice's
of $\textup{R}$;

[dashed] (1,-4.5) rectangle (2,-2.5); at (1.5,-5.2) Bob's
of $\textup{S}$;

(6,-1.5) rectangle nodeUrsula's
measurement (8,0.5); [->] (8,-0.5)–(9,-0.5); at (10.2,-0.5) $u\in \{\textup{ok},\textup{fail}\}$;
(6,-4.5) rectangle nodeWigner's
measurement (8,-2.5);  [->] (8,-3.5)–(9,-3.5); at (10.2,-3.5) $w\in \{\textup{ok},\textup{fail}\}$;

[blue] (4,-1.5) rectangle node$\mathtt{\Pi}^A_{x_1}$ (5,1);
[->, blue] (3.5,1)–(4,0.5);  [->, blue] (5,0.5)–(5.5,1);[blue] at (3.3,1.3) $x_1\in \{0,1\}$; [blue] at (5.7,1.3) $a\in \{\perp,0,1\}$;

[blue] (4,-5) rectangle node$\mathtt{\Pi}^B_{x_2}$ (5,-2.5);
[->, blue] (3.5,-5)–(4,-4.5);  [->, blue] (5,-4.5)–(5.5,-5);[blue] at (3.3,-5.3) $x_2\in \{0,1\}$; [blue] at (5.7,-5.3) $b\in \{\perp,0,1\}$;

(5,0)–(6,0);  (5,-1)–(6,-1);  (5,-3)–(6,-3);  (5,-4)–(6,-4);

Augmented circuit for the entanglement version of the FR protocol. Unlike the circuit of <ref>, this circuit allows agents to model the measurements of Alice and Bob as unitary evolutions and at the same time also reason about their classical measurement outcomes. To model Alice unitarily, one must set $x_1=0$, in which case the trivial outcome $a=\perp$ is obtained deterministically and the blue box acts as an identity operation. To reason about Alice's classical outcome, one must set $x_2=1$, in which case the blue box applies the projectors corresponding to the classical outcome $a\in\{0,1\}$. All possible reasoning in this FR set-up can be derived from this circuit under different choices of settings, but these statements can no longer be combined to yield a paradox as explained in the main text.

We now proceed to show how our framework provides a resolution of the apparent paradox reviewed in the previous section.
For this, we first cast the logical inferences of the FR protocol in an equivalent, probabilistic form. An implication of the form $b=1\Rightarrow a=1$ for two outcomes $a$ and $b$, can be equivalently expressed in terms of their joint probability distribution as $P(a=0|b=1)=0$. This means that the super-agents Ursula and Wigner, in order to reason about the knowledge of the agents Alice and Bob must consider the probabilities of the outcomes $a$ and $b$ of Alice and Bob's measurements. In order to calculate the probabilities of $a$ and/or $b$, we must specify what they are probabilities of i.e., of which projectors/final states. The super-agents know that if Alice's lab $\R\A$ was measured in the basis $\big\{\ket{00}_{\R\A},\ket{01}_{\R\A}, \ket{10}_{\R\A},\ket{11}_{\R\A}\big\}$ between $t=2$ and $t=3$, the first outcome would be obtained whenever Alice observed $a=0$, and the last outcome would be obtained whenever Alice observed $a=1$ i.e., they would associate the projectors $\pi^A_{1,0}:=\ketbra{00}{00}_{\R\A}$ and $\pi^A_{1,1}:=\ketbra{11}{11}_{\R\A}$ with Alice's outcome $a=0$ and $a=1$, and similarly the projectors $\pi^B_{1,0}:=\ketbra{00}{00}_{\Ss\B}$ and $\pi^B_{1,1}:=\ketbra{11}{11}_{\Ss\B}$ with Bob's outcome $b=0$ and $b=1$.

In order for any agent to calculate the probability of Alice's outcome $a\in\{0,1\}$, they must use $x_1=1$. However, there are two ways that such an agent may calculate the probability of Alice's outcome $a\in\{0,1\}$ conditioned on the knowledge that the super-agents observed $u=\textup{ok}$, $w=\textup{ok}$: either using the setting $x_2=0$ for Bob or the setting $x_2=1$ for Bob. Similarly, there are two ways that we may calculate the probability of Bob's outcome $b\in\{0,1\}$ conditioned on the knowledge that a post-selection on $u=\textup{ok}$, $w=\textup{ok}$ succeeded, either using the settings $(x_1,x_2)=(0,1)$ or the settings $(x_1,x_2)=(1,1)$. One may be tempted to say that these two ways that only differ by Bob's choice of setting $y$, must yield the same probability for the probability of for Alice's outcome $a$ due to the no-signalling property of quantum theory. However this is no longer the case once we calculate a conditional probability of $a$, conditioned on success of the post-selection on future outcomes $u$ and $w$. In the FR protocol, the super-agents consider the reasoning of all agents only in an experimental round where this post-selection succeeds.

From Born's rule and the definition of conditional probability from probability theory, one obtains (see <ref> for a derivation) the following expression for the probability of obtaining a measurement outcome $k$ when measuring a set of projectors $\{\pi_k\}_k$ on an initial state $\rho$ (the pre-selected state), conditioned on the knowledge that a successful post-selection onto another state $\phi$ is performed after the measurement.

\begin{equation}
\label{eq: prob_rule generalised 2}
P(k|\rho,\phi,M)=\frac{\tr[\pi_{\phi}\pi_k\rho \pi_k]}{\sum_j \tr[\pi_{\phi}\pi_j\rho \pi_j]},
\end{equation}

where the summation runs over the POVM elements in the set $M=\{\pi_k\}_k$.
Here we have conditioned on pre-selected state $\rho$, post-selected state $\phi:= \pi_\phi \pi_k \rho\pi_k\pi_\phi/ \tr[\pi_\phi \pi_k \rho\pi_k\pi_\phi]$, and an intermediate measurement $M=\{\pi_k\}_k$ with outcome $k$.
This then reduces to the familiar expression for in the two-state formalism [24]

\begin{equation}
\label{eq: prob_rule}
\end{equation}

in the case that the pre and post selected states are pure, namely $\rho=\proj{\psi}$, $\phi=\proj{\phi}$.  Notice that the denominator is nothing but the success probability of the final post-selection on $\phi$, given that we preselected on $\psi$ and then performed a measurement $M=\{\pi_k\}_k$ before post-selecting. This rule is not special to quantum mechanics but arises naturally in classical probability theory, when we wish to calculate the probability of an event $e$ in a given post-selected sample, we must renormalise by the probability that the post-selection succeeded. This makes the calculated probability a conditional probability, conditioned on the success of the post-selection.

Furthermore, note that this success probability of the post-selection, given by the denominator will in general depend on the measurement $M=\{\pi_k\}_k$ which means that under the post-selection, the probability associated with the projector $\pi_k$ depends on the measurement $M=\{\pi_k\}_k$ to which it belongs (i.e. on the settings). Therefore, if there is a projector $\pi_k$ which is common to two distinct POVMs $M$, and $M'$, then in general $ P(k|\psi,\phi,M)\neq  P(k|\psi,\phi,M')$.
This is in contrast to the Born rule which is applied to calculate measurement probabilities only under pre-selection (and no post-selection), where the probability associated with a given measurement outcome on a given quantum state does not depend on the other POVM elements. Recasting the FR protocol in terms of a pre and post-selection scheme allows us to correctly account for the knowledge regarding the success of the post-selection along with settings introduced in our framework. As we show below, both these aspects play a role in fully resolving the apparent paradox in this case,

In the present case, we consider the pre-selection $\ket{\psi^{t=2}}_{\R\A\Ss\B}$ (<ref>), and post-selection $\ket{\psi^{t=3}}_{\R\A\Ss\B}=\ket{\textup{ok}}_{\R\A}\otimes\ket{\textup{ok}}_{\Ss\B}$, and four possible intermediate measurements, corresponding to the setting choices $(x_1,x_2)\in\{(0,0),(0,1),(1,0),(1,1)\}$. Noting that for the setting choice $(x_1,x_2)=(0,0)$, both Alice and Bob's measurements are modelled purely unitarily and hence associated with the trivial deterministic outcome $a=b=\perp$, we only need to calculate these probabilities for the remaining three setting choices.

Under the setting choice $(x_1,x_2)=(0,1)$, we can only calculate the probability associated with $b\in\{0,1\}$ (and not $a\in\{0,1\}$). For calculating the probability of $b$ given the pre-selection, post-selection and intermediate measurement of this setting choice, we first require the post-selection success probability in this case, which is given as follows, where we condition on the setting choice in place of the measurement $M$ as this fully specifies the intermediate measurement being considered in our case.

\begin{align}
\label{eq: denominator_B}
\begin{split}
=&\sum_{b\in\{0,1\}}|\bra{\phi^{t=3}}\Big(\id_{RA}\otimes \pi_{x_2=1,b}^{B}\Big) \ket{\psi^{t=2}}|^2 =\frac{1}{12}.
\end{split}
\end{align}

Using this in <ref>, we find.

\begin{align}
\begin{split}
\label{eq: prob_MB}
\end{split}
\end{align}

For the setting choice $(x_1,x_2)=(1,0)$, we can only calculate the probabilities of $a\in\{0,1\}$, which is done through an analogous calculation. First we calculate the post-selection success probability for this case.

\begin{align}
\label{eq: denominator_A}
\begin{split}
=&\sum_{a\in\{0,1\}}|\bra{\phi^{t=3}}\Big( \pi_{x_1=1,a}^{A}\otimes\id_{\Ss\B}\Big) \ket{\psi^{t=2}}|^2 =\frac{1}{12}.
\end{split}
\end{align}

Using this in <ref>, we find

\begin{align}
\begin{split}
\label{eq: prob_MA}
\end{split}
\end{align}

Finally, for the setting choice $(x_1,x_2)=(1,1)$, the post-selection success probability is as follows.

\begin{align}
\label{eq: denominator_AB}
\begin{split}
=&\sum_{a,b\in\{0,1\}}|\bra{\phi^{t=3}}\Big( \pi_{x_1=1,a}^{A}\otimes\pi_{x_2=1,b}^{B}\Big) \ket{\psi^{t=2}}|^2 =\frac{5}{6}.
\end{split}
\end{align}

Notice that the post-selection success probability differs depending on the settings, a similar point was also noted in [12]. Using this in <ref>, we obtain the following.

\begin{align}
\begin{split}
\label{eq: prob_M_AB}
\end{split}
\end{align}

This gives the marginals

\begin{align}
\label{eq: marginals_M_AB}
\end{align}

Every method that the super-agents could adopt for calculating the probabilities of the outcomes $a$ and/or $b$ of Alice and Bob given their own observations $u=w=\textup{ok}$, yields a valid probability distribution and no paradox arises in any of these cases. Crucially, the probability of $a$ ($b$) depends on whether it was obtained by assuming the setting choice $(x_1,x_2)=(1,1)$ or $(x_1,x_2)=(1,0)$ ($(x_1,x_2)=(0,1)$), as one would generally expect in post-selected experiments. This means that probabilities $P(a|u=w=\textup{ok})$ and $P(b|u=w=\textup{ok})$ that are required in the FR scenario are not well defined unless the method of calculating them (through $(x_1,x_2)=(1,1)$ or $(x_1,x_2)=(1,0)$ or $(x_1,x_2)=(0,1)$) is specified. Importantly, while the (unconditional) probability $P(a)$ is the same for $(x_1,x_2)=(1,1)$ and $(x_1,x_2)=(1,0)$ (and similarly $P(b)$ is the same under $(x_1,x_2)=(1,1)$ and $(x_1,x_2)=(0,1)$), the conditional probability $P(a|u=w=\textup{ok})$ that accounts for successful post-selection does depend on the value of the setting $x_2$ which is assumed for Bob's side, and vice versa. This feature where two independent variables can get correlated under post-selection on other variables also arises in classical probability theory, where it is better known as collider bias, and is no special feature of quantum theory. In <ref> we provide an example of a classical protocol that exhibits the same property.

In the FR scenario, the reasoning of all agents starts with the same pre-selected state $\ket{\psi^{t=2}}$ (<ref>, see [3] for details of this reasoning) and the super-agents begin to consider the different reasoning steps only once the post-selection $u=w=\textup{ok}$ has succeeded. Together, let us denote this given information as $G$. The first inference $u=w=\textup{ok}\Rightarrow b=1$ (<ref>) can be expressed as $P(b=1|G)=1$. The third inference $a=1\Rightarrow w=\textup{fail}$ (<ref>), which is equivalent to $w=\textup{ok}\Rightarrow a=0$, can be expressed as $P(a=0|G)=1$. The second inference $b=1\Rightarrow a=1$ can then be expressed as $P(a=1|b=1)=1$. This implies that $P(a=1|G,b=1)=1$ and consequently that $P(a=0|G,b=1)=0$, which in turn gives $P(a=0,b=1|G)=0$. That is, we have a seemingly incompatible set of probability assignments

\begin{align}
\label{eq: FR_Prob}
\begin{split}
P(b=1|G)&=1 .
\end{split}
\end{align}

Our analysis shows that these are not statements about the same probability distribution, but correspond to three different conditional probability distributions and the apparent paradox is resolved once the parties explicitly specify the implicit assumptions that need to be made on the settings. Furthermore, we have seen that the choice of these settings does matter, in particular, $P(b|G)$ depends on Alice's setting $x_1$ and $P(a|G)$ depends on Bob's setting $x_2$. Once we calculate all probabilities while taking into account implicit assumptions regarding setting choices, we have the following, which is completely unparadoxical.

\begin{align}
\label{eq: Correct_Prob}
\begin{split}
P(b=1|G, (x_1,x_2)=(0,1))&=1.
\end{split}
\end{align}

Translating the above back into logical implications by the same procedure that we used for obtaining <ref> from the FR chain of statements <ref>, we can explicitly formulate the conclusions drawn in the FR scenario as shown in <ref>.

original  formulation      our explicit formulation

$u=\textup{ok}\Rightarrow b=1$          $(x_1,x_2)=(0,1) \land u=\textup{ok} \Rightarrow b=1$

$b=1\Rightarrow a=1$          $(x_1,x_2)=(1,1) \land b=1 \Rightarrow a=1$

$a=1\Rightarrow w=\textup{fail}$          $(x_1,x_2)=(1,0) \land a=1 \Rightarrow w=\textup{fail}$

Explicit versions of the FR statements as given in our framework, which provides a logically consistent resolution to the FR apparent paradox without giving up any of the original assumptions of FR. While the original statements can be chained together to yield $u=\textup{ok} \Rightarrow w=\textup{fail}$ which yields a contradiction along with the fact that $P(u=w=\textup{ok})>0$, our explicit version of the statements cannot be chained together to yield this conclusion even using the axioms of classical logic.

Then we can immediately see that while the original statements can be chained together using classical logical rules to yield $u=w=\textup{ok}\Rightarrow w=\textup{fail}$, the explicit version of the statements given in <ref> cannot be chained together in the same manner, even under the standard rules of classical logic.

Finally, we can also consider other alternate ways of reasoning, for instance by averaging over the setting choices (using a prior distribution over the settings) or by conditioning only one of the two post-selections $u=\textup{ok}$ and $w=\textup{ok}$ succeeding. In <ref> we apply our framework to these and show that no paradox ensues even in these cases.
While the entanglement version is commonly regarded as being equivalent to the original prepare and measure version of the FR protocol, the authors have often argued that it oversimplifies their arguments by washing out the subtle details of the temporal aspects of the reasoning present in the original protocol. Therefore, we also analyse the original protocol in detail in the next section and discuss how our framework resolves the apparent paradox there in a similar manner.

§.§ Prepare and measure version

§.§.§ Review of the scenario

Here we show that the resolution proposed for the entanglement version is also applicable to the original (prepare and measure) version of the FR paradox, ref. [2]. We will go through the reasoning of the prepare and measure version on a statement-by-statement basis of their apparent proof of their paradox. For every statement, we now revealing the different settings which said statements are contingent on, but not stated by the authors. We will use a notation which is close to, but not identical to, that of the authors to aid comparison.

The scenario in [2] describes a protocol realised by agents F, F, W and W. Agents F and F have their own individual labs while W and W are so-called super-observers, i.e. W can perform arbitrary measurements on F and the lab of F, while W can perform arbitrary measurements on F and the lab of F. The labs of F and F are completely isolated from W and W until W and W measure at the end of the protocol. It is also assumed that the labs F and F are initially in pure states. The lab systems of F and F are denoted L and L respectively. L includes everything in F's lab such as the agent F and a random generator R that they use, but excludes a spin qubit S which will start off in the lab of F and move to the lab of F during the protocol. The lab system L of F will include the spin S that arrives to F, as well as the agent F and other devices in their lab which are not explicitly specified.

The protocol is repeated $n$ times. Between each implementation, it is reset to the initial state. There is a halting condition which is examined at the end of each round. When the condition is satisfied, the protocol is stopped and the last round of the experiment is analysed. The $n^\text{th}$ round of the protocol from the perspective of W and W is as follows:

Before time $n\!:\!00$, F tosses a coin in her lab which gives heads with probability 1/3 and tails with probability 2/3. This coin toss is a random variable which is obtained by measuring the following quantum state in the same basis in which it is expressed.

\begin{align}
\label{eq: FR_PM_instate}
\ket{\textup{init}}_\R:=\sqrt{\frac13}\ket{\textup{heads}}_\R+\sqrt{\frac23}\ket{\textup{tails}}_\R.
\end{align}

The lab of F consists of the random generator (or coin) R, a spin S and $\Lbar\backslash$ which represents the rest of the lab. In the following, $\Lbar:=\R\otimes \Lbar\backslash$ is the lab of F, excluding the spin S.
Then the unitary $U_{\mb{F}}$ (from the perspective of F, W and W) that describes F's coin toss (measurement of R) implements the evolution

\begin{align}
U_{\mb{F}}:\ket{\textup{init},\phi_0,S_0}_{\Lbar\Ss}\to \big(\sqrt{\frac{1}{3}}\ket{\mb h}_{\Lbar}+\sqrt{\frac{2}{3}}\ket{\mb t}_{\Lbar}\big)\ket{S_0}_{\Ss},\label{eq:FR_PM_UF}
\end{align}

where $\ket{\textup{init},\phi_0,S_0}_{\Lbar\Ss}:=\ket{\textup{init}}_\R\ket{\phi_0}_{\Lbar\backslash}\ket{S_0}_\Ss$ with $\ket{\phi_0}_{\Lbar\backslash}$ the initial state of F's lab excluding the spin system and the random generator; the latter two being $\ket{S_0}_\Ss$ and $\ket{\textup{init}}_\R$ respectively, where $\ket{S_0}_\Ss$ is some initial state of $S$. The kets $\ket{\mb h}$, $\ket{\mb t}$ represent the state of F's lab (excluding the spin qubit) after her measurement of the random variable ($\ket{\mb h}$ in the case her measurement revealed heads while $\ket{\mb t}$ when she obtained tails).

Following the coin toss, F prepares a spin qubit in her lab in state $\ket{\downarrow}_\Ss$ if she gets heads, while $\ket{\rightarrow}_\Ss$ if she gets tails. From the perspective of F, W and W, this is a unitary process since her lab is an isolated system.
The unitary that describes this preparation of $\Ss$ is denoted as $U_{\textup{spin}}$ and together with $U_{\mb{F}}$, this implements the evolution

\begin{align}
U_{\textup{spin}}U_{\mb{F}}:\ket{\textup{init},\phi_0,S_0}_{\Lbar\Ss}\to\sqrt{\frac13}\ket{\mb h,\downarrow}_{\Lbar\Ss}+\sqrt{\frac23}\ket{\mb t,\rightarrow}_{\Lbar\Ss},\label{eq:initial to final ket}
\end{align}

Meanwhile, F waits patiently in her lab, which we denote $\ket{\phi_0}_{\Lab\backslash}$ initially, where $\Lab\backslash$ denotes F's lab without the spin qubit $S$ and we will use $\Lab:=\Ss\otimes \Lab\backslash$. Between times $n\!:\!10$ and $n\!:\!20$, F sends her qubit system to F's lab and F subsequently measures the qubit in the $\ket{\uparrow}_\Ss$, $\ket{\downarrow}_\Ss$ basis, denoting her outcome $+1/2$ and $-1/2$ respectively.
From the perspective of W and W, the labs of F and F are subsequently modelled through the series of evolutions $U_{\mb{F}}$, followed by $U_{\textup{spin}}$ followed by $U_{\textup{F}}$ where $U_{\textup{F}}$ is the unitary evolution corresponding to F's measurement of S.

\begin{align}\label{eq:final state FR version}
\begin{split}
&U_{\textup{F}}U_{\textup{spin}}U_{\mb{F}}: \ket{\textup{init},\phi_0,S_0}_{\Lbar\Ss}\ket{\phi_0}_{\Lab\backslash}
\to\\
&\qquad\sqrt{\frac13}\Big(\ket{\mb h}_\Lbar\ket{\downarrow,-1/2}_{\Lab}
+\ket{\mb t}_\Lbar\ket{\downarrow,-1/2}_{\Lab}+ \ket{\mb t}_\Lbar\ket{\uparrow,1/2}_{\Lab}\Big),
\end{split}
\end{align}

where $\ket{\downarrow,-1/2}_{\Lab}$ denotes the spin in the down state $\ket{\downarrow}_\Ss$ and the state of the rest of lab L when F obtains measurement outcome $-1/2$; similarly for $\ket{\downarrow,-1/2}_{\Lab}$.
Between times $n\!:\!20$ and $n\!:\!30$, W measures lab L in the basis $\{ \ket{\mb{\textup{ok}}}_\Lbar, \ket{\mb{\textup{fail}}}_\Lbar\}$, where $\ket{\mb{\textup{ok}}}_\Lbar:=\sqrt{\frac12} (\ket{\mb h}_\Lbar-\ket{\mb t}_\Lbar)$, $\ket{\mb{\textup{fail}}}_\Lbar:=\sqrt{\frac12} (\ket{\mb h}_\Lbar+\ket{\mb t}_\Lbar)$. After time $n=30$,  W measures lab L in the basis $\{ \ket{{\textup{ok}}}_\Lab, \ket{{\textup{fail}}}_\Lab\}$, where $\ket{{\textup{ok}}}_{\Lab}:=\sqrt{\frac12} (\ket{\downarrow,-1/2}_\Lab-\ket{\uparrow,1/2}_\Lab)$, $\ket{{\textup{fail}}}_\Lab:=\sqrt{\frac12} (\ket{\downarrow,-1/2}_\Lab+\ket{\uparrow,1/2}_\Lab$. The final state of the labs (right hand side of <ref>) in this measurement basis takes on the form

\begin{align}
\begin{split}
&\sqrt{\frac{1}{12}} \left(\ket{\mb{\textup{fail}}}_\Lbar+\ket{\mb{\textup{ok}}}_\Lbar\right)\left(\ket{\textup{fail}}_\Lab+\ket{\textup{ok}}_\Lab\right)+\\
&\sqrt{\frac{1}{6}} \left(\ket{\mb{\textup{fail}}}_\Lbar-\ket{\mb{\textup{ok}}}_\Lbar\right)\ket{\textup{fail}}_\Lab.
\end{split}
\end{align}

In <ref>, we summarise this thought experiment using branching notation.
If the outcomes of W and W are not ok, ok respectively, then the protocol is re-set and repeated. If their outcomes are ok, ok, then the experiment is finished and F, F, W and W reason about their ok, ok measurement outcomes and what they should be able to predict about the measurement outcomes of the other agents in the last round of the protocol. The obtention of ok, ok by W and W respectively is the halting condition mentioned previously, and from the above form of the final state, it is clear that this outcome occurs with probability $\frac{1}{12}$.

The FR thought experiment expressed using branching notation. The quantum state as per a unitary description from the viewpoint of W and W at any time, is the sum of the states of each branched at said time. Arrows indicate the splitting of the amplitudes due to the actions of individual observers. We refer to these as branches and each branch has its own number above the corresponding arrow. The two purple kets on branches 1.1.1. and 2.1.1 cancel each other out when said branches are added together, while the two blue kets on branches 2.1.1. and 2.1.2. cancel when said branches are added together.

While reasoning, they assume that all agents are aware of the entire experimental procedure as described above, and that they all employ the same theory. As we will see, all agents, when reasoning from their perspective, assume unitary dynamics for all agent's measurements other than those they are reasoning about. In other words, their protocol is a special case of a LWFS. In <ref> we present the augmented circuit of the original FR protocol as a simplified version that makes the mapping back to the entanglement version more apparent.

In FR's reasoning, they make the three assumptions $Q$, $C$, $S$ explicitly, in addition to the assumptions $U$ and $D$ implicitly, as described in <ref>.

In particular, the authors then claim to prove the following theorem:

Theorem 1: Any theory that satisfies assumptions ($Q$), ($C$), and ($S$) yields contradictory statements when applied to their thought experiment of Box 1.
By “Box 1” the authors are referring to the above protocol.

§.§.§ Resolution of apparent paradox

We will now analyse their constructive proof step by step and point out what settings are required to reproduce their statements.